--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on October 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis and termination



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