--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on March 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie: Timeout for Simplify broken?



Hello Jens and Virgile,

I also noticed that Jessie generates VCs for arithmetic safety even if
there are no arithmetic operations apart from comparisons. Eg, for enums
val1, val2,

if(val1 != val2)

generates 4 VCs and

switch(val1)

generates 2 VCs. I don't see how a arithmetic overflow might occur here.
What does Jessie try to prover here?

Regards,
Boris