Bug fixed for horn traces option with stateful asserts
do not use lusi for horn, and some logging for horn
Major revision due to severe limitations and bugs of inlining capabilities: - destination dir should now work properly - lusic files now have a version number, to avoid nasty segfaults when loading lusic files created by an older compiler version - inlining should now work with generic nodes and generic array library...
LOTS of bug correction wrt inlining, still a work in progress... - global constants were not accounted for - no good avoidance of name capture when inlining - static parameters (array sizes and clocks) not handled - ill-typed generated expressions, when inlining array expressions
Changed the option horntraces to a general traces optionThis annotation phases would have to be moved in optimization of normalized code
Reactivated the generation of traceability informationChanged the test-compile to use the horn-traces and the horn-queries option
Solved bug found by Teme about asserts.
Previously assert expression containing -> would lead to unnormalized ite. Now each expression within the assert is normalized and may bind new node equations.This could be later optimized but is working now.
- corrected a bug in optimizating mode (option -O 3) - changed the printing of unused variables
- 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
- started refactoring type definitions in .lus/.lusi, in order to ease the way .lusi interface files are handled.
- added missing constraint check when sub-clocking tuple expressions - added an algorithm that reuses dead or clock-disjoint variables instead of declaring/using new ones. - NOT carefully tested. Use option -O 3 if you want to give it a try...
Updated the licence info and header for each file.Moved backends in separate folders
- many bugs/limitations in lifting operators to tuples have been worked out: - typing/clock calculus/normalization now work properly - still, a bug in annot generation (this one is for Ploc !!) in file normalization, line 396 - bug corrected in subtyping...
Merged horn_traces branch
Prepared first stage of code reorg:1. moved type def in lustrespec.ml2. moved constructor and basic functions in corelang3. Modified eexpr with prenext quantifiers
Added the lustre backendStill some work on adapating the instruction scheduling
- corrected causality bug (cf. previous commit)
improved code generation by factorizing out arrows
- work in progress for stateless/stateful status computation (to turn conditionals into merges, which yield more efficient C code)
Merge (if it works) of the lustre interfaces branche providing lusi files into trunk
Moved files to trunk in lustre_compiler