From a19eb81876d9739b569b946ccdbf2778d2e9aca7 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 13:36:57 +0000 Subject: Add _a memory accesses. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- checklink/Check.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'checklink') diff --git a/checklink/Check.ml b/checklink/Check.ml index 6c1739c..6f48b23 100644 --- a/checklink/Check.ml +++ b/checklink/Check.ml @@ -1836,7 +1836,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Plfd(rd, cst, r1) -> + | Plfd(rd, cst, r1) | Plfd_a(rd, cst, r1) -> begin match ecode with | LFD(frD, rA, d) :: es -> OK(fw) @@ -1846,7 +1846,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Plfdx(rd, r1, r2) -> + | Plfdx(rd, r1, r2) | Plfdx_a(rd, r1, r2) -> begin match ecode with | LFDX(frD, rA, rB) :: es -> OK(fw) @@ -2004,7 +2004,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Plwz(rd, cst, r1) -> + | Plwz(rd, cst, r1) | Plwz_a(rd, cst, r1) -> begin match ecode with | LWZ(rD, rA, d) :: es -> OK(fw) @@ -2014,7 +2014,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Plwzx(rd, r1, r2) -> + | Plwzx(rd, r1, r2) | Plwzx_a(rd, r1, r2) -> begin match ecode with | LWZX(rD, rA, rB) :: es -> OK(fw) @@ -2272,7 +2272,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pstfd(rd, cst, r1) -> + | Pstfd(rd, cst, r1) | Pstfd_a(rd, cst, r1) -> begin match ecode with | STFD(frS, rA, d) :: es -> OK(fw) @@ -2282,7 +2282,7 @@ let rec compare_code ccode ecode pc: checker = fun fw -> >>= recur_simpl | _ -> error end - | Pstfdx(rd, r1, r2) -> + | Pstfdx(rd, r1, r2) | Pstfdx_a(rd, r1, r2) -> begin match ecode with | STFDX(frS, rA, rB) :: es -> OK(fw) -- cgit v1.2.3