--- layout: fc_discuss_archives title: Message 101 from Frama-C-discuss on February 2012 ---
[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