Maxime Arthaud

Pyre should exit with code 1 on type errors. If not, it might be a bug. Does `pyre check` give you a different error code?

I was able to reproduce. Let me see if I can fix this quickly.

It seems like a bug in click, see https://github.com/pallets/click/issues/2124

A simple idea would be to create two separate analyses: * uninitialized variable analysis (**uva**): check for uninitialized operands in statements * uninitialized memory analysis (**uma**): read of uninitialized memory...

The uninitialized variable analysis (**uva**) now only checks for uninitialized variables, and is enabled by default. The next step is to implement the uninitialized memory analysis (**uma**).

Hi @Earnestly, Thanks for trying ikos. This is indeed a false positive. This is similar to #94 and is due to temporary variables. The LLVM bitcode looks like: ```c++ char*...

Thanks Boris. I would like to implement this in IKOS as well. I tried to read the source code of Frama-C before to understand how you implemented a bunch of...

Thank you @yakobowski, I will take a look at it.

Confirmed. I think it might be because of the loop, ikos might think that `push_back` is called multiple times. In that case `std::vector` will grow, and ikos might have lost...

Hi @gh2375, The first warning can be eliminated by using the interval-congruence domain. The second and third warnings are false positives because ikos cannot prove that the loop is executed...