diff options
| author |  varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-12 21:57:29 +0000 |
|---|---|---|
| committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-04-12 21:57:29 +0000 |
| commit | cf3240e47400afd9485c596b65171e6dbc53ffcf (patch) | |
| tree | 53d7b9bf8d9ac55070feb142ee0728cfe3c0c92e /checklink | |
| parent | 23b04dd211287eb1c841c129705af39afbe0ab15 (diff) | |
Added Pallocframe second form
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1876 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink')
| -rw-r--r-- | checklink/Check.ml | 16 |
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 |