CristalCaveGem » LustreC

Added default ensures statements

- added dummy_lib.lusi (accidentally removed !?)

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)

Merge trunk modif in branch

Merge inlining branch within trunk.
The test target requires branch lustrec/horn as binary lustreh.

Minor bugs

Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process

Improvements as suggested by e. Noulard: better install of include; modified generated makefile

Updated version of test script: timeout for z3

First fully working version of horn backend.

Has to be called with "-horn -node main_node"

The test script compute the smt2 file and calls z3 on them.

lego robot example

missing dummy lib for arrays

- small bug correction in dimension typing
- #open keyword instead of open
- dummy generic matrix/vector library interface added
- modified examples according to the new syntax

Merge (if it works) of the lustre interfaces branche providing lusi files into trunk

Moved files to trunk in lustre_compiler