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] Assignments proof
- Subject: [Frama-c-discuss] Assignments proof
- From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
- Date: Tue, 3 Sep 2013 10:08:31 -0300
Hi, We are trying to prove if the assignments of variables Ang1 and Ang2[] are correct. We are using the ensure clause below for proving these assignments. For the Ang1, we have gotten the proved VC using the Gappa prover. However, for the Ang2 array the two Vcs were not proved. What is the problem? Is not possible to handle this kind of annotation with array? The source code and the screen shot are attached. We are using the Carbon version. Best regards, Luciana, Nanci, Rovedy ----------------------------------------------------------------------------------------- #define ANGLE 3.490659e-2 float Ang1; float Ang2[2]; /*@ assigns Ang1, Ang2[0..1]; ensures \abs(Ang1-ANGLE) <= 0x1p-25; ensures \abs(Ang2[0]-ANGLE) <= 0x1p-10; ensures \abs(Ang2[1]-ANGLE) <= 0x1p-10; */ void Inic2 (void) { Ang1 = ANGLE; Ang2[0] = ANGLE; Ang2[1] = ANGLE; } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130903/4d29f0bd/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: Tela_forum1.png Type: image/png Size: 159461 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130903/4d29f0bd/attachment-0001.png>
- Follow-Ups:
- [Frama-c-discuss] Assignments proof
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] Assignments proof
- Prev by Date: [Frama-c-discuss] JFLA 2014 - Troisieme appel a Communication
- Next by Date: [Frama-c-discuss] Introductory slides on Frama-C
- Previous by thread: [Frama-c-discuss] JFLA 2014 - Troisieme appel a Communication
- Next by thread: [Frama-c-discuss] Assignments proof
- Index(es):