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