swh:1:snp:960b089228f647a5f611503985d0a438173f35bc
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: ee7c5ffc9805916e0e782a2667c79a7bb9ff50fa authored by François Dupressoir on 21 March 2022, 16:15:38 UTC
force delta on convertibility checks
force delta on convertibility checks
Tip revision: ee7c5ff
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 ...