Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / options.ml @ 5500edb8

History | View | Annotate | Download (4.36 KB)

# Date Author Comment
9b04601c 08/18/2015 11:51 AM Eric Noulard

Post 1.1 release.
Back to dev version
3fb19815 08/13/2015 04:58 PM Eric Noulard

prepare lustrec 1.1
5fe9fe22 05/05/2015 01:29 AM Teme Kahsai

changed name from -horn-queries to -horn-query
01d48bb0 04/08/2015 10:03 PM Xavier Thirioux

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...
f8b3de19 04/08/2015 03:54 PM Pierre-Loïc Garoche

horn queries back
00b2c9f8 04/08/2015 08:53 AM Pierre-Loïc Garoche

Post Xia dev
ba2f9fa1 04/08/2015 08:50 AM Pierre-Loïc Garoche

Prepare for tagging : Xia version 1.0
c065827c 03/06/2015 11:09 AM Pierre-Loïc Garoche

Changed the option horntraces to a general traces option
This annotation phases would have to be moved in optimization of normalized code
3c862628 03/03/2015 09:10 PM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex
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