diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/c/pattern_concat_nest.sail | 22 | ||||
| -rw-r--r-- | test/c/rv_duopod_bug.expect | 2 | ||||
| -rw-r--r-- | test/c/rv_duopod_bug.sail | 13 |
3 files changed, 16 insertions, 21 deletions
diff --git a/test/c/pattern_concat_nest.sail b/test/c/pattern_concat_nest.sail index 92150e66..398e814f 100644 --- a/test/c/pattern_concat_nest.sail +++ b/test/c/pattern_concat_nest.sail @@ -1,26 +1,6 @@ default Order dec -type bits ('n : Int) = vector('n, dec, bit) - -union option ('a : Type) = {None : unit, Some : 'a} - -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec", c: "vector_subrange"} - : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm & 'm <= 'n. - (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1)) - -val bitvector_access = {ocaml: "access", lem: "access_vec_dec", c: "vector_access"} - : forall ('n : Int) ('m : Int), 0 <= 'm & 'm + 1 <= 'n. - (bits('n), atom('m)) -> bit - -overload vector_access = {bitvector_access} - -val eq_bit = {ocaml: "eq_bit", lem: "eq", interpreter: "eq_anything", c: "eq_bit"}: (bit, bit) -> bool - -overload operator == = { - eq_bit -} - -val and_bool = {ocaml: "and_bool", lem: "and_bool", smt: "and_bool", interpreter: "and_bool", c: "and_bool"}: (bool, bool) -> bool +$include <prelude.sail> //////////////////////////////////////////////////////////// diff --git a/test/c/rv_duopod_bug.expect b/test/c/rv_duopod_bug.expect new file mode 100644 index 00000000..681c7c43 --- /dev/null +++ b/test/c/rv_duopod_bug.expect @@ -0,0 +1,2 @@ +0 0x0000000000000000 +1 0xFFFFFFFFFFFFFFFF diff --git a/test/c/rv_duopod_bug.sail b/test/c/rv_duopod_bug.sail new file mode 100644 index 00000000..9a11996c --- /dev/null +++ b/test/c/rv_duopod_bug.sail @@ -0,0 +1,13 @@ +default Order dec + +$include <prelude.sail> + +val rX : int -> bits(64) + +function rX 0 = sail_zeros(64) +and rX (r if r > 0) = sail_ones(64) + +function main() -> unit = { + print_bits("0 ", rX(0)); + print_bits("1 ", rX(1)) +} |
