--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on April 2016 ---
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>