diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-12-15 19:33:03 +0100 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-02-20 10:39:49 +0100 |
commit | b6ba61c4c7df3f173f7aad2d96d8927d1a525fe3 (patch) | |
tree | 6c943b8eb0d383abae3415c61b6544a81ca611e3 /extraction | |
parent | 668d546f670996d22e5d2a2f6f83752a8254dc23 (diff) | |
download | compcert-b6ba61c4c7df3f173f7aad2d96d8927d1a525fe3.tar.gz compcert-b6ba61c4c7df3f173f7aad2d96d8927d1a525fe3.zip |
ARM code generation: fix offset checks for loads
The check `Int.ltu x Int.zero` is always false, we replace this by using
signed integer comparisons.
We cannot use `Int.sign_ext` because the offsets are not signed
integers but rather unsigned integers plus an additional sign bit.
Diffstat (limited to 'extraction')
0 files changed, 0 insertions, 0 deletions