--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Behavior of the ghost functions



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>