diff options
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/no_vector/spec.sail | 4 | ||||
| -rw-r--r-- | aarch64/prelude.sail | 6 |
2 files changed, 3 insertions, 7 deletions
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail index d8a05777..ccf8aba1 100644 --- a/aarch64/no_vector/spec.sail +++ b/aarch64/no_vector/spec.sail @@ -6984,7 +6984,7 @@ function __TakeColdReset () = { val AArch64_TakeException : (bits(2), ExceptionRecord, bits(64), int) -> unit effect {escape, rreg, undef, wreg} function AArch64_TakeException (target_el, exception, preferred_exception_return, vect_offset__arg) = { - vect_offset = vect_offset__arg; + vect_offset : int = vect_offset__arg; SynchronizeContext(); assert((HaveEL(target_el) & ~(ELUsingAArch32(target_el))) & UInt(target_el) >= UInt(PSTATE.EL), "((HaveEL(target_el) && !(ELUsingAArch32(target_el))) && (UInt(target_el) >= UInt((PSTATE).EL)))"); from_32 : bool = UsingAArch32(); @@ -8507,7 +8507,7 @@ val aarch64_memory_vector_single_nowb : forall ('esize : Int) ('selem : Int). function aarch64_memory_vector_single_nowb (datasize, esize, index, m, memop, n, replicate, selem, t__arg, wback) = { assert(constraint('selem >= 1 & 'esize >= 0)); - t = t__arg; + t : int = t__arg; CheckFPAdvSIMDEnabled64(); address : bits(64) = undefined; offs : bits(64) = undefined; diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail index 902f448f..5cf4ce48 100644 --- a/aarch64/prelude.sail +++ b/aarch64/prelude.sail @@ -103,10 +103,6 @@ val not_vec = { overload ~ = {not_bool, not_vec} -val neq_int = {lem: "neq"} : (int, int) -> bool - -function neq_int (x, y) = not_bool(eq_int(x, y)) - val neq_vec = {lem: "neq_vec"} : forall 'n. (bits('n), bits('n)) -> bool function neq_vec (x, y) = not_bool(eq_vec(x, y)) @@ -115,7 +111,7 @@ val neq_anything = {lem: "neq"} : forall ('a : Type). ('a, 'a) -> bool function neq_anything (x, y) = not_bool(x == y) -overload operator != = {neq_atom, neq_int, neq_vec, neq_anything} +overload operator != = {neq_vec, neq_anything} val builtin_and_vec = {ocaml: "and_vec", c: "and_bits"} : forall 'n. (bits('n), bits('n)) -> bits('n) |