major branche merging salsa/mpfr with trunk
Merge of last trunk commitsAdded fbyn(expr, n, init) to encodeinit -> pre (init -> pre (init -> ... pre expr))with n occurences of init
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...
Prepare for tagging : Xia version 1.0
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
- 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...
- 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
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