--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on May 2014 ---
Hello, I have some code that was proved with the Fluorine version of Frama-C and is no more proved using Neon. A simplified version of the code is available in the test_po_time_double_behavior_1.c file. I have tried to write the code differently, see test_po_time_double_behavior_2.c and test_po_time_double_behavior_3.c (notice also that one postcondition in test_po_time_double_behavior_3.c cannot be proved with Fluorine). But Neon cannot prove one of the postcondition in a behavior in all files. Frama-C and Alt-Ergo were installed via opam and I use the following command line : frama-c -pp-annot -wp -wp-timeout 60 file.c z3 4.3.1 via why3 seems to prove all the assertions under Neon, so it may be an Alt-Ergo problem. I will look at the generated mlw files by both Frama-C versions, but is there something obvious I have missed? Thanks in advance, Christophe -- Christophe Garion ISAE/DMIA - SUPAERO/IN garion at isae.fr 10 avenue Edouard Belin T?l : (33)5 61 33 80 57 BP 54032 Fax : (33)5 61 33 83 45 31055 Toulouse Cedex 4 -------------- next part -------------- A non-text attachment was scrubbed... Name: test_po_time_double_behavior_1.c Type: text/x-csrc Size: 1504 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140527/41e2ecbe/attachment.c> -------------- next part -------------- A non-text attachment was scrubbed... Name: test_po_time_double_behavior_2.c Type: text/x-csrc Size: 1580 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140527/41e2ecbe/attachment-0001.c> -------------- next part -------------- A non-text attachment was scrubbed... Name: test_po_time_double_behavior_3.c Type: text/x-csrc Size: 1579 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140527/41e2ecbe/attachment-0002.c>