Skip to content
Snippets Groups Projects
Commit b6556cc7 authored by Jan Rochel's avatar Jan Rochel
Browse files

[e-acsl] new compilation scheme via intermedia language

Introduce a new compilation scheme where E-ACSL logic terms are
translated to CIL is implemented as a two-stage process.
First, E-ACSL is translated into an intermediate language. Only then in
the second stage the intermediate language is translated into CIL.

The module Interlang specifies the E-ACSL intermediate language type,
along with pretty printing functions. As this language is still subject
to frequent changes, documentation remains scant for the moment.

The module Interlang_gen helps in the creation of Interlang expressions,
and is thus useful for the first stage. The module Interlang_trans
specifies the translation of Interlang expression to CIL and is relevant
for the second stage.
Both modules make heavy use of the RWS monad, defined in the Monad_rws
module. RWS stands for Reader, Writer, State. The RWS monad is a monad
to model computations with side-effects and environments in a purely
functional and type-safe manner.

As the new compilation scheme covers E-ACSL only partially, it fails on
many E-ACSL terms. Therefore we keep for the moment the old
direct-to-CIL compilation scheme, and, whenever the new compilation
scheme fails for a given sub-term raising the Interlang_gen.Not_covered
exception, we fall back on the direct-to-CIL compilation scheme for that
sub-term.
parent d1f4955d
No related branches found
No related tags found
No related merge requests found
Showing
with 1330 additions and 21 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment