CristalCaveGem » LustreC

riny

Post 1.1 release.
Back to dev version

prepare lustrec 1.1

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

Put back the test path

Ca marche mieux avec le fichier

Ignore rm error in clean rules

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

Merge r458 fix into trunk

- 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

small logging change

Bug fixed for horn traces option with stateful asserts

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

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

corrected a small bug when -horn option was active

some optimization in code optimization !!

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

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

some tiny mistakes corrected...

some cosmetic changes in error messages when loading libraries

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

Cleaning lusic when installing

horn queries back

Add teme

Post Xia dev

Prepare for tagging : Xia version 1.0

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

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

added some test files

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

synch with svn

fixing double printing of horn rules

Fixed conflict with the svn trunk version

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

Print the types

revert back to previous expression for path

mapping horn values to lustre values in xml format

sync horn backend

sync horn backend

modifed / to div in horn backend

fixing double printing of horn rules

Changed configuration and update the horn_backend.ml

Fixed conflict with the svn trunk version

Install FindLustre.cmake as well

Changed the option horntraces to a general traces option
This annotation phases would have to be moved in optimization of normalized code

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

README.md edited online with Bitbucket

added invariants

including invariants

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

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.

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

Added an install target in the src folder

modified optimization info printout (option -print_reuse)

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

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.

Moved Makefile into src folder

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

Almost nothing

Properly handle generated files

Doc file

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

- Dealt with compiling lusic from distant lusi files.
- Header now do not allow the generation of function previously declared as C prototype

Small update

Add first version of FindLustre.cmake

Added compilation and install of include/*.lusi

Add more functions in math.lusi

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

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

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

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

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

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

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

- work in progress for automata...

- more work towards automata

- some steps towards integration of automata

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

- corrected bugs with the inlining mode

- corrected bug with destination directory (-d option)
- corrected several bugs in inlining
- STILL, BUGS REMAINING in inlined code !!??!!

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

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

added some functions, prior to code refactoring

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

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

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

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

- corrected a small bug in clock calculus

- several bugs corrected when mixing tuples with clocks

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

Updated the licence info and header for each file.
Moved backends in separate folders

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

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

added git version of svn_version

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

work in progress in liveness analysis...

work in progress (code optimization again)

Merged horn_traces branch

added some infrastructure to ease optimization (reusing vars)

Merged branches specification_reorg_corelang_parser (see last commit message, moved definitions/functions btw files and changed eexpr type)