--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on January 2014 ---
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