Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] matrix addition

  • Subject: [Frama-c-discuss] matrix addition
  • From: virgile.prevosto at m4x.org (Virgile Prevosto)
  • Date: Tue, 20 Jun 2017 14:39:13 +0200
  • In-reply-to: <21e9-5947b700-2b7-12a6dac0@145891439>
  • References: <21e9-5947b700-2b7-12a6dac0@145891439>
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>