diff options
| author | Alasdair | 2019-07-16 22:12:42 +0100 |
|---|---|---|
| committer | Alasdair | 2019-07-16 22:12:42 +0100 |
| commit | 92f50f2564834fcbeda250337c3acce571f7d6f0 (patch) | |
| tree | 46056b1bbe8a960413c3f068a8d13ef4aff31f9f /aarch64_small | |
| parent | d40c8a94f4ab62421394c2c46f27cdf1454b9d26 (diff) | |
Fix all remaining tests for this branch
Diffstat (limited to 'aarch64_small')
| -rw-r--r-- | aarch64_small/armV8.h.sail | 2 | ||||
| -rw-r--r-- | aarch64_small/prelude.sail | 7 |
2 files changed, 2 insertions, 7 deletions
diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail index d0f0b830..8b38f2eb 100644 --- a/aarch64_small/armV8.h.sail +++ b/aarch64_small/armV8.h.sail @@ -32,8 +32,6 @@ /* SUCH DAMAGE. */ /*========================================================================*/ -default Order dec - type boolean = bit type integer = int type uinteger = nat /* ARM ARM does not have nat/uint type */ diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail index d94112ad..c904aec6 100644 --- a/aarch64_small/prelude.sail +++ b/aarch64_small/prelude.sail @@ -1,9 +1,8 @@ +default Order dec + let b1 = bitone let b0 = bitzero - -/* default Order dec */ - val "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg} /* sneaky deref with no effect necessary for bitfield writes */ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a @@ -13,8 +12,6 @@ val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a /* val eq_bit2 = "eq_bit" : (bit, bit) -> bool */ /* overload operator == = {eq_bit2} */ - - $include <smt.sail> $include <flow.sail> $include <arith.sail> |