diff options
Diffstat (limited to 'src/test')
| -rw-r--r-- | src/test/power.sail | 4 | ||||
| -rw-r--r-- | src/test/run_power.ml | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/test/power.sail b/src/test/power.sail index 5f1f532b..9a89c9e4 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -333,8 +333,8 @@ register (bit[64]) NIA (* next instruction address *) register (bit[64]) CIA (* current instruction address *) -val extern forall Nat 'n. ( nat , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw -val extern forall Nat 'n. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr +val extern forall Nat 'n. ( bit[64] , [|'n|] , bit[8*'n]) -> unit effect { wmem } MEMw +val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem } MEMr (* XXX effect for trap? *) val extern unit -> unit effect pure trap diff --git a/src/test/run_power.ml b/src/test/run_power.ml index 667792c0..70cf5d4b 100644 --- a/src/test/run_power.ml +++ b/src/test/run_power.ml @@ -33,7 +33,9 @@ let mem = ref Mem.empty ;; let add_mem byte addr = assert(byte >= 0 && byte < 256); + (*Printf.printf "adder is %s, byte is %s\n" (Big_int.string_of_big_int addr) (string_of_int byte);*) let addr = big_int_to_vec true addr (Big_int.big_int_of_int 64) in + (*Printf.printf "adder is %s byte is %s\n" (val_to_string addr) (string_of_int byte);*) match addr with | Bytevector addr -> mem := Mem.add addr byte !mem ;; |