Module Loops

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_named_predicate_ref : (Cil_types.kernel_function -> Env.t -> Cil_types.predicate -> Env.t)
Pervasives.ref
val named_predicate_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.predicate -> Cil_types.exp * Env.t)
Pervasives.ref
val term_to_exp_ref : (Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Env.t)
Pervasives.ref