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 invarariants. 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.