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] 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.