Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec/src/backends/Ada @ 75c459f4

Name Size Revision Age Author Comment
README 2.04 KB 230b168e about 4 years Guillaume DAVY Ada: Refactor Ada Backend to reduce redundancy,...
ada_backend.ml 6.72 KB 7ee5f69e about 2 years Lélio Brun corrections on loggers + spec in AST
ada_backend_adb.ml 8.55 KB 75c459f4 about 2 years Lélio Brun start with Spec AST generation
ada_backend_ads.ml 9.27 KB ca7e8027 over 2 years Lélio Brun fix almost all warnings
ada_backend_common.ml 14 KB ca7e8027 over 2 years Lélio Brun fix almost all warnings
ada_backend_common.mli 1.7 KB 173a2a8f about 4 years Guillaume DAVY Ada: Lot of specification is exported in Ada. W...
ada_backend_wrapper.ml 6.75 KB ca7e8027 over 2 years Lélio Brun fix almost all warnings
ada_printer.ml 11.5 KB 05f85b44 about 4 years Guillaume DAVY Ada: Start cleaning Ada to prepare for why beckend
ada_printer.mli 2.42 KB 05f85b44 about 4 years Guillaume DAVY Ada: Start cleaning Ada to prepare for why beckend
misc_lustre_function.ml 11.7 KB 75c459f4 about 2 years Lélio Brun start with Spec AST generation
misc_printer.ml 710 Bytes 230b168e about 4 years Guillaume DAVY Ada: Refactor Ada Backend to reduce redundancy,...

Latest revisions

# Date Author Comment
75c459f4 05/04/2021 06:24 PM Lélio Brun

start with Spec AST generation
7ee5f69e 05/04/2021 10:20 AM Lélio Brun

corrections on loggers + spec in AST
ca7e8027 02/05/2021 02:36 PM Lélio Brun

fix almost all warnings
719ae9fd 02/03/2021 02:47 PM Lélio Brun

migration draft on dune
04a188ec 11/21/2019 03:45 AM Pierre-Loïc Garoche

- Refactored Error exception and messages
- Bugs in partial evaluation for equalities among bool constants
and a nice recursive call generating a stack overflow! Now solved
- Setup a timeout for z3 in seal
- Better log for seal
c2db420f 11/20/2019 05:09 PM Pierre-Loïc Garoche

comment some code to avoid warning at compile time
e8f55c25 11/15/2019 12:34 AM Pierre-Loïc Garoche

- tag_true and tag_false moved to lustre_types
- real constants are hidden in Real.ml{i} module
05f85b44 04/29/2019 01:53 PM Guillaume DAVY

Ada: Start cleaning Ada to prepare for why beckend
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.

View revisions

Also available in: Atom