diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/mono/flow_extend.sail | 16 | ||||
| -rw-r--r-- | test/mono/pass/flow_extend | 1 |
2 files changed, 17 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); +} diff --git a/test/mono/pass/flow_extend b/test/mono/pass/flow_extend new file mode 100644 index 00000000..fea386e5 --- /dev/null +++ b/test/mono/pass/flow_extend @@ -0,0 +1 @@ +flow_extend.sail -auto_mono |