CristalCaveGem » LustreC

sync horn backend

fixing double printing of horn rules

Fixed conflict with the svn trunk version

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

added invariants

including invariants

Fixed horn backend to make query for properties. More work needed for cex

Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful

- Dealt with compiling lusic from distant lusi files.
- Header now do not allow the generation of function previously declared as C prototype

- corrected a bug in C code generation for multi-dimension arrays

- corrected bug in node reset clock
- cleaner (but heavier !) code generation scheme for automata

- Added major feature: Lustre V6 automata !!!
- one automata example added
- changed the reset condition in node calls (now a simple bool expr)
- bug corrected in clock calculus
- bug corrected in traceability info
- added field in variables to test whether they are original...

- work in progress for automata...

This is a major revision:
- added interface files (.lusi) in the language, that can be compiled on their own, giving an object file (.lusic) and a header file (.h)
- modular code generation, from Lustre to C level included.
- nice amount of code refactoring

Updated the licence info and header for each file.
Moved backends in separate folders

Merged horn_traces branch

Prepared first stage of code reorg:
1. moved type def in lustrespec.ml
2. moved constructor and basic functions in corelang
3. Modified eexpr with prenext quantifiers

Merged trunk updates

Specialized the prefix/postfix modifiers through functors arguments

Split all functions of C backends in separate files

Moved c_backend in separate folder