Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Ada / ada_printer.ml @ 173a2a8f

History | View | Annotate | Download (11.3 KB)

# Date Author Comment
173a2a8f 04/19/2019 12:47 PM Guillaume DAVY

Ada: Lot of specification is exported in Ada. We use ghost code to store all states,
we generate the transition pridicate but also the invariant. But two problems, occured.
The first one is a visibility problem for the record which is private but must be
public for ghost variable which have to be public for specifaction. The second...

b5b745fb 04/05/2019 04:37 PM Guillaume DAVY

Ada: First support for transition predicate generation.

230b168e 04/04/2019 02:14 PM Guillaume DAVY

Ada: Refactor Ada Backend to reduce redundancy, make it more modular and
more simple.