Module Loops

module Loops: sig .. end

Loop specific actions.


val apply_after_transformation : Project.t -> unit
val mv_invariants : Env.t -> old:Cil_types.stmt -> Cil_types.stmt -> unit

Transfer the loop invariants from the old loop to the new one. Both statements must be loops.

val preserve_invariant : Project.t ->
Env.t -> Kernel_function.t -> Cil_types.stmt -> Cil_types.stmt * Env.t * bool

modify the given stmt loop to insert the code which preserves its loop invariants. Also return the modify environment and a boolean which indicates whether the annotations corresponding to the loop invariant must be moved from the new statement to the old one.

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)
Stdlib.ref
val named_predicate_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