--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on June 2014 ---
[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