Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>