CristalCaveGem » LustreC

Plugin based framework

major branche merging salsa/mpfr with trunk

bug correction in typing: tuple types were computed but not recorded

bug corrected: in some cases, local const vars were assigned twice

numerous bugs corrected:
- bug in expansion of array accesses with constant arrays
- bug in printing complex array indexes (not C compliant)
- bug wrt C99 typing policy for constant arrays
- bug in signaling wrong useless static input

fixed a printing bug in horn backend

small logging change

do not use lusi for horn, and some logging for horn

some tiny mistakes corrected...

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...

corrected various bugs in the compilation/installation Makefile.in.

synch with svn

fixing double printing of horn rules

Print the types

mapping horn values to lustre values in xml format

sync horn backend

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