Project

General

Profile

Statistics
| Branch: | Tag: | Revision:
Name Size Revision Age Author Comment
  backends 53c9845b 10 months Lélio Brun fix optimization for variable reuse that was no...
  checks 17d63fff 10 months Lélio Brun remove unused variables after tag elimination i...
  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 53c9845b 10 months Lélio Brun fix optimization for variable reuse that was no...
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.54 KB 17d63fff 10 months Lélio Brun remove unused variables after tag elimination i...
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.48 KB 17d63fff 10 months Lélio Brun remove unused variables after tag elimination i...
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.68 KB 53c9845b 10 months Lélio Brun fix optimization for variable reuse that was no...
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 22 KB 53c9845b 10 months Lélio Brun fix optimization for variable reuse that was no...
machine_code.mli 135 Bytes ca7ff3f7 about 1 year Lélio Brun reformatting
machine_code_common.ml 16.9 KB a56f563e 10 months Lélio Brun more compact assign clauses for state variables...
machine_code_common.mli 1.88 KB cc852504 about 1 year Lélio Brun comment dead code with (* XXX: UNUSED *) discla...
machine_code_dep.ml 1.72 KB 17d63fff 10 months Lélio Brun remove unused variables after tag elimination i...
machine_code_dep.mli 76 Bytes 17d63fff 10 months Lélio Brun remove unused variables after tag elimination i...
machine_code_types.mli 2.23 KB a56f563e 10 months Lélio Brun more compact assign clauses for state variables...
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 36.5 KB 17d63fff 10 months Lélio Brun remove unused variables after tag elimination i...
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 3.09 KB 53c9845b 10 months Lélio Brun fix optimization for variable reuse that was no...
spec_common.mli 694 Bytes 3d1f9d9f 10 months Lélio Brun more agressive optim propagation in spec in ord...
spec_types.ml 1.62 KB 3d1f9d9f 10 months Lélio Brun more agressive optim propagation in spec in ord...
spec_types.mli 1.51 KB 3d1f9d9f 10 months Lélio Brun more agressive optim propagation in spec in ord...
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 53c9845b 10 months Lélio Brun fix optimization for variable reuse that was no...
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
17d63fff 10/22/2021 02:57 PM Lélio Brun

remove unused variables after tag elimination in machine code (-O >= 3)

134e6b64 10/21/2021 06:32 PM Lélio Brun

remove debug line

53c9845b 10/21/2021 06:32 PM Lélio Brun

fix optimization for variable reuse that was not propagated in branches

ebbe2fc3 10/15/2021 02:37 PM Lélio Brun

state variables ar not free

a56f563e 10/13/2021 06:42 PM Lélio Brun

more compact assign clauses for state variables, and remove useless memory pack predicates and assertions

7cb1f579 10/07/2021 06:33 PM Lélio Brun

reintroduce existential for variables that may appear free when performing substitution
hopefully those are less problematic since they actually exists in the program as variables

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

View revisions

Also available in: Atom