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
added some test files
Reactivated the generation of traceability informationChanged the test-compile to use the horn-traces and the horn-queries option
- corrected bug with destination directory (-d option) - corrected several bugs in inlining - STILL, BUGS REMAINING in inlined code !!??!!
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
- 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.
- 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.
Merge (if it works) of the lustre interfaces branche providing lusi files into trunk
Moved files to trunk in lustre_compiler