--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on July 2015 ---
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>