History | View | Annotate | Download (4.36 KB)
Post 1.1 release.Back to dev version
prepare lustrec 1.1
changed name from -horn-queries to -horn-query
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...
horn queries back
Post Xia dev
Prepare for tagging : Xia version 1.0
Changed the option horntraces to a general traces optionThis annotation phases would have to be moved in optimization of normalized code
Fixed horn backend to make query for properties. More work needed for cex
added a new option -print_reuse that prints clock disjoint variables and reuse policy. useful for debugging and carrying correctness proofs to the C code level. non trivial result only when option -O 3 or above is activated.
- Dealt with compiling lusic from distant lusi files.- Header now do not allow the generation of function previously declared as C prototype
- corrected bug with destination directory (-d option) - corrected several bugs in inlining - STILL, BUGS REMAINING in inlined code !!??!!
added some functions, prior to code refactoring
Updated the licence info and header for each file.Moved backends in separate folders
Merged horn_traces branch
Merged trunk updates
Restructured the main: call to optimization, scheduling performed out of machine_code, etcMerge Xavier last commitsUnfinished lustre backend
Reenabled the generation of witnesses for inline process.Systematic use of the build path
- merged test script - added -d support - corrected #open parser problem - corrected interface/implementation (.lusi/.lus) checking for types (not yet for clocks)
Merge back horn backend branch in trunk
Merge trunk modif in branch
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
Initial copy of the horn output version. Not really working yet
Moved files to trunk in lustre_compiler