Module Frama_c_kernel.Inline

val inline_calls : Cil_types.file -> unit
val inline_term : inline:(Cil_types.logic_info -> bool) -> ?current:Cil_types.logic_label -> Cil_types.term -> Cil_types.term option

inline_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 definitiion.

val inline_predicate : inline:(Cil_types.logic_info -> bool) -> ?current:Cil_types.logic_label -> Cil_types.predicate -> Cil_types.predicate option

Inlines predicates and logic functions in a predicate. See inline_term for details.