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

[Frama-c-discuss] Prove the reverse of a char*, ensure problems



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