Frama-C:
Plug-ins:
Libraries:

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.

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.

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.)

type out = unit
exception Not_covered

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

Transforms a Cil binary operator to an Interlang binary operator. Not all Cil operators are supported (yet).