--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on April 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] VC not the same when verifying function in isolation or in complete compilation unit



Hello,

I am using Frama-C to verify a runtime written in C and I have
encountered a strange (at least to me) behaviour for VC generation. I
have tried to produce a minimal example that you will find
attached. There are two functions, get_data and append_msg, that
manipulate a struct representing a simple message.

When using Alt-Ergo, the contract of get_data can be proved in isolation
with

frama-c -wp -wp-prover alt-ergo -wp-fct get_data msg_minimal.c

but the postcondition of get_data cannot be proved when using the whole
.c file with

frama-c -wp -wp-prover alt-ergo msg_minimal.c

Notice that the postcondition VC can be proved by CVC4 or Z3 in both
cases.

The VC produced by -wp-print are the same in both cases (see
wp-print-complete.txt and wp-print-isolation.txt), but if I use Why3,
the VC are different (see why-goal-complete.why and
why-goal-isolation.why). The only difference between the two goals,
besides variables permutation between i, i_1 and i2, is the last
addition in the goal: in one case, it is i_1 + i_2, in another, it is
i_2 + i_1. This causes Alt-Ergo not being able to prove the VC "from
scratch", because the generated triggers for the corresponding axioms
are not sufficient (see a discussion on alt-ergo-beginners mailing list
with Mohamed Iguernlala).

I do not understand why the VC produced for Why or Alt-Ergo are
different when asking to verify the function in isolation or in complete
file, am I missing something?

Notice also that if I remove the first postcondition of append_msg, then
the VC generated for get_data postcondition is the same in isolation or
with complete compilation unit.

Sorry if this has already been answered on the mailing list.

Best regards,

Christophe

--
Christophe Garion          ISAE-SUPAERO/DISC
garion at isae-supaero.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: msg_minimal.c
Type: text/x-csrc
Size: 1099 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160407/b0d49a5a/attachment.c>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: wp-print-complete.txt
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160407/b0d49a5a/attachment.txt>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: wp-print-isolation.txt
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160407/b0d49a5a/attachment-0001.txt>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: why-goal-complete.why
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160407/b0d49a5a/attachment.ksh>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: why-goal-isolation.why
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20160407/b0d49a5a/attachment-0001.ksh>