swh:1:snp:f06d4d1f1c56d17a2f00ca108b0c7636a874db0d
Revision ba545a9c82d684be976cec846ab5359fabbcd4dd authored by Benjamin Grégoire on 12 June 2018, 05:31:11 UTC, committed by Pierre-Yves Strub on 12 June 2018, 05:34:41 UTC
The tactic statically unroll while loops of the form
x <- int-constant
while (guard) {
body (does not write x);
x <- f(x);
}
where "guard" and "f" can be statically evaluated at each
iteration. The code is then replaced by the while loop
fully unrolled.
The tactic does not terminate if the unrolling leads to
a infinite process.
1 parent 43fd7aa
Tip revision: 644ddc2e7f7b1bab87c4775250c430104c7d9f69 authored by Pierre-Yves Strub on 09 August 2022, 07:51:07 UTC
Fix a typing annotation bug in distribution tags' axioms
Fix a typing annotation bug in distribution tags' axioms
Tip revision: 644ddc2
| File | Mode | Size |
|---|---|---|
| config | ||
| examples | ||
| lint | ||
| scripts | ||
| src | ||
| system | ||
| theories | ||
| .dir-locals.el | -rw-r--r-- | 285 bytes |
| .gitignore | -rw-r--r-- | 504 bytes |
| .merlin | -rw-r--r-- | 230 bytes |
| .travis.yml | -rw-r--r-- | 2.0 KB |
| COPYRIGHT | -rw-r--r-- | 581 bytes |
| COPYRIGHT.yaml | -rw-r--r-- | 596 bytes |
| MANIFEST | -rw-r--r-- | 690 bytes |
| Makefile | -rw-r--r-- | 5.0 KB |
| Makefile.system | -rw-r--r-- | 478 bytes |
| README.md | -rw-r--r-- | 6.1 KB |
| _tags | -rw-r--r-- | 791 bytes |
| myocamlbuild.ml | -rw-r--r-- | 2.3 KB |
Computing file changes ...
