From b45aa7c205617b62e0d7b7d65442612d11c6d8d2 Mon Sep 17 00:00:00 2001 From: Golovin Pavel Date: Mon, 6 May 2024 15:05:48 +0200 Subject: [PATCH] motoko-san: fix bug with array initialization Problem: permissions are reset incorrectly. Namely, after initialization write access was dropped by exhaling full permission which leads to forgetting assigned before values Solution: do not exhale anything for mutable array and exhale-inhale wildcard for immutable which models losing write access better --- src/viper/prelude.ml | 5 +- src/viper/trans.ml | 44 +++++++------ test/repl/ok/viper.stdout.ok | 5 +- test/viper/array.mo | 13 ++++ test/viper/ok/array.silicon.ok | 2 +- test/viper/ok/array.tc.ok | 10 ++- test/viper/ok/array.vpr.ok | 83 +++++++++++-------------- test/viper/ok/array.vpr.stderr.ok | 10 ++- test/viper/ok/assertions.silicon.ok | 4 +- test/viper/ok/assertions.vpr.ok | 5 +- test/viper/ok/async.silicon.ok | 2 +- test/viper/ok/async.vpr.ok | 5 +- test/viper/ok/claim-broken.silicon.ok | 2 +- test/viper/ok/claim-broken.vpr.ok | 5 +- test/viper/ok/claim-reward-naive.vpr.ok | 5 +- test/viper/ok/claim-simple.silicon.ok | 2 +- test/viper/ok/claim-simple.vpr.ok | 5 +- test/viper/ok/claim.vpr.ok | 5 +- test/viper/ok/counter.silicon.ok | 2 +- test/viper/ok/counter.vpr.ok | 5 +- test/viper/ok/invariant.silicon.ok | 2 +- test/viper/ok/invariant.vpr.ok | 5 +- test/viper/ok/loop-invariant.silicon.ok | 4 +- test/viper/ok/loop-invariant.vpr.ok | 5 +- test/viper/ok/method-call.silicon.ok | 4 +- test/viper/ok/method-call.vpr.ok | 5 +- test/viper/ok/nats.silicon.ok | 2 +- test/viper/ok/nats.vpr.ok | 5 +- test/viper/ok/polymono.silicon.ok | 4 +- test/viper/ok/polymono.vpr.ok | 5 +- test/viper/ok/private.vpr.ok | 5 +- test/viper/ok/reverse.silicon.ok | 4 +- test/viper/ok/reverse.vpr.ok | 37 +++++------ test/viper/ok/simple-funs.silicon.ok | 4 +- test/viper/ok/simple-funs.vpr.ok | 5 +- 35 files changed, 151 insertions(+), 164 deletions(-) diff --git a/src/viper/prelude.ml b/src/viper/prelude.ml index c0367f8c590..89816322ca2 100644 --- a/src/viper/prelude.ml +++ b/src/viper/prelude.ml @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/src/viper/trans.ml b/src/viper/trans.ml index 9878d2f7b19..752be5cf38b 100644 --- a/src/viper/trans.ml +++ b/src/viper/trans.ml @@ -36,11 +36,11 @@ let (!!!) at it = (^^^) at it NoInfo let intLitE at i = !!! at (IntLitE (Mo_values.Numerics.Int.of_int i)) -let accE at fldacc = +let accE at ?(perm=FullP) fldacc = !!! at (AccE( fldacc, - !!! at (PermE (!!! at FullP)))) + !!! at (PermE (!!! at perm)))) let conjoin es at = match es with @@ -56,6 +56,15 @@ let rec adjoin ctxt e = function | [] -> e | f :: fs -> f ctxt (adjoin ctxt e fs) +let locE at exp_arr exp_ix field_name = + !!! at (CallE ("$loc", [exp_arr; exp_ix])), !!! at field_name + +let sizeE at lhs = + !!! at (CallE ("$size", [lhs])) + +let arrayAccE at lhs field_name perm = + let (!!) p = !!! at p in + !! (CallE ("$array_acc", [lhs; !!(FldE field_name); !!(PermE(!! perm))])) let (|:) (x_opt : 'a option) (xs : 'a list) : 'a list = match x_opt with @@ -539,7 +548,7 @@ and exp ctxt e = | M.AnnotE(a, b) -> exp ctxt a | M.CallE ({it=M.DotE (e1, {it="size";_});_}, _inst, {it=M.TupE ([]);at;_}) - -> array_size at (exp ctxt e1) + -> sizeE at (exp ctxt e1) | M.LitE r -> begin match !r with | M.BoolLit b -> @@ -623,31 +632,28 @@ and array_field t = | T.Prim T.Bool -> "$bool" | _ -> unsupported Source.no_region (Mo_types.Arrange_type.typ t) -and array_size at lhs = - !!! at (CallE ("$size", [lhs])) - and array_size_inv at ctxt lhs n = - !!! at (EqCmpE (array_size at lhs, intLitE at n)) + !!! at (EqCmpE (sizeE at lhs, intLitE at n)) and array_acc at lhs t = - let (!!) p = !!! at p in - let call = fun pred -> !! (CallE (pred, [lhs; !!(FldE (array_field t))])) in match T.normalize t with - | T.Mut _ -> call "$array_acc_mut" - | _ -> call "$array_acc" + | T.Mut _-> arrayAccE at lhs (array_field t) FullP + | _ -> arrayAccE at lhs (array_field t) WildcardP and array_alloc at ctxt lhs t es : stmt list = let (!!) p = !!! at p in - let ref_field = !! (array_field t) in let init_array = List.mapi (fun i e -> - FieldAssignS ((!! (CallE ("$loc", [lhs; intLitE at i])), ref_field), exp ctxt e)) es in - (* InhaleS (!! (FldAcc (!! (CallE ("$loc", [var; from_int i])), ref_field)) === e)) es in *) + FieldAssignS (locE at lhs (intLitE at i) (array_field t), exp ctxt e)) es in + (* InhaleS (!! (FldAcc (locE at lhs (intLitE at i) (array_field t))) === e)) es in *) + let reset_perm = + (match T.normalize t with + | 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 ctxt lhs (List.length es)) - ] @ init_array @ [ - ExhaleS (array_acc at lhs (T.Mut t)) - ; InhaleS (array_acc at lhs t)] + ; InhaleS (array_size_inv at ctxt lhs (List.length es))] + @ init_array + @ reset_perm in List.map (!!) stmts and array_loc ctxt at e1 e2 t = - !!! at (CallE ("$loc", [exp ctxt e1; exp ctxt e2])), !!! at (array_field t) \ No newline at end of file + locE at (exp ctxt e1) (exp ctxt e2) (array_field t) diff --git a/test/repl/ok/viper.stdout.ok b/test/repl/ok/viper.stdout.ok index 9104ff7b7bd..ff565e86e95 100644 --- a/test/repl/ok/viper.stdout.ok +++ b/test/repl/ok/viper.stdout.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/array.mo b/test/viper/array.mo index cd6a784af7b..74ddc29dfac 100644 --- a/test/viper/array.mo +++ b/test/viper/array.mo @@ -8,16 +8,29 @@ actor { var count : Int = 42; // let is not supported public func foo(): async Int { + // declarations var vi_a : [Int] = (([1] : [Int]) : [Int]); var vm_a : [var Int] = [var 1, 2]; let li_a : [Bool] = [false]; let lm_a : [var Bool] = [var false]; + + assert:system vi_a[0] == 1; + assert:system vm_a[0] == 1; + assert:system li_a[0] == false; + assert:system lm_a[0] == false; + + // assignments // vi_a = [1, 2] vi_a := [1, 2]; // li_a := [1, 2]; // error 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.silicon.ok b/test/viper/ok/array.silicon.ok index 7b91a64ac36..55888cdebf9 100644 --- a/test/viper/ok/array.silicon.ok +++ b/test/viper/ok/array.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (array.vpr@23.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (array.vpr@22.1) diff --git a/test/viper/ok/array.tc.ok b/test/viper/ok/array.tc.ok index bf84d27a2e0..cde570c72ca 100644 --- a/test/viper/ok/array.tc.ok +++ b/test/viper/ok/array.tc.ok @@ -1,8 +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:13.13-13.17: warning [M0194], unused identifier li_a (delete or rename to wildcard `_` or `_li_a`) -array.mo:14.13-14.17: warning [M0194], unused identifier lm_a (delete or rename to wildcard `_` or `_lm_a`) -array.mo:29.18-29.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`) -array.mo:34.18-34.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`) -array.mo:38.11-38.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`) -array.mo:46.11-46.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 index 023466bac80..0f6cdb8d24f 100644 --- a/test/viper/ok/array.vpr.ok +++ b/test/viper/ok/array.vpr.ok @@ -7,18 +7,17 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref field $array: Array /* END PRELUDE */ -define $Perm($Self) ((((true && (acc(($Self).arr,write) && ($array_acc_mut( +define $Perm($Self) ((((true && (acc(($Self).arr,write) && ($array_acc( ($Self).arr, - $int) && ( + $int, write) && ( $size(($Self).arr) == 2)))) && acc(($Self).f,write)) && acc(($Self).count,write))) define $Inv($Self) (true) method __init__($Self: Ref) @@ -27,12 +26,10 @@ method __init__($Self: Ref) ensures $Perm($Self) ensures $Inv($Self) { - inhale $array_acc_mut(($Self).arr, $int) + inhale $array_acc(($Self).arr, $int, write) inhale ($size(($Self).arr) == 2) ($loc(($Self).arr, 0)).$int := 1 ($loc(($Self).arr, 1)).$int := 2 - exhale $array_acc_mut(($Self).arr, $int) - inhale $array_acc_mut(($Self).arr, $int) ($Self).f := 2 ($Self).count := 42 } @@ -51,40 +48,42 @@ method foo($Self: Ref) var lm_a: Array var vi_a_2: Array var vm_a_2: Array - inhale $array_acc_mut(vi_a, $int) + inhale $array_acc(vi_a, $int, write) inhale ($size(vi_a) == 1) ($loc(vi_a, 0)).$int := 1 - exhale $array_acc_mut(vi_a, $int) - inhale $array_acc(vi_a, $int) - inhale $array_acc_mut(vm_a, $int) + exhale $array_acc(vi_a, $int, wildcard) + inhale $array_acc(vi_a, $int, wildcard) + inhale $array_acc(vm_a, $int, write) inhale ($size(vm_a) == 2) ($loc(vm_a, 0)).$int := 1 ($loc(vm_a, 1)).$int := 2 - exhale $array_acc_mut(vm_a, $int) - inhale $array_acc_mut(vm_a, $int) - inhale $array_acc_mut(li_a, $bool) + inhale $array_acc(li_a, $bool, write) inhale ($size(li_a) == 1) ($loc(li_a, 0)).$bool := false - exhale $array_acc_mut(li_a, $bool) - inhale $array_acc(li_a, $bool) - inhale $array_acc_mut(lm_a, $bool) + exhale $array_acc(li_a, $bool, wildcard) + inhale $array_acc(li_a, $bool, wildcard) + inhale $array_acc(lm_a, $bool, write) inhale ($size(lm_a) == 1) ($loc(lm_a, 0)).$bool := false - exhale $array_acc_mut(lm_a, $bool) - inhale $array_acc_mut(lm_a, $bool) - inhale $array_acc_mut(vi_a_2, $int) + assert (($loc(vi_a, 0)).$int == 1) + assert (($loc(vm_a, 0)).$int == 1) + assert (($loc(li_a, 0)).$bool == false) + assert (($loc(lm_a, 0)).$bool == false) + inhale $array_acc(vi_a_2, $int, write) inhale ($size(vi_a_2) == 2) ($loc(vi_a_2, 0)).$int := 1 ($loc(vi_a_2, 1)).$int := 2 - exhale $array_acc_mut(vi_a_2, $int) - inhale $array_acc(vi_a_2, $int) + exhale $array_acc(vi_a_2, $int, wildcard) + inhale $array_acc(vi_a_2, $int, wildcard) vi_a := vi_a_2 - inhale $array_acc_mut(vm_a_2, $int) + inhale $array_acc(vm_a_2, $int, write) inhale ($size(vm_a_2) == 1) ($loc(vm_a_2, 0)).$int := 42 - exhale $array_acc_mut(vm_a_2, $int) - inhale $array_acc_mut(vm_a_2, $int) 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 @@ -94,15 +93,15 @@ method baz1($Self: Ref) requires $Perm($Self) requires $Inv($Self) ensures $Perm($Self) - ensures $array_acc($Res, $int) + ensures $array_acc($Res, $int, wildcard) ensures $Inv($Self) { var r: Array - inhale $array_acc_mut(r, $int) + inhale $array_acc(r, $int, write) inhale ($size(r) == 2) ($loc(r, 0)).$int := 1 ($loc(r, 1)).$int := 2 - exhale $array_acc_mut(r, $int) - inhale $array_acc(r, $int) + exhale $array_acc(r, $int, wildcard) + inhale $array_acc(r, $int, wildcard) $Res := r goto $Ret label $Ret @@ -111,14 +110,12 @@ method baz2($Self: Ref) returns ($Res: Array) requires $Perm($Self) ensures $Perm($Self) - ensures $array_acc_mut($Res, $int) + ensures $array_acc($Res, $int, write) { var r: Array - inhale $array_acc_mut(r, $int) + inhale $array_acc(r, $int, write) inhale ($size(r) == 2) ($loc(r, 0)).$int := 1 ($loc(r, 1)).$int := 2 - exhale $array_acc_mut(r, $int) - inhale $array_acc_mut(r, $int) $Res := r goto $Ret label $Ret @@ -130,17 +127,15 @@ method bar($Self: Ref) { var x: Array var y: Array var z: Int - inhale $array_acc_mut(x, $int) + inhale $array_acc(x, $int, write) inhale ($size(x) == 2) ($loc(x, 0)).$int := 42 ($loc(x, 1)).$int := 24 - exhale $array_acc_mut(x, $int) - inhale $array_acc(x, $int) - inhale $array_acc_mut(y, $bool) + exhale $array_acc(x, $int, wildcard) + inhale $array_acc(x, $int, wildcard) + inhale $array_acc(y, $bool, write) inhale ($size(y) == 1) ($loc(y, 0)).$bool := false - exhale $array_acc_mut(y, $bool) - inhale $array_acc_mut(y, $bool) ($loc(y, 0)).$bool := true z := (($loc(x, 0)).$int + ($loc(x, 1)).$int) $Res := ($loc(x, 1)).$int @@ -150,19 +145,17 @@ method bar($Self: Ref) method bar2($Self: Ref, x: Array) returns ($Res: Int) requires $Perm($Self) - requires $array_acc(x, $int) + requires $array_acc(x, $int, wildcard) requires ($size(x) == 2) requires $Inv($Self) ensures $Perm($Self) - ensures $array_acc(x, $int) + ensures $array_acc(x, $int, wildcard) ensures $Inv($Self) { var y: Array var z: Int - inhale $array_acc_mut(y, $bool) + inhale $array_acc(y, $bool, write) inhale ($size(y) == 1) ($loc(y, 0)).$bool := false - exhale $array_acc_mut(y, $bool) - inhale $array_acc_mut(y, $bool) ($loc(y, 0)).$bool := true z := (($loc(x, 0)).$int + ($loc(x, 1)).$int) $Res := ($loc(x, 1)).$int diff --git a/test/viper/ok/array.vpr.stderr.ok b/test/viper/ok/array.vpr.stderr.ok index bf84d27a2e0..cde570c72ca 100644 --- a/test/viper/ok/array.vpr.stderr.ok +++ b/test/viper/ok/array.vpr.stderr.ok @@ -1,8 +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:13.13-13.17: warning [M0194], unused identifier li_a (delete or rename to wildcard `_` or `_li_a`) -array.mo:14.13-14.17: warning [M0194], unused identifier lm_a (delete or rename to wildcard `_` or `_lm_a`) -array.mo:29.18-29.22: warning [M0194], unused identifier baz2 (delete or rename to wildcard `_` or `_baz2`) -array.mo:34.18-34.21: warning [M0194], unused identifier bar (delete or rename to wildcard `_` or `_bar`) -array.mo:38.11-38.12: warning [M0194], unused identifier z (delete or rename to wildcard `_` or `_z`) -array.mo:46.11-46.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/assertions.silicon.ok b/test/viper/ok/assertions.silicon.ok index 032e89077dc..f4d3cdb1d8a 100644 --- a/test/viper/ok/assertions.silicon.ok +++ b/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@28.13--28.24) - [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@46.15--46.44) + [0] Postcondition of __init__ might not hold. Assertion $Self.u might not hold. (assertions.vpr@27.13--27.24) + [1] Assert might fail. Assertion $Self.u ==> $Self.v > 0 might not hold. (assertions.vpr@45.15--45.44) diff --git a/test/viper/ok/assertions.vpr.ok b/test/viper/ok/assertions.vpr.ok index 27469915b21..a8cecf6bf96 100644 --- a/test/viper/ok/assertions.vpr.ok +++ b/test/viper/ok/assertions.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/async.silicon.ok b/test/viper/ok/async.silicon.ok index 88be506c084..3840541b951 100644 --- a/test/viper/ok/async.silicon.ok +++ b/test/viper/ok/async.silicon.ok @@ -1 +1 @@ - [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@51.15--51.42) + [0] Exhale might fail. Assertion $Self.$message_async <= 1 might not hold. (async.vpr@50.15--50.42) diff --git a/test/viper/ok/async.vpr.ok b/test/viper/ok/async.vpr.ok index f7980e0c6b2..14c16e30a29 100644 --- a/test/viper/ok/async.vpr.ok +++ b/test/viper/ok/async.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/claim-broken.silicon.ok b/test/viper/ok/claim-broken.silicon.ok index 319c328500b..c36e1b794aa 100644 --- a/test/viper/ok/claim-broken.silicon.ok +++ b/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@49.20--49.47) + [0] Exhale might fail. Assertion $Self.$message_async == 1 ==> $Self.claimed && $Self.count == 0 might not hold. (claim-broken.vpr@48.20--48.47) diff --git a/test/viper/ok/claim-broken.vpr.ok b/test/viper/ok/claim-broken.vpr.ok index 4e1ab2d9f8d..65384fcbe40 100644 --- a/test/viper/ok/claim-broken.vpr.ok +++ b/test/viper/ok/claim-broken.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/claim-reward-naive.vpr.ok b/test/viper/ok/claim-reward-naive.vpr.ok index b64d52eee79..cec82496547 100644 --- a/test/viper/ok/claim-reward-naive.vpr.ok +++ b/test/viper/ok/claim-reward-naive.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/claim-simple.silicon.ok b/test/viper/ok/claim-simple.silicon.ok index 0f575b37f8d..0baf1a7c731 100644 --- a/test/viper/ok/claim-simple.silicon.ok +++ b/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@20.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (claim-simple.vpr@19.1) diff --git a/test/viper/ok/claim-simple.vpr.ok b/test/viper/ok/claim-simple.vpr.ok index 859c7e93588..f7f0cfeb155 100644 --- a/test/viper/ok/claim-simple.vpr.ok +++ b/test/viper/ok/claim-simple.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/claim.vpr.ok b/test/viper/ok/claim.vpr.ok index e9f284e382d..a9e96b2d83e 100644 --- a/test/viper/ok/claim.vpr.ok +++ b/test/viper/ok/claim.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/counter.silicon.ok b/test/viper/ok/counter.silicon.ok index 9af3e35204a..5f86aba1580 100644 --- a/test/viper/ok/counter.silicon.ok +++ b/test/viper/ok/counter.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (counter.vpr@20.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (counter.vpr@19.1) diff --git a/test/viper/ok/counter.vpr.ok b/test/viper/ok/counter.vpr.ok index 4fef56e0a8e..9d805c7526c 100644 --- a/test/viper/ok/counter.vpr.ok +++ b/test/viper/ok/counter.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/invariant.silicon.ok b/test/viper/ok/invariant.silicon.ok index c8f4e03fb6d..3b4ee4b89e4 100644 --- a/test/viper/ok/invariant.silicon.ok +++ b/test/viper/ok/invariant.silicon.ok @@ -1 +1 @@ - [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@25.13--25.24) + [0] Postcondition of __init__ might not hold. Assertion $Self.count > 0 might not hold. (invariant.vpr@24.13--24.24) diff --git a/test/viper/ok/invariant.vpr.ok b/test/viper/ok/invariant.vpr.ok index 00910cbf7a8..030d0482b69 100644 --- a/test/viper/ok/invariant.vpr.ok +++ b/test/viper/ok/invariant.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/loop-invariant.silicon.ok b/test/viper/ok/loop-invariant.silicon.ok index ea4b44a4b95..1de4fc5390f 100644 --- a/test/viper/ok/loop-invariant.silicon.ok +++ b/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@19.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (loop-invariant.vpr@20.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (loop-invariant.vpr@18.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (loop-invariant.vpr@19.1) diff --git a/test/viper/ok/loop-invariant.vpr.ok b/test/viper/ok/loop-invariant.vpr.ok index bd41167b03f..158b2586b24 100644 --- a/test/viper/ok/loop-invariant.vpr.ok +++ b/test/viper/ok/loop-invariant.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/method-call.silicon.ok b/test/viper/ok/method-call.silicon.ok index 8aa6cc1649a..8dfa76475a1 100644 --- a/test/viper/ok/method-call.silicon.ok +++ b/test/viper/ok/method-call.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (method-call.vpr@19.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (method-call.vpr@20.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (method-call.vpr@18.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (method-call.vpr@19.1) diff --git a/test/viper/ok/method-call.vpr.ok b/test/viper/ok/method-call.vpr.ok index b19574c5ba0..93ca8c7493c 100644 --- a/test/viper/ok/method-call.vpr.ok +++ b/test/viper/ok/method-call.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/nats.silicon.ok b/test/viper/ok/nats.silicon.ok index ec7e3600186..e2f84af7b86 100644 --- a/test/viper/ok/nats.silicon.ok +++ b/test/viper/ok/nats.silicon.ok @@ -1 +1 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (nats.vpr@20.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (nats.vpr@19.1) diff --git a/test/viper/ok/nats.vpr.ok b/test/viper/ok/nats.vpr.ok index 082dd24aa0f..a6f6b687277 100644 --- a/test/viper/ok/nats.vpr.ok +++ b/test/viper/ok/nats.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/polymono.silicon.ok b/test/viper/ok/polymono.silicon.ok index 2a50072854c..f890dbb10d7 100644 --- a/test/viper/ok/polymono.silicon.ok +++ b/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@19.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (polymono.vpr@20.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (polymono.vpr@18.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (polymono.vpr@19.1) diff --git a/test/viper/ok/polymono.vpr.ok b/test/viper/ok/polymono.vpr.ok index d644dcbac48..00ba6502c3b 100644 --- a/test/viper/ok/polymono.vpr.ok +++ b/test/viper/ok/polymono.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/private.vpr.ok b/test/viper/ok/private.vpr.ok index 582bc5a5a1f..4d917d1b700 100644 --- a/test/viper/ok/private.vpr.ok +++ b/test/viper/ok/private.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref diff --git a/test/viper/ok/reverse.silicon.ok b/test/viper/ok/reverse.silicon.ok index 1193a6b9872..b0121216dd3 100644 --- a/test/viper/ok/reverse.silicon.ok +++ b/test/viper/ok/reverse.silicon.ok @@ -1,2 +1,2 @@ -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (reverse.vpr@23.1) - [0] Postcondition of reverse might not hold. Assertion $size($Self.xarray) == 5 might not hold. (reverse.vpr@113.13--113.25) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (reverse.vpr@22.1) + [0] Postcondition of reverse might not hold. Assertion $size($Self.xarray) == 5 might not hold. (reverse.vpr@108.13--108.25) diff --git a/test/viper/ok/reverse.vpr.ok b/test/viper/ok/reverse.vpr.ok index 7d16fbcc65c..7913fa8e96b 100644 --- a/test/viper/ok/reverse.vpr.ok +++ b/test/viper/ok/reverse.vpr.ok @@ -7,18 +7,17 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref field $array: Array /* END PRELUDE */ -define $Perm($Self) ((true && (acc(($Self).xarray,write) && ($array_acc_mut( +define $Perm($Self) ((true && (acc(($Self).xarray,write) && ($array_acc( ($Self).xarray, - $int) && ( + $int, write) && ( $size(($Self).xarray) == 5))))) define $Inv($Self) (true) method __init__($Self: Ref) @@ -27,34 +26,32 @@ method __init__($Self: Ref) ensures $Perm($Self) ensures $Inv($Self) { - inhale $array_acc_mut(($Self).xarray, $int) + inhale $array_acc(($Self).xarray, $int, write) inhale ($size(($Self).xarray) == 5) ($loc(($Self).xarray, 0)).$int := 1 ($loc(($Self).xarray, 1)).$int := 2 ($loc(($Self).xarray, 2)).$int := 3 ($loc(($Self).xarray, 3)).$int := 4 - ($loc(($Self).xarray, 4)).$int := 5 - exhale $array_acc_mut(($Self).xarray, $int) - inhale $array_acc_mut(($Self).xarray, $int) + ($loc(($Self).xarray, 4)).$int := 5 } method reverseArray$Nat($Self: Ref, a: Array) requires $Perm($Self) - requires $array_acc_mut(a, $int) + requires $array_acc(a, $int, write) ensures $Perm($Self) - ensures $array_acc_mut(a, $int) + ensures $array_acc(a, $int, write) ensures ($size(a) == $size(old(a))) { var b: Array var length: Int var i: Int var j: Int - inhale $array_acc_mut(b, $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_mut(b, $int) - inhale $array_acc(b, $int) + exhale $array_acc(b, $int, wildcard) + inhale $array_acc(b, $int, wildcard) length := $size(a) if ((length == 0)) { @@ -65,8 +62,8 @@ method reverseArray$Nat($Self: Ref, a: Array) while ((i > j)) invariant ((i < length) && (i >= 0)) invariant ((j < length) && (j >= 0)) - invariant $array_acc(b, $int) - invariant $array_acc_mut(a, $int) + invariant $array_acc(b, $int, wildcard) + invariant $array_acc(a, $int, write) invariant ($Perm($Self) && $Inv($Self)) { var tmp: Int tmp := ($loc(a, i)).$int @@ -83,21 +80,19 @@ method copy_xarray($Self: Ref) returns ($Res: Array) requires $Perm($Self) ensures $Perm($Self) - ensures $array_acc_mut($Res, $int) + ensures $array_acc($Res, $int, write) { var t: Array var i: Int - inhale $array_acc_mut(t, $int) + 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 - exhale $array_acc_mut(t, $int) - inhale $array_acc_mut(t, $int) i := 0 while ((i < 5)) - invariant $array_acc_mut(t, $int) + invariant $array_acc(t, $int, write) invariant ($Perm($Self) && $Inv($Self)) { ($loc(t, i)).$int := ($loc(($Self).xarray, i)).$int diff --git a/test/viper/ok/simple-funs.silicon.ok b/test/viper/ok/simple-funs.silicon.ok index e104157e47e..dc3058f6f4d 100644 --- a/test/viper/ok/simple-funs.silicon.ok +++ 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@19.1) -Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (simple-funs.vpr@20.1) +Parse warning: In macro $Perm, the following parameters were defined but not used: $Self (simple-funs.vpr@18.1) +Parse warning: In macro $Inv, the following parameters were defined but not used: $Self (simple-funs.vpr@19.1) diff --git a/test/viper/ok/simple-funs.vpr.ok b/test/viper/ok/simple-funs.vpr.ok index 040a449823e..34a7ede0f83 100644 --- a/test/viper/ok/simple-funs.vpr.ok +++ b/test/viper/ok/simple-funs.vpr.ok @@ -7,9 +7,8 @@ domain Array { axiom $all_diff { forall a: Array, i: Int :: {$loc(a, i)} $first($loc(a, i)) == a && $second($loc(a, i)) == i } axiom $size_nonneg { forall a: Array :: $size(a) >= 0 } } -define $array_acc_mut(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t) -define $array_acc(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> acc($loc(a, j).t, 1/2) -define $untouched(a, t) forall j: Int :: 0 <= j && j < $size(a) ==> $loc(a, j).t == old($loc(a, j).t) +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) field $int: Int field $bool: Bool field $ref: Ref