--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on August 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Functions in Predicates



> is it maybe
> not possible to use C-functions in predicates?

Exactly.

It is only possible to use logic functions in predicate. Logic
functions are complete and side-effect-free by construction, plus the
syntax reminds you to think of the dependencies towards the memory
state? well, as dependencies. And the result can depend on several
such states, since you are making them explicit.

If your C function isn't too complicated, rewriting it in ACSL
shouldn't be any trouble (and if you ever programmed in Prolog, it
will remind you of these good memories). If you are having trouble
expressing your function as a logic function, I am sure a good soul on
this list can take a look and help.

Regards,

Pascal
PS: alternately, you can also use ghost code in the verified code. The
check that ghost code does not interfere with normal code is currently
missing, but it is planned.