--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on August 2010 ---
> 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.