Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Jessie: Timeout for Simplify broken?
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Thu, 3 Mar 2011 13:48:14 +0100 (CET)
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