module Translate:sig
..end
Generate C implementations of E-ACSL predicates and terms.
Generate C implementations of E-ACSL predicates and terms.
val predicate_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 ACSL predicate into a corresponding C expression.
val generalized_untyped_predicate_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 translate_predicate : ?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.
val term_to_exp : adata:Assert.t ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t
Convert an ACSL term into a corresponding C expression.
val translate_rte_annots : (Stdlib.Format.formatter -> 'a -> unit) ->
'a ->
Cil_types.kernel_function -> Env.t -> Cil_types.code_annotation list -> Env.t
Translate the given RTE annotations into runtime checks in the given environment.
val gmp_to_sizet : adata:Assert.t ->
loc:Cil_types.location ->
name:string ->
?check_lower_bound:bool ->
?pp:Cil_types.term ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t
Translate the given GMP integer to an expression of type size_t
. RTE
checks are generated to ensure that the GMP value holds in this type.
The parameter name
is used to generate relevant predicate names.
If check_lower_bound
is set to false
, then the GMP value is assumed to
be positive.
If pp
is provided, this term is used in the messages of the RTE checks.
exception No_simple_term_translation of Cil_types.term
Exceptin raised if untyped_term_to_exp
would generate new statements in
the environment
exception No_simple_predicate_translation of Cil_types.predicate
Exceptin raised if untyped_predicate_to_exp
would generate new statements
in the environment
val untyped_term_to_exp : Cil_types.typ option -> Cil_types.term -> Cil_types.exp
Convert an untyped ACSL term into a corresponding C expression.
val untyped_predicate_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.