add a test for concolic global sharing, written by @filipeom

OCamlPro · Jun 5, 2024 · b06034e · b06034e
1 parent 8327c97
commit b06034e
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 1 deletion.
diff --git a/test/conc/dune b/test/conc/dune
@@ -1,2 +1,2 @@
 (cram
- (deps %{bin:owi} immediately_fail.wat))
+ (deps %{bin:owi} global_sharing.wat immediately_fail.wat))
diff --git a/test/conc/global_sharing.t b/test/conc/global_sharing.t
@@ -0,0 +1,2 @@
+  $ owi conc global_sharing.wat
+  OK
diff --git a/test/conc/global_sharing.wat b/test/conc/global_sharing.wat
@@ -0,0 +1,26 @@
+;; Loads symbolic memory in various iterations
+(module
+  (import "symbolic" "i32_symbol" (func $i32 (result i32)))
+  (import "symbolic" "assert" (func $assert (param i32)))
+
+  (func $test_globals (param i32)
+        (global.get 0)
+        (i32.const 2)
+        (i32.sub)
+        (global.set 0)
+        (global.get 0)
+        (local.get 0)
+        (i32.eq)
+        (call $assert))
+
+  (func $main
+        (i32.const 40)
+        (call $test_globals)
+        (if (i32.eq (call $i32) (i32.const 0))
+          (then
+            (i32.const 38)
+            (call $test_globals))))
+  (memory $0 1)
+  (global $0 (mut i32) (i32.const 42))
+  (export "main" (func $main))
+  (start $main))