Frama-C API - Interlang_gen
The compilation of E-ACSL to Cil is implemented as a two-stage process, where E-ACSL is first translated into an intermediate language Interlang
and only then into Cil. This module defines a monad M
for specifying computations that generate Interlang
expressions, and is thus used for the first stage.
It is an instance of the RWS monad (Monad_rws
), operating on the following background data.
type env = {
kf : Frama_c_kernel.Cil_types.kernel_function;
loc : Frama_c_kernel.Cil_types.location;
vars : Interlang.exp Frama_c_kernel.Cil_datatype.Term.Map.t;
env : Env.t;
rte : bool;
}
The Reader variable of M
. See Monad_rws.Conf.env
.
Computations within the Interlang_gen.M
monad are initiated from within a larger compilation context with its own environment of type Env.t
. Moreover in that context the current kernel_function
and current location are known. These data will not change during the computation, and are simply made available (as a sort of global variable) through this Reader variable env
.
Additionally the rte
field specifies whether RTEs are to be generated. This value might be locally shadowed during the computation.
type state = Interlang.exp Frama_c_kernel.Cil_datatype.Term.Map.t
The State variable of M
includes a map of local variables (initially empty) which is enriched with newly generated variables. This is done such that at the end of a block these variables can be cleaned. (The cleaning mechanism is not yet implemented in the new compilation scheme, and effectuated by the direct-to-Cil compilation scheme.)
This exception is raised when the language element to be translated is not yet supported by the intermediate language compilation scheme. In that case the old direct-to-Cil compilation scheme is used. The preferred method of raising this exception is using M.not_covered
.
module M : sig ... end
The intermediate language generation monad. It is used for translating E-ACSL predicates to expressions of the E-ACSL intermediate language (see Interlang
).
type 'a m = 'a M.t
an abbreviation for the monad type
val binop : Frama_c_kernel.Cil_types.binop -> Interlang.binop
Transforms a Cil binary operator to an Interlang
binary operator. Not all Cil operators are supported (yet).