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] Code proved with Fluorine is more proved with Neon

  • Subject: [Frama-c-discuss] Code proved with Fluorine is more proved with Neon
  • From: christophe.garion at isae.fr (Christophe Garion)
  • Date: Tue, 27 May 2014 10:36:24 +0200
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>