module Loops:sig
..end
Loop specific actions.
val preserve_invariant : Env.t -> Kernel_function.t -> Cil_types.stmt -> Cil_types.stmt * Env.t
Modify the given stmt loop to insert the code which preserves its loop invariants. Also return the modified environment.
val mk_nested_loops : loc:Cil_types.location ->
(Env.t -> Cil_types.stmt list * Env.t) ->
Cil_types.kernel_function ->
Env.t -> Lscope.lscope_var list -> Cil_types.stmt list * Env.t
mk_nested_loops ~loc mk_innermost_block kf env lvars
creates nested
loops (with the proper statements for initializing the loop counters)
from the list of logic variables lvars
. Quantified variables create
loops while let-bindings simply create new variables.
The mk_innermost_block
closure creates the statements of the innermost
block.
val translate_predicate_ref : (Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t)
Stdlib.ref
val predicate_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
Stdlib.ref
val term_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
Stdlib.ref