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] VC not the same when verifying function in isolation or in complete compilation unit

  • Subject: [Frama-c-discuss] VC not the same when verifying function in isolation or in complete compilation unit
  • From: christophe.garion at isae-supaero.fr (Christophe Garion)
  • Date: Thu, 07 Apr 2016 16:55:27 +0200
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>