Module Translate_predicates

module Translate_predicates: sig .. end

Generate C implementations of E-ACSL predicates.


Generate C implementations of E-ACSL predicates.

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

Convert an untyped ACSL predicate into a corresponding C expression.

val do_it : ?pred_to_print:Cil_types.predicate ->
Cil_types.kernel_function -> Env.t -> 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 Cil_types.predicate

Exceptin raised if untyped_to_exp would generate new statements in the environment

val untyped_to_exp : Cil_types.predicate -> 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 -> Cil_types.code_annotation -> unit) ->
Cil_types.code_annotation ->
Cil_types.kernel_function ->
Env.t -> Cil_types.code_annotation list -> Env.t)
Stdlib.ref
val translate_rte_exp_ref : (?filter:(Cil_types.code_annotation -> bool) ->
Cil_types.kernel_function -> Env.t -> Cil_types.exp -> Env.t)
Stdlib.ref