Module Translate_terms

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.

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