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] Frama-c: WP issues


Thanks for your response. There are no loops in the code.

I do not know whether you had a chance to see the stackoverflow link I gave. According to a developer of alt-ergo (0.95), he thinks this behavior is valid for Oxygen (after he fixes syntax errors in the generated why/mlw code). This behavior is reported as unknown for the newest version Fluorine.

Best regards,

-----Original Message-----
From: frama-c-discuss-bounces at [mailto:frama-c-discuss-bounces at] On Behalf Of David MENTRE
Sent: Wednesday, January 15, 2014 11:31 AM
To: frama-c-discuss at
Subject: Re: [Frama-c-discuss] Frama-c: WP issues


Le 13/01/2014 21:47, Dharmalingam Ganesan a ?crit :
> 2.
You said:
> This behavior should be true because there is no other place tenumRMode is updated except the first conditional statement's else section.
> The wierd thing is that if I comment some lines arbitrarily I always get "valid" from Alt-ergo.

Have you some loop in the commented out code?

You can also add "assert tenumRMode == SS_A_MODE;" at various points in 
your code to see where WP is failing to prove it.

Best regards,
David MENTR? - Research engineer, Ph.D.
   Formal Methods and tools
Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59

Frama-c-discuss mailing list
Frama-c-discuss at