| Branch: | Tag: | Revision:

lustrec / src / @ 355b543d

History | View | Annotate | Download (4.46 KB)

# Date Author Comment
3d04f75e 10/23/2015 05:35 PM Pierre-Loïc Garoche


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