Module `E_ACSL.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.t

Modify 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.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_predicate_ref : 
  (Frama_c_kernel.Cil_types.kernel_function ->
    Env.t ->
    Frama_c_kernel.Cil_types.toplevel_predicate ->
    Env.t)
    ref

val 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)
    ref

val 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)
    ref

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Loops/index.html

Module `E_ACSL.Loops`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-e-acsl.core/E_ACSL/Loops/index.html

Module E_ACSL.Loops

Module `E_ACSL.Loops`