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

  • Subject: [Frama-c-discuss] Behavior of the ghost functions
  • From: barbaraisabelvieira at gmail.com (Barbara Vieira)
  • Date: Thu, 11 Nov 2010 16:16:12 +0000
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>