--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on June 2014 ---
Hello, 2014-06-11 12:26 GMT+02:00 arnaud <arnaud.dieumegard at enseeiht.fr>: > 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); > */ > When I launch frama-c with this code I get following error: > > user error: unbound function val in annotation Ghost functions are still code: you cannot use them in annotations. You have to define (either directly or within an axiomatic) logic functions for that. > > 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 ? In theory this is the case: you should only be able to call val inside ghost code. However, as mentioned in the ACSL implementation manual, the type-checker does not verify this at the moment. Best regards, -- E tutto per oggi, a la prossima volta Virgile