From a19eb81876d9739b569b946ccdbf2778d2e9aca7 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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