diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-27 12:54:38 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-27 12:54:38 +0000 |
| commit | 3a082fd7f15c9b88d37bc2fbb0a92d93683414c4 (patch) | |
| tree | 01f2df86adab36e7781658eaa21036c961d2cc36 /checklink | |
| parent | 66d25f7c0f2aff6e65bfd4607288931cb200bdbc (diff) | |
More tweaking re: builtin_memcpy
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2377 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Check.ml | 16 |
1 files changed, 10 insertions, 6 deletions
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) -> |