module Translate_terms:sig
..end
Generate C implementations of E-ACSL terms.
Generate C implementations of E-ACSL terms.
val to_exp : adata:Assert.t ->
?inplace:bool ->
Cil_types.kernel_function ->
Env.t -> Cil_types.term -> Cil_types.exp * Assert.t * Env.t
to_exp ~adata ?inplace kf env t
converts an ACSL term into a
corresponding C expression.
adata
: assertion context.inplace
: if the root term has a label, indicates if it should be
immediately translated or if Translate_ats
should be used to retrieve
the translation.kf
: The enclosing function.env
: The current environment.t
: The term to translate.exception No_simple_translation of Cil_types.term
Exceptin raised if untyped_to_exp
would generate new statements in
the environment
val untyped_to_exp : Cil_types.typ option -> Cil_types.term -> Cil_types.exp
Convert an untyped ACSL term into a corresponding C expression.
val translate_rte_exp_ref : (?filter:(Cil_types.code_annotation -> bool) ->
Cil_types.kernel_function -> Env.t -> Cil_types.exp -> Env.t)
Stdlib.ref