History | View | Annotate | Download (4.35 KB)
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
Fixed horn backend to make query for properties. More work needed for cex
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