Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src @ 7231d0e4

Name Size Revision Age Author Comment
Print.ml 2.69 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
Print.mli 5.31 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
access.ml 3.79 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
basic_library.ml 8.69 KB df647a81 almost 6 years Guillaume Davy First commit in acsl proof branch
c_backend.ml 75.9 KB df647a81 almost 6 years Guillaume Davy First commit in acsl proof branch
causality.ml 15.4 KB 2196a0a6 about 6 years Pierre-Loïc Garoche Cleaned tons of useless debugging prints
clock_calculus.ml 30.2 KB c518d082 about 6 years Xavier Thirioux - added generation of clock information in inte...
clock_predef.ml 1.77 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
clocks.ml 18 KB c518d082 about 6 years Xavier Thirioux - added generation of clock information in inte...
com_protocol.ml 6.41 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
corelang.ml 30 KB 302670bb about 6 years Pierre-Loïc Garoche Bug solved when using arrows in annotations. - ...
corelang.mli 9.07 KB 302670bb about 6 years Pierre-Loïc Garoche Bug solved when using arrows in annotations. - ...
deadline_calculus.ml 5.96 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
deadlines.ml 2.58 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
delay.ml 3.3 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
delay_predef.ml 1.55 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
dimension.ml 11.5 KB c518d082 about 6 years Xavier Thirioux - added generation of clock information in inte...
dot_backend.ml 4.33 KB df647a81 almost 6 years Guillaume Davy First commit in acsl proof branch
env.ml 2.06 KB 302670bb about 6 years Pierre-Loïc Garoche Bug solved when using arrows in annotations. - ...
expand.ml 11.1 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
horn_backend.ml 13.4 KB aa223e69 about 6 years Xavier Thirioux more steps towards struct types... Cette ligne,...
init_calculus.ml 11.5 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
init_predef.ml 2.62 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
inliner.ml 9.91 KB 302670bb about 6 years Pierre-Loïc Garoche Bug solved when using arrows in annotations. - ...
java_backend.ml 14.6 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
lexerLustreSpec.mll 3.44 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
lexer_lustre.mll 5.25 KB accbb04d over 6 years Xavier Thirioux - small bug correction in dimension typing - ...
lexer_prelude.mll 3.54 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
location.ml 2.88 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
log.ml 1.29 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
machine_code.ml 27.9 KB df647a81 almost 6 years Guillaume Davy First commit in acsl proof branch
main_lustre_compiler.ml 10.8 KB df647a81 almost 6 years Guillaume Davy First commit in acsl proof branch
normalization.ml 16.8 KB 7231d0e4 almost 6 years Guillaume Davy Trying to correct support for pre in acsl annot...
options.ml 3.48 KB df647a81 almost 6 years Guillaume Davy First commit in acsl proof branch
parse.ml 1.48 KB 6affc9f5 about 6 years Xavier Thirioux - added struct types declaration - added const...
parserLustreSpec.mly 7.11 KB 6affc9f5 about 6 years Xavier Thirioux - added struct types declaration - added const...
parser_lustre.mly 17.4 KB cfff99fd about 6 years Pierre-Loïc Garoche Solved bug when loading preexisting lusi files
precedence_functions.ml 2.92 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
printers.ml 14.1 KB 96fecb0f about 6 years Pierre-Loïc Garoche Lots of changes: mainly solved bugs - specifica...
scheduling.ml 5.31 KB 0cbf0839 over 6 years Pierre-Loïc Garoche Moved files to trunk in lustre_compiler
sortProg.ml 1.29 KB ae78dfee about 6 years Eric Noulard Do not use stable sort because it requires rece...
splitting.ml 4.32 KB 2196a0a6 about 6 years Pierre-Loïc Garoche Cleaned tons of useless debugging prints
type_predef.ml 2.96 KB aa223e69 about 6 years Xavier Thirioux more steps towards struct types... Cette ligne,...
types.ml 8.95 KB 96fecb0f about 6 years Pierre-Loïc Garoche Lots of changes: mainly solved bugs - specifica...
typing.ml 30.4 KB 2196a0a6 about 6 years Pierre-Loïc Garoche Cleaned tons of useless debugging prints
utils.ml 8.49 KB c02d255e about 6 years Pierre-Loïc Garoche Solved some bugs in the lustre printer Generati...

Latest revisions

# Date Author Comment
7231d0e4 05/20/2014 01:54 PM Guillaume Davy

Trying to correct support for pre in acsl annotation but it is not perfect.

df647a81 05/06/2014 03:01 PM Guillaume Davy

First commit in acsl proof branch

224d9d76 03/15/2014 02:01 PM Pierre-Loïc Garoche

Hack to avoid empty struct. This is mandatory for frama-c (for the moment)

57ec37a1 03/15/2014 01:56 PM Pierre-Loïc Garoche

New functions to identify stateless machines

07f1f2e1 03/15/2014 12:16 AM Pierre-Loïc Garoche

Modified the makefile to fit eacsl issues

1d3e339d 03/14/2014 03:28 PM Pierre-Loïc Garoche

Bug solved: comma in function calls

f2a319ff 03/14/2014 02:49 PM Pierre-Loïc Garoche

ACSL spec: produce memory related properties: valid pointers, speration, assigns

302670bb 03/14/2014 01:56 AM Pierre-Loïc Garoche

Bug solved when using arrows in annotations.
- arrows are inlined
- specification memories are initialized in the reset function.

a64d9fe9 03/12/2014 07:12 PM Pierre-Loïc Garoche

Bug solved on complex ACSL predicates

df52f39b 03/12/2014 06:10 PM Pierre-Loïc Garoche

Default is "no ghost mode"

View revisions

Also available in: Atom