diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/smt/reg_ref.unsat.sail | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/smt/reg_ref.unsat.sail b/test/smt/reg_ref.unsat.sail new file mode 100644 index 00000000..300657df --- /dev/null +++ b/test/smt/reg_ref.unsat.sail @@ -0,0 +1,18 @@ +default Order dec + +$include <prelude.sail> + +val "reg_deref" : forall ('a: Type). register('a) -> 'a effect {rreg} + +register R0 : bits(32) +register R1 : bits(32) +register R2 : bits(32) +register R3 : bits(32) + +let GPRs = [ref R3, ref R2, ref R1, ref R0] + +$property +function prop() -> bool = { + R0 = 0xDEAD_BEEF; + reg_deref(GPRs[0]) == 0xDEAD_BEEF +}
\ No newline at end of file |