summaryrefslogtreecommitdiff
path: root/test/c
diff options
context:
space:
mode:
authorJon French2019-04-15 16:23:44 +0100
committerJon French2019-04-15 16:23:44 +0100
commita230fb980a70f0484daa01bb69c0204b431c9267 (patch)
tree5fb4b9749afff963635b0d31301ebc3af124f208 /test/c
parenta9f0b829507e9882efdb59cce4d83ea7e87f5f71 (diff)
parent4529e0acc377bed4d1bab4230f4023e4bee3ae85 (diff)
Merge branch 'sail2' of github.com:rems-project/sail into sail2
Diffstat (limited to 'test/c')
-rw-r--r--test/c/zero_length_bv.expect1
-rw-r--r--test/c/zero_length_bv.sail14
2 files changed, 15 insertions, 0 deletions
diff --git a/test/c/zero_length_bv.expect b/test/c/zero_length_bv.expect
new file mode 100644
index 00000000..9766475a
--- /dev/null
+++ b/test/c/zero_length_bv.expect
@@ -0,0 +1 @@
+ok
diff --git a/test/c/zero_length_bv.sail b/test/c/zero_length_bv.sail
new file mode 100644
index 00000000..332b8aae
--- /dev/null
+++ b/test/c/zero_length_bv.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+$include <prelude.sail>
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+ let x: bits(0) = [];
+ if x == sail_zeros(0) then {
+ print_endline("ok")
+ };
+ let x: vector(0, dec, string) = [];
+ ()
+} \ No newline at end of file