Project

General

Profile

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

Latest revisions

# Date Author Comment
3d1f9d9f 10/07/2021 01:27 PM Lélio Brun

more agressive optim propagation in spec in order to remove unecessarry existential variables that were eliminated (helps the solvers)

74ebe1f9 10/06/2021 06:32 PM Lélio Brun

fix bug in handling state variables in nested expressions

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

View revisions

Also available in: Atom