| Branch: | Tag: | Revision:

lustrec / test / @ e42fb618

History | View | Annotate | Download (6.78 KB)

# Date Author Comment
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 !!??!!

36454535 07/03/2014 10:46 PM Pierre-Loïc Garoche

Merged horn_traces branch

839ca600 06/17/2014 11:56 PM Pierre-Loïc Garoche

Update on the test script

4437ddbc 05/19/2014 01:57 PM Pierre-Loïc Garoche

Updated list with new tests

6cf31814 03/18/2014 06:05 PM Xavier Thirioux

added liveness analysis for reusing dead variables. Not yet used.

14ebde97 03/17/2014 01:01 PM Xavier Thirioux

improved code generation by factorizing out arrows

8a5f633d 03/17/2014 12:46 PM Pierre-Loïc Garoche

Version compatible avec le francais

1699b8ff 03/17/2014 09:06 AM Pierre-Loïc Garoche

Updated test script: changed path and verbose mode

c518d082 03/01/2014 03:37 PM Xavier Thirioux

- added generation of clock information in interface (.lusi) files
- added clock checking between interface and implementation files

626e6f03 02/28/2014 11:59 PM Pierre-Loïc Garoche

Updated script. Does not seem to be fully functional yet.

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)

64aa99c4 02/28/2014 02:05 PM Pierre-Loïc Garoche

Merge trunk modif in branch

49b32cb6 02/28/2014 01:52 PM Pierre-Loïc Garoche

Merge inlining branch within trunk.
The test target requires branch lustrec/horn as binary lustreh.

b63536a0 02/28/2014 10:39 AM Pierre-Loïc Garoche

Minor bugs

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

b8ae1bbc 02/26/2014 07:48 AM Pierre-Loïc Garoche

Improvements as suggested by e. Noulard: better install of include; modified generated makefile

f1da5111 02/24/2014 04:47 PM Pierre-Loïc Garoche

Updated version of test script: timeout for z3

3e209698 02/24/2014 11:47 AM Pierre-Loïc Garoche

First fully working version of horn backend.

Has to be called with "-horn -node main_node"

The test script compute the smt2 file and calls z3 on them.

f22632aa 10/22/2013 10:39 AM Pierre-Loïc Garoche

Merge (if it works) of the lustre interfaces branche providing lusi files into trunk

0cbf0839 10/02/2013 08:13 AM Pierre-Loïc Garoche

Moved files to trunk in lustre_compiler