diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2023-01-19 17:05:02 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-02-20 13:29:09 +0100 |
| commit | bdcd260ab0e6f2453069f348a5ba3d8e3ca38ce2 (patch) | |
| tree | 86aa9f691a5ea141389a43d694ba4d4fda4d172e | |
| parent | 431b64db94583fc5e8d08ecc9bd4e105567ed4d5 (diff) | |
| download | compcert-bdcd260ab0e6f2453069f348a5ba3d8e3ca38ce2.tar.gz compcert-bdcd260ab0e6f2453069f348a5ba3d8e3ca38ce2.zip | |
Move the old `offset_in_range` function inside `memcpy_small_arg`
It is no longer used elsewhere.
| -rw-r--r-- | arm/Asmexpand.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index a3f6187c..4096a267 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -82,10 +82,9 @@ let expand_annot_val kind txt targ args res = (* The ARM has strict alignment constraints for 2 and 4 byte accesses. 8-byte accesses must be 4-aligned. *) -let offset_in_range ofs = - let n = camlint_of_coqint ofs in n <= 128l && n >= -128l - let memcpy_small_arg sz arg tmp = + let offset_in_range ofs = + let n = camlint_of_coqint ofs in n <= 128l && n >= -128l in match arg with | BA (IR r) -> (r, _0) |