Module E_ACSL.Interlang

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 the E-ACSL intermediate language type, along with pretty printing functions.

This language is currently subject to frequent modifications, so documentation remains scant for the moment.

Since it is an intermediate language betwen E-ACSL and Cil its characteristics are situated somewhere between the two languages, i.e. Interlang expressions (of type exp) are reminiscent of both Cil expressions (Cil_types.exp) and logic terms (Cil_types.term).

All the record fields are present because they are currently strictly necessary for the compilation to be correct, in the sense that it yields Cil code that is equivalent modulo position to the code generated by the old direct-to-Cil compilation scheme. Some of these fields are bound to disappear as the first compilation stage takes over more of the second stage's tasks.