CristalCaveGem » LustreC

improved code generation by factorizing out arrows

Version compatible avec le francais

Updated test script: changed path and verbose mode

Moved tests outside of source code to avoid useless duplication.

Added Alice Tailliar example

In order to export any type of constants, moved type definitions from .c to .h

- stupid svn had removed a file, again

- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files

Updated script. Does not seem to be fully functional yet.

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