--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on July 2015 ---
Sorry for my ignorance, I just installed FramaC via apt-get and I launch it writing "frama-c-gui my_code.c" into the terminal. I think it is using WP because I saw it written somewhere! Thank you a lot for the help and patience. I like a lot to think about the verification of C programs. Have a nice day, Francesco Bonizzi ---------------------------------------- Date: Tue, 21 Jul 2015 11:48:11 +0200 From: Claude.Marche at inria.fr To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] Prove the reverse of a char*, ensure problems On 07/21/2015 11:16 AM, Francesco Bonizzi wrote: > Hi and thanks for answering. I didn't install any particular plugin, I just did "sudo apt-get installa frama-c", nothing more. Nothing more really? Not even a command-line like frama-c -wp my_code.c to run the WP plugin? Going back to the original question: yes it seems that automatic provers need a little help to establish the post-condition. I attach the file I obtained after small modifications, and a dump of the proof session obtained by the Jessie plugin. As you may see, you need the Z3 prover to complete the proof. Nice little exercise indeed, - Claude -- Claude Marché | tel: +33 1 69 15 66 08 INRIA Saclay - Ãle-de-France | Université Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex | --Allegato al messaggio inoltrato-- Why3 Proof Results for Project "reverse_array" Theory "reverse_array.Jessie_program": fully verified in 6.52 s Obligations Alt-Ergo (0.95.2) Alt-Ergo (0.99.1) CVC3 (2.4.1) CVC4 (1.4) Z3 (4.3.2) Function reverse, default behavior --- --- --- --- --- split_goal_wp 1. postcondition --- 0.04 --- 0.14 1.09 2. assertion --- Timeout (5s) --- 0.19 0.05 3. assertion --- 0.84 --- 0.29 0.22 4. assertion --- 0.06 0.09 0.15 0.10 5. postcondition --- Timeout (5s) --- Timeout (5s) 1.05 Function reverse, Safety --- --- --- --- --- split_goal_wp 1. arithmetic overflow (precondition) --- 0.03 --- 0.12 0.09 2. precondition for call (precondition) --- 0.03 --- 0.14 0.06 3. arithmetic overflow (precondition) --- 0.03 --- 0.09 0.08 4. check 0.04 0.07 --- 0.14 0.09 5. precondition for call (precondition) --- 0.02 --- 0.09 0.07 Function swap, default behavior --- --- --- --- --- split_goal_wp 1. postcondition --- 0.08 --- 0.16 0.06 Function swap, Safety --- --- --- --- --- split_goal_wp 1. pointer dereference (precondition) --- 0.02 --- 0.11 0.05 2. pointer dereference (precondition) --- 0.03 --- 0.11 0.06 3. pointer dereference (precondition) --- 0.02 --- 0.08 0.05 4. pointer dereference (precondition) --- 0.04 --- 0.11 0.04 _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss