https://github.com/EasyCrypt/easycrypt
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: ba545a9c82d684be976cec846ab5359fabbcd4dd authored by Benjamin Grégoire on 12 June 2018, 05:31:11 UTC
New tactic for static unrolling of "for-loops"
New tactic for static unrolling of "for-loops"
Tip revision: ba545a9
| 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 ...
