motoko-san: final test fixup

test/viper/ok/reverse.tc.ok

@@ -1,7 +1,6 @@
-reverse.mo:43.13-43.23: warning [M0155], operator may trap for inferred type
+reverse.mo:41.13-41.23: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:49.35-49.47: warning [M0155], operator may trap for inferred type
+reverse.mo:47.35-47.47: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:49.35-49.51: warning [M0155], operator may trap for inferred type
+reverse.mo:47.35-47.51: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:37.9-37.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)

test/viper/ok/reverse.vpr.ok

@@ -46,25 +46,16 @@ method reverseArray$Nat($Self: Ref, a: Array)
 
     requires $Perm($Self)
     requires $array_acc(a, $int, write)
-    requires ($size(($Self).xarray) == 5)
     ensures $Perm($Self)
     ensures $array_acc(a, $int, write)
-    ensures ($size(($Self).xarray) == 5)
+    ensures ($size(($Self).xarray) == old($size(($Self).xarray)))
     ensures ($size(a) == old($size(a)))
     ensures (forall k : Int :: (((0 <= k) && (k < $size(a))) ==> (($loc(a,
                                                                     k)).$int == 
              old(($loc(a, (($size(a) - 1) - k))).$int))))
-    { var b: Array
-      var length: Int
+    { var length: Int
       var i: Int
       var j: Int
-      inhale $array_acc(b, $int, write);
-      inhale ($size(b) == 3);
-      ($loc(b, 0)).$int := 1;
-      ($loc(b, 1)).$int := 2;
-      ($loc(b, 2)).$int := 4;
-      exhale $array_acc(b, $int, wildcard);
-      inhale $array_acc(b, $int, wildcard);
       length := $size(a);
       if ((length == 0))
          { 
@@ -74,9 +65,8 @@ method reverseArray$Nat($Self: Ref, a: Array)
       j := 0;
       while ((i > j))
          invariant $Perm($Self)
-         invariant $array_acc(b, $int, wildcard)
          invariant $array_acc(a, $int, write)
-         invariant ($size(($Self).xarray) == 5)
+         invariant ($size(($Self).xarray) == old($size(($Self).xarray)))
          invariant ((i < length) && (i >= 0))
          invariant ((j < length) && (j >= 0))
          invariant (i == (($size(a) - 1) - j))

test/viper/ok/reverse.vpr.stderr.ok

@@ -1,7 +1,6 @@
-reverse.mo:43.13-43.23: warning [M0155], operator may trap for inferred type
+reverse.mo:41.13-41.23: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:49.35-49.47: warning [M0155], operator may trap for inferred type
+reverse.mo:47.35-47.47: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:49.35-49.51: warning [M0155], operator may trap for inferred type
+reverse.mo:47.35-47.51: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:37.9-37.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)

test/viper/ok/todo_record.tc.ok

@@ -1,2 +1,2 @@
-todo_record.mo:109.23-109.28: warning [M0155], operator may trap for inferred type
+todo_record.mo:110.23-110.28: warning [M0155], operator may trap for inferred type
   Nat

test/viper/ok/todo_record.vpr.ok

@@ -319,7 +319,7 @@ method showTodos($Self: Ref)
       goto $Ret;
       label $Ret; 
     }
-method clearstate($Self: Ref)
+method clearCompleted($Self: Ref)
 
     requires $Perm($Self)
     requires $Inv($Self)

test/viper/ok/todo_record.vpr.stderr.ok

@@ -1,2 +1,2 @@
-todo_record.mo:109.23-109.28: warning [M0155], operator may trap for inferred type
+todo_record.mo:110.23-110.28: warning [M0155], operator may trap for inferred type
   Nat

test/viper/reverse.mo

@@ -1,7 +1,7 @@
+// @verify
 import Array "mo:base/Array";
 import Prim "mo:⛔";
 
-// @verify
 actor Reverse {
   var xarray : [var Nat] = [var 1, 2, 3, 4, 5];
 
@@ -28,13 +28,11 @@ actor Reverse {
 
   private func reverseArray<T>(a : [var T]) : () {
     // actor invariant is preserved:
-    assert:func xarray.size() == 5;
-    assert:return xarray.size() == 5;
+    assert:return xarray.size() == (old(xarray.size()));
 
     assert:return a.size() == (old (a.size()));
     assert:return Prim.forall<Nat>(
       func (k : Nat) = (0 <= k and k < a.size()) implies a[k] == (old (a[a.size() - 1 - k])));
-    let b = [1, 2, 4]; // space variable to test loop invariant deducing
     var length = a.size();
     if (length == 0) {
       return;
@@ -43,7 +41,7 @@ actor Reverse {
     var i = length - 1;
     var j = 0;
     while (i > j) {
-      assert:loop:invariant xarray.size() == 5; // actor invariant
+      assert:loop:invariant xarray.size() == (old(xarray.size())); // actor invariant
       assert:loop:invariant (i < length and i >= 0);
       assert:loop:invariant (j < length and j >= 0);
       assert:loop:invariant (i == a.size() - 1 - j);

test/viper/todo_record.mo

@@ -56,7 +56,8 @@ actor Assistant {
     assert:return todos.size() == (old(todos.size()));
     assert:return Prim.forall<Nat>(func i =
       (0 <= i and i < (old(todos.size())) implies todos[i] == (old(todos[i]))));
-    // TODO: is not supported yet, do it manually (as in reverse.mo)
+    // TODO: Array.tabulate is not supported yet, do it manually (as in reverse.mo)
+    // Alternative: support Array.freeze
     // assert:return Prim.forall<Nat>(func i =
     //   (0 <= i and i < (old(todos.size())) implies todos[i] == Prim.Ret<[ToDo]>()[i]));
     // let new_array = Array.tabulate<(Nat, Text, State)>(num, func i = todos[i]);
@@ -179,7 +180,7 @@ actor Assistant {
     return output # "\n";
   };
 
-  public func clearstate() : async () {
+  public func clearCompleted() : async () {
     assert:return num <= (old(num));
     assert:return nextId == (old(nextId));
     assert:return todos.size() == (old(todos.size()));