fixup! motoko-san: fix bug with array initialization

serokell · May 6, 2024 · 643c8de · 643c8de
1 parent 5707d5b
commit 643c8de
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 8 deletions.
diff --git a/test/viper/array.mo b/test/viper/array.mo
@@ -26,6 +26,11 @@ actor {
         vm_a := [var 42];
         // lm_a := [1, 2]; // error
 
+        assert:system vi_a[0] != 0;
+        assert:system vi_a[0] == 1;
+        assert:system vm_a[0] != 1;
+        assert:system vm_a[0] == 42;
+
         return 42;
     };
 

diff --git a/test/viper/ok/array.tc.ok b/test/viper/ok/array.tc.ok
@@ -1,6 +1,6 @@
 array.mo:7.9-7.10: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
 array.mo:8.9-8.14: warning [M0194], unused identifier count (delete or rename to wildcard `_` or `_count`)
-array.mo:37.18-37.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
-array.mo:42.18-42.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
-array.mo:46.11-46.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
-array.mo:54.11-54.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:42.18-42.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:47.18-47.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:51.11-51.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:59.11-59.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
diff --git a/test/viper/ok/array.vpr.ok b/test/viper/ok/array.vpr.ok
@@ -80,6 +80,10 @@ method foo($Self: Ref)
       inhale ($size(vm_a_2) == 1)
       ($loc(vm_a_2, 0)).$int := 42
       vm_a := vm_a_2
+      assert (($loc(vi_a, 0)).$int != 0)
+      assert (($loc(vi_a, 0)).$int == 1)
+      assert (($loc(vm_a, 0)).$int != 1)
+      assert (($loc(vm_a, 0)).$int == 42)
       $Res := 42
       goto $Ret
       label $Ret 

diff --git a/test/viper/ok/array.vpr.stderr.ok b/test/viper/ok/array.vpr.stderr.ok
@@ -1,6 +1,6 @@
 array.mo:7.9-7.10: warning [M0194], unused identifier f (delete or rename to wildcard `_` or `_f`)
 array.mo:8.9-8.14: warning [M0194], unused identifier count (delete or rename to wildcard `_` or `_count`)
-array.mo:37.18-37.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
-array.mo:42.18-42.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
-array.mo:46.11-46.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
-array.mo:54.11-54.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:42.18-42.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`)
+array.mo:47.18-47.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`)
+array.mo:51.11-51.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)
+array.mo:59.11-59.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`)