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
.gitignore
*~
_build
*.native
*.byte
*.exe
*.pyc
*.pyo
.vagrant
/local
/why3
/_tools
/proofgeneral/_local
setup.data
setup.log
/attic
/attic.ec*
/theories/attic
/system/*.o
/system/callprover
/system/callprover.exe
*.aux
*.bbl
*.blg
*.brf
*.fdb_latexmk
*.fls
*.idx
*.ilg
*.ind
*.log
*.out
*.toc
*.synctex.gz
*.kilepr
/src/ecVersion.ml
/doc/refman/easycrypt.pdf
/doc/userman/easycrypt.pdf
/extraction/Makefile
/extraction/setup.*
/extraction/configure
/extraction/_build/
/sandbox
/attic
/*.ec
/*.smt
/*.why
Computing file changes ...
