--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2017 ---
Hello, 2017-06-19 13:36 GMT+02:00 CLAVIERE Arthur < Arthur.CLAVIERE at student.isae-supaero.fr>: > I want to prove the correctness of a simple function which adds two 3-by-3 > matrices. Using wp plug-in, I can prove the assign clause but I can't prove > the ensures clause (I use the real model for computing weakest > preconditions). Did I forget a precondition, is it a known problem ? > > Regards, > > As long as you use `-wp-model +real`, your specification looks ok. It's just that the provers seem to have some difficulties with the proof obligations generated by WP (I suspect that the separation properties get a little messy so that they fail to distinguish between the array cells that are updated and the others). Fortunately, since Frama-C 15 Phosporus, you can help them a little bit by writing scripts directly within the WP (double-click on the `Script` column in the `WP Goals` tab for the PO you want to complete interactively. The user interface (see also section 2.3 of WP's user manual) is still a bit rough, but in the end, it can get the job done. Attached is an archive containing the 3 scripts needed to complete the proofs in your development. To use it, extract it somewhere and use the following command (adapting path to directory matrix_script and/or matrix.c if needed) frama-c -wp -wp-model +real -wp-session matrix_script -wp-prover script,alt-ergo matrix.c Best regards, -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pièce jointe HTML a été nettoyée... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170620/869aa607/attachment.html> -------------- section suivante -------------- Une pièce jointe autre que texte a été nettoyée... Nom: matrix_script.tar.gz Type: application/x-gzip Taille: 1838 octets Desc: non disponible URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170620/869aa607/attachment.bin>