--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on November 2010 ---
We would usually Write this as a normal C function and call it on ghost variables. Jens Von meinem iPhone gesendet Am 11.11.2010 um 17:16 schrieb "Barbara Vieira" <barbaraisabelvieira at gmail.com>: > Hi everyone, > > I'm using the Jessie plug-in of the Frama-C Boron. > I would like to know if I am doing something wrong in the declaration of the behavior of a ghost function, because something is going wrong. > > As an example, consider the declaration the following ghost function: > /*@ ghost > @ //@ ensures \forall int k; 0<=k<32 ==> a[k] == \at(a[k],Old) + v; > @ int* sum_n(int a[32], int v) > @ { > @ int i; > @ for(i=0;i<32;i++) { > @ a[i] +=v; > @ } > @ return a; > @ } > @*/ > > After running the plug-in on this example, it does not generate the proof obligation that is related with the post condition. > > I checked how the translation from C to Jessie is done and it seems that the translation of the behavior is missed. > The following Jessie code corresponds to the one that is generated by the plugin when running it on the code presented above: > > int_P[..] sum_n(int_P[0] a, int32 v) > behavior default: > ensures (C_14 : true); > { > ... > } > > It seems that the behavior is not properly translated. My question is: am I doing something wrong in the declaration of the ghost function? > > Thanks in advance. > Best regards, > B?rbara Vieira > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101111/24ca8255/attachment.htm>