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

[Frama-c-discuss] Frama-c: WP issues



Hello,

Le 13/01/2014 21:47, Dharmalingam Ganesan a ?crit :
> 2.http://stackoverflow.com/questions/21036098/wp-plugin-with-alt-ergo-unable-to-prove
>
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
-- 
David MENTR? - Research engineer, Ph.D.
   Formal Methods and tools
MITSUBISHI ELECTRIC R&D Centre Europe (MERCE)
Phone: +33 2 23 45 58 29 / Fax: +33 2 23 45 58 59
http://www.fr.mitsubishielectric-rce.eu