Module Inline

module Inline: sig .. end

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.