- Mar 24, 2015
-
-
Pierre Loic Garoche authored
-
- Mar 17, 2015
-
-
Pierre Loic Garoche authored
-
Pierre Loic Garoche authored
-
- Mar 16, 2015
-
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
- Mar 12, 2015
-
-
Eric Noulard authored
-
- Mar 06, 2015
-
-
Pierre Loic Garoche authored
This annotation phases would have to be moved in optimization of normalized code
-
- Mar 05, 2015
-
-
Pierre Loic Garoche authored
Changed the test-compile to use the horn-traces and the horn-queries option
-
- Mar 03, 2015
-
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
Temesghen Kahsai authored
-
- Feb 16, 2015
-
-
Pierre Loic Garoche authored
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.
-
- Dec 10, 2014
-
-
Pierre Loic Garoche authored
Revert the commit 384 by Xavier: adding dirname to the source_name introduced a bug: the .h file is empty!!! Strange behavior.
-
Pierre Loic Garoche authored
-
- Dec 09, 2014
-
-
THIRIOUX Xavier authored
-
THIRIOUX Xavier authored
-
THIRIOUX Xavier authored
useful for debugging and carrying correctness proofs to the C code level. non trivial result only when option -O 3 or above is activated.
-
Pierre Loic Garoche authored
-
- Dec 08, 2014
-
-
Pierre Loic Garoche authored
-
Pierre Loic Garoche authored
-
Eric Noulard authored
-
- Dec 01, 2014
-
-
Pierre Loic Garoche authored
-
Pierre Loic Garoche authored
-
Pierre Loic Garoche authored
- Header now do not allow the generation of function previously declared as C prototype
-
Eric Noulard authored
-
Eric Noulard authored
-
Pierre Loic Garoche authored
-
Eric Noulard authored
-
- Nov 27, 2014
-
-
THIRIOUX Xavier authored
-
- Sep 29, 2014
-
-
THIRIOUX Xavier authored
-
- Sep 26, 2014
-
-
THIRIOUX Xavier authored
local variables and global variables that are either cheap to evaluate or used no more than once.
-
- Sep 24, 2014
-
-
THIRIOUX Xavier authored
- changed the printing of unused variables
-
- Sep 18, 2014
-
-
THIRIOUX Xavier authored
- cleaner (but heavier !) code generation scheme for automata
-
- Sep 14, 2014
-
-
THIRIOUX Xavier authored
- 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 or created by normalization process: better error message for causality problems Warning: this is the first working version of automata, needs further testing (and debugging). AFAIK, the semantics is close to Lustre V6, but further changes may be needed to equate them.
-