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>