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