--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] matrix addition



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>