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] Ghost function call

Hi list,

I wanted to use ghost functions that I can call in some other
annotations but it seems not to work. Here is a toy example as an
illustration:

/*@ ghost int val (int a){
      return a;
    }
*/

/*@ ensures a == val(a);
*/
int min(int a, int b){
    if (a > b) return b;
    else return a;
}

When I launch frama-c with this code I get following error:

user error: unbound function val in annotation

But it is possible to call the val(int) function from the code itself
(as non-ghost code) !
Is this behavior normal ? In my mind, ghost code can access non-ghost
elements but not the opposite ?
Maybe my ghost function declaration is not correct ?

PS: I'm using Frama-C version Neon-20140301

Arnaud