--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on September 2013 ---
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>