Maxime Arthaud

See https://github.com/facebookincubator/SPARTA/pull/5#issuecomment-566288425, that could impact our implementation too.

Improve the uninitialized variable analysis

7

The uninitialized variable analysis (uva) is currently disabled because it produces false positives on very simple programs. For instance, see the following code: ```c #include #define N 10 int main()...

Implement a union of N disjunctive abstract values

2

We could implement an abstract domain containing a union of at most **N** disjunctive abstract values. This should be implemented as an option to the analyzer, so that the user...

The analyzer generates false positives when the code uses the following pattern: ```c #include #define SUCCESS 0 extern int f(void); extern int g(void); extern int h(void); int x = 0;...

Catch buffer overflows in structures

2

The current analysis cannot catch a buffer overflow in a structure. For instance: ```c #include typedef struct { int tab[10]; int x; } Struct; int main() { Struct s; s.tab[10]...

Using a small integer (e.g, `uint8_t`, `int16_t`, etc.) as a loop counter usually results into false positives. For instance: ```c #include void f(int* p, uint16_t n) { for (uint16_t i...

The current analysis is imprecise when merging branches where one side has uninitialized variables. For instance: ```c #include int main(int argc, char** argv) { int tab[10]; if (argc > 2)...

We could implement backward operators to improve the precision on guards. This could help with #97 and #134.

Improve the value domain to keep track of integer sets

1

On the following code: ```c int main() { const int indexes[5] = {2, 0, 4, 1, 3}; int array[5]; for (int i = 0; i < 5; i++) { int...

When running ikos on the following code: ```c extern int __ikos_nondet_int(void); int main() { int x; int y = __ikos_nondet_int(); int tab[10]; for (x = 0; x < 10 &&...