summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-04-12 21:57:29 +0000
committerGravatar varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-04-12 21:57:29 +0000
commitcf3240e47400afd9485c596b65171e6dbc53ffcf (patch)
tree53d7b9bf8d9ac55070feb142ee0728cfe3c0c92e
parent23b04dd211287eb1c841c129705af39afbe0ab15 (diff)
Added Pallocframe second form
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1876 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--checklink/Check.ml16
1 files changed, 13 insertions, 3 deletions
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