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

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