--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on November 2010 ---
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 -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20101111/a75d181c/attachment.htm>