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

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.

The intermediate language generation monad. It is used for translating E-ACSL predicates to expressions of the E-ACSL intermediate language (see Interlang).

an abbreviation for the monad type

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

• raises Not_covered

  if the Interlang does not yet support the operator