Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec @ 53206908

# Date Author Comment
53206908 11/26/2015 04:45 PM Xavier Thirioux

major branche merging salsa/mpfr with trunk

812c0369 11/22/2015 12:05 AM Xavier Thirioux

corrected pessimistic behavior of optimization phase -O 3

89137ae1 11/21/2015 10:14 PM Xavier Thirioux

bug correction in typing: tuple types were computed but not recorded

da07e470 11/07/2015 11:48 PM Xavier Thirioux

bug corrected: in some cases, local const vars were assigned twice

79614a15 11/07/2015 07:40 PM Xavier Thirioux

numerous bugs corrected:
- bug in expansion of array accesses with constant arrays
- bug in printing complex array indexes (not C compliant)
- bug wrt C99 typing policy for constant arrays
- bug in signaling wrong useless static input

6c4902ae 11/06/2015 06:09 PM Teme Kahsai

fixed a printing bug in horn backend

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

719f4b27 08/13/2015 03:52 PM Eric Noulard

Update FindLustre in order to handle a default VERBOSE option set to 0
and the proper c99 compiler option

94a9eddf 06/09/2015 03:00 PM Pierre-Loïc Garoche

Put back the test path

e0523910 06/09/2015 02:54 PM Pierre-Loïc Garoche

Ca marche mieux avec le fichier

b2a445af 06/09/2015 09:09 AM Eric Noulard

Ignore rm error in clean rules

ed736b69 06/05/2015 11:01 PM Pierre-Loïc Garoche

Merge of last trunk commits
Added fbyn(expr, n, init) to encode
init -> pre (init -> pre (init -> ... pre expr))
with n occurences of init

1b31ffde 05/13/2015 01:10 PM Eric Noulard

Merge r458 fix into trunk

e275249d 05/05/2015 10:43 PM Xavier Thirioux

- corrected a regression bug in main_lustre_compiler.ml (optional generation of lusic files was in a bad ocaml pattern-matching rule...)
- added a flush in Log to help find out the exact phase when the compiler crashes or stops silently

ad6b7375 05/05/2015 07:30 PM Teme Kahsai

small logging change

7a442071 05/05/2015 03:47 PM Pierre-Loïc Garoche

Bug fixed for horn traces option with stateful asserts

5fe9fe22 05/05/2015 01:29 AM Teme Kahsai

changed name from -horn-queries to -horn-query

9c4624e4 05/05/2015 01:17 AM Teme Kahsai

do not use lusi for horn, and some logging for horn

b3b0dd56 05/04/2015 08:13 AM Xavier Thirioux

corrected a small bug when -horn option was active

e24b2e9b 04/13/2015 10:08 AM Xavier Thirioux

some optimization in code optimization !!

5f31b494 04/09/2015 10:57 PM Xavier Thirioux

corrected a bug when activating optimization (-O 3) (edge missing in a dep graph)

3a958c40 04/08/2015 11:04 PM Xavier Thirioux

updated version of README.lustrec about how to install lustrec and how to compile.

4f4a77a4 04/08/2015 11:01 PM Xavier Thirioux

some tiny mistakes corrected...

b3543e39 04/08/2015 10:43 PM Xavier Thirioux

some cosmetic changes in error messages when loading libraries

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

8958262e 04/08/2015 04:01 PM Pierre-Loïc Garoche

Cleaning lusic when installing

f8b3de19 04/08/2015 03:54 PM Pierre-Loïc Garoche

horn queries back

330b42e3 04/08/2015 09:08 AM Pierre-Loïc Garoche

Add teme

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

e9350b02 04/04/2015 03:59 PM Xavier Thirioux

corrected various bugs in the compilation/installation Makefile.in.

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

f4acee4c 04/01/2015 04:10 PM Xavier Thirioux

correction of bugs:
- a small problem in the parser
- regarding the handling of destination directory, source directory, current directory, etc.
It seems to be working now. A nice chasing after weird behaviors...

933ee7a3 03/24/2015 09:54 PM Teme Kahsai

synch with svn

eec8ce11 03/24/2015 09:54 PM Teme Kahsai

fixing double printing of horn rules

a5193ff5 03/24/2015 09:54 PM Teme Kahsai

Fixed conflict with the svn trunk version

6394042a 03/24/2015 07:26 PM Pierre-Loïc Garoche

Added local inlining using the keyword (*! /inlining/:true *)

9d01f989 03/17/2015 08:30 AM Pierre-Loïc Garoche

Print the types

c9570528 03/17/2015 08:24 AM Pierre-Loïc Garoche

revert back to previous expression for path

720f159a 03/16/2015 08:31 PM Teme Kahsai

mapping horn values to lustre values in xml format

96d33ff2 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

97d3f81a 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

58272238 03/16/2015 08:31 PM Teme Kahsai

modifed / to div in horn backend

24a55d0d 03/16/2015 08:30 PM Teme Kahsai

fixing double printing of horn rules

545772c4 03/16/2015 08:30 PM Teme Kahsai

Changed configuration and update the horn_backend.ml

62f65f02 03/16/2015 08:30 PM Teme Kahsai

Fixed conflict with the svn trunk version

89f551c9 03/12/2015 02:24 PM Eric Noulard

Install FindLustre.cmake as well

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

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

56d3f3e1 03/03/2015 09:10 PM Teme Kahsai

README.md edited online with Bitbucket

f133f964 03/03/2015 09:10 PM Teme Kahsai

added invariants

ea94d58f 03/03/2015 09:10 PM Teme Kahsai

including invariants

3c862628 03/03/2015 09:10 PM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

e42fb618 02/16/2015 11:52 PM Pierre-Loïc Garoche

Solved bug found by Teme about asserts.

Previously assert expression containing -> would lead to unnormalized ite. Now each expression within the assert is normalized and may bind new node equations.
This could be later optimized but is working now.

13fa31c2 12/10/2014 11:15 AM Pierre-Loïc Garoche

Revert the commit 384 by Xavier: adding dirname to the source_name introduced a bug: the .h file is empty!!! Strange behavior.

5d8ddbf7 12/10/2014 11:14 AM Pierre-Loïc Garoche

Added an install target in the src folder

86b99b69 12/09/2014 04:54 PM Xavier Thirioux

modified optimization info printout (option -print_reuse)

fb8b1da7 12/09/2014 04:30 PM Xavier Thirioux

supports again relative path for lustre source file (regression bug)

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.

bed8ea64 12/09/2014 01:41 PM Pierre-Loïc Garoche

Moved Makefile into src folder

830de634 12/08/2014 09:09 PM Pierre-Loïc Garoche

Added a construct for Dependencies (was a tuple before) and a boolean attribute stateful

a6208edd 12/08/2014 09:06 PM Pierre-Loïc Garoche

Almost nothing

76b2936d 12/08/2014 02:36 PM Eric Noulard

Properly handle generated files

24d59df8 12/01/2014 11:37 PM Pierre-Loïc Garoche

Doc file

a8e66e98 12/01/2014 11:35 PM Pierre-Loïc Garoche

Removed oasis, now use the classical autoconf; ./configure; make

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

30a4debf 12/01/2014 03:13 PM Eric Noulard

Small update

801f63fa 12/01/2014 02:53 PM Eric Noulard

Add first version of FindLustre.cmake

c7879e4f 12/01/2014 01:56 PM Pierre-Loïc Garoche

Added compilation and install of include/*.lusi

ab51e2a7 12/01/2014 12:58 PM Eric Noulard

Add more functions in math.lusi

95763423 11/27/2014 03:30 PM Xavier Thirioux

corrected a bug that made an error silent, confusing users...

bc916448 09/29/2014 05:33 PM Xavier Thirioux

- corrected a bug in C code generation for multi-dimension arrays

307aba8d 09/26/2014 05:52 PM Xavier Thirioux

- changed the basic optimization scheme (option -O 2), which unfolds
local variables and global variables that are either cheap to evaluate
or used no more than once.

67896f6d 09/24/2014 12:13 PM Xavier Thirioux

- corrected a bug in optimizating mode (option -O 3)
- changed the printing of unused variables

d5fe9ac9 09/18/2014 05:25 PM Xavier Thirioux

- corrected bug in node reset clock
- cleaner (but heavier !) code generation scheme for automata

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

bc7b6c62 09/10/2014 06:01 PM Xavier Thirioux

- code complete for automata
- debugging in progress, not usable yet

1eda3e78 09/09/2014 06:03 PM Xavier Thirioux

- work in progress for automata...

77a01213 09/05/2014 03:06 PM Xavier Thirioux

- more work towards automata

29ced7be 09/04/2014 04:20 PM Xavier Thirioux

- some steps towards integration of automata

2ac56807 09/03/2014 08:47 PM Xavier Thirioux

- some code cleaning
- removed a potential source of bug in scheduler

cfdb4fe9 09/03/2014 04:02 PM Xavier Thirioux

- corrected bugs with the inlining mode

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 !!??!!

70e1006b 09/02/2014 02:43 PM Xavier Thirioux

This is a major revision:
- added interface files (.lusi) in the language, that can be compiled on their own, giving an object file (.lusic) and a header file (.h)
- modular code generation, from Lustre to C level included.
- nice amount of code refactoring

ed431cc2 07/15/2014 03:01 PM Xavier Thirioux

ooops, things got a bit scrambled with svn, restoring...

7dedc5f0 07/15/2014 02:15 PM Xavier Thirioux

added some functions, prior to code refactoring

6aeb3388 07/15/2014 09:27 AM Xavier Thirioux

- started refactoring type definitions in .lus/.lusi,
in order to ease the way .lusi interface files are handled.

084c1ce4 07/12/2014 02:23 PM Xavier Thirioux

- reimplementation of the reuse algorithm (option -O 3),
much more simple and efficient.

8fa083d5 07/11/2014 04:29 PM Xavier Thirioux

- still some improvements in optimizing in machine code ...

8ac7a0c7 07/11/2014 02:57 PM Xavier Thirioux

- missing case in clock disjunction predicate, the absence of which produced
weak (but still correct) optimization results.

32f508aa 07/10/2014 11:19 PM Xavier Thirioux

- corrected a small bug in clock calculus

d52e7821 07/10/2014 05:19 PM Xavier Thirioux

- several bugs corrected when mixing tuples with clocks

01f1a1f4 07/10/2014 12:49 PM Xavier Thirioux

- added missing constraint check when sub-clocking
tuple expressions
- added an algorithm that reuses dead or clock-disjoint
variables instead of declaring/using new ones.
- NOT carefully tested. Use option -O 3 if you want
to give it a try...

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

817d5bcb 07/09/2014 12:35 AM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

fcf1fd96 07/09/2014 12:35 AM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

15787c5b 07/08/2014 06:17 PM Teme Kahsai

added git version of svn_version

2cf39a8e 07/08/2014 04:53 PM Xavier Thirioux

- many bugs/limitations in lifting operators to tuples have been worked out:
- typing/clock calculus/normalization now work properly
- still, a bug in annot generation (this one is for Ploc !!)
in file normalization, line 396
- bug corrected in subtyping...