summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-11-27 10:59:42 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-11-27 10:59:42 +0000
commit66d25f7c0f2aff6e65bfd4607288931cb200bdbc (patch)
tree019ad5ff24dbf5ae5fe6efda0e5a7dbd949e232e
parentca65141bc7cebea973cb62093a874cad0e9c642a (diff)
Attempted update to cchecklink re: memcpy.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2376 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--checklink/Check.ml12
1 files changed, 4 insertions, 8 deletions
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 59ee4ee..ca7afea 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -1492,17 +1492,13 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
let al = z_int al in
begin match args with
| [IR dst; IR src] ->
- if sz <= 64
- then (
- match match_memcpy_small ecode pc sz al src dst fw with
- | ERR(s) -> ERR(s)
- | OK(fw, es, pc) -> compare_code cs es pc fw
- )
- else (
+ begin match match_memcpy_small ecode pc sz al src dst fw with
+ | OK(fw, es, pc) -> compare_code cs es pc fw
+ | ERR(s) ->
match match_memcpy_big ecode pc sz al src dst fw with
| ERR(s) -> ERR(s)
| OK(fw, es, pc) -> compare_code cs es pc fw
- )
+ end
| _ -> error
end
| EF_annot_val(text, targ) ->