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