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.