Project

General

Profile

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

Latest revisions

# Date Author Comment
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

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

View revisions

Also available in: Atom