ikos

ikos copied to clipboard

compile_commands.json support

5

Some tools like [bear](https://github.com/rizsotto/Bear) can generate a [compile_commands.json file](https://clang.llvm.org/docs/JSONCompilationDatabase.html) which is a standard format [many other tools accept](https://sarcasm.github.io/notes/dev/compilation-database.html#what-is-it-good-for). (I thought scan-build supports this as input, but cant seem to find...

nickdesaulniers

False positive because of unknown intrinsic function

3

### Code: ``` #include int main(int argc, char * argv[]) { int n = 10; int * arr = new int[n]; for(int * p = arr; n > 0; n--,...

gh2375

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...

arthaud

False positive because of temporary variables

5

Potentially a false positive: ```c #include #include struct Storage { char *a; char *b; }; int main(void) { struct Storage storage = {0}; char *message = "hello world"; size_t length...

Earnestly

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;...

arthaud

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]...

arthaud

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...

arthaud

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)...

arthaud

Support multi-threaded code

1

I donnu if it is a know issue or not but IKOS fails pretty much to analyze posit threaded code regarding locking etc... I understand that it might be out...

nihilus

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

arthaud