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.