From 3a082fd7f15c9b88d37bc2fbb0a92d93683414c4 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 27 Nov 2013 12:54:38 +0000 Subject: More tweaking re: builtin_memcpy git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'checklink') diff --git a/checklink/Check.ml b/checklink/Check.ml index ca7afea..50928d2 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -610,10 +610,10 @@ let match_memcpy_small ecode pc sz al src dst (fw: f_framework) | LFD (frD0, rA0, d0) :: STFD(frS1, rA1, d1) :: es -> OK(fw) - >>= match_fregs FPR0 frD0 + >>= match_fregs FPR13 frD0 >>= match_iregs src rA0 >>= match_int32s ofs32 (exts d0) - >>= match_fregs FPR0 frS1 + >>= match_fregs FPR13 frS1 >>= match_iregs dst rA1 >>= match_int32s ofs32 (exts d1) >>= match_memcpy_small_aux (ofs + 8) (sz - 8) es (Int32.add 8l pc) @@ -1492,13 +1492,17 @@ let rec compare_code ccode ecode pc: checker = fun fw -> let al = z_int al in begin match args with | [IR dst; IR src] -> - 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) -> + if sz <= 48 + 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 ( 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) -> -- cgit v1.2.3