Module `E_ACSL.Translate_predicates`

Generate C implementations of E-ACSL predicates.

val generalized_untyped_to_exp : 
  adata:Assert.t ->
  ?name:string ->
  Frama_c_kernel.Cil_types.kernel_function ->
  ?rte:bool ->
  Env.t ->
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.exp * Assert.t * Env.t

Convert an untyped ACSL predicate into a corresponding C expression.

val do_it : 
  ?pred_to_print:Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Env.t ->
  Frama_c_kernel.Cil_types.toplevel_predicate ->
  Env.t

Translate the given predicate to a runtime check in the given environment. If pred_to_print is set, then the runtime check will use this predicate as message.

exception No_simple_translation of Frama_c_kernel.Cil_types.predicate

Exceptin raised if untyped_to_exp would generate new statements in the environment

val untyped_to_exp : 
  Frama_c_kernel.Cil_types.predicate ->
  Frama_c_kernel.Cil_types.exp

Convert an untyped ACSL predicate into a corresponding C expression. This expression is valid only in certain contexts and shouldn't be used.

val translate_rte_annots_ref : 
  ((Format.formatter -> Frama_c_kernel.Cil_types.code_annotation -> unit) ->
    Frama_c_kernel.Cil_types.code_annotation ->
    Frama_c_kernel.Cil_types.kernel_function ->
    Env.t ->
    Frama_c_kernel.Cil_types.code_annotation list ->
    Env.t)
    ref

val translate_rte_exp_ref : 
  (?filter:(Frama_c_kernel.Cil_types.code_annotation -> bool) ->
    Frama_c_kernel.Cil_types.kernel_function ->
    Env.t ->
    Frama_c_kernel.Cil_types.exp ->
    Env.t)
    ref

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `E_ACSL.Translate_predicates`

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module E_ACSL.Translate_predicates

Module `E_ACSL.Translate_predicates`