Frama-C API - Inline
val inline_calls : Cil_types.file -> unitval inline_term : inline:(Cil_types.logic_info -> bool) -> ?current:Cil_types.logic_label -> Cil_types.term -> Cil_types.term optioninline_term ~inline term inlines in term the application of predicates and logic functions for which inline is true. If provided, current is the current label of the term; it is Here by default. Returns None if the inlining of a predicate or a logic function fails, in particular when they are recursive or have no direct definition.
val inline_predicate : inline:(Cil_types.logic_info -> bool) -> ?current:Cil_types.logic_label -> Cil_types.predicate -> Cil_types.predicate optionInlines predicates and logic functions in a predicate. See inline_term for details.