From 26e59493cde0ffbf1868426fe3bec158f2dbaad0 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Wed, 26 Jul 2017 12:03:12 +0100
Subject: Improve rewriting of sizeof expressions

If some type-level variables in a sizeof expression in a function body cannot
be directly extracted from the parameters of the function, add a new parameter
for each unresolved parameter, and rewrite calls to the function accordingly
---
 test/typecheck/pass/sizeof_vector_start_index.sail | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test/typecheck/pass/sizeof_vector_start_index.sail

(limited to 'test/typecheck')

diff --git a/test/typecheck/pass/sizeof_vector_start_index.sail b/test/typecheck/pass/sizeof_vector_start_index.sail
new file mode 100644
index 00000000..6ad8ef06
--- /dev/null
+++ b/test/typecheck/pass/sizeof_vector_start_index.sail
@@ -0,0 +1,12 @@
+val forall Num 'n, Num 'm, Order 'ord, Type 'a. vector<'n,'m,'ord,'a> -> [:'n:] effect pure vector_start_index
+
+function forall Num 'n, Num 'm, Order 'ord, Type 'a. [:'n:] vector_start_index ((vector<'n,'m,'ord,'a>) vec) =
+{
+  sizeof 'n
+}
+
+function int test ((vector<47,11,dec,bit>) vec) =
+{
+  vector_start_index(vec)
+}
+
-- 
cgit v1.2.3