--- layout: fc_discuss_archives title: Message 4 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




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                    |
-------------- section suivante --------------
Une pièce jointe autre que texte a été nettoyée...
Nom: reverse_array.c
Type: text/x-csrc
Taille: 813 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150721/b090d492/attachment.c>
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150721/b090d492/attachment.html>