diff options
| author | Thomas Bauereiss | 2018-05-08 18:13:03 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-05-09 14:40:13 +0100 |
| commit | b6b46102fc49eae53c27d5d6540d41981c75da0c (patch) | |
| tree | 2a4a7838ffbd4a451fcaa1e12377c46f60b56df9 /lib/elf.sail | |
| parent | c6710bb09c1d492b4434f0b3b375750275b4d4b5 (diff) | |
Add more annotations for loop bounds in Lem rewriting
Typechecking for-loops failed after the Lem rewriting passes in some cases: if
the lower bound for the loop may be greater than the upper bound, the loop
variable's type might be empty, and it cannot be initialised. This patch adds
a guard "lower <= upper" around the loop body, and removes it again during
pretty-printing.
Diffstat (limited to 'lib/elf.sail')
0 files changed, 0 insertions, 0 deletions