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

  • Subject: [Frama-c-discuss] Frama-c: WP issues
  • From: d.mentre at fr.merce.mee.com (David MENTRE)
  • Date: Wed, 15 Jan 2014 17:30:40 +0100
  • In-reply-to: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local>
  • References: <B517F47C2F6D914AA8121201F9EBEE6701C76682DC29@Mail1.FCMD.local>
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