Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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.

type binop =
  1. | Plus
  2. | Minus
  3. | Mult
  4. | Div
  5. | Mod
  6. | Lt
  7. | Gt
  8. | Le
  9. | Ge
  10. | Eq
  11. | Ne
module Varinfo : sig ... end
type varinfo = Varinfo.t
type exp = {
  1. enode : exp_node;
  2. origin : Frama_c_kernel.Cil_types.term option;
}

origin is required to calculate casts. Note that origin is None when it stems from a predicate as predicates never require casts.

and exp_node =
  1. | True
  2. | False
  3. | Integer of Z.t
  4. | BinOp of binop_node
  5. | Lval of lval
  6. | SizeOf of Frama_c_kernel.Cil_types.typ
and binop_node = {
  1. ity : Analyses_types.number_ty;
  2. binop : binop;
  3. op1 : exp;
  4. op2 : exp;
}
and lhost =
  1. | Var of varinfo
  2. | Mem of exp
and lval = lhost * offset
and offset =
  1. | NoOffset
  2. | Field of Frama_c_kernel.Cil_types.fieldinfo * offset
  3. | Index of exp * offset
module Pretty : sig ... end