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 /aarch64 | |
| 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 'aarch64')
| -rw-r--r-- | aarch64/aarch64_extras.lem | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/aarch64/aarch64_extras.lem b/aarch64/aarch64_extras.lem index e823dbfe..ab67f506 100644 --- a/aarch64/aarch64_extras.lem +++ b/aarch64/aarch64_extras.lem @@ -119,3 +119,7 @@ val read_ram : forall 'rv 'e. integer -> integer -> list bitU -> list bitU -> monad 'rv (list bitU) 'e let read_ram addrsize size hexRAM address = read_mem Read_plain address size + +val elf_entry : unit -> integer +let elf_entry () = 0 +declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry` |