Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  backends 5cf953ec almost 10 years Teme Kahsai Fixed horn backend to make query for properties...
Makefile.in 1 KB 40875a30 about 10 years Pierre-Loïc Garoche Added an install target in the src folder git-...
_tags 275 Bytes e8b6d5ca about 10 years Pierre-Loïc Garoche Moved Makefile into src folder git-svn-id: ht...
access.ml 3.58 KB b08ffca7 over 10 years Xavier Thirioux - work in progress for automata... git-svn-i...
automata.ml 13.1 KB b4d9710b over 10 years Xavier Thirioux - corrected bug in node reset clock - cleaner ...
basic_library.ml 7.21 KB ef34b4ae over 10 years Xavier Thirioux This is a major revision: - added interface f...
causality.ml 19.4 KB d0b1ec56 over 10 years Xavier Thirioux - changed the basic optimization scheme (option...
clock_calculus.ml 31.8 KB b4d9710b over 10 years Xavier Thirioux - corrected bug in node reset clock - cleaner ...
clock_predef.ml 1.67 KB 70df2f87 over 10 years Xavier Thirioux - corrected bugs with the inlining mode git-s...
clocks.ml 19.9 KB 54d032f5 over 10 years Xavier Thirioux - Added major feature: Lustre V6 automata !!! ...
compiler_common.ml 8.16 KB 58a463e7 about 10 years Pierre-Loïc Garoche Added a construct for Dependencies (was a tuple...
corelang.ml 32.3 KB f2b1c245 almost 10 years Pierre-Loïc Garoche Solved bug found by Teme about asserts. Previo...
corelang.mli 5.07 KB 54d032f5 over 10 years Xavier Thirioux - Added major feature: Lustre V6 automata !!! ...
delay.ml 2.97 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
delay_predef.ml 1.28 KB ef34b4ae over 10 years Xavier Thirioux This is a major revision: - added interface f...
dimension.ml 10.5 KB ed81df06 over 10 years Xavier Thirioux added some functions, prior to code refactoring...
env.ml 1.62 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
expand.ml 10.8 KB 54d032f5 over 10 years Xavier Thirioux - Added major feature: Lustre V6 automata !!! ...
init_calculus.ml 11.1 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
init_predef.ml 2.29 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
inliner.ml 11.1 KB b08ffca7 over 10 years Xavier Thirioux - work in progress for automata... git-svn-i...
lexerLustreSpec.mll 4.13 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
lexer_lustre.mll 5.12 KB ef34b4ae over 10 years Xavier Thirioux This is a major revision: - added interface f...
lexer_prelude.mll 3.21 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
liveness.ml 11.3 KB d0b1ec56 over 10 years Xavier Thirioux - changed the basic optimization scheme (option...
location.ml 2.86 KB ef34b4ae over 10 years Xavier Thirioux This is a major revision: - added interface f...
log.ml 874 Bytes a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
lusic.ml 2.62 KB 9603460e over 10 years Xavier Thirioux - corrected bug with destination directory (-d ...
lustreSpec.ml 6.33 KB 58a463e7 about 10 years Pierre-Loïc Garoche Added a construct for Dependencies (was a tuple...
machine_code.ml 18.9 KB f2b1c245 almost 10 years Pierre-Loïc Garoche Solved bug found by Teme about asserts. Previo...
main_lustre_compiler.ml 12.1 KB f2b1c245 almost 10 years Pierre-Loïc Garoche Solved bug found by Teme about asserts. Previo...
modules.ml 7.15 KB 1e48ef45 about 10 years Pierre-Loïc Garoche - Dealt with compiling lusic from distant lusi ...
myocamlbuild.ml.in 295 Bytes e8b6d5ca about 10 years Pierre-Loïc Garoche Moved Makefile into src folder git-svn-id: ht...
normalization.ml 16.6 KB f2b1c245 almost 10 years Pierre-Loïc Garoche Solved bug found by Teme about asserts. Previo...
optimize_machine.ml 10.9 KB d0b1ec56 over 10 years Xavier Thirioux - changed the basic optimization scheme (option...
optimize_prog.ml 4.43 KB d0b1ec56 over 10 years Xavier Thirioux - changed the basic optimization scheme (option...
options.ml 4.34 KB 5cf953ec almost 10 years Teme Kahsai Fixed horn backend to make query for properties...
parse.ml 1.36 KB ef34b4ae over 10 years Xavier Thirioux This is a major revision: - added interface f...
parserLustreSpec.mly 7.98 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
parser_lustre.mly 15.6 KB 54d032f5 over 10 years Xavier Thirioux - Added major feature: Lustre V6 automata !!! ...
printers.ml 12.6 KB 54d032f5 over 10 years Xavier Thirioux - Added major feature: Lustre V6 automata !!! ...
scheduling.ml 8.04 KB 790765c0 about 10 years Xavier Thirioux modified optimization info printout (option -pr...
sortProg.ml 2 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
splitting.ml 3.17 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
stateless.ml 2.88 KB b08ffca7 over 10 years Xavier Thirioux - work in progress for automata... git-svn-i...
type_predef.ml 2.66 KB a2d97a3e over 10 years Pierre-Loïc Garoche Updated the licence info and header for each fi...
types.ml 9.64 KB ef34b4ae over 10 years Xavier Thirioux This is a major revision: - added interface f...
typing.ml 29.1 KB 54d032f5 over 10 years Xavier Thirioux - Added major feature: Lustre V6 automata !!! ...
utils.ml 8.76 KB 45c13277 over 10 years Xavier Thirioux - added missing constraint check when sub-clock...
version.ml.in 107 Bytes 1e48ef45 about 10 years Pierre-Loïc Garoche - Dealt with compiling lusic from distant lusi ...

Latest revisions

# Date Author Comment
5cf953ec 03/03/2015 09:10 PM Teme Kahsai

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@410 041b043f-8d7c-46b2-b46e-ef0dd855326e

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@406 041b043f-8d7c-46b2-b46e-ef0dd855326e

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@387 041b043f-8d7c-46b2-b46e-ef0dd855326e

40875a30 12/10/2014 11:14 AM Pierre-Loïc Garoche

Added an install target in the src folder

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@386 041b043f-8d7c-46b2-b46e-ef0dd855326e

790765c0 12/09/2014 04:54 PM Xavier Thirioux

modified optimization info printout (option -print_reuse)

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@385 041b043f-8d7c-46b2-b46e-ef0dd855326e

862ccfb1 12/09/2014 04:30 PM Xavier Thirioux

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@384 041b043f-8d7c-46b2-b46e-ef0dd855326e

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@383 041b043f-8d7c-46b2-b46e-ef0dd855326e

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

Moved Makefile into src folder

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@382 041b043f-8d7c-46b2-b46e-ef0dd855326e

58a463e7 12/08/2014 09:09 PM Pierre-Loïc Garoche

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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@380 041b043f-8d7c-46b2-b46e-ef0dd855326e

1e48ef45 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

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@375 041b043f-8d7c-46b2-b46e-ef0dd855326e

View revisions

Also available in: Atom