diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 13:36:57 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-23 13:36:57 +0000 |
| commit | a19eb81876d9739b569b946ccdbf2778d2e9aca7 (patch) | |
| tree | b1f1abe9df22354423e91b407b91a598d02c448a /checklink | |
| parent | 582eeac94b777f99b28a2b373c8e1c825763cada (diff) | |
Add _a memory accesses.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Check.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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) |