motoko-san: mock the Array module

src/viper/prelude.ml

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

src/viper/trans.ml

@@ -95,10 +95,16 @@ let lvalue_str (lval : lvalue) : string =
   | LValueUninitVar x -> x.it
   | LValueFld fld -> (snd fld).it
 
+type imported_module =
+  | IM_Prim         (* mo:⛔ *)
+  | IM_base_Array   (* mo:base/Array *)
+
 module Env = T.Env
+module Imports = Map.Make(String)
 
 type ctxt =
   { self : string option;
+    imports : imported_module Imports.t;
     ids : (sort * T.t) T.Env.t;
     ghost_items : (ctxt -> item) list ref;
     ghost_inits : (ctxt -> seqn') list ref;
@@ -178,7 +184,15 @@ and unit' (u : M.comp_unit) : prog =
   let { M.imports; M.body } = u.it in
   match body.it with
   | M.ActorU(id_opt, decs) ->
-    let ctxt = { self = None; ids = Env.empty; ghost_items = ref []; ghost_inits = ref []; ghost_perms = ref []; ghost_conc = ref [] } in
+    let ctxt = {
+      self = None;
+      imports = tr_imports imports;
+      ids = Env.empty;
+      ghost_items = ref [];
+      ghost_inits = ref [];
+      ghost_perms = ref [];
+      ghost_conc = ref []
+    } in
     let ctxt', perms, inits, mk_is = dec_fields ctxt decs in
     let is' = List.map (fun mk_i -> mk_i ctxt') mk_is in
     (* given is', compute ghost_is *)
@@ -250,6 +264,20 @@ and unit' (u : M.comp_unit) : prog =
     !!! (body.at) is
   | _ -> assert false
 
+and tr_imports (imps : M.import list) : imported_module Imports.t =
+  List.fold_left
+    (fun acc imp ->
+      let k, v = tr_import imp in
+      Imports.add k v acc)
+    Imports.empty
+    imps
+
+and tr_import (imp : M.import) : (string * imported_module) =
+  match imp.it with
+  | ({it=M.VarP s;_}, "mo:⛔", _) -> (s.it, IM_Prim)
+  | ({it=M.VarP s;_}, "mo:base/Array", _) -> (s.it, IM_base_Array)
+  | (p, _, _) -> unsupported p.at (Arrange.pat p)
+
 and dec_fields (ctxt : ctxt) (ds : M.dec_field list) =
   match ds with
   | [] ->
@@ -271,7 +299,7 @@ and dec_field ctxt d =
 and static_invariants at lhs e =
   match e.it with
  | M.AnnotE (e, _) -> static_invariants at lhs e
- | M.ArrayE (_, es) -> [array_size_inv at lhs (List.length es)]
+ | M.ArrayE (_, es) -> [array_size_inv at lhs (intLitE at (List.length es))]
  | _ -> []
 
 and dec_field' ctxt d =
@@ -643,6 +671,20 @@ and assign_stmts ctxt at (lval : lvalue) (e : M.exp) : seqn' =
   match e with
   | M.({it=TupE [];_}) -> [], []
   | M.({it=AnnotE (e, _);_}) -> assign_stmts ctxt at lval e
+  | M.({it=CallE ({it=M.DotE ({it=M.VarE(m);_}, {it="init";_});_}, _inst, args);_})
+      when Imports.find_opt (m.it) ctxt.imports = Some(IM_base_Array)
+      ->
+    begin match args with
+    | M.({it=TupE([e1;e2]); _}) ->
+      fld_via_tmp_var lval t (fun x ->
+        let lhs = !!(LocalVar (x, tr_typ t)) in
+        [], [ !!(AssertS !!(GeCmpE (exp ctxt e1, intLitE at 0)))
+            ; !!(InhaleS (array_acc at lhs (array_elem_t t)))
+            ; !!(InhaleS (array_size_inv at lhs (exp ctxt e1)))
+            ; !!(InhaleS (array_init_const at lhs (array_elem_t t) (exp ctxt e2))) ]
+      )
+    | _ -> unsupported args.at (Arrange.exp args)
+    end
   | M.({it = CallE({it = VarE m; _}, inst, args); _}) ->
     fld_via_tmp_var lval t (fun x ->
       let self_var = self ctxt m.at in
@@ -759,7 +801,10 @@ and exp ctxt e =
      !!(match e.it with
         | M.TupE es -> CallE (tag.it, List.map (exp ctxt) es)
         | _ -> CallE (tag.it, [exp ctxt e]))
-  | M.CallE ({ it = M.DotE (_, { it = "forall" | "exists" as predicate_name; _ }); _ }, _inst, { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ }) ->
+  | M.CallE ({ it = M.DotE ({it=M.VarE(m);_}, {it=predicate_name;_}); _ }, _inst, { it = M.FuncE (_, _, _, pattern, _, _, e); note; _ })
+    when Imports.find_opt (m.it) ctxt.imports = Some(IM_Prim)
+      && (predicate_name = "forall" || predicate_name = "exists")
+    ->
     let binders = extract_binders pattern in
     let typs =
       match M.(note.note_typ) with
@@ -845,7 +890,7 @@ and typed_field t =
   | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
 
 and array_size_inv at lhs n =
-  !!! at (EqCmpE (sizeE at lhs, intLitE at n))
+  !!! at (EqCmpE (sizeE at lhs, n))
 
 and array_acc at lhs t =
   match T.normalize t with
@@ -865,11 +910,15 @@ and array_alloc at ctxt lhs t es : stmt list =
      | T.Mut _ -> []
      | _       -> [ExhaleS (array_acc at lhs t); InhaleS (array_acc at lhs t)])in
   let stmts = [ InhaleS (array_acc at lhs (T.Mut t))
-              ; InhaleS (array_size_inv at lhs (List.length es))]
+              ; InhaleS (array_size_inv at lhs (intLitE at (List.length es)))]
               @ init_array
               @ reset_perm
   in List.map (!!) stmts
 
+and array_init_const at lhs t x =
+  let (!!) p = !!! at p in
+  !! (CallE ("$array_init", [lhs; !!(FldE (typed_field t)); x]))
+
 and array_loc ctxt at e1 e2 t =
   locE at (exp ctxt e1) (exp ctxt e2) (typed_field t)
 

test/run.sh

@@ -314,6 +314,10 @@ do
     else
       TEST_MOC_ARGS=$EXTRA_MOC_ARGS
     fi
+    if [ $VIPER = 'yes' ]
+    then
+      TEST_MOC_ARGS="$TEST_MOC_ARGS --package base pkg/base"
+    fi
     moc_with_flags="env $moc_extra_env moc $moc_extra_flags $TEST_MOC_ARGS"
 
     # Typecheck

test/viper/ok/array.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@46.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (array.vpr@47.1)

test/viper/ok/array.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/assertions.silicon.ok

@@ -1,2 +1,2 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@46.13--46.24)
-  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@64.15--64.44)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@47.13--47.24)
+  [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@65.15--65.44)

test/viper/ok/assertions.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/async.silicon.ok

@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@69.15--69.42)
+  [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@70.15--70.42)

test/viper/ok/async.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/claim-broken.silicon.ok

@@ -1 +1 @@
-  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@67.20--67.47)
+  [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@68.20--68.47)

test/viper/ok/claim-broken.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/claim-reward-naive.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/claim-simple.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (claim-simple.vpr@39.1)

test/viper/ok/claim-simple.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/claim.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/counter.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (counter.vpr@39.1)

test/viper/ok/counter.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/invariant.silicon.ok

@@ -1 +1 @@
-  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@43.13--43.24)
+  [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@44.13--44.24)

test/viper/ok/invariant.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/lits.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (lits.vpr@37.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (lits.vpr@38.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (lits.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (lits.vpr@39.1)

test/viper/ok/lits.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/loop-invariant.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@37.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@38.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (loop-invariant.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (loop-invariant.vpr@39.1)

test/viper/ok/loop-invariant.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/method-call.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (method-call.vpr@39.1)

test/viper/ok/method-call.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/nats.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (nats.vpr@39.1)

test/viper/ok/nats.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/odd-even.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (odd-even.vpr@37.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (odd-even.vpr@38.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (odd-even.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (odd-even.vpr@39.1)

test/viper/ok/odd-even.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/option.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (option.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (option.vpr@39.1)

test/viper/ok/option.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/polymono.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@37.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@38.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (polymono.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (polymono.vpr@39.1)

test/viper/ok/polymono.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/private.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref

test/viper/ok/reverse.silicon.ok

@@ -1 +1 @@
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (reverse.vpr@41.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (reverse.vpr@42.1)

test/viper/ok/reverse.tc.ok

@@ -1,7 +1,7 @@
-reverse.mo:31.13-31.23: warning [M0155], operator may trap for inferred type
+reverse.mo:32.13-32.23: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:36.35-36.47: warning [M0155], operator may trap for inferred type
+reverse.mo:37.35-37.47: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:36.35-36.51: warning [M0155], operator may trap for inferred type
+reverse.mo:37.35-37.51: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:25.9-25.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)
+reverse.mo:26.9-26.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)

test/viper/ok/reverse.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref
@@ -115,13 +116,10 @@ method copy_xarray($Self: Ref)
       var t: Array
       var i: Int
       length := $size(($Self).xarray);
+      assert (length >= 0);
       inhale $array_acc(t, $int, write);
-      inhale ($size(t) == 5);
-      ($loc(t, 0)).$int := 0;
-      ($loc(t, 1)).$int := 0;
-      ($loc(t, 2)).$int := 0;
-      ($loc(t, 3)).$int := 0;
-      ($loc(t, 4)).$int := 0;
+      inhale ($size(t) == length);
+      inhale $array_init(t, $int, 0);
       i := 0;
       while ((i < length))
          invariant $array_acc(t, $int, write)

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

@@ -1,7 +1,7 @@
-reverse.mo:31.13-31.23: warning [M0155], operator may trap for inferred type
+reverse.mo:32.13-32.23: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:36.35-36.47: warning [M0155], operator may trap for inferred type
+reverse.mo:37.35-37.47: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:36.35-36.51: warning [M0155], operator may trap for inferred type
+reverse.mo:37.35-37.51: warning [M0155], operator may trap for inferred type
   Nat
-reverse.mo:25.9-25.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)
+reverse.mo:26.9-26.10: warning [M0194], unused identifier b (delete or rename to wildcard `_` or `_b`)

test/viper/ok/simple-funs.silicon.ok

@@ -1,2 +1,2 @@
-Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@37.1)
-Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@38.1)
+Parse warning: In macro $Perm, the following parameters were defined but not used: $Self  (simple-funs.vpr@38.1)
+Parse warning: In macro $Inv, the following parameters were defined but not used: $Self  (simple-funs.vpr@39.1)

test/viper/ok/simple-funs.vpr.ok

@@ -10,6 +10,7 @@ domain Array {
 }
 define $array_acc(a, t, p) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, p)
 define $array_untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t)
+define $array_init(a, t, x) forall i : Int :: 0 <= i && i < $size(a) ==> $loc(a, i).t == x
 /* Tuple encoding */
 domain Tuple {
   function $prj(a: Tuple, i: Int): Ref