Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / options.ml @ e42fb618

History | View | Annotate | Download (4.35 KB)

# Date Author Comment
c825868a 12/09/2014 02:03 PM Xavier Thirioux

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.
5ae8db15 12/01/2014 11:32 PM Pierre-Loïc Garoche

- Dealt with compiling lusic from distant lusi files.
- Header now do not allow the generation of function previously declared as C prototype
3f823d04 09/02/2014 05:46 PM Xavier Thirioux

- corrected bug with destination directory (-d option)
- corrected several bugs in inlining
- STILL, BUGS REMAINING in inlined code !!??!!
7dedc5f0 07/15/2014 02:15 PM Xavier Thirioux

added some functions, prior to code refactoring
b38ffff3 07/09/2014 09:57 AM Pierre-Loïc Garoche

Updated the licence info and header for each file.
Moved backends in separate folders
fcf1fd96 07/09/2014 12:35 AM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex
36454535 07/03/2014 10:46 PM Pierre-Loïc Garoche

Merged horn_traces branch
e95470b3 06/25/2014 05:37 PM Pierre-Loïc Garoche

Merged trunk updates
59294251 06/24/2014 03:57 PM Pierre-Loïc Garoche

Restructured the main: call to optimization, scheduling performed out of machine_code, etc
Merge Xavier last commits
Unfinished lustre backend
2842f7ca 03/01/2014 12:01 AM Pierre-Loïc Garoche

Reenabled the generation of witnesses for inline process.
Systematic use of the build path
8b3afe43 02/28/2014 04:56 PM Xavier Thirioux

- merged test script
- added -d support
- corrected #open parser problem
- corrected interface/implementation (.lusi/.lus) checking
for types (not yet for clocks)
29ad4531 02/28/2014 03:28 PM Pierre-Loïc Garoche

Merge back horn backend branch in trunk
64aa99c4 02/28/2014 02:05 PM Pierre-Loïc Garoche

Merge trunk modif in branch
c02d255e 02/28/2014 10:33 AM Pierre-Loïc Garoche

Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process
f6923c9e 02/19/2014 05:02 PM Pierre-Loïc Garoche

Initial copy of the horn output version. Not really working yet
0cbf0839 10/02/2013 08:13 AM Pierre-Loïc Garoche

Moved files to trunk in lustre_compiler