| Branch: | Tag: | Revision:

# Date Author Comment
4f4a77a4 04/08/2015 11:01 PM Xavier Thirioux

some tiny mistakes corrected...

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...

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

Prepare for tagging : Xia version 1.0

b3f91fdb 04/03/2015 06:22 PM Xavier Thirioux

LOTS of bug correction wrt inlining, still a work in progress...
- global constants were not accounted for
- no good avoidance of name capture when inlining
- static parameters (array sizes and clocks) not handled
- ill-typed generated expressions, when inlining array expressions

7dd90f72 04/01/2015 06:41 PM Xavier Thirioux

added some test files

e9c64a30 03/05/2015 11:48 PM Pierre-Loïc Garoche

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

6a1a01d2 09/14/2014 08:08 PM Xavier Thirioux

- Added major feature: Lustre V6 automata !!!
- one automata example added
- changed the reset condition in node calls (now a simple bool expr)
- bug corrected in clock calculus
- bug corrected in traceability info
- added field in variables to test whether they are original...

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

67ba882b 03/17/2014 07:44 AM Pierre-Loïc Garoche

Moved tests outside of source code to avoid useless duplication.

cbe93c65 03/17/2014 07:40 AM Pierre-Loïc Garoche

Added Alice Tailliar example

6bab3787 03/05/2014 02:35 PM Xavier Thirioux

In order to export any type of constants, moved type definitions from .c to .h

3e79b3a5 03/01/2014 03:38 PM Xavier Thirioux

- stupid svn had removed a file, again

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.

3e36d4e0 02/28/2014 11:59 PM Pierre-Loïc Garoche

Added default ensures statements

7f611a35 02/28/2014 05:09 PM Xavier Thirioux

- added dummy_lib.lusi (accidentally removed !?)

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.

7bc15356 02/05/2014 03:03 PM Pierre-Loïc Garoche

lego robot example

ed226e0d 11/25/2013 10:39 AM Xavier Thirioux

missing dummy lib for arrays

accbb04d 11/07/2013 07:03 PM Xavier Thirioux

- small bug correction in dimension typing
- #open keyword instead of open
- dummy generic matrix/vector library interface added
- modified examples according to the new syntax

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