--- layout: fc_discuss_archives title: Message 26 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



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