--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on January 2014 ---
Hi, One update: I added this code snippet to the end of the foo function as given below. if (fRrValue == 0) { /*@ assert(tenumRMode == SS_A_MODE); */ } I removed the behavior basic from annotations. wp shows this assert is valid as expected. It appears there is some problem in the way the basic behavior is parsed, transformed, etc. Any comments? Dharma ________________________________________ From: frama-c-discuss-bounces at lists.gforge.inria.fr [frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of David MENTRE [dmentre at linux-france.org] Sent: Wednesday, January 15, 2014 11:39 AM To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] Frama-c: WP issues Hello, Le 15/01/2014 17:35, Dharmalingam Ganesan a ?crit : > 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. You should always use the latest version (currently Fluorine). Have you applied my suggestion (adding asserts)? We cannot help you much without the code. BTW, frama-c provides a C code obfuscator, it might be sufficient for you to provide the code. Best regards, david _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://cp.mcafee.com/d/FZsS820Od6QmnzhOZtyZTztPqtTAnC67QkPqtTAnC67T6jqtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1ISeYQsA744T-LP9EVspphpWZOWqoVXDbELTpoVqWdAkRrLcYG7DR8OJMddECQjt-hojuv78I9CzATsS03fBite8Kw0vWk8OTDoU0xsxa62qKMM-l9OwXn7oWHFuNt2lbdQErtzGKBX5Q9kITixsxlK5LE2zVkDjybE07-B2cJVS9JAQszHCMnWhEwdboL7ltbSbEiFpKB3iWq81ueGWnIAq8052NEwBizvQdTdZCzILpi3G-XJ