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] Substitution in Cil_types.predicate

Hello Boris,

2012/2/24 Boris Hollas <hollas at informatik.htw-dresden.de>:
> I want to perform a substitution in a Cil_types.predicate, for example
> x->a in (0 <= x <= n). Is there a function in the Frama-C API to do so?

There's nothing built-in, but a tiny copy visitor should do the trick.
An example of such a visitor can be found e.g. in
src/logic/logic_interp.ml with the make_pre_var class that is
responsible to enclose occurrences of formals in post-conditions of
functions' contract inside \at(_,Pre), as per ACSL's semantics.

> I've found Cil_manipulation.predicate_substitution in aorai, but I'm
> unsure whether I should use functions that aren't part of the Frama-C
> API.

Indeed, you cannot directly use functions of another plugin, unless
they are registred through Dynamic (or Db for historical plug-ins)
Besides, Cil_manipulation is completely obsolete, not used by Aora?
anymore, and thus a good candidate for removal in a future version.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile