Frama-C API - Loops
Loop specific actions.
val handle_annotations : Env.t -> Frama_c_kernel.Kernel_function.t -> Frama_c_kernel.Cil_types.stmt -> Frama_c_kernel.Cil_types.stmt * Env.tModify the given stmt loop to insert the code which verifies the loop annotations, ie. preserves its loop invariants and checks the loop variant. Also return the modified environment.
val mk_nested_loops : loc:Frama_c_kernel.Cil_types.location -> (Env.t -> Frama_c_kernel.Cil_types.stmt list * Env.t) -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Analyses_types.lscope_var list -> Frama_c_kernel.Cil_types.stmt list * Env.tmk_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 : (Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.toplevel_predicate -> Env.t) Stdlib.refval predicate_to_exp_ref : (adata:Assert.t -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.predicate -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.t) Stdlib.refval term_to_exp_ref : (adata:Assert.t -> Frama_c_kernel.Cil_types.kernel_function -> Env.t -> Frama_c_kernel.Cil_types.term -> Frama_c_kernel.Cil_types.exp * Assert.t * Env.t) Stdlib.ref