diff options
| author | Gabriel Kerneis | 2014-07-04 13:12:54 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-07-04 13:13:11 +0100 |
| commit | 8522c1dbf5fc7b739a89873a1d86d45b11bc136f (patch) | |
| tree | 08130b57e77daf63b7633668c71771eb004f7169 /src | |
| parent | 423d32995427a289480fd5447d656754bcc58815 (diff) | |
Update power.sail
Diffstat (limited to 'src')
| -rw-r--r-- | src/test/power.sail | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/test/power.sail b/src/test/power.sail index 59a529e3..098057e2 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -7,8 +7,11 @@ function forall Type 'a . 'a BCD_TO_DEC ( x ) = x function bit carry_out ( x ) = bitzero (* XXX length *) function nat length ( x ) = 64 -(* XXX break *) -function unit break () = () + +(* XXX *) +val extern forall Nat 'k, Nat 'r, + 0 <= 'k, 'k <= 64, 'r + 'k = 64. + (bit[64], [|'k|]) -> [|0:'r|] effect pure countLeadingZeroes function forall Nat 'n, Nat 'm . bit['m] EXTS_EXPLICIT((bit['n]) v, ([|'m|]) m) = @@ -340,7 +343,6 @@ function clause decode ([bitone, bitzero, bitzero, bitzero, bitzero, bitzero] : function clause execute (Lwz (RT, RA, D)) = { - (bit[64]) EA := 0; (bit[64]) b := 0; if RA == 0 then b := 0 else b := GPR[RA]; EA := b + EXTS (D); @@ -357,7 +359,6 @@ function clause decode ([bitone, bitzero, bitzero, bitone, bitzero, bitzero] : function clause execute (Stw (RS, RA, D)) = { - (bit[64]) EA := 0; (bit[64]) b := 0; if RA == 0 then b := 0 else b := GPR[RA]; EA := b + EXTS (D); @@ -374,7 +375,6 @@ function clause decode ([bitone, bitzero, bitzero, bitone, bitzero, bitone] : function clause execute (Stwu (RS, RA, D)) = { - (bit[64]) EA := 0; EA := GPR[RA] + EXTS (D); MEM(EA,4) := (GPR[RS])[32 .. 63]; GPR[RA] := EA |