Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ 97d3f81a

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

Latest revisions

# Date Author Comment
97d3f81a 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

58272238 03/16/2015 08:31 PM Teme Kahsai

modifed / to div in horn backend

24a55d0d 03/16/2015 08:30 PM Teme Kahsai

fixing double printing of horn rules

62f65f02 03/16/2015 08:30 PM Teme Kahsai

Fixed conflict with the svn trunk version

c065827c 03/06/2015 11:09 AM Pierre-Loïc Garoche

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

e9c64a30 03/05/2015 11:48 PM Pierre-Loïc Garoche

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

f133f964 03/03/2015 09:10 PM Teme Kahsai

added invariants

ea94d58f 03/03/2015 09:10 PM Teme Kahsai

including invariants

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.

View revisions

Also available in: Atom