From cf3240e47400afd9485c596b65171e6dbc53ffcf Mon Sep 17 00:00:00 2001
From: varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 12 Apr 2012 21:57:29 +0000
Subject: Added Pallocframe second form

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1876 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 checklink/Check.ml | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

(limited to 'checklink')

diff --git a/checklink/Check.ml b/checklink/Check.ml
index dc010a3..abae47b 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -817,9 +817,19 @@ let rec compare_code ccode ecode pc fw: f_framework or_err =
           |   ADDIS   (rD0, rA0, simm0)  ::
               ORI     (rS1, rA1, uimm1)  ::
               STWUX   (rS2, rA2, rB2)    :: es ->
-              fw
-              >>> ff_ef ^%=
-              add_log (ERROR("TODO"))
+              let sz32 = Int32.neg (z_int32 sz) in
+              let sz_hi = Int32.shift_right_logical sz32 16 in
+              let sz_lo = Int32.logand sz32 0xFFFFl in
+              fw
+              >>> match_iregs  GPR12 rD0
+              >>> match_iregs  GPR0  rA0
+              >>> match_int32s sz_hi (Safe32.of_int simm0)
+              >>> match_iregs  GPR12 rS1
+              >>> match_iregs  GPR12 rA1
+              >>> match_int32s sz_lo (Safe32.of_int uimm1)
+              >>> match_iregs  GPR1  rS2
+              >>> match_iregs  GPR1  rA2
+              >>> match_iregs  GPR12 rB2
               >>> compare_code cs es (Int32.add 12l pc)
           | _ -> error
           end
-- 
cgit v1.2.3