Module Translate

module Translate: sig .. end

Generate C implementations of expressions.

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

Convert an ACSL predicate into a corresponding C expression.

val generalized_untyped_predicate_to_exp : ?name:string ->
Cil_types.kernel_function ->
?rte:bool ->
?must_clear_typing:bool ->
Env.t -> Cil_types.predicate -> Cil_types.exp * 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 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.

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.