Merged horn_traces branch
Update on the test script
Updated list with new tests
added liveness analysis for reusing dead variables. Not yet used.
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.
Solved some bugs in the lustre printerGeneration of a witness with both the main node and hte inlined main nodeTest 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