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
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 optionThis annotation phases would have to be moved in optimization of normalized code
Reactivated the generation of traceability informationChanged the test-compile to use the horn-traces and the horn-queries option
README.md edited online with Bitbucket
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
Properly handle generated files
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
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
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)
Prepared first stage of code reorg:1. moved type def in lustrespec.ml2. moved constructor and basic functions in corelang3. Modified eexpr with prenext quantifiers
more steps toward reusing variables (dead ones + clock disjoint ones)
added construction of a fanin table for local variables of a node. could be useful for a finer variable elimination scheme at the Lustre level. to be continued...
added warnings for useless variables (at verbose level 1) - exact definition of 'useless' may be further refined - display could certainly be improved
Merged with new specification backend: only eacsl makefile for the now on
Merged trunk updates
Solved Bug in horn backend: when main node is stateless
work in progress: - warnings for unused input/memory variables - optimization of machine code
New branch to copy the specgeneration using the new backend functors
Merged the new backend split into trunk
Specialized the prefix/postfix modifiers through functors arguments
Split all functions of C backends in separate files
Added the lustre backendStill some work on adapating the instruction scheduling
Moved c_backend in separate folder
Solved bug in optimization of machine code: output variable def should not be eliminated
Solved local var name bugs for stateless nodes as outlined by Teme
Added branch to separate code gen/file creation/spec/proof
Mini bug solved: do not unfold array constants
Restructured the main: call to optimization, scheduling performed out of machine_code, etcMerge Xavier last commitsUnfinished lustre backend
Extracted scheduling from machine code computation
Create a Step call only for functions that are not in basic lib
- bug correction (regression from previous versions !) introduced in C code generated from relational operators.
- refactorization of typing code (simpler subtyping rules) - simplification of clock calculus (may be still buggy, work in progress) no impact on unclocked programs.
Update on the test script
clean handling of undefined node application
Updated typing error
bug correction in homomorphic extension
typo corrected in code generation for array memories (bad parentheses)
Math lusi (trigo)
bug corrected for allocation of dynamic arrays in node memory