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 :
((Stdlib.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)
Stdlib.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)
Stdlib.ref