--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on October 2010 ---
Hi, I wanted to use the following example to explain that abstract interpretation can determine that i \in {-4,4} at the end of main(). However, the value analysis shows i \in {-4,0,4} at this point. But i == 0 is not possible since !(i % 2 == 0) is necessary for the loop to terminate. Why doesn't the value analysis detect this? int foo(); int main() { int i; i = foo(); while(i % 2 == 0) { i = i/2; } i = 4 * (i % 2); return 0; } -- Regards, Boris