Support case splitting on variables as well as sizeof in cast introduction

1 files changed, 16 insertions, 0 deletions

diff --git a/test/mono/flow_extend.sail b/test/mono/flow_extend.sail
new file mode 100644
index 00000000..7e118993
--- /dev/null
+++ b/test/mono/flow_extend.sail
@@ -0,0 +1,16 @@
+default Order dec
+$include <prelude.sail>
+
+val bitvector_cast_in = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+val bitvector_cast_out = "zeroExtend" : forall 'n. bits('n) -> bits('n) effect pure
+
+val byte_extend : forall 'n, 'n >= 8. (bits(8), int('n)) -> bits('n)
+
+function byte_extend (v, n) = if (n == 8) then v else sail_zero_extend(v, n)
+
+val run : unit -> unit effect {escape}
+
+function run() = {
+  assert(byte_extend(0x12,8) == 0x12);
+  assert(byte_extend(0x12,16) == 0x0012);
+}