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

[Frama-c-discuss] Code proved with Fluorine is more proved with Neon



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>