Maxime Arthaud

Hi @nickdesaulniers and @AbigailBuccaneer, thanks for suggesting it. It would be nice to have this, yes. I'm trying to think about the best way to implement this. We will first...

Hi @AbigailBuccaneer, > I think a good first step would be `compile_commands.json` support for projects that have _already_ been compiled with the magic flags that `ikos` needs. Then the compilation...

Hi @neon12345, I'm not working on ikos anymore, but just to answer your question: yes, it should be possible to support `llvm::VectorType` in `llvm::CmpInst`. Note that the analysis ignores all...

Hi @kbittick, Most likely, this is so obvious that clang/llvm optimized the error away. Could you try running ikos with the `--display-llvm` option?

Yes, that's `ikos-pp`, which does some very basic optimization, such as `-mem2reg` which hoists those `alloca` into llvm registers.

Hi @nihilus, Yes, this is a known issue. IKOS doesn't handle multi-threaded code. Handling multi-threaded code in a sound static analyzer based on Abstract Interpretation such as IKOS is challenging....

Hello, What operating system are you using? Under https://github.com/NASA-SW-VnV/ikos/tree/master/doc/install there are installation instructions for a few operating systems. If yours is not there, then it means it's not officially supported....

Please provide your logs (each command you ran and their output), otherwise we cannot help you.

This is again due to a conversion from pointer to integer. ```c if(p2 - p1 < 1) ``` is translated into: ```c if ((size_t)p2 - (size_t)p1 < 1) ``` Because...

This could be implemented in the memory domain by adding a map from memory locations to a value set abstraction. This is already implemented for pointers with the `_pointer_sets` map....