From dda95db0f6c2c739e2ba7c29150f8f4a1eb3f403 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Sun, 12 Apr 2020 21:36:23 +0100
Subject: Mono: Check for non-constant calls to make_the_value

... and try to resolve them using constant propagation.
---
 test/mono/itself_rewriting.sail | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'test')

diff --git a/test/mono/itself_rewriting.sail b/test/mono/itself_rewriting.sail
index 0501cf1e..dfc76cf9 100644
--- a/test/mono/itself_rewriting.sail
+++ b/test/mono/itself_rewriting.sail
@@ -1,5 +1,6 @@
 $include <smt.sail>
 $include <flow.sail>
+$include <arith.sail>
 default Order dec
 type bits ('n : Int) = bitvector('n, dec)
 val operator & = "and_bool" : (bool, bool) -> bool
@@ -67,10 +68,26 @@ function willsplit(x) = {
   shadowed(n);
 }
 
+val execute : forall 'datasize. int('datasize) -> unit
+
+function execute(datasize) = {
+  let x : bits('datasize) = replicate_bits(0b1, datasize);
+  ()
+}
+
+val test_execute : unit -> unit
+
+function test_execute() = {
+  let exp = 4;
+  let datasize = shl_int(1, exp);
+  execute(datasize)
+}
+
 val run : unit -> unit effect {escape}
 
 function run () = {
   assert(true); /* To force us into the monad */
+  test_execute();
   willsplit(true);
   willsplit(false);
-}
\ No newline at end of file
+}
-- 
cgit v1.2.3