--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on September 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assignments proof



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>