diff options
| author | Gabriel Kerneis | 2014-06-11 17:46:41 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-06-11 17:46:41 +0100 |
| commit | f2fa48b95a789fdeca777ea1cb932a3657faeed3 (patch) | |
| tree | 0fd7558d1f3865814c5fec4b5f05e21948bab67c /src | |
| parent | 6883558e6b8352f77cb1ff342789af0280dc32c1 (diff) | |
power.sail: store mode64bit in a bool register
This is now possible because we handle coercions better.
Diffstat (limited to 'src')
| -rw-r--r-- | src/test/power.sail | 5 | ||||
| -rw-r--r-- | src/test/run_power.ml | 1 |
2 files changed, 2 insertions, 4 deletions
diff --git a/src/test/power.sail b/src/test/power.sail index 6fe84602..a9e56c7f 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -1,5 +1,3 @@ -(* XXX sign extension --- note that this produces a signed integer, - the constraints on the range of the result is TODO *) val extern forall Nat 'n. bit['n] -> bit[64] effect pure exts (* XXX binary coded decimal *) function forall Type 'a . 'a dec_to_bcd ( x ) = x @@ -99,8 +97,7 @@ val extern forall Nat 'n. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { wmem , rmem (* XXX effect for trap? *) val extern unit -> unit effect pure trap -(* XXX should be register<bool>, this is a workaround for limitations in coercions *) -let (bit) mode64bit = bitone +register (bool) mode64bit scattered function unit execute scattered typedef ast = const union diff --git a/src/test/run_power.ml b/src/test/run_power.ml index ca4dbc97..61f60ef3 100644 --- a/src/test/run_power.ml +++ b/src/test/run_power.ml @@ -74,6 +74,7 @@ let init_reg () = init "CTR" Big_int.zero_big_int 64; init "CR" Big_int.zero_big_int 32; init "LR" lr_init_value 64; + Id_aux(Id "mode64bit", Unknown), V_lit (L_aux (L_true, Unknown)); ] ;; |