Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  backends 4240dfcb 10 months Lélio Brun add basic support to protect against some ACSL ...
  checks d29fbec5 11 months Lélio Brun working version for stateful contracts
  features d978c46e about 1 year Lélio Brun start instrumenting the main C function
  parsers 9c227bad 10 months Lélio Brun fix offline tests
  plugins d29fbec5 11 months Lélio Brun working version for stateful contracts
  tools d29fbec5 11 months Lélio Brun working version for stateful contracts
  utils 9c227bad 10 months Lélio Brun fix offline tests
Makefile-lustresf.in 758 Bytes 3b4b7a2e over 4 years Christophe Garion [lustresf] lustresf targets are optional in Mak...
Makefile.in 1.58 KB 325f07c0 over 3 years Christophe Garion doc: use SVG format instead of PNG for dependen...
_tags.in 2.04 KB b43b8eb5 over 1 year Pierre-Loic Garoche add thread dependency required by z3 lib
annotations.ml 1.15 KB 50a8778a about 1 year Lélio Brun refactoring first step
annotations.mli 238 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
arrow.ml 926 Bytes 50a8778a about 1 year Lélio Brun refactoring first step
arrow.mli 164 Bytes ca7ff3f7 about 1 year Lélio Brun reformatting
automata.ml 16.4 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
automata.mli 543 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
basic_library.ml 11.8 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
basic_library.mli 662 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
causality.ml 27.2 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
causality.mli 2.5 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
clock_calculus.ml 26.7 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
clock_calculus.mli 335 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
clock_predef.ml 1.89 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
clock_predef.mli 131 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
clocks.ml 14.3 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
clocks.mli 2.52 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
compiler_common.ml 15 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
compiler_common.mli 824 Bytes d29fbec5 11 months Lélio Brun working version for stateful contracts
compiler_stages.ml 12.7 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
compiler_stages.mli 359 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
corelang.ml 49.5 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
corelang.mli 8.46 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
delay.ml 2.82 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
delay.mli 371 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
delay_predef.ml 1.33 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
delay_predef.mli 144 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
dune 3.46 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
error.ml 1.78 KB 9c227bad 10 months Lélio Brun fix offline tests
error.mli 476 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
global.ml 643 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
global.mli 128 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
inliner.ml 21.9 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
inliner.mli 142 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
log.ml 1 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
log.mli 111 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
lusic.ml 3.39 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
lusic.mli 476 Bytes d29fbec5 11 months Lélio Brun working version for stateful contracts
lustre_live.ml 3.67 KB e164da10 10 months Lélio Brun fix live variable calculation for spec: take va...
lustre_live.mli 256 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
lustre_types.ml 7.51 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
lustre_types.mli 6.05 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
lustrec.odocl 1.05 KB aa85bd44 over 3 years Guillaume DAVY Doc: update rule and remove old module in odocl
machine_code.ml 21.7 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
machine_code.mli 135 Bytes ca7ff3f7 about 1 year Lélio Brun reformatting
machine_code_common.ml 16.9 KB 10131419 10 months Lélio Brun add offline tests and fix a bug in generated sp...
machine_code_common.mli 1.88 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
machine_code_types.mli 2.22 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
main_lustre_compiler.ml 4.9 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
main_lustre_testgen.ml 7.44 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
main_lustre_verifier.ml 5.37 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
modules.ml 12 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
modules.mli 826 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
mutation.ml 29 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
mutation.mli 480 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
normalization.ml 34.3 KB dccec723 11 months Lélio Brun a version that almost work for the k-inuctive t...
normalization.mli 347 Bytes 5b98398a about 1 year Lélio Brun first version working with stateless contracts
optimize_machine.ml 33.3 KB 10131419 10 months Lélio Brun add offline tests and fix a bug in generated sp...
optimize_machine.mli 719 Bytes d29fbec5 11 months Lélio Brun working version for stateful contracts
optimize_prog.ml 4.99 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
optimize_prog.mli 67 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
options.ml 2.42 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
options.mli 1.29 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
options_management.ml 9.78 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
options_management.mli 504 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
pathConditions.ml 12.4 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
pathConditions.mli 60 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
printers.ml 22.8 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
printers.mli 1.09 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
real.ml 1.34 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
real.mli 653 Bytes ca7ff3f7 about 1 year Lélio Brun reformatting
scheduling.ml 10.6 KB d29fbec5 11 months Lélio Brun working version for stateful contracts
scheduling.mli 732 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
scheduling_type.mli 561 Bytes 50a8778a about 1 year Lélio Brun refactoring first step
sortProg.ml 2.42 KB 5b98398a about 1 year Lélio Brun first version working with stateless contracts
sortProg.mli 101 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
spec.ml 538 Bytes ca7ff3f7 about 1 year Lélio Brun reformatting
spec.mli 66 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
spec_common.ml 2.92 KB 10131419 10 months Lélio Brun add offline tests and fix a bug in generated sp...
spec_common.mli 672 Bytes 10131419 10 months Lélio Brun add offline tests and fix a bug in generated sp...
spec_types.ml 1.61 KB 10131419 10 months Lélio Brun add offline tests and fix a bug in generated sp...
spec_types.mli 1.5 KB 10131419 10 months Lélio Brun add offline tests and fix a bug in generated sp...
splitting.ml 3.52 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
splitting.mli 100 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
type_predef.ml 3.36 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
type_predef.mli 1 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
types.ml 16.1 KB 81d69074 10 months Lélio Brun fix bug where singleton tuples were generated
types.mli 3.18 KB 81d69074 10 months Lélio Brun fix bug where singleton tuples were generated
typing.ml 39.9 KB 81d69074 10 months Lélio Brun fix bug where singleton tuples were generated
typing.mli 1.05 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
verifierList.ml 166 Bytes ca7ff3f7 about 1 year Lélio Brun reformatting
verifierList.mli 53 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
verifierType.mli 336 Bytes 2926ceee about 1 year Lélio Brun mli additions complete
verifiers.ml 1.19 KB d978c46e about 1 year Lélio Brun start instrumenting the main C function
verifiers.mli 104 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
version.ml 185 Bytes ca7ff3f7 about 1 year Lélio Brun reformatting
version.mli 97 Bytes cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...

Latest revisions

# Date Author Comment
4240dfcb 10/06/2021 06:04 PM Lélio Brun

add basic support to protect against some ACSL keywords

e164da10 10/06/2021 05:12 PM Lélio Brun

fix live variable calculation for spec: take variables occuring in clocks into account

fb6e2cfd 10/06/2021 12:52 PM Lélio Brun

print (*mem) instead of *mem to avoid ambiguities with accesses

e77a0fa5 10/06/2021 11:25 AM Lélio Brun

fix handling of state variables in spec expressions

81d69074 10/06/2021 10:18 AM Lélio Brun

fix bug where singleton tuples were generated

9c227bad 10/05/2021 01:55 PM Lélio Brun

fix offline tests

10131419 10/05/2021 11:17 AM Lélio Brun

add offline tests and fix a bug in generated spec where optimization was not performed

b2ad5de3 10/01/2021 01:46 PM Lélio Brun

fix tests procedure

89fd79f0 09/27/2021 06:00 PM Lélio Brun

a working version for automata with 'last' case of enums as default case

d29fbec5 09/27/2021 01:36 PM Lélio Brun

working version for stateful contracts

View revisions

Also available in: Atom