// // Translation of Viper program. // // Date: 2024-07-11 15:14:43 // Tool: carbon 1.0 // Arguments: : /Users/jkai/Dropbox/SURE-2024/ViperScratchpad/arrayTestChainIrrel3.vpr --print /Users/jkai/ViperTests/arrayTestChainIrrel3.bpl --boogieExe /Users/jkai/.dotnet/tools/boogie --boogieOpt /vcsCores:1 --timeout 1 --z3Exe /opt/homebrew/bin/z3 // Dependencies: // Boogie , located at /Users/jkai/.dotnet/tools/boogie. // Z3 4.13.0 - 64 bit, located at /opt/homebrew/bin/z3. // // ================================================== // Preamble of State module. // ================================================== function state(Heap: HeapType, Mask: MaskType): bool; axiom state(dummyHeap, ZeroMask); // ================================================== // Preamble of Heap module. // ================================================== type Ref; var Heap: HeapType; const null: Ref; type Field A B; type NormalField; const dummyHeap: HeapType; type HeapType = [Ref, Field A B]B; const unique $allocated: Field NormalField bool; axiom (forall o: Ref, f: (Field NormalField Ref), Heap: HeapType :: { Heap[o, f] } Heap[o, $allocated] ==> Heap[Heap[o, f], $allocated] ); function succHeap(Heap0: HeapType, Heap1: HeapType): bool; function succHeapTrans(Heap0: HeapType, Heap1: HeapType): bool; function IdenticalOnKnownLocations(Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType): bool; function IsPredicateField(f_1: (Field A B)): bool; function IsWandField(f_1: (Field A B)): bool; function getPredWandId(f_1: (Field A B)): int; // Frame all locations with direct permissions axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, o_1: Ref, f_2: (Field A B) :: { IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), ExhaleHeap[o_1, f_2] } IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, o_1, f_2) ==> Heap[o_1, f_2] == ExhaleHeap[o_1, f_2] ); // Frame all predicate mask locations of predicates with direct permission axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, pm_f: (Field C FrameType) :: { IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), IsPredicateField(pm_f), ExhaleHeap[null, PredicateMaskField(pm_f)] } IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, null, pm_f) && IsPredicateField(pm_f) ==> Heap[null, PredicateMaskField(pm_f)] == ExhaleHeap[null, PredicateMaskField(pm_f)] ); // Frame all locations with known folded permissions axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, pm_f: (Field C FrameType) :: { IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), IsPredicateField(pm_f) } IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, null, pm_f) && IsPredicateField(pm_f) ==> (forall o2: Ref, f_2: (Field A B) :: { ExhaleHeap[o2, f_2] } Heap[null, PredicateMaskField(pm_f)][o2, f_2] ==> Heap[o2, f_2] == ExhaleHeap[o2, f_2] ) ); // Frame all wand mask locations of wands with direct permission axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, pm_f: (Field C FrameType) :: { IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), IsWandField(pm_f), ExhaleHeap[null, WandMaskField(pm_f)] } IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, null, pm_f) && IsWandField(pm_f) ==> Heap[null, WandMaskField(pm_f)] == ExhaleHeap[null, WandMaskField(pm_f)] ); // Frame all locations in the footprint of magic wands axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, pm_f: (Field C FrameType) :: { IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), IsWandField(pm_f) } IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> HasDirectPerm(Mask, null, pm_f) && IsWandField(pm_f) ==> (forall o2: Ref, f_2: (Field A B) :: { ExhaleHeap[o2, f_2] } Heap[null, WandMaskField(pm_f)][o2, f_2] ==> Heap[o2, f_2] == ExhaleHeap[o2, f_2] ) ); // All previously-allocated references are still allocated axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType, o_1: Ref :: { IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask), ExhaleHeap[o_1, $allocated] } IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> Heap[o_1, $allocated] ==> ExhaleHeap[o_1, $allocated] ); // Updated Heaps are Successor Heaps axiom (forall Heap: HeapType, o: Ref, f_3: (Field A B), v: B :: { Heap[o, f_3:=v] } succHeap(Heap, Heap[o, f_3:=v]) ); // IdenticalOnKnownLocations Heaps are Successor Heaps axiom (forall Heap: HeapType, ExhaleHeap: HeapType, Mask: MaskType :: { IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) } IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask) ==> succHeap(Heap, ExhaleHeap) ); // Successor Heaps are Transitive Successor Heaps axiom (forall Heap0: HeapType, Heap1: HeapType :: { succHeap(Heap0, Heap1) } succHeap(Heap0, Heap1) ==> succHeapTrans(Heap0, Heap1) ); // Transitivity of Transitive Successor Heaps axiom (forall Heap0: HeapType, Heap1: HeapType, Heap2: HeapType :: { succHeapTrans(Heap0, Heap1), succHeap(Heap1, Heap2) } succHeapTrans(Heap0, Heap1) && succHeap(Heap1, Heap2) ==> succHeapTrans(Heap0, Heap2) ); // ================================================== // Preamble of Permission module. // ================================================== type Perm = real; type MaskType = [Ref, Field A B]Perm; var Mask: MaskType; const ZeroMask: MaskType; axiom (forall o_2: Ref, f_4: (Field A B) :: { ZeroMask[o_2, f_4] } ZeroMask[o_2, f_4] == NoPerm ); type PMaskType = [Ref, Field A B]bool; const ZeroPMask: PMaskType; axiom (forall o_2: Ref, f_4: (Field A B) :: { ZeroPMask[o_2, f_4] } !ZeroPMask[o_2, f_4] ); function PredicateMaskField(f_5: (Field A FrameType)): Field A PMaskType; function WandMaskField(f_5: (Field A FrameType)): Field A PMaskType; const NoPerm: Perm; axiom NoPerm == 0.000000000; const FullPerm: Perm; axiom FullPerm == 1.000000000; function Perm(a: real, b: real): Perm; function GoodMask(Mask: MaskType): bool; axiom (forall Heap: HeapType, Mask: MaskType :: { state(Heap, Mask) } state(Heap, Mask) ==> GoodMask(Mask) ); axiom (forall Mask: MaskType, o_2: Ref, f_4: (Field A B) :: { GoodMask(Mask), Mask[o_2, f_4] } GoodMask(Mask) ==> Mask[o_2, f_4] >= NoPerm && ((GoodMask(Mask) && !IsPredicateField(f_4)) && !IsWandField(f_4) ==> Mask[o_2, f_4] <= FullPerm) ); function HasDirectPerm(Mask: MaskType, o_2: Ref, f_4: (Field A B)): bool; axiom (forall Mask: MaskType, o_2: Ref, f_4: (Field A B) :: { HasDirectPerm(Mask, o_2, f_4) } HasDirectPerm(Mask, o_2, f_4) <==> Mask[o_2, f_4] > NoPerm ); function sumMask(ResultMask: MaskType, SummandMask1: MaskType, SummandMask2: MaskType): bool; axiom (forall ResultMask: MaskType, SummandMask1: MaskType, SummandMask2: MaskType, o_2: Ref, f_4: (Field A B) :: { sumMask(ResultMask, SummandMask1, SummandMask2), ResultMask[o_2, f_4] } { sumMask(ResultMask, SummandMask1, SummandMask2), SummandMask1[o_2, f_4] } { sumMask(ResultMask, SummandMask1, SummandMask2), SummandMask2[o_2, f_4] } sumMask(ResultMask, SummandMask1, SummandMask2) ==> ResultMask[o_2, f_4] == SummandMask1[o_2, f_4] + SummandMask2[o_2, f_4] ); // ================================================== // Function for trigger used in checks which are never triggered // ================================================== function neverTriggered1(__ind_4: int): bool; function neverTriggered2(__ind_6: int): bool; function neverTriggered3(__ind_9: int): bool; function neverTriggered4(__ind_10: int): bool; function neverTriggered5(__ind_11: int): bool; function neverTriggered6(__ind_12: int): bool; function neverTriggered7(__ind_13: int): bool; function neverTriggered8(__ind_3: int): bool; function neverTriggered9(j_1: int): bool; function neverTriggered10(__ind_2: int): bool; function neverTriggered11(__ind_3: int): bool; function neverTriggered12(__ind_7: int): bool; function neverTriggered13(__ind_8: int): bool; function neverTriggered14(__ind_12: int): bool; function neverTriggered15(__ind_13: int): bool; function neverTriggered16(__ind_17: int): bool; function neverTriggered17(__ind_18: int): bool; function neverTriggered18(__ind_22: int): bool; function neverTriggered19(__ind_23: int): bool; function neverTriggered20(__ind_27: int): bool; function neverTriggered21(__ind_28: int): bool; function neverTriggered22(__ind_32: int): bool; function neverTriggered23(__ind_33: int): bool; function neverTriggered24(__ind_37: int): bool; function neverTriggered25(__ind_38: int): bool; function neverTriggered26(__ind_42: int): bool; function neverTriggered27(__ind_43: int): bool; function neverTriggered28(__ind_45: int): bool; function neverTriggered29(__ind_46: int): bool; // ================================================== // Functions used as inverse of receiver expressions in quantified permissions during inhale and exhale // ================================================== function invRecv1(recv: Ref): int; function invRecv2(recv: Ref): int; function invRecv3(recv: Ref): int; function invRecv4(recv: Ref): int; function invRecv5(recv: Ref): int; function invRecv6(recv: Ref): int; function invRecv7(recv: Ref): int; function invRecv8(recv: Ref): int; function invRecv9(recv: Ref): int; function invRecv10(recv: Ref): int; function invRecv11(recv: Ref): int; function invRecv12(recv: Ref): int; function invRecv13(recv: Ref): int; function invRecv14(recv: Ref): int; function invRecv15(recv: Ref): int; function invRecv16(recv: Ref): int; function invRecv17(recv: Ref): int; function invRecv18(recv: Ref): int; function invRecv19(recv: Ref): int; function invRecv20(recv: Ref): int; function invRecv21(recv: Ref): int; function invRecv22(recv: Ref): int; function invRecv23(recv: Ref): int; function invRecv24(recv: Ref): int; function invRecv25(recv: Ref): int; function invRecv26(recv: Ref): int; function invRecv27(recv: Ref): int; function invRecv28(recv: Ref): int; function invRecv29(recv: Ref): int; // ================================================== // Functions used to represent the range of the projection of each QP instance onto its receiver expressions for quantified permissions during inhale and exhale // ================================================== function qpRange1(recv: Ref): bool; function qpRange2(recv: Ref): bool; function qpRange3(recv: Ref): bool; function qpRange4(recv: Ref): bool; function qpRange5(recv: Ref): bool; function qpRange6(recv: Ref): bool; function qpRange7(recv: Ref): bool; function qpRange8(recv: Ref): bool; function qpRange9(recv: Ref): bool; function qpRange10(recv: Ref): bool; function qpRange11(recv: Ref): bool; function qpRange12(recv: Ref): bool; function qpRange13(recv: Ref): bool; function qpRange14(recv: Ref): bool; function qpRange15(recv: Ref): bool; function qpRange16(recv: Ref): bool; function qpRange17(recv: Ref): bool; function qpRange18(recv: Ref): bool; function qpRange19(recv: Ref): bool; function qpRange20(recv: Ref): bool; function qpRange21(recv: Ref): bool; function qpRange22(recv: Ref): bool; function qpRange23(recv: Ref): bool; function qpRange24(recv: Ref): bool; function qpRange25(recv: Ref): bool; function qpRange26(recv: Ref): bool; function qpRange27(recv: Ref): bool; function qpRange28(recv: Ref): bool; function qpRange29(recv: Ref): bool; // ================================================== // Preamble of Function and predicate module. // ================================================== // Function heights (higher height means its body is available earlier): // - height 1: __snap_Int_Int_Int_val_prime // - height 0: __snap_Int_Int_Int_val const AssumeFunctionsAbove: int; // Declarations for function framing type FrameType; const EmptyFrame: FrameType; function FrameFragment(t: T): FrameType; function ConditionalFrame(p: Perm, f_6: FrameType): FrameType; function dummyFunction(t: T): bool; function CombineFrames(a_1: FrameType, b_1: FrameType): FrameType; // ================================================== // Definition of conditional frame fragments // ================================================== axiom (forall p: Perm, f_6: FrameType :: { ConditionalFrame(p, f_6) } ConditionalFrame(p, f_6) == (if p > 0.000000000 then f_6 else EmptyFrame) ); // Function for recording enclosure of one predicate instance in another function InsidePredicate(p: (Field A FrameType), v_1: FrameType, q: (Field B FrameType), w: FrameType): bool; // Transitivity of InsidePredicate axiom (forall p: (Field A FrameType), v_1: FrameType, q: (Field B FrameType), w: FrameType, r: (Field C FrameType), u: FrameType :: { InsidePredicate(p, v_1, q, w), InsidePredicate(q, w, r, u) } InsidePredicate(p, v_1, q, w) && InsidePredicate(q, w, r, u) ==> InsidePredicate(p, v_1, r, u) ); // Knowledge that two identical instances of the same predicate cannot be inside each other axiom (forall p: (Field A FrameType), v_1: FrameType, w: FrameType :: { InsidePredicate(p, v_1, p, w) } !InsidePredicate(p, v_1, p, w) ); // ================================================== // Preamble of Set module. // ================================================== type Set T = [T]bool; function Set#Card(Set T): int; axiom (forall s: Set T :: { Set#Card(s) } 0 <= Set#Card(s)); function Set#Empty(): Set T; axiom (forall o: T :: { Set#Empty()[o] } !Set#Empty()[o]); axiom (forall s: Set T :: { Set#Card(s) } (Set#Card(s) == 0 <==> s == Set#Empty()) && (Set#Card(s) != 0 ==> (exists x: T :: s[x]))); function Set#Singleton(T): Set T; axiom (forall r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]); axiom (forall r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o); axiom (forall r: T :: { Set#Card(Set#Singleton(r)) } Set#Card(Set#Singleton(r)) == 1); function Set#UnionOne(Set T, T): Set T; axiom (forall a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] } Set#UnionOne(a,x)[o] <==> o == x || a[o]); axiom (forall a: Set T, x: T :: { Set#UnionOne(a, x) } Set#UnionOne(a, x)[x]); axiom (forall a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] } a[y] ==> Set#UnionOne(a, x)[y]); axiom (forall a: Set T, x: T :: { Set#Card(Set#UnionOne(a, x)) } a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a)); axiom (forall a: Set T, x: T :: { Set#Card(Set#UnionOne(a, x)) } !a[x] ==> Set#Card(Set#UnionOne(a, x)) == Set#Card(a) + 1); function Set#Union(Set T, Set T): Set T; axiom (forall a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] } Set#Union(a,b)[o] <==> a[o] || b[o]); axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), a[y] } a[y] ==> Set#Union(a, b)[y]); axiom (forall a, b: Set T, y: T :: { Set#Union(a, b), b[y] } b[y] ==> Set#Union(a, b)[y]); //axiom (forall a, b: Set T :: { Set#Union(a, b) } // Set#Disjoint(a, b) ==> // Set#Difference(Set#Union(a, b), a) == b && // Set#Difference(Set#Union(a, b), b) == a); function Set#Intersection(Set T, Set T): Set T; axiom (forall a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] } {Set#Intersection(a,b), a[o]} {Set#Intersection(a,b), b[o]} // AS: added alternative triggers 20/06/19 Set#Intersection(a,b)[o] <==> a[o] && b[o]); axiom (forall a, b: Set T :: { Set#Union(Set#Union(a, b), b) } Set#Union(Set#Union(a, b), b) == Set#Union(a, b)); axiom (forall a, b: Set T :: { Set#Union(a, Set#Union(a, b)) } Set#Union(a, Set#Union(a, b)) == Set#Union(a, b)); axiom (forall a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) } Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b)); axiom (forall a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) } Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b)); axiom (forall a, b: Set T :: { Set#Card(Set#Union(a, b)) }{ Set#Card(Set#Intersection(a, b)) } Set#Card(Set#Union(a, b)) + Set#Card(Set#Intersection(a, b)) == Set#Card(a) + Set#Card(b)); function Set#Difference(Set T, Set T): Set T; axiom (forall a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] } { Set#Difference(a,b), a[o] } Set#Difference(a,b)[o] <==> a[o] && !b[o]); axiom (forall a, b: Set T, y: T :: { Set#Difference(a, b), b[y] } b[y] ==> !Set#Difference(a, b)[y] ); axiom (forall a, b: Set T :: { Set#Card(Set#Difference(a, b)) } Set#Card(Set#Difference(a, b)) + Set#Card(Set#Difference(b, a)) + Set#Card(Set#Intersection(a, b)) == Set#Card(Set#Union(a, b)) && Set#Card(Set#Difference(a, b)) == Set#Card(a) - Set#Card(Set#Intersection(a, b))); function Set#Subset(Set T, Set T): bool; axiom(forall a: Set T, b: Set T :: { Set#Subset(a,b) } Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o])); // axiom(forall a: Set T, b: Set T :: // { Set#Subset(a,b), Set#Card(a), Set#Card(b) } // very restrictive trigger // Set#Subset(a,b) ==> Set#Card(a) <= Set#Card(b)); function Set#Equal(Set T, Set T): bool; axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) } Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o])); axiom(forall a: Set T, b: Set T :: { Set#Equal(a,b) } // extensionality axiom for sets Set#Equal(a,b) ==> a == b); //function Set#Disjoint(Set T, Set T): bool; //axiom (forall a: Set T, b: Set T :: { Set#Disjoint(a,b) } // Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o])); // --------------------------------------------------------------- // -- Axiomatization of multisets -------------------------------- // --------------------------------------------------------------- function Math#min(a: int, b: int): int; axiom (forall a: int, b: int :: { Math#min(a, b) } a <= b <==> Math#min(a, b) == a); axiom (forall a: int, b: int :: { Math#min(a, b) } b <= a <==> Math#min(a, b) == b); axiom (forall a: int, b: int :: { Math#min(a, b) } Math#min(a, b) == a || Math#min(a, b) == b); function Math#clip(a: int): int; axiom (forall a: int :: { Math#clip(a) } 0 <= a ==> Math#clip(a) == a); axiom (forall a: int :: { Math#clip(a) } a < 0 ==> Math#clip(a) == 0); type MultiSet T; // = [T]int; function MultiSet#Select(ms: MultiSet T, x:T): int; //function $IsGoodMultiSet(ms: MultiSet T): bool; // ints are non-negative, used after havocing, and for conversion from sequences to multisets. //axiom (forall ms: MultiSet T :: { $IsGoodMultiSet(ms) } // $IsGoodMultiSet(ms) <==> // (forall bx: T :: { ms[bx] } 0 <= ms[bx] && ms[bx] <= MultiSet#Card(ms))); axiom (forall ms: MultiSet T, x: T :: {MultiSet#Select(ms,x)} MultiSet#Select(ms,x) >= 0); // NEW function MultiSet#Card(MultiSet T): int; axiom (forall s: MultiSet T :: { MultiSet#Card(s) } 0 <= MultiSet#Card(s)); //axiom (forall s: MultiSet T, x: T, n: int :: { MultiSet#Card(s[x := n]) } // 0 <= n ==> MultiSet#Card(s[x := n]) == MultiSet#Card(s) - s[x] + n); // function MultiSet#Empty(): MultiSet T; axiom (forall o: T :: { MultiSet#Select(MultiSet#Empty(),o) } MultiSet#Select(MultiSet#Empty(),o) == 0); axiom (forall s: MultiSet T :: { MultiSet#Card(s) } (MultiSet#Card(s) == 0 <==> s == MultiSet#Empty()) && (MultiSet#Card(s) != 0 ==> (exists x: T :: 0 < MultiSet#Select(s,x)))); function MultiSet#Singleton(T): MultiSet T; axiom (forall r: T, o: T :: { MultiSet#Select(MultiSet#Singleton(r),o) } (MultiSet#Select(MultiSet#Singleton(r),o) == 1 <==> r == o) && (MultiSet#Select(MultiSet#Singleton(r),o) == 0 <==> r != o)); axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Card(MultiSet#Singleton(r)) == 1 && MultiSet#Select(MultiSet#Singleton(r),r) == 1); // AS: added axiom (forall r: T :: { MultiSet#Singleton(r) } MultiSet#Singleton(r) == MultiSet#UnionOne(MultiSet#Empty(), r)); // AS: remove this? function MultiSet#UnionOne(MultiSet T, T): MultiSet T; // union-ing increases count by one for x, not for others axiom (forall a: MultiSet T, x: T, o: T :: { MultiSet#Select(MultiSet#UnionOne(a,x),o) } { MultiSet#UnionOne(a, x), MultiSet#Select(a,o) } // AS: added back this trigger (used on a similar axiom before) MultiSet#Select(MultiSet#UnionOne(a, x),o) == (if x==o then MultiSet#Select(a,o) + 1 else MultiSet#Select(a,o))); // non-decreasing axiom (forall a: MultiSet T, x: T :: { MultiSet#Card(MultiSet#UnionOne(a, x)) } {MultiSet#UnionOne(a, x), MultiSet#Card(a)} // AS: added alternative trigger MultiSet#Card(MultiSet#UnionOne(a, x)) == MultiSet#Card(a) + 1); // AS: added - concrete knowledge of element added axiom (forall a: MultiSet T, x: T :: { MultiSet#UnionOne(a,x)} MultiSet#Select(MultiSet#UnionOne(a, x),x) > 0 && MultiSet#Card(MultiSet#UnionOne(a, x)) > 0); function MultiSet#Union(MultiSet T, MultiSet T): MultiSet T; // union-ing is the sum of the contents axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Select(MultiSet#Union(a,b),o) } {MultiSet#Union(a,b), MultiSet#Select(a,o), MultiSet#Select(b,o)}// AS: added triggers MultiSet#Select(MultiSet#Union(a,b),o) == MultiSet#Select(a,o) + MultiSet#Select(b,o)); axiom (forall a: MultiSet T, b: MultiSet T :: { MultiSet#Card(MultiSet#Union(a,b)) } {MultiSet#Card(a), MultiSet#Union(a,b)} {MultiSet#Card(b), MultiSet#Union(a,b)} MultiSet#Card(MultiSet#Union(a,b)) == MultiSet#Card(a) + MultiSet#Card(b)); function MultiSet#Intersection(MultiSet T, MultiSet T): MultiSet T; axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Select(MultiSet#Intersection(a,b),o) } MultiSet#Select(MultiSet#Intersection(a,b),o) == Math#min(MultiSet#Select(a,o), MultiSet#Select(b,o))); // left and right pseudo-idempotence axiom (forall a, b: MultiSet T :: { MultiSet#Intersection(MultiSet#Intersection(a, b), b) } MultiSet#Intersection(MultiSet#Intersection(a, b), b) == MultiSet#Intersection(a, b)); axiom (forall a, b: MultiSet T :: { MultiSet#Intersection(a, MultiSet#Intersection(a, b)) } MultiSet#Intersection(a, MultiSet#Intersection(a, b)) == MultiSet#Intersection(a, b)); // multiset difference, a - b. clip() makes it positive. function MultiSet#Difference(MultiSet T, MultiSet T): MultiSet T; axiom (forall a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Select(MultiSet#Difference(a,b),o) } MultiSet#Select(MultiSet#Difference(a,b),o) == Math#clip(MultiSet#Select(a,o) - MultiSet#Select(b,o))); axiom (forall a, b: MultiSet T, y: T :: { MultiSet#Difference(a, b), MultiSet#Select(b,y), MultiSet#Select(a,y) } MultiSet#Select(a,y) <= MultiSet#Select(b,y) ==> MultiSet#Select(MultiSet#Difference(a, b),y) == 0 ); axiom (forall a, b: MultiSet T :: { MultiSet#Card(MultiSet#Difference(a, b)) } MultiSet#Card(MultiSet#Difference(a, b)) + MultiSet#Card(MultiSet#Difference(b, a)) + 2 * MultiSet#Card(MultiSet#Intersection(a, b)) == MultiSet#Card(MultiSet#Union(a, b)) && MultiSet#Card(MultiSet#Difference(a, b)) == MultiSet#Card(a) - MultiSet#Card(MultiSet#Intersection(a, b))); // multiset subset means a must have at most as many of each element as b function MultiSet#Subset(MultiSet T, MultiSet T): bool; axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Subset(a,b) } MultiSet#Subset(a,b) <==> (forall o: T :: {MultiSet#Select(a,o)} {MultiSet#Select(b,o)} MultiSet#Select(a,o) <= MultiSet#Select(b,o))); function MultiSet#Equal(MultiSet T, MultiSet T): bool; axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) } MultiSet#Equal(a,b) <==> (forall o: T :: {MultiSet#Select(a,o)} {MultiSet#Select(b,o)} MultiSet#Select(a,o) == MultiSet#Select(b,o))); // extensionality axiom for multisets axiom(forall a: MultiSet T, b: MultiSet T :: { MultiSet#Equal(a,b) } MultiSet#Equal(a,b) ==> a == b); function MultiSet#Disjoint(MultiSet T, MultiSet T): bool; axiom (forall a: MultiSet T, b: MultiSet T :: { MultiSet#Disjoint(a,b) } MultiSet#Disjoint(a,b) <==> (forall o: T :: {MultiSet#Select(a,o)} {MultiSet#Select(b,o)} MultiSet#Select(a,o) == 0 || MultiSet#Select(b,o) == 0)); // ================================================== // Preamble of Map module. // ================================================== type Map U V; // A Map is defined by three functions, Map#Domain, Map#Elements, and #Map#Card. function Map#Domain(Map U V) : Set U; function Map#Elements(Map U V) : [U]V; function Map#Card(Map U V) : int; axiom (forall m: Map U V :: { Map#Card(m) } 0 <= Map#Card(m)); // The set of Keys of a Map are available by Map#Domain, and the cardinality of that // set is given by Map#Card. /* added second trigger set */ axiom (forall m: Map U V :: { Set#Card(Map#Domain(m)) } { Map#Card(m) } Set#Card(Map#Domain(m)) == Map#Card(m)); // The set of Values of a Map can be obtained by the function Map#Values, which is // defined as follows. Remember, a Set is defined by membership (using Boogie's // square brackets) and Map#Card, so we need to define what these mean for the Set // returned by Map#Values. function Map#Values(Map U V) : Set V; /* split axiom into each direction */ axiom (forall m: Map U V, v: V :: { Map#Values(m)[v] } Map#Values(m)[v] ==> (exists u: U :: { Map#Domain(m)[u] } { Map#Elements(m)[u] } Map#Domain(m)[u] && v == Map#Elements(m)[u])); axiom (forall m: Map U V, u: U :: { Map#Elements(m)[u] } // { Map#Domain(m)[u] } // REMOVED this trigger due to a potential for matching loops Map#Domain(m)[u] ==> Map#Values(m)[Map#Elements(m)[u]]); // There's a potential for matching loops with the extra trigger if two maps have equal domains: // v in range(m1); some k in dom(m1) = dom(m2) s.t. m1[k] = v; m2[k] in range(m2); some k' in dom(m2) s.t. m2[k'] = m2[k] axiom (forall m: Map U V, u: U :: { Map#Domain(m)[u] } { Map#Elements(m)[u] } Map#Domain(m)[u] ==> Set#Card(Map#Values(m)) > 0); // weaker property than above, with weaker triggers // Here are the operations that produce Map values. function Map#Empty(): Map U V; axiom (forall u: U :: { Map#Domain(Map#Empty(): Map U V)[u] } !Map#Domain(Map#Empty(): Map U V)[u]); axiom (forall m: Map U V :: { Map#Card(m) } (Map#Card(m) == 0 <==> m == Map#Empty()) && (Map#Card(m) != 0 ==> (exists x: U :: Map#Domain(m)[x])) && ((forall x: U :: {Map#Domain(m)[x]} Map#Domain(m)[x] ==> Map#Card(m) != 0))); //Build is used in displays, and for map updates function Map#Build(Map U V, U, V): Map U V; /* added second trigger set (cf. example3 test case, test3) */ axiom (forall m: Map U V, u: U, u': U, v: V :: { Map#Domain(Map#Build(m, u, v))[u'] } { Map#Domain(m)[u'],Map#Build(m, u, v) } { Map#Elements(Map#Build(m, u, v))[u'] } (u' == u ==> Map#Domain(Map#Build(m, u, v))[u'] && Map#Elements(Map#Build(m, u, v))[u'] == v) && (u' != u ==> Map#Domain(Map#Build(m, u, v))[u'] == Map#Domain(m)[u'] && Map#Elements(Map#Build(m, u, v))[u'] == Map#Elements(m)[u'])); /* added second trigger set (not sure of a test case needing it, though) */ axiom (forall m: Map U V, u: U, v: V :: { Map#Card(Map#Build(m, u, v)) }{ Map#Card(m),Map#Build(m, u, v) } Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m)); /* added second trigger set (not sure of a test case needing it, though) */ axiom (forall m: Map U V, u: U, v: V :: { Map#Card(Map#Build(m, u, v)) }{ Map#Card(m),Map#Build(m, u, v) } !Map#Domain(m)[u] ==> Map#Card(Map#Build(m, u, v)) == Map#Card(m) + 1); //equality for maps // this axiom is only needed in one direction; the other is implied by the next axiom function Map#Equal(Map U V, Map U V): bool; axiom (forall m: Map U V, m': Map U V:: { Map#Equal(m, m') } (forall u : U :: Map#Domain(m)[u] == Map#Domain(m')[u]) && (forall u : U :: Map#Domain(m)[u] ==> Map#Elements(m)[u] == Map#Elements(m')[u]) ==> Map#Equal(m, m')); // extensionality axiom (forall m: Map U V, m': Map U V:: { Map#Equal(m, m') } Map#Equal(m, m') ==> m == m'); function Map#Disjoint(Map U V, Map U V): bool; // split in both directions axiom (forall m: Map U V, m': Map U V :: { Map#Disjoint(m, m') } Map#Disjoint(m, m') ==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o])); axiom (forall m: Map U V, m': Map U V :: { Map#Disjoint(m, m') } !Map#Disjoint(m, m') ==> (exists o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} Map#Domain(m)[o] && Map#Domain(m')[o])); // ================================================== // Translation of domain Array // ================================================== // The type for domain Array type ArrayDomainType; // Translation of domain function loc function loc(a_2: ArrayDomainType, i: int): Ref; // Translation of domain function len function len(a_2: ArrayDomainType): int; // Translation of domain function first function first(r_1: Ref): ArrayDomainType; // Translation of domain function second function second(r_1: Ref): int; // Translation of domain axiom all_diff axiom (forall a_3: ArrayDomainType, i_1: int :: { (loc(a_3, i_1): Ref) } (first((loc(a_3, i_1): Ref)): ArrayDomainType) == a_3 && (second((loc(a_3, i_1): Ref)): int) == i_1 ); // Translation of domain axiom len_nonneg axiom (forall a_3: ArrayDomainType :: { (len(a_3): int) } (len(a_3): int) >= 0 ); // ================================================== // Translation of domain Fold // ================================================== // The type for domain Fold type FoldDomainType A V B; // Translation of domain function hfold function hfold(r_1: (ReceiverDomainType A), m: (MappingDomainType V B), op: (OperatorDomainType B)): FoldDomainType A V B; // Translation of domain function hfoldApply function hfoldApply(c: (FoldDomainType A V B), snap: (Map A B)): B; // Translation of domain function hfoldApply1 function hfoldApply1(c: (FoldDomainType A V B), snap: (Map A B)): B; // Translation of domain function getreceiver function getreceiver(c: (FoldDomainType A V B)): ReceiverDomainType A; // Translation of domain function getoperator function getoperator(c: (FoldDomainType A V B)): OperatorDomainType B; // Translation of domain function getmapping function getmapping(c: (FoldDomainType A V B)): MappingDomainType V B; // Translation of domain function dummy1 function dummy1(a_2: B): bool; // Translation of domain function _triggerDeleteBlock function _triggerDeleteBlock(applyC: B, block: (Set A)): bool; // Translation of domain function _triggerDeleteKey1 function _triggerDeleteKey1(applyC: B, key: A): bool; // Translation of domain function exhaleCompMap function exhaleCompMap(c: (FoldDomainType A V B), m: (Map A B), fieldID: int): bool; // Translation of domain function getSnapFieldID function getSnapFieldID(m: (Map A B)): int; // Translation of domain axiom applyComp1Eq axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap: (Map A B) :: { (hfoldApply(__fold_c, __fold_snap): B) } (hfoldApply(__fold_c, __fold_snap): B) == (hfoldApply1(__fold_c, __fold_snap): B) ); // Translation of domain axiom _invAxFold axiom (forall __fold_r: (ReceiverDomainType A), __fold_m: (MappingDomainType V B), __fold_o: (OperatorDomainType B) :: { (hfold(__fold_r, __fold_m, __fold_o): FoldDomainType A V B) } (getreceiver((hfold(__fold_r, __fold_m, __fold_o): FoldDomainType A V B)): ReceiverDomainType A) == __fold_r && ((getmapping((hfold(__fold_r, __fold_m, __fold_o): FoldDomainType A V B)): MappingDomainType V B) == __fold_m && (getoperator((hfold(__fold_r, __fold_m, __fold_o): FoldDomainType A V B)): OperatorDomainType B) == __fold_o) ); // Translation of domain axiom _emptyFold axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap: (Map A B) :: { (hfoldApply(__fold_c, __fold_snap): B) } Set#Equal((Map#Domain(__fold_snap): Set A), (Set#Empty(): Set A)) ==> Set#Equal((Map#Domain(__fold_snap): Set A), (Set#Empty(): Set A)) && (hfoldApply(__fold_c, __fold_snap): B) == (opGetIden((getoperator(__fold_c): OperatorDomainType B)): B) ); // Translation of domain axiom _singleton axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap: (Map A B), __fold_elem: A :: { (hfoldApply(__fold_c, __fold_snap): B), (Set#Singleton(__fold_elem): Set A) } Set#Equal((Map#Domain(__fold_snap): Set A), (Set#Singleton(__fold_elem): Set A)) ==> Set#Equal((Map#Domain(__fold_snap): Set A), (Set#Singleton(__fold_elem): Set A)) && (hfoldApply(__fold_c, __fold_snap): B) == Map#Elements(__fold_snap)[__fold_elem] ); // Translation of domain axiom _dropOne1 axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap1: (Map A B), __fold_key: A :: { (_triggerDeleteKey1((hfoldApply(__fold_c, __fold_snap1): B), __fold_key): bool) } (Map#Domain(__fold_snap1): Set A)[__fold_key] ==> (Map#Domain(__fold_snap1): Set A)[__fold_key] && (hfoldApply(__fold_c, __fold_snap1): B) == (opApply((getoperator(__fold_c): OperatorDomainType B), (hfoldApply1(__fold_c, (mapDelete(__fold_snap1, (Set#Singleton(__fold_key): Set A)): Map A B)): B), Map#Elements(__fold_snap1)[__fold_key]): B) ); // Translation of domain axiom loseMany axiom (forall __fold_c: (FoldDomainType A V B), __fold_snap1: (Map A B), __fold_keys: (Set A) :: { (_triggerDeleteBlock((hfoldApply(__fold_c, __fold_snap1): B), __fold_keys): bool) } Set#Subset(__fold_keys, (Map#Domain(__fold_snap1): Set A)) ==> Set#Subset(__fold_keys, (Map#Domain(__fold_snap1): Set A)) && (hfoldApply(__fold_c, __fold_snap1): B) == (opApply((getoperator(__fold_c): OperatorDomainType B), (hfoldApply1(__fold_c, (mapDelete(__fold_snap1, __fold_keys): Map A B)): B), (hfoldApply1(__fold_c, (mapSubmap(__fold_snap1, __fold_keys): Map A B)): B)): B) ); // ================================================== // Translation of domain Receiver // ================================================== // The type for domain Receiver type ReceiverDomainType A; // Translation of domain function recApply function recApply(r_1: (ReceiverDomainType A), a_2: A): Ref; // Translation of domain function recInv function recInv(rec: (ReceiverDomainType A), ref: Ref): A; // Translation of domain function filterReceiverGood function filterReceiverGood(f_7: (Set A), r_1: (ReceiverDomainType A)): bool; // Translation of domain function filterNotLost function filterNotLost(f1: (Set A), r_1: (ReceiverDomainType A), lostR: (Set Ref)): Set A; // Translation of domain axiom _inverse_receiver axiom (forall __fold_a: A, __fold_f: (Set A), __fold_r: (ReceiverDomainType A) :: { (recApply(__fold_r, __fold_a): Ref), (filterReceiverGood(__fold_f, __fold_r): bool) } { (filterReceiverGood(__fold_f, __fold_r): bool), __fold_f[__fold_a] } (filterReceiverGood(__fold_f, __fold_r): bool) && __fold_f[__fold_a] ==> (filterReceiverGood(__fold_f, __fold_r): bool) && (__fold_f[__fold_a] && (recInv(__fold_r, (recApply(__fold_r, __fold_a): Ref)): A) == __fold_a) ); // Translation of domain axiom _inverse_receiver1 axiom (forall __fold_ref: Ref, __fold_f: (Set A), __fold_r: (ReceiverDomainType A) :: { (filterReceiverGood(__fold_f, __fold_r): bool), (recInv(__fold_r, __fold_ref): A) } (filterReceiverGood(__fold_f, __fold_r): bool) && __fold_f[(recInv(__fold_r, __fold_ref): A)] ==> (filterReceiverGood(__fold_f, __fold_r): bool) && (__fold_f[(recInv(__fold_r, __fold_ref): A)] && (recApply(__fold_r, (recInv(__fold_r, __fold_ref): A)): Ref) == __fold_ref) ); // Translation of domain axiom smallerF axiom (forall __fold_f1: (Set A), __fold_f2: (Set A), __fold_r: (ReceiverDomainType A) :: { Set#Subset(__fold_f2, __fold_f1), (filterReceiverGood(__fold_f1, __fold_r): bool) } (filterReceiverGood(__fold_f1, __fold_r): bool) && Set#Subset(__fold_f2, __fold_f1) ==> (filterReceiverGood(__fold_f1, __fold_r): bool) && (Set#Subset(__fold_f2, __fold_f1) && (filterReceiverGood(__fold_f2, __fold_r): bool)) ); // Translation of domain axiom smallerFDelete axiom (forall __fold_f1: (Set A), __fold_f2: (Set A), __fold_r: (ReceiverDomainType A) :: { (filterReceiverGood(__fold_f1, __fold_r): bool), (Set#Difference(__fold_f1, __fold_f2): Set A) } (filterReceiverGood(__fold_f1, __fold_r): bool) ==> (filterReceiverGood(__fold_f1, __fold_r): bool) && (filterReceiverGood((Set#Difference(__fold_f1, __fold_f2): Set A), __fold_r): bool) ); // Translation of domain axiom unionF axiom (forall __fold_f1: (Set A), __fold_f2: (Set A), __fold_r: (ReceiverDomainType A) :: { (filterReceiverGood((Set#Union(__fold_f1, __fold_f2): Set A), __fold_r): bool) } (filterReceiverGood((Set#Union(__fold_f1, __fold_f2): Set A), __fold_r): bool) ==> (filterReceiverGood((Set#Union(__fold_f1, __fold_f2): Set A), __fold_r): bool) && ((filterReceiverGood(__fold_f1, __fold_r): bool) && (filterReceiverGood(__fold_f2, __fold_r): bool)) ); // Translation of domain axiom _filterNotLostAxiom axiom (forall __fold_a: A, __fold_fs: (Set A), __fold_r: (ReceiverDomainType A), __fold_lostR: (Set Ref) :: { (filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set A)[__fold_a] } (filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set A)[__fold_a] == (__fold_fs[__fold_a] && !__fold_lostR[(recApply(__fold_r, __fold_a): Ref)]) ); // Translation of domain axiom _filterNotLostSubset axiom (forall __fold_fs: (Set A), __fold_r: (ReceiverDomainType A), __fold_lostR: (Set Ref) :: { (filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set A) } Set#Subset((filterNotLost(__fold_fs, __fold_r, __fold_lostR): Set A), __fold_fs) ); // ================================================== // Translation of domain Operator // ================================================== // The type for domain Operator type OperatorDomainType B; // Translation of domain function _noTrigOp function _noTrigOp(out: B): bool; // Translation of domain function opApply function opApply(op: (OperatorDomainType B), val1: B, val2: B): B; // Translation of domain function opGetIden function opGetIden(op: (OperatorDomainType B)): B; // ================================================== // Translation of domain Mapping // ================================================== // The type for domain Mapping type MappingDomainType V B; // Translation of domain function mapApply function mapApply(m: (MappingDomainType V B), _mInput: V): B; // Translation of domain function mapIdentity function mapIdentity(): MappingDomainType V V; // Translation of anonymous domain axiom axiom (forall __v: V :: { (mapApply((mapIdentity(): MappingDomainType V V), __v): V) } (mapApply((mapIdentity(): MappingDomainType V V), __v): V) == __v ); // ================================================== // Translation of domain MapEdit // ================================================== // The type for domain MapEdit type MapEditDomainType A B; // Translation of domain function mapDelete function mapDelete(m: (Map A B), e: (Set A)): Map A B; // Translation of domain function mapSubmap function mapSubmap(m: (Map A B), es: (Set A)): Map A B; // Translation of domain function disjUnionEq function disjUnionEq(s1: (Set A), s2: (Set A), s3: (Set A)): bool; // Translation of domain axiom disjUnionEqDef axiom (forall __fold_s1: (Set A), __fold_s2: (Set A), __fold_s3: (Set A) :: { (disjUnionEq(__fold_s1, __fold_s2, __fold_s3): bool) } (disjUnionEq(__fold_s1, __fold_s2, __fold_s3): bool) == (Set#Equal((Set#Intersection(__fold_s1, __fold_s2): Set A), (Set#Empty(): Set A)) && Set#Equal((Set#Union(__fold_s1, __fold_s2): Set A), __fold_s3)) ); // ================================================== // Translation of domain setFunc // ================================================== // The type for domain setFunc type setFuncDomainType A; // Translation of domain axiom setminusAssoc axiom (forall __fold_s1: (Set A), __fold_s2: (Set A), __fold_s3: (Set A) :: { (Set#Difference((Set#Difference(__fold_s1, __fold_s2): Set A), __fold_s3): Set A) } Set#Equal((Set#Difference((Set#Difference(__fold_s1, __fold_s2): Set A), __fold_s3): Set A), (Set#Difference((Set#Difference(__fold_s1, __fold_s3): Set A), __fold_s2): Set A)) ); // Translation of domain axiom setminusRepeated axiom (forall __fold_s1: (Set A), __fold_s2: (Set A) :: { (Set#Difference((Set#Difference(__fold_s1, __fold_s2): Set A), __fold_s2): Set A) } Set#Equal((Set#Difference((Set#Difference(__fold_s1, __fold_s2): Set A), __fold_s2): Set A), (Set#Difference(__fold_s1, __fold_s2): Set A)) ); // Translation of domain axiom _emptySubset axiom (forall __fold_s1: (Set A), __fold_s2: (Set A) :: { Set#Subset(__fold_s2, __fold_s1) } Set#Equal(__fold_s1, (Set#Empty(): Set A)) ==> Set#Subset(__fold_s2, __fold_s1) == Set#Equal(__fold_s2, (Set#Empty(): Set A)) ); // ================================================== // Translation of domain ___arrayRec_Receiver_Domain // ================================================== // The type for domain ___arrayRec_Receiver_Domain type ___arrayRec_Receiver_DomainDomainType; // Translation of domain function arrayRec function arrayRec(a_2: ArrayDomainType): ReceiverDomainType int; // Translation of anonymous domain axiom axiom (forall a_3: ArrayDomainType, i_1: int :: { (recApply((arrayRec(a_3): ReceiverDomainType int), i_1): Ref) } { (loc(a_3, i_1): Ref) } (recApply((arrayRec(a_3): ReceiverDomainType int), i_1): Ref) == (loc(a_3, i_1): Ref) ); // ================================================== // Translation of domain ___allInt_Filter_Domain // ================================================== // The type for domain ___allInt_Filter_Domain type ___allInt_Filter_DomainDomainType; // Translation of domain function allInt function allInt(start: int, end: int): Set int; // Translation of anonymous domain axiom axiom (forall start_1: int, end_1: int, i_1: int :: { (allInt(start_1, end_1): Set int)[i_1] } (allInt(start_1, end_1): Set int)[i_1] == (i_1 >= start_1 && i_1 < end_1) ); // ================================================== // Translation of domain ___add_Operator_Domain // ================================================== // The type for domain ___add_Operator_Domain type ___add_Operator_DomainDomainType; // Translation of domain function add function add(): OperatorDomainType int; // Translation of anonymous domain axiom axiom (forall a_3: int, b_2: int :: { (opApply((add(): OperatorDomainType int), a_3, b_2): int) } (opApply((add(): OperatorDomainType int), a_3, b_2): int) == a_3 + b_2 ); // Translation of anonymous domain axiom axiom (opGetIden((add(): OperatorDomainType int)): int) == 0; // ================================================== // Translation of all fields // ================================================== const unique val: Field NormalField int; axiom !IsPredicateField(val); axiom !IsWandField(val); // ================================================== // Translation of function __snap_Int_Int_Int_val // ================================================== // Uninterpreted function definitions function __snap_Int_Int_Int_val(Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int; function __snap_Int_Int_Int_val'(Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int; axiom (forall Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { __snap_Int_Int_Int_val(Heap, c_1, f_8) } __snap_Int_Int_Int_val(Heap, c_1, f_8) == __snap_Int_Int_Int_val'(Heap, c_1, f_8) && dummyFunction(__snap_Int_Int_Int_val#triggerStateless(c_1, f_8)) ); axiom (forall Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { __snap_Int_Int_Int_val'(Heap, c_1, f_8) } dummyFunction(__snap_Int_Int_Int_val#triggerStateless(c_1, f_8)) ); // Framing axioms function __snap_Int_Int_Int_val#frame(frame: FrameType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int; axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) ==> __snap_Int_Int_Int_val'(Heap, c_1, f_8) == __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8) ); // ================================================== // Function used for framing of quantified permission (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10)) in function __snap_Int_Int_Int_val // ================================================== function __snap_Int_Int_Int_val#condqp1(Heap: HeapType, c_1_1: (FoldDomainType int int int), f_1_1: (Set int)): int; axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { __snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8), succHeapTrans(Heap2Heap, Heap1Heap) } (forall __ind: int :: (f_8[__ind] && NoPerm < 1 / 10 <==> f_8[__ind] && NoPerm < 1 / 10) && (f_8[__ind] && NoPerm < 1 / 10 ==> Heap2Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind): Ref), val] == Heap1Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind): Ref), val]) ) ==> __snap_Int_Int_Int_val#condqp1(Heap2Heap, c_1, f_8) == __snap_Int_Int_Int_val#condqp1(Heap1Heap, c_1, f_8) ); // Postcondition axioms axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) ); axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> Set#Equal(Map#Domain(__snap_Int_Int_Int_val'(Heap, c_1, f_8)), f_8) ); axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> (forall __ind_2: int :: { Map#Elements(__snap_Int_Int_Int_val'(Heap, c_1, f_8))[__ind_2] } f_8[__ind_2] ==> Map#Elements(__snap_Int_Int_Int_val'(Heap, c_1, f_8))[__ind_2] == (mapApply((getmapping(c_1): MappingDomainType int int), Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_2): Ref), val]): int) ) ); axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> (forall __s: (Set int) :: { (mapDelete(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __s): Map int int) } !Set#Equal(__s, (Set#Empty(): Set int)) ==> Map#Equal(__snap_Int_Int_Int_val_prime(Heap, c_1, Set#Difference(f_8, __s)), (mapDelete(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __s): Map int int)) ) ); axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> (forall __s_1: (Set int) :: { (mapSubmap(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __s_1): Map int int) } Set#Subset(__s_1, f_8) && !Set#Equal(__s_1, f_8) ==> Set#Subset(__s_1, f_8) && (!Set#Equal(__s_1, f_8) && Map#Equal(__snap_Int_Int_Int_val_prime(Heap, c_1, __s_1), (mapSubmap(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __s_1): Map int int))) ) ); axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> (forall __s1: (Set int), __s2: (Set int) :: { (disjUnionEq(__s1, __s2, f_8): bool) } (disjUnionEq(__s1, __s2, f_8): bool) ==> (disjUnionEq(__s1, __s2, f_8): bool) && (hfoldApply1(c_1, __snap_Int_Int_Int_val'(Heap, c_1, f_8)): int) == (opApply((getoperator(c_1): OperatorDomainType int), (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime(Heap, c_1, __s1)): int), (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime(Heap, c_1, __s2)): int)): int) ) ); axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> (forall __s_2: (Set int) :: { (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime#frame(FrameFragment(__snap_Int_Int_Int_val_prime#condqp2(Heap, c_1, __s_2)), c_1, __s_2)): int) } (dummy1(Set#Equal(__s_2, f_8)): bool) ) ); axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> Map#Equal(__snap_Int_Int_Int_val'(Heap, c_1, f_8), __snap_Int_Int_Int_val_prime(Heap, c_1, f_8)) ); axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 0 || __snap_Int_Int_Int_val#trigger(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { f_8[__ind1], f_8[__ind2] } f_8[__ind1] && (f_8[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2): Ref) ) ==> (getSnapFieldID(__snap_Int_Int_Int_val'(Heap, c_1, f_8)): int) == 0 ); // Trigger function (controlling recursive postconditions) function __snap_Int_Int_Int_val#trigger(frame: FrameType, c_1: (FoldDomainType int int int), f_8: (Set int)): bool; // State-independent trigger function function __snap_Int_Int_Int_val#triggerStateless(c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int; // Check contract well-formedness and postcondition procedure __snap_Int_Int_Int_val#definedness(c_1: (FoldDomainType int int int), f_8: (Set int)) returns (Result: (Map int int)) modifies Heap, Mask; { var QPMask: MaskType; var __ind_1: int; var __s_3: (Set int); var ExhaleWellDef0Mask: MaskType; var ExhaleWellDef0Heap: HeapType; var ExhaleHeap: HeapType; var __s_5: (Set int); var __s1_1: (Set int); var __s2_1: (Set int); // -- Initializing the state Mask := ZeroMask; assume state(Heap, Mask); assume AssumeFunctionsAbove == 0; // -- Inhaling precondition (with checking) // -- Do welldefinedness check of the exhale part. if (*) { // -- Check definedness of (filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in f), (__ind2 in f) } (__ind1 in f) && ((__ind2 in f) && __ind1 != __ind2) ==> (recApply((getreceiver(c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(c): Receiver[Int]), __ind2): Ref)) if (!(filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool)) { if (*) { assume false; } } assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) || (forall __ind1_2: int, __ind2_2: int :: { f_8[__ind1_2], f_8[__ind2_2] } f_8[__ind1_2] && (f_8[__ind2_2] && __ind1_2 != __ind2_2) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind1_2): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind2_2): Ref) ); assume state(Heap, Mask); // -- Check definedness of (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10)) if (*) { assume false; } havoc QPMask; assert {:msg " Contract might not be well-formed. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@294.13--298.10) [506]"} (forall __ind_4: int, __ind_4_1: int :: (((__ind_4 != __ind_4_1 && f_8[__ind_4]) && f_8[__ind_4_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4_1): Ref) ); // -- Define Inverse Function assume (forall __ind_4: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) } { f_8[__ind_4] } f_8[__ind_4] && NoPerm < 1 / 10 ==> qpRange1((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref)) && invRecv1((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref)) == __ind_4 ); assume (forall o_3: Ref :: { invRecv1(o_3) } (f_8[invRecv1(o_3)] && NoPerm < 1 / 10) && qpRange1(o_3) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv1(o_3)): Ref) == o_3 ); // Check that permission expression is non-negative for all fields assert {:msg " Contract might not be well-formed. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@294.13--298.10) [507]"} (forall __ind_4: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) } { f_8[__ind_4] } f_8[__ind_4] ==> 1 / 10 >= NoPerm ); // -- Assume set of fields is nonNull assume (forall __ind_4: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) } { f_8[__ind_4] } f_8[__ind_4] && 1 / 10 > NoPerm ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_4): Ref) != null ); // -- Define permissions assume (forall o_3: Ref :: { QPMask[o_3, val] } ((f_8[invRecv1(o_3)] && NoPerm < 1 / 10) && qpRange1(o_3) ==> (NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv1(o_3)): Ref) == o_3) && QPMask[o_3, val] == Mask[o_3, val] + 1 / 10) && (!((f_8[invRecv1(o_3)] && NoPerm < 1 / 10) && qpRange1(o_3)) ==> QPMask[o_3, val] == Mask[o_3, val]) ); assume (forall o_3: Ref, f_5: (Field A B) :: { Mask[o_3, f_5] } { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; assume state(Heap, Mask); assume state(Heap, Mask); assume false; } // -- Normally inhale the inhale part. assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool); assume state(Heap, Mask); // -- Check definedness of (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10)) if (*) { assume false; } havoc QPMask; assert {:msg " Contract might not be well-formed. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@294.13--298.10) [508]"} (forall __ind_6: int, __ind_6_1: int :: (((__ind_6 != __ind_6_1 && f_8[__ind_6]) && f_8[__ind_6_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6_1): Ref) ); // -- Define Inverse Function assume (forall __ind_6: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) } { f_8[__ind_6] } f_8[__ind_6] && NoPerm < 1 / 10 ==> qpRange2((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref)) && invRecv2((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref)) == __ind_6 ); assume (forall o_3: Ref :: { invRecv2(o_3) } (f_8[invRecv2(o_3)] && NoPerm < 1 / 10) && qpRange2(o_3) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv2(o_3)): Ref) == o_3 ); // Check that permission expression is non-negative for all fields assert {:msg " Contract might not be well-formed. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@294.13--298.10) [509]"} (forall __ind_6: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) } { f_8[__ind_6] } f_8[__ind_6] ==> 1 / 10 >= NoPerm ); // -- Assume set of fields is nonNull assume (forall __ind_6: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) } { f_8[__ind_6] } f_8[__ind_6] && 1 / 10 > NoPerm ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_6): Ref) != null ); // -- Define permissions assume (forall o_3: Ref :: { QPMask[o_3, val] } ((f_8[invRecv2(o_3)] && NoPerm < 1 / 10) && qpRange2(o_3) ==> (NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv2(o_3)): Ref) == o_3) && QPMask[o_3, val] == Mask[o_3, val] + 1 / 10) && (!((f_8[invRecv2(o_3)] && NoPerm < 1 / 10) && qpRange2(o_3)) ==> QPMask[o_3, val] == Mask[o_3, val]) ); assume (forall o_3: Ref, f_5: (Field A B) :: { Mask[o_3, f_5] } { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; assume state(Heap, Mask); assume state(Heap, Mask); // -- Checking definedness of postcondition (no body) assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool); assume state(Heap, Mask); assume Set#Equal(Map#Domain(Result), f_8); assume state(Heap, Mask); // -- Check definedness of (forall __ind: Int :: { result[__ind] } (__ind in f) ==> result[__ind] == (mapApply((getmapping(c): Mapping[Int, Int]), (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val): Int)) if (*) { if (f_8[__ind_1]) { assert {:msg " Contract might not be well-formed. Map result might not contain an entry at key __ind. (arrayTestChainIrrel3.vpr@301.12--306.30) [510]"} Map#Domain(Result)[__ind_1]; assert {:msg " Contract might not be well-formed. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@301.12--306.30) [511]"} HasDirectPerm(Mask, (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_1): Ref), val); } assume false; } assume (forall __ind_8: int :: { Map#Elements(Result)[__ind_8] } f_8[__ind_8] ==> Map#Elements(Result)[__ind_8] == (mapApply((getmapping(c_1): MappingDomainType int int), Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_8): Ref), val]): int) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Check definedness of (forall __s: Set[Int] :: { (mapDelete(result, __s): Map[Int,Int]) } __s != Set[Int]() ==> __snap_Int_Int_Int_val_prime(c, (f setminus __s)) == (mapDelete(result, __s): Map[Int,Int])) if (*) { if (!Set#Equal(__s_3, (Set#Empty(): Set int))) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood((f setminus __s), (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@310.7--310.56) [512]"} (filterReceiverGood(Set#Difference(f_8, __s_3), (getreceiver(c_1): ReceiverDomainType int)): bool); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@310.7--310.56) [513]"} (forall __ind_9: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref) } { Set#Difference(f_8, __s_3)[__ind_9] } Set#Difference(f_8, __s_3)[__ind_9] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@310.7--310.56) [514]"} (forall __ind_9: int, __ind_9_1: int :: { neverTriggered3(__ind_9), neverTriggered3(__ind_9_1) } (((__ind_9 != __ind_9_1 && Set#Difference(f_8, __s_3)[__ind_9]) && Set#Difference(f_8, __s_3)[__ind_9_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@310.7--310.56) [515]"} (forall __ind_9: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref) } { Set#Difference(f_8, __s_3)[__ind_9] } Set#Difference(f_8, __s_3)[__ind_9] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) assume (forall __ind_9: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref) } { Set#Difference(f_8, __s_3)[__ind_9] } Set#Difference(f_8, __s_3)[__ind_9] && NoPerm < 1 / 10 ==> qpRange3((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref)) && invRecv3((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_9): Ref)) == __ind_9 ); assume (forall o_3: Ref :: { invRecv3(o_3) } Set#Difference(f_8, __s_3)[invRecv3(o_3)] && (NoPerm < 1 / 10 && qpRange3(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv3(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (Set#Difference(f_8, __s_3)[invRecv3(o_3)] && (NoPerm < 1 / 10 && qpRange3(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv3(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(Set#Difference(f_8, __s_3)[invRecv3(o_3)] && (NoPerm < 1 / 10 && qpRange3(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } } assume false; } assume (forall __s_4: (Set int) :: { (mapDelete(Result, __s_4): Map int int) } !Set#Equal(__s_4, (Set#Empty(): Set int)) ==> Map#Equal(__snap_Int_Int_Int_val_prime(Heap, c_1, Set#Difference(f_8, __s_4)), (mapDelete(Result, __s_4): Map int int)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Check definedness of (forall __s: Set[Int] :: { (mapSubmap(result, __s): Map[Int,Int]) } (__s subset f) && __s != f ==> (__s subset f) && (__s != f && __snap_Int_Int_Int_val_prime(c, __s) == (mapSubmap(result, __s): Map[Int,Int]))) if (*) { if (Set#Subset(__s_5, f_8) && !Set#Equal(__s_5, f_8)) { if (Set#Subset(__s_5, f_8)) { if (!Set#Equal(__s_5, f_8)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood(__s, (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@317.7--317.43) [516]"} (filterReceiverGood(__s_5, (getreceiver(c_1): ReceiverDomainType int)): bool); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@317.7--317.43) [517]"} (forall __ind_10: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref) } { __s_5[__ind_10] } __s_5[__ind_10] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@317.7--317.43) [518]"} (forall __ind_10: int, __ind_10_1: int :: { neverTriggered4(__ind_10), neverTriggered4(__ind_10_1) } (((__ind_10 != __ind_10_1 && __s_5[__ind_10]) && __s_5[__ind_10_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@317.7--317.43) [519]"} (forall __ind_10: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref) } { __s_5[__ind_10] } __s_5[__ind_10] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) assume (forall __ind_10: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref) } { __s_5[__ind_10] } __s_5[__ind_10] && NoPerm < 1 / 10 ==> qpRange4((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref)) && invRecv4((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_10): Ref)) == __ind_10 ); assume (forall o_3: Ref :: { invRecv4(o_3) } __s_5[invRecv4(o_3)] && (NoPerm < 1 / 10 && qpRange4(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv4(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__s_5[invRecv4(o_3)] && (NoPerm < 1 / 10 && qpRange4(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv4(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__s_5[invRecv4(o_3)] && (NoPerm < 1 / 10 && qpRange4(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __s_6: (Set int) :: { (mapSubmap(Result, __s_6): Map int int) } Set#Subset(__s_6, f_8) && !Set#Equal(__s_6, f_8) ==> Set#Subset(__s_6, f_8) && (!Set#Equal(__s_6, f_8) && Map#Equal(__snap_Int_Int_Int_val_prime(Heap, c_1, __s_6), (mapSubmap(Result, __s_6): Map int int))) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Check definedness of (forall __s1: Set[Int], __s2: Set[Int] :: { (disjUnionEq(__s1, __s2, f): Bool) } (disjUnionEq(__s1, __s2, f): Bool) ==> (disjUnionEq(__s1, __s2, f): Bool) && (hfoldApply1(c, result): Int) == (opApply((getoperator(c): Operator[Int]), (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c, __s1)): Int), (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c, __s2)): Int)): Int)) if (*) { if ((disjUnionEq(__s1_1, __s2_1, f_8): bool)) { if ((disjUnionEq(__s1_1, __s2_1, f_8): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood(__s1, (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@324.65--325.12) [520]"} (filterReceiverGood(__s1_1, (getreceiver(c_1): ReceiverDomainType int)): bool); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@324.65--325.12) [521]"} (forall __ind_11: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref) } { __s1_1[__ind_11] } __s1_1[__ind_11] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@324.65--325.12) [522]"} (forall __ind_11: int, __ind_11_1: int :: { neverTriggered5(__ind_11), neverTriggered5(__ind_11_1) } (((__ind_11 != __ind_11_1 && __s1_1[__ind_11]) && __s1_1[__ind_11_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@324.65--325.12) [523]"} (forall __ind_11: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref) } { __s1_1[__ind_11] } __s1_1[__ind_11] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) assume (forall __ind_11: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref) } { __s1_1[__ind_11] } __s1_1[__ind_11] && NoPerm < 1 / 10 ==> qpRange5((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref)) && invRecv5((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_11): Ref)) == __ind_11 ); assume (forall o_3: Ref :: { invRecv5(o_3) } __s1_1[invRecv5(o_3)] && (NoPerm < 1 / 10 && qpRange5(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv5(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__s1_1[invRecv5(o_3)] && (NoPerm < 1 / 10 && qpRange5(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv5(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__s1_1[invRecv5(o_3)] && (NoPerm < 1 / 10 && qpRange5(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood(__s2, (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@325.37--325.74) [524]"} (filterReceiverGood(__s2_1, (getreceiver(c_1): ReceiverDomainType int)): bool); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@325.37--325.74) [525]"} (forall __ind_12: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref) } { __s2_1[__ind_12] } __s2_1[__ind_12] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@325.37--325.74) [526]"} (forall __ind_12: int, __ind_12_1: int :: { neverTriggered6(__ind_12), neverTriggered6(__ind_12_1) } (((__ind_12 != __ind_12_1 && __s2_1[__ind_12]) && __s2_1[__ind_12_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@325.37--325.74) [527]"} (forall __ind_12: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref) } { __s2_1[__ind_12] } __s2_1[__ind_12] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) assume (forall __ind_12: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref) } { __s2_1[__ind_12] } __s2_1[__ind_12] && NoPerm < 1 / 10 ==> qpRange6((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref)) && invRecv6((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_12): Ref)) == __ind_12 ); assume (forall o_3: Ref :: { invRecv6(o_3) } __s2_1[invRecv6(o_3)] && (NoPerm < 1 / 10 && qpRange6(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv6(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__s2_1[invRecv6(o_3)] && (NoPerm < 1 / 10 && qpRange6(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv6(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__s2_1[invRecv6(o_3)] && (NoPerm < 1 / 10 && qpRange6(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } } } assume false; } assume (forall __s1_2: (Set int), __s2_2: (Set int) :: { (disjUnionEq(__s1_2, __s2_2, f_8): bool) } (disjUnionEq(__s1_2, __s2_2, f_8): bool) ==> (disjUnionEq(__s1_2, __s2_2, f_8): bool) && (hfoldApply1(c_1, Result): int) == (opApply((getoperator(c_1): OperatorDomainType int), (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime(Heap, c_1, __s1_2)): int), (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime(Heap, c_1, __s2_2)): int)): int) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Check definedness of (forall __s: Set[Int] :: { (hfoldApply1(c, __snap_Int_Int_Int_val_prime(c, __s)): Int) } (dummy1(__s == f): Bool)) if (*) { assume false; } assume (forall __s_8: (Set int) :: { (hfoldApply1(c_1, __snap_Int_Int_Int_val_prime#frame(FrameFragment(__snap_Int_Int_Int_val_prime#condqp2(Heap, c_1, __s_8)), c_1, __s_8)): int) } (dummy1(Set#Equal(__s_8, f_8)): bool) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Check definedness of result == __snap_Int_Int_Int_val_prime(c, f) if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Assertion (filterReceiverGood(f, (getreceiver(c): Receiver[Int])): Bool) might not hold. (arrayTestChainIrrel3.vpr@329.21--329.55) [528]"} (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@329.21--329.55) [529]"} (forall __ind_13: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref) } { f_8[__ind_13] } f_8[__ind_13] && dummyFunction(Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@329.21--329.55) [530]"} (forall __ind_13: int, __ind_13_1: int :: { neverTriggered7(__ind_13), neverTriggered7(__ind_13_1) } (((__ind_13 != __ind_13_1 && f_8[__ind_13]) && f_8[__ind_13_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val_prime might not hold. There might be insufficient permission to access (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@329.21--329.55) [531]"} (forall __ind_13: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref) } { f_8[__ind_13] } f_8[__ind_13] ==> Mask[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(c): Receiver[Int]), __ind): Ref) assume (forall __ind_13: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref) } { f_8[__ind_13] } f_8[__ind_13] && NoPerm < 1 / 10 ==> qpRange7((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref)) && invRecv7((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_13): Ref)) == __ind_13 ); assume (forall o_3: Ref :: { invRecv7(o_3) } f_8[invRecv7(o_3)] && (NoPerm < 1 / 10 && qpRange7(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv7(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (f_8[invRecv7(o_3)] && (NoPerm < 1 / 10 && qpRange7(o_3)) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv7(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(f_8[invRecv7(o_3)] && (NoPerm < 1 / 10 && qpRange7(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } assume Map#Equal(Result, __snap_Int_Int_Int_val_prime(Heap, c_1, f_8)); assume state(Heap, Mask); assume (getSnapFieldID(Result): int) == 0; assume state(Heap, Mask); } // ================================================== // Translation of function __snap_Int_Int_Int_val_prime // ================================================== // Uninterpreted function definitions function __snap_Int_Int_Int_val_prime(Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int; function __snap_Int_Int_Int_val_prime'(Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int; axiom (forall Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { __snap_Int_Int_Int_val_prime(Heap, c_1, f_8) } __snap_Int_Int_Int_val_prime(Heap, c_1, f_8) == __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) && dummyFunction(__snap_Int_Int_Int_val_prime#triggerStateless(c_1, f_8)) ); axiom (forall Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) } dummyFunction(__snap_Int_Int_Int_val_prime#triggerStateless(c_1, f_8)) ); // Framing axioms function __snap_Int_Int_Int_val_prime#frame(frame: FrameType, c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int; axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) } state(Heap, Mask) ==> __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) == __snap_Int_Int_Int_val_prime#frame(FrameFragment(__snap_Int_Int_Int_val_prime#condqp2(Heap, c_1, f_8)), c_1, f_8) ); // ================================================== // Function used for framing of quantified permission (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10)) in function __snap_Int_Int_Int_val_prime // ================================================== function __snap_Int_Int_Int_val_prime#condqp2(Heap: HeapType, c_2_1: (FoldDomainType int int int), f_2_1: (Set int)): int; axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { __snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8), __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8), succHeapTrans(Heap2Heap, Heap1Heap) } (forall __ind: int :: (f_8[__ind] && NoPerm < 1 / 10 <==> f_8[__ind] && NoPerm < 1 / 10) && (f_8[__ind] && NoPerm < 1 / 10 ==> Heap2Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind): Ref), val] == Heap1Heap[(recApply((getreceiver(c_1): ReceiverDomainType int), __ind): Ref), val]) ) ==> __snap_Int_Int_Int_val_prime#condqp2(Heap2Heap, c_1, f_8) == __snap_Int_Int_Int_val_prime#condqp2(Heap1Heap, c_1, f_8) ); // Postcondition axioms axiom (forall Heap: HeapType, Mask: MaskType, c_1: (FoldDomainType int int int), f_8: (Set int) :: { state(Heap, Mask), __snap_Int_Int_Int_val_prime'(Heap, c_1, f_8) } state(Heap, Mask) && (AssumeFunctionsAbove < 1 || __snap_Int_Int_Int_val_prime#trigger(FrameFragment(__snap_Int_Int_Int_val_prime#condqp2(Heap, c_1, f_8)), c_1, f_8)) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) ==> (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool) ); // Trigger function (controlling recursive postconditions) function __snap_Int_Int_Int_val_prime#trigger(frame: FrameType, c_1: (FoldDomainType int int int), f_8: (Set int)): bool; // State-independent trigger function function __snap_Int_Int_Int_val_prime#triggerStateless(c_1: (FoldDomainType int int int), f_8: (Set int)): Map int int; // Check contract well-formedness and postcondition procedure __snap_Int_Int_Int_val_prime#definedness(c_1: (FoldDomainType int int int), f_8: (Set int)) returns (Result: (Map int int)) modifies Heap, Mask; { var QPMask: MaskType; // -- Initializing the state Mask := ZeroMask; assume state(Heap, Mask); assume AssumeFunctionsAbove == 1; // -- Inhaling precondition (with checking) assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool); assume state(Heap, Mask); // -- Check definedness of (forall __ind: Int :: { (__ind in f) } (__ind in f) ==> acc((recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val, 1 / 10)) if (*) { assume false; } havoc QPMask; assert {:msg " Contract might not be well-formed. Quantified resource (recApply((getreceiver(c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@335.13--339.10) [532]"} (forall __ind_3: int, __ind_3_1: int :: (((__ind_3 != __ind_3_1 && f_8[__ind_3]) && f_8[__ind_3_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) != (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3_1): Ref) ); // -- Define Inverse Function assume (forall __ind_3: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) } { f_8[__ind_3] } f_8[__ind_3] && NoPerm < 1 / 10 ==> qpRange8((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref)) && invRecv8((recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref)) == __ind_3 ); assume (forall o_3: Ref :: { invRecv8(o_3) } (f_8[invRecv8(o_3)] && NoPerm < 1 / 10) && qpRange8(o_3) ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv8(o_3)): Ref) == o_3 ); // Check that permission expression is non-negative for all fields assert {:msg " Contract might not be well-formed. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@335.13--339.10) [533]"} (forall __ind_3: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) } { f_8[__ind_3] } f_8[__ind_3] ==> 1 / 10 >= NoPerm ); // -- Assume set of fields is nonNull assume (forall __ind_3: int :: { (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) } { f_8[__ind_3] } f_8[__ind_3] && 1 / 10 > NoPerm ==> (recApply((getreceiver(c_1): ReceiverDomainType int), __ind_3): Ref) != null ); // -- Define permissions assume (forall o_3: Ref :: { QPMask[o_3, val] } ((f_8[invRecv8(o_3)] && NoPerm < 1 / 10) && qpRange8(o_3) ==> (NoPerm < 1 / 10 ==> (recApply((getreceiver(c_1): ReceiverDomainType int), invRecv8(o_3)): Ref) == o_3) && QPMask[o_3, val] == Mask[o_3, val] + 1 / 10) && (!((f_8[invRecv8(o_3)] && NoPerm < 1 / 10) && qpRange8(o_3)) ==> QPMask[o_3, val] == Mask[o_3, val]) ); assume (forall o_3: Ref, f_5: (Field A B) :: { Mask[o_3, f_5] } { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; assume state(Heap, Mask); assume state(Heap, Mask); // -- Checking definedness of postcondition (no body) assume (filterReceiverGood(f_8, (getreceiver(c_1): ReceiverDomainType int)): bool); assume state(Heap, Mask); } // ================================================== // Translation of method operator_add_welldef_check // ================================================== procedure operator_add_welldef_check() returns () modifies Heap, Mask; { var oldMask: MaskType; var oldHeap: HeapType; var ExhaleWellDef0Mask: MaskType; var ExhaleWellDef0Heap: HeapType; var _i1_1: int; var _i2_1: int; var _i1_4: int; var _i2_4: int; var _i3_1: int; var _i1_7: int; // -- Initializing the state Mask := ZeroMask; assume state(Heap, Mask); assume AssumeFunctionsAbove == -1; // -- Initializing of old state // -- Initializing the old state oldMask := Mask; oldHeap := Heap; // -- Translating statement: assert (forall _i1: Int, _i2: Int :: // { (_noTrigOp((opApply(add(), _i1, _i2): Int)): Bool) } // (opApply(add(), _i1, _i2): Int) == (opApply(add(), _i2, _i1): Int)) -- arrayTestChainIrrel3.vpr@345.3--348.56 ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; // -- Check definedness of (forall _i1: Int, _i2: Int :: { (_noTrigOp((opApply(add(), _i1, _i2): Int)): Bool) } (opApply(add(), _i1, _i2): Int) == (opApply(add(), _i2, _i1): Int)) if (*) { assume false; } if (*) { assert {:msg " Assert might fail. Assertion (opApply(add(), _i1, _i2): Int) == (opApply(add(), _i2, _i1): Int) might not hold. (arrayTestChainIrrel3.vpr@345.11--348.55) [534]"} (opApply((add(): OperatorDomainType int), _i1_1, _i2_1): int) == (opApply((add(): OperatorDomainType int), _i2_1, _i1_1): int); assume false; } assume (forall _i1_2_1: int, _i2_2_1: int :: { (_noTrigOp((opApply((add(): OperatorDomainType int), _i1_2_1, _i2_2_1): int)): bool) } (opApply((add(): OperatorDomainType int), _i1_2_1, _i2_2_1): int) == (opApply((add(): OperatorDomainType int), _i2_2_1, _i1_2_1): int) ); assume state(Heap, Mask); // -- Translating statement: assert (forall _i1: Int, _i2: Int, _i3: Int :: // { (_noTrigOp((opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int)): Bool) } // (opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int) == // (opApply(add(), _i1, (opApply(add(), _i2, _i3): Int)): Int)) -- arrayTestChainIrrel3.vpr@349.3--355.30 ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; // -- Check definedness of (forall _i1: Int, _i2: Int, _i3: Int :: { (_noTrigOp((opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int)): Bool) } (opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int) == (opApply(add(), _i1, (opApply(add(), _i2, _i3): Int)): Int)) if (*) { assume false; } if (*) { assert {:msg " Assert might fail. Assertion (opApply(add(), (opApply(add(), _i1, _i2): Int), _i3): Int) == (opApply(add(), _i1, (opApply(add(), _i2, _i3): Int)): Int) might not hold. (arrayTestChainIrrel3.vpr@349.11--355.29) [535]"} (opApply((add(): OperatorDomainType int), (opApply((add(): OperatorDomainType int), _i1_4, _i2_4): int), _i3_1): int) == (opApply((add(): OperatorDomainType int), _i1_4, (opApply((add(): OperatorDomainType int), _i2_4, _i3_1): int)): int); assume false; } assume (forall _i1_5_1: int, _i2_5_1: int, _i3_2_1: int :: { (_noTrigOp((opApply((add(): OperatorDomainType int), (opApply((add(): OperatorDomainType int), _i1_5_1, _i2_5_1): int), _i3_2_1): int)): bool) } (opApply((add(): OperatorDomainType int), (opApply((add(): OperatorDomainType int), _i1_5_1, _i2_5_1): int), _i3_2_1): int) == (opApply((add(): OperatorDomainType int), _i1_5_1, (opApply((add(): OperatorDomainType int), _i2_5_1, _i3_2_1): int)): int) ); assume state(Heap, Mask); // -- Translating statement: assert (forall _i1: Int :: // { (_noTrigOp((opApply(add(), _i1, (opGetIden(add()): Int)): Int)): Bool) } // (opApply(add(), _i1, (opGetIden(add()): Int)): Int) == _i1) -- arrayTestChainIrrel3.vpr@356.3--359.11 ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; // -- Check definedness of (forall _i1: Int :: { (_noTrigOp((opApply(add(), _i1, (opGetIden(add()): Int)): Int)): Bool) } (opApply(add(), _i1, (opGetIden(add()): Int)): Int) == _i1) if (*) { assume false; } if (*) { assert {:msg " Assert might fail. Assertion (opApply(add(), _i1, (opGetIden(add()): Int)): Int) == _i1 might not hold. (arrayTestChainIrrel3.vpr@356.11--359.10) [536]"} (opApply((add(): OperatorDomainType int), _i1_7, (opGetIden((add(): OperatorDomainType int)): int)): int) == _i1_7; assume false; } assume (forall _i1_8_1: int :: { (_noTrigOp((opApply((add(): OperatorDomainType int), _i1_8_1, (opGetIden((add(): OperatorDomainType int)): int)): int)): bool) } (opApply((add(): OperatorDomainType int), _i1_8_1, (opGetIden((add(): OperatorDomainType int)): int)): int) == _i1_8_1 ); assume state(Heap, Mask); } // ================================================== // Translation of method test1 // ================================================== procedure test1(a_3: ArrayDomainType) returns () modifies Heap, Mask; { var _compLabell6_lblGuard: bool; var _compLabell7_lblGuard: bool; var _compLabell8_lblGuard: bool; var _compLabell9_lblGuard: bool; var _compLabell0_lblGuard: bool; var _compLabell1_lblGuard: bool; var _compLabell2_lblGuard: bool; var _compLabell3_lblGuard: bool; var _compLabell4_lblGuard: bool; var _compLabell5_lblGuard: bool; var QPMask: MaskType; var oldMask: MaskType; var oldHeap: HeapType; var Label_compLabell0Mask: MaskType; var Label_compLabell0Heap: HeapType; var js: (Set int); var vis: (Set int); var j1: int; var j2: int; var j3: int; var i1: int; var i2: int; var i3: int; var i4: int; var i5: int; var i6: int; var Label_compLabell1Mask: MaskType; var Label_compLabell1Heap: HeapType; var __f: (Set int); var __c: (FoldDomainType int int int); var ExhaleWellDef0Mask: MaskType; var ExhaleWellDef0Heap: HeapType; var ExhaleHeap: HeapType; var Label_compLabell2Mask: MaskType; var Label_compLabell2Heap: HeapType; var __f_2: (Set int); var __c_2: (FoldDomainType int int int); var Label_compLabell3Mask: MaskType; var Label_compLabell3Heap: HeapType; var __f_4: (Set int); var __c_4: (FoldDomainType int int int); var Label_compLabell4Mask: MaskType; var Label_compLabell4Heap: HeapType; var __f_6: (Set int); var __c_6: (FoldDomainType int int int); var Label_compLabell5Mask: MaskType; var Label_compLabell5Heap: HeapType; var __f_8: (Set int); var __c_8: (FoldDomainType int int int); var Label_compLabell6Mask: MaskType; var Label_compLabell6Heap: HeapType; var __f_10: (Set int); var __c_10: (FoldDomainType int int int); var Label_compLabell7Mask: MaskType; var Label_compLabell7Heap: HeapType; var __f_12: (Set int); var __c_12: (FoldDomainType int int int); var Label_compLabell8Mask: MaskType; var Label_compLabell8Heap: HeapType; var __f_14: (Set int); var __c_14: (FoldDomainType int int int); var Label_compLabell9Mask: MaskType; var Label_compLabell9Heap: HeapType; var __f_16: (Set int); var __c_16: (FoldDomainType int int int); var ExhaleWellDef1Mask: MaskType; var ExhaleWellDef1Heap: HeapType; // -- Initializing the state Mask := ZeroMask; assume state(Heap, Mask); assume AssumeFunctionsAbove == -1; _compLabell6_lblGuard := false; _compLabell7_lblGuard := false; _compLabell8_lblGuard := false; _compLabell9_lblGuard := false; _compLabell0_lblGuard := false; _compLabell1_lblGuard := false; _compLabell2_lblGuard := false; _compLabell3_lblGuard := false; _compLabell4_lblGuard := false; _compLabell5_lblGuard := false; // -- Checked inhaling of precondition // -- Check definedness of (forall j: Int :: { loc(a, j) } 0 <= j && j < len(a) ==> acc(loc(a, j).val, write)) if (*) { assume false; } havoc QPMask; assert {:msg " Contract might not be well-formed. Quantified resource loc(a, j).val might not be injective. (arrayTestChainIrrel3.vpr@363.13--365.57) [537]"} (forall j_1: int, j_1_1: int :: (((j_1 != j_1_1 && (0 <= j_1 && j_1 < (len(a_3): int))) && (0 <= j_1_1 && j_1_1 < (len(a_3): int))) && NoPerm < FullPerm) && NoPerm < FullPerm ==> (loc(a_3, j_1): Ref) != (loc(a_3, j_1_1): Ref) ); // -- Define Inverse Function assume (forall j_1: int :: { (loc(a_3, j_1): Ref) } { (loc(a_3, j_1): Ref) } (0 <= j_1 && j_1 < (len(a_3): int)) && NoPerm < FullPerm ==> qpRange9((loc(a_3, j_1): Ref)) && invRecv9((loc(a_3, j_1): Ref)) == j_1 ); assume (forall o_3: Ref :: { invRecv9(o_3) } ((0 <= invRecv9(o_3) && invRecv9(o_3) < (len(a_3): int)) && NoPerm < FullPerm) && qpRange9(o_3) ==> (loc(a_3, invRecv9(o_3)): Ref) == o_3 ); // -- Assume set of fields is nonNull assume (forall j_1: int :: { (loc(a_3, j_1): Ref) } { (loc(a_3, j_1): Ref) } 0 <= j_1 && j_1 < (len(a_3): int) ==> (loc(a_3, j_1): Ref) != null ); // -- Define permissions assume (forall o_3: Ref :: { QPMask[o_3, val] } (((0 <= invRecv9(o_3) && invRecv9(o_3) < (len(a_3): int)) && NoPerm < FullPerm) && qpRange9(o_3) ==> (NoPerm < FullPerm ==> (loc(a_3, invRecv9(o_3)): Ref) == o_3) && QPMask[o_3, val] == Mask[o_3, val] + FullPerm) && (!(((0 <= invRecv9(o_3) && invRecv9(o_3) < (len(a_3): int)) && NoPerm < FullPerm) && qpRange9(o_3)) ==> QPMask[o_3, val] == Mask[o_3, val]) ); assume (forall o_3: Ref, f_5: (Field A B) :: { Mask[o_3, f_5] } { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; assume state(Heap, Mask); assume state(Heap, Mask); assume (len(a_3): int) > 10; assume state(Heap, Mask); // -- Initializing of old state // -- Initializing the old state oldMask := Mask; oldHeap := Heap; // -- Translating statement: label _compLabell0 -- arrayTestChainIrrel3.vpr@379.3--379.21 _compLabell0: Label_compLabell0Mask := Mask; Label_compLabell0Heap := Heap; _compLabell0_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (js subset allInt(0, len(a))) -- arrayTestChainIrrel3.vpr@380.3--380.39 assume Set#Subset(js, (allInt(0, (len(a_3): int)): Set int)); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (is subset allInt(0, len(a))) -- arrayTestChainIrrel3.vpr@381.3--381.39 assume Set#Subset(vis, (allInt(0, (len(a_3): int)): Set int)); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (j1 in js) -- arrayTestChainIrrel3.vpr@382.3--382.20 assume js[j1]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (j2 in js) -- arrayTestChainIrrel3.vpr@383.3--383.20 assume js[j2]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (j3 in js) -- arrayTestChainIrrel3.vpr@384.3--384.20 assume js[j3]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (i1 in is) -- arrayTestChainIrrel3.vpr@385.3--385.20 assume vis[i1]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (i2 in is) -- arrayTestChainIrrel3.vpr@386.3--386.20 assume vis[i2]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (i3 in is) -- arrayTestChainIrrel3.vpr@387.3--387.20 assume vis[i3]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (i4 in is) -- arrayTestChainIrrel3.vpr@388.3--388.20 assume vis[i4]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (i5 in is) -- arrayTestChainIrrel3.vpr@389.3--389.20 assume vis[i5]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (i6 in is) -- arrayTestChainIrrel3.vpr@390.3--390.20 assume vis[i6]; assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, i1).val := loc(a, i1).val + 1 -- arrayTestChainIrrel3.vpr@391.3--391.39 // -- Check definedness of loc(a, i1).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i1).val (arrayTestChainIrrel3.vpr@391.3--391.39) [538]"} HasDirectPerm(Mask, (loc(a_3, i1): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i1).val (arrayTestChainIrrel3.vpr@391.3--391.39) [539]"} FullPerm == Mask[(loc(a_3, i1): Ref), val]; Heap := Heap[(loc(a_3, i1): Ref), val:=Heap[(loc(a_3, i1): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell1 -- arrayTestChainIrrel3.vpr@392.3--392.21 _compLabell1: Label_compLabell1Mask := Mask; Label_compLabell1Heap := Heap; _compLabell1_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@393.3--406.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i1)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool) && (forall __ind_1_1: int :: { __f[__ind_1_1] } __f[__ind_1_1] ==> NoPerm < Mask[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_1_1): Ref), val] )) { if ((filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@403.45--403.77) [540]"} (filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool) || (forall __ind1: int, __ind2: int :: { __f[__ind1], __f[__ind2] } __f[__ind1] && (__f[__ind2] && __ind1 != __ind2) ==> (recApply((getreceiver(__c): ReceiverDomainType int), __ind1): Ref) != (recApply((getreceiver(__c): ReceiverDomainType int), __ind2): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@403.45--403.77) [541]"} (forall __ind_2: int :: { (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref) } { __f[__ind_2] } __f[__ind_2] && dummyFunction(Heap[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@403.45--403.77) [542]"} (forall __ind_2: int, __ind_2_1: int :: { neverTriggered10(__ind_2), neverTriggered10(__ind_2_1) } (((__ind_2 != __ind_2_1 && __f[__ind_2]) && __f[__ind_2_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref) != (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@403.45--403.77) [543]"} (forall __ind_2: int :: { (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref) } { __f[__ind_2] } __f[__ind_2] ==> Mask[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_2: int :: { (recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref) } { __f[__ind_2] } __f[__ind_2] && NoPerm < 1 / 10 ==> qpRange10((recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref)) && invRecv10((recApply((getreceiver(__c): ReceiverDomainType int), __ind_2): Ref)) == __ind_2 ); assume (forall o_3: Ref :: { invRecv10(o_3) } __f[invRecv10(o_3)] && (NoPerm < 1 / 10 && qpRange10(o_3)) ==> (recApply((getreceiver(__c): ReceiverDomainType int), invRecv10(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f[invRecv10(o_3)] && (NoPerm < 1 / 10 && qpRange10(o_3)) ==> (recApply((getreceiver(__c): ReceiverDomainType int), invRecv10(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f[invRecv10(o_3)] && (NoPerm < 1 / 10 && qpRange10(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(Heap, __c, __f)): int), (recInv((getreceiver(__c): ReceiverDomainType int), (loc(a_3, i1): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell0 required to evaluate old[_compLabell0]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@393.11--406.90) [544]"} _compLabell0_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell0Mask; ExhaleWellDef0Heap := Label_compLabell0Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@405.62--406.11) [545]"} (filterReceiverGood(__f, (getreceiver(__c): ReceiverDomainType int)): bool) || (forall __ind1_1: int, __ind2_1: int :: { __f[__ind1_1], __f[__ind2_1] } __f[__ind1_1] && (__f[__ind2_1] && __ind1_1 != __ind2_1) ==> (recApply((getreceiver(__c): ReceiverDomainType int), __ind1_1): Ref) != (recApply((getreceiver(__c): ReceiverDomainType int), __ind2_1): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@405.62--406.11) [546]"} (forall __ind_3: int :: { (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref) } { __f[__ind_3] } __f[__ind_3] && dummyFunction(Label_compLabell0Heap[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@405.62--406.11) [547]"} (forall __ind_3: int, __ind_3_1: int :: { neverTriggered11(__ind_3), neverTriggered11(__ind_3_1) } (((__ind_3 != __ind_3_1 && __f[__ind_3]) && __f[__ind_3_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref) != (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@405.62--406.11) [548]"} (forall __ind_3: int :: { (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref) } { __f[__ind_3] } __f[__ind_3] ==> Label_compLabell0Mask[(recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_3: int :: { (recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref) } { __f[__ind_3] } __f[__ind_3] && NoPerm < 1 / 10 ==> qpRange11((recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref)) && invRecv11((recApply((getreceiver(__c): ReceiverDomainType int), __ind_3): Ref)) == __ind_3 ); assume (forall o_3: Ref :: { invRecv11(o_3) } __f[invRecv11(o_3)] && (NoPerm < 1 / 10 && qpRange11(o_3)) ==> (recApply((getreceiver(__c): ReceiverDomainType int), invRecv11(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f[invRecv11(o_3)] && (NoPerm < 1 / 10 && qpRange11(o_3)) ==> (recApply((getreceiver(__c): ReceiverDomainType int), invRecv11(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell0Mask[o_3, val] - 1 / 10) && (!(__f[invRecv11(o_3)] && (NoPerm < 1 / 10 && qpRange11(o_3))) ==> QPMask[o_3, val] == Label_compLabell0Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell0Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell0Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell0Heap, ExhaleHeap, Label_compLabell0Mask); Label_compLabell0Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_1: (FoldDomainType int int int), __f_1: (Set int) :: { (hfoldApply(__c_1, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell0Heap, __c_1, __f_1)), __c_1, __f_1)): int) } { (hfoldApply(__c_1, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_1, __f_1)), __c_1, __f_1)): int) } (filterReceiverGood(__f_1, (getreceiver(__c_1): ReceiverDomainType int)): bool) && (forall __ind_4: int :: { __f_1[__ind_4] } __f_1[__ind_4] ==> NoPerm < Mask[(recApply((getreceiver(__c_1): ReceiverDomainType int), __ind_4): Ref), val] ) ==> (filterReceiverGood(__f_1, (getreceiver(__c_1): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_1, __snap_Int_Int_Int_val(Heap, __c_1, __f_1)): int), (recInv((getreceiver(__c_1): ReceiverDomainType int), (loc(a_3, i1): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_1, __snap_Int_Int_Int_val(Label_compLabell0Heap, __c_1, __f_1)): int), (recInv((getreceiver(__c_1): ReceiverDomainType int), (loc(a_3, i1): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, j1).val := loc(a, j1).val + 1 -- arrayTestChainIrrel3.vpr@407.3--407.39 // -- Check definedness of loc(a, j1).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j1).val (arrayTestChainIrrel3.vpr@407.3--407.39) [549]"} HasDirectPerm(Mask, (loc(a_3, j1): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j1).val (arrayTestChainIrrel3.vpr@407.3--407.39) [550]"} FullPerm == Mask[(loc(a_3, j1): Ref), val]; Heap := Heap[(loc(a_3, j1): Ref), val:=Heap[(loc(a_3, j1): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell2 -- arrayTestChainIrrel3.vpr@408.3--408.21 _compLabell2: Label_compLabell2Mask := Mask; Label_compLabell2Heap := Heap; _compLabell2_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@409.3--422.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j1)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool) && (forall __ind_6: int :: { __f_2[__ind_6] } __f_2[__ind_6] ==> NoPerm < Mask[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_6): Ref), val] )) { if ((filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@419.45--419.77) [551]"} (filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool) || (forall __ind1_2: int, __ind2_2: int :: { __f_2[__ind1_2], __f_2[__ind2_2] } __f_2[__ind1_2] && (__f_2[__ind2_2] && __ind1_2 != __ind2_2) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind1_2): Ref) != (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind2_2): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@419.45--419.77) [552]"} (forall __ind_7: int :: { (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref) } { __f_2[__ind_7] } __f_2[__ind_7] && dummyFunction(Heap[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@419.45--419.77) [553]"} (forall __ind_7: int, __ind_7_1: int :: { neverTriggered12(__ind_7), neverTriggered12(__ind_7_1) } (((__ind_7 != __ind_7_1 && __f_2[__ind_7]) && __f_2[__ind_7_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref) != (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@419.45--419.77) [554]"} (forall __ind_7: int :: { (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref) } { __f_2[__ind_7] } __f_2[__ind_7] ==> Mask[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_7: int :: { (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref) } { __f_2[__ind_7] } __f_2[__ind_7] && NoPerm < 1 / 10 ==> qpRange12((recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref)) && invRecv12((recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_7): Ref)) == __ind_7 ); assume (forall o_3: Ref :: { invRecv12(o_3) } __f_2[invRecv12(o_3)] && (NoPerm < 1 / 10 && qpRange12(o_3)) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), invRecv12(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_2[invRecv12(o_3)] && (NoPerm < 1 / 10 && qpRange12(o_3)) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), invRecv12(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_2[invRecv12(o_3)] && (NoPerm < 1 / 10 && qpRange12(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c_2, __snap_Int_Int_Int_val(Heap, __c_2, __f_2)): int), (recInv((getreceiver(__c_2): ReceiverDomainType int), (loc(a_3, j1): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell1 required to evaluate old[_compLabell1]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@409.11--422.90) [555]"} _compLabell1_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell1Mask; ExhaleWellDef0Heap := Label_compLabell1Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@421.62--422.11) [556]"} (filterReceiverGood(__f_2, (getreceiver(__c_2): ReceiverDomainType int)): bool) || (forall __ind1_3: int, __ind2_3: int :: { __f_2[__ind1_3], __f_2[__ind2_3] } __f_2[__ind1_3] && (__f_2[__ind2_3] && __ind1_3 != __ind2_3) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind1_3): Ref) != (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind2_3): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@421.62--422.11) [557]"} (forall __ind_8: int :: { (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref) } { __f_2[__ind_8] } __f_2[__ind_8] && dummyFunction(Label_compLabell1Heap[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@421.62--422.11) [558]"} (forall __ind_8: int, __ind_8_1: int :: { neverTriggered13(__ind_8), neverTriggered13(__ind_8_1) } (((__ind_8 != __ind_8_1 && __f_2[__ind_8]) && __f_2[__ind_8_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref) != (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@421.62--422.11) [559]"} (forall __ind_8: int :: { (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref) } { __f_2[__ind_8] } __f_2[__ind_8] ==> Label_compLabell1Mask[(recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_8: int :: { (recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref) } { __f_2[__ind_8] } __f_2[__ind_8] && NoPerm < 1 / 10 ==> qpRange13((recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref)) && invRecv13((recApply((getreceiver(__c_2): ReceiverDomainType int), __ind_8): Ref)) == __ind_8 ); assume (forall o_3: Ref :: { invRecv13(o_3) } __f_2[invRecv13(o_3)] && (NoPerm < 1 / 10 && qpRange13(o_3)) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), invRecv13(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_2[invRecv13(o_3)] && (NoPerm < 1 / 10 && qpRange13(o_3)) ==> (recApply((getreceiver(__c_2): ReceiverDomainType int), invRecv13(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell1Mask[o_3, val] - 1 / 10) && (!(__f_2[invRecv13(o_3)] && (NoPerm < 1 / 10 && qpRange13(o_3))) ==> QPMask[o_3, val] == Label_compLabell1Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell1Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell1Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell1Heap, ExhaleHeap, Label_compLabell1Mask); Label_compLabell1Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_3: (FoldDomainType int int int), __f_3: (Set int) :: { (hfoldApply(__c_3, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell1Heap, __c_3, __f_3)), __c_3, __f_3)): int) } { (hfoldApply(__c_3, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_3, __f_3)), __c_3, __f_3)): int) } (filterReceiverGood(__f_3, (getreceiver(__c_3): ReceiverDomainType int)): bool) && (forall __ind_9: int :: { __f_3[__ind_9] } __f_3[__ind_9] ==> NoPerm < Mask[(recApply((getreceiver(__c_3): ReceiverDomainType int), __ind_9): Ref), val] ) ==> (filterReceiverGood(__f_3, (getreceiver(__c_3): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_3, __snap_Int_Int_Int_val(Heap, __c_3, __f_3)): int), (recInv((getreceiver(__c_3): ReceiverDomainType int), (loc(a_3, j1): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_3, __snap_Int_Int_Int_val(Label_compLabell1Heap, __c_3, __f_3)): int), (recInv((getreceiver(__c_3): ReceiverDomainType int), (loc(a_3, j1): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, i2).val := loc(a, i2).val + 1 -- arrayTestChainIrrel3.vpr@423.3--423.39 // -- Check definedness of loc(a, i2).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i2).val (arrayTestChainIrrel3.vpr@423.3--423.39) [560]"} HasDirectPerm(Mask, (loc(a_3, i2): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i2).val (arrayTestChainIrrel3.vpr@423.3--423.39) [561]"} FullPerm == Mask[(loc(a_3, i2): Ref), val]; Heap := Heap[(loc(a_3, i2): Ref), val:=Heap[(loc(a_3, i2): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell3 -- arrayTestChainIrrel3.vpr@424.3--424.21 _compLabell3: Label_compLabell3Mask := Mask; Label_compLabell3Heap := Heap; _compLabell3_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@425.3--438.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i2)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool) && (forall __ind_11: int :: { __f_4[__ind_11] } __f_4[__ind_11] ==> NoPerm < Mask[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_11): Ref), val] )) { if ((filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@435.45--435.77) [562]"} (filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool) || (forall __ind1_4: int, __ind2_4: int :: { __f_4[__ind1_4], __f_4[__ind2_4] } __f_4[__ind1_4] && (__f_4[__ind2_4] && __ind1_4 != __ind2_4) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind1_4): Ref) != (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind2_4): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@435.45--435.77) [563]"} (forall __ind_12: int :: { (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref) } { __f_4[__ind_12] } __f_4[__ind_12] && dummyFunction(Heap[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@435.45--435.77) [564]"} (forall __ind_12: int, __ind_12_1: int :: { neverTriggered14(__ind_12), neverTriggered14(__ind_12_1) } (((__ind_12 != __ind_12_1 && __f_4[__ind_12]) && __f_4[__ind_12_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref) != (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@435.45--435.77) [565]"} (forall __ind_12: int :: { (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref) } { __f_4[__ind_12] } __f_4[__ind_12] ==> Mask[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_12: int :: { (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref) } { __f_4[__ind_12] } __f_4[__ind_12] && NoPerm < 1 / 10 ==> qpRange14((recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref)) && invRecv14((recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_12): Ref)) == __ind_12 ); assume (forall o_3: Ref :: { invRecv14(o_3) } __f_4[invRecv14(o_3)] && (NoPerm < 1 / 10 && qpRange14(o_3)) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), invRecv14(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_4[invRecv14(o_3)] && (NoPerm < 1 / 10 && qpRange14(o_3)) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), invRecv14(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_4[invRecv14(o_3)] && (NoPerm < 1 / 10 && qpRange14(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c_4, __snap_Int_Int_Int_val(Heap, __c_4, __f_4)): int), (recInv((getreceiver(__c_4): ReceiverDomainType int), (loc(a_3, i2): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell2 required to evaluate old[_compLabell2]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@425.11--438.90) [566]"} _compLabell2_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell2Mask; ExhaleWellDef0Heap := Label_compLabell2Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@437.62--438.11) [567]"} (filterReceiverGood(__f_4, (getreceiver(__c_4): ReceiverDomainType int)): bool) || (forall __ind1_5: int, __ind2_5: int :: { __f_4[__ind1_5], __f_4[__ind2_5] } __f_4[__ind1_5] && (__f_4[__ind2_5] && __ind1_5 != __ind2_5) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind1_5): Ref) != (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind2_5): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@437.62--438.11) [568]"} (forall __ind_13: int :: { (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref) } { __f_4[__ind_13] } __f_4[__ind_13] && dummyFunction(Label_compLabell2Heap[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@437.62--438.11) [569]"} (forall __ind_13: int, __ind_13_1: int :: { neverTriggered15(__ind_13), neverTriggered15(__ind_13_1) } (((__ind_13 != __ind_13_1 && __f_4[__ind_13]) && __f_4[__ind_13_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref) != (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@437.62--438.11) [570]"} (forall __ind_13: int :: { (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref) } { __f_4[__ind_13] } __f_4[__ind_13] ==> Label_compLabell2Mask[(recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_13: int :: { (recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref) } { __f_4[__ind_13] } __f_4[__ind_13] && NoPerm < 1 / 10 ==> qpRange15((recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref)) && invRecv15((recApply((getreceiver(__c_4): ReceiverDomainType int), __ind_13): Ref)) == __ind_13 ); assume (forall o_3: Ref :: { invRecv15(o_3) } __f_4[invRecv15(o_3)] && (NoPerm < 1 / 10 && qpRange15(o_3)) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), invRecv15(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_4[invRecv15(o_3)] && (NoPerm < 1 / 10 && qpRange15(o_3)) ==> (recApply((getreceiver(__c_4): ReceiverDomainType int), invRecv15(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell2Mask[o_3, val] - 1 / 10) && (!(__f_4[invRecv15(o_3)] && (NoPerm < 1 / 10 && qpRange15(o_3))) ==> QPMask[o_3, val] == Label_compLabell2Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell2Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell2Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell2Heap, ExhaleHeap, Label_compLabell2Mask); Label_compLabell2Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_5: (FoldDomainType int int int), __f_5: (Set int) :: { (hfoldApply(__c_5, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell2Heap, __c_5, __f_5)), __c_5, __f_5)): int) } { (hfoldApply(__c_5, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_5, __f_5)), __c_5, __f_5)): int) } (filterReceiverGood(__f_5, (getreceiver(__c_5): ReceiverDomainType int)): bool) && (forall __ind_14: int :: { __f_5[__ind_14] } __f_5[__ind_14] ==> NoPerm < Mask[(recApply((getreceiver(__c_5): ReceiverDomainType int), __ind_14): Ref), val] ) ==> (filterReceiverGood(__f_5, (getreceiver(__c_5): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_5, __snap_Int_Int_Int_val(Heap, __c_5, __f_5)): int), (recInv((getreceiver(__c_5): ReceiverDomainType int), (loc(a_3, i2): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_5, __snap_Int_Int_Int_val(Label_compLabell2Heap, __c_5, __f_5)): int), (recInv((getreceiver(__c_5): ReceiverDomainType int), (loc(a_3, i2): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, i3).val := loc(a, i3).val + 1 -- arrayTestChainIrrel3.vpr@439.3--439.39 // -- Check definedness of loc(a, i3).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i3).val (arrayTestChainIrrel3.vpr@439.3--439.39) [571]"} HasDirectPerm(Mask, (loc(a_3, i3): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i3).val (arrayTestChainIrrel3.vpr@439.3--439.39) [572]"} FullPerm == Mask[(loc(a_3, i3): Ref), val]; Heap := Heap[(loc(a_3, i3): Ref), val:=Heap[(loc(a_3, i3): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell4 -- arrayTestChainIrrel3.vpr@440.3--440.21 _compLabell4: Label_compLabell4Mask := Mask; Label_compLabell4Heap := Heap; _compLabell4_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@441.3--454.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i3)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool) && (forall __ind_16: int :: { __f_6[__ind_16] } __f_6[__ind_16] ==> NoPerm < Mask[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_16): Ref), val] )) { if ((filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@451.45--451.77) [573]"} (filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool) || (forall __ind1_6: int, __ind2_6: int :: { __f_6[__ind1_6], __f_6[__ind2_6] } __f_6[__ind1_6] && (__f_6[__ind2_6] && __ind1_6 != __ind2_6) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind1_6): Ref) != (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind2_6): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@451.45--451.77) [574]"} (forall __ind_17: int :: { (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref) } { __f_6[__ind_17] } __f_6[__ind_17] && dummyFunction(Heap[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@451.45--451.77) [575]"} (forall __ind_17: int, __ind_17_1: int :: { neverTriggered16(__ind_17), neverTriggered16(__ind_17_1) } (((__ind_17 != __ind_17_1 && __f_6[__ind_17]) && __f_6[__ind_17_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref) != (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@451.45--451.77) [576]"} (forall __ind_17: int :: { (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref) } { __f_6[__ind_17] } __f_6[__ind_17] ==> Mask[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_17: int :: { (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref) } { __f_6[__ind_17] } __f_6[__ind_17] && NoPerm < 1 / 10 ==> qpRange16((recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref)) && invRecv16((recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_17): Ref)) == __ind_17 ); assume (forall o_3: Ref :: { invRecv16(o_3) } __f_6[invRecv16(o_3)] && (NoPerm < 1 / 10 && qpRange16(o_3)) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), invRecv16(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_6[invRecv16(o_3)] && (NoPerm < 1 / 10 && qpRange16(o_3)) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), invRecv16(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_6[invRecv16(o_3)] && (NoPerm < 1 / 10 && qpRange16(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c_6, __snap_Int_Int_Int_val(Heap, __c_6, __f_6)): int), (recInv((getreceiver(__c_6): ReceiverDomainType int), (loc(a_3, i3): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell3 required to evaluate old[_compLabell3]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@441.11--454.90) [577]"} _compLabell3_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell3Mask; ExhaleWellDef0Heap := Label_compLabell3Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@453.62--454.11) [578]"} (filterReceiverGood(__f_6, (getreceiver(__c_6): ReceiverDomainType int)): bool) || (forall __ind1_7: int, __ind2_7: int :: { __f_6[__ind1_7], __f_6[__ind2_7] } __f_6[__ind1_7] && (__f_6[__ind2_7] && __ind1_7 != __ind2_7) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind1_7): Ref) != (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind2_7): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@453.62--454.11) [579]"} (forall __ind_18: int :: { (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref) } { __f_6[__ind_18] } __f_6[__ind_18] && dummyFunction(Label_compLabell3Heap[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@453.62--454.11) [580]"} (forall __ind_18: int, __ind_18_1: int :: { neverTriggered17(__ind_18), neverTriggered17(__ind_18_1) } (((__ind_18 != __ind_18_1 && __f_6[__ind_18]) && __f_6[__ind_18_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref) != (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@453.62--454.11) [581]"} (forall __ind_18: int :: { (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref) } { __f_6[__ind_18] } __f_6[__ind_18] ==> Label_compLabell3Mask[(recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_18: int :: { (recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref) } { __f_6[__ind_18] } __f_6[__ind_18] && NoPerm < 1 / 10 ==> qpRange17((recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref)) && invRecv17((recApply((getreceiver(__c_6): ReceiverDomainType int), __ind_18): Ref)) == __ind_18 ); assume (forall o_3: Ref :: { invRecv17(o_3) } __f_6[invRecv17(o_3)] && (NoPerm < 1 / 10 && qpRange17(o_3)) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), invRecv17(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_6[invRecv17(o_3)] && (NoPerm < 1 / 10 && qpRange17(o_3)) ==> (recApply((getreceiver(__c_6): ReceiverDomainType int), invRecv17(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell3Mask[o_3, val] - 1 / 10) && (!(__f_6[invRecv17(o_3)] && (NoPerm < 1 / 10 && qpRange17(o_3))) ==> QPMask[o_3, val] == Label_compLabell3Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell3Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell3Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell3Heap, ExhaleHeap, Label_compLabell3Mask); Label_compLabell3Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_7: (FoldDomainType int int int), __f_7: (Set int) :: { (hfoldApply(__c_7, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell3Heap, __c_7, __f_7)), __c_7, __f_7)): int) } { (hfoldApply(__c_7, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_7, __f_7)), __c_7, __f_7)): int) } (filterReceiverGood(__f_7, (getreceiver(__c_7): ReceiverDomainType int)): bool) && (forall __ind_19: int :: { __f_7[__ind_19] } __f_7[__ind_19] ==> NoPerm < Mask[(recApply((getreceiver(__c_7): ReceiverDomainType int), __ind_19): Ref), val] ) ==> (filterReceiverGood(__f_7, (getreceiver(__c_7): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_7, __snap_Int_Int_Int_val(Heap, __c_7, __f_7)): int), (recInv((getreceiver(__c_7): ReceiverDomainType int), (loc(a_3, i3): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_7, __snap_Int_Int_Int_val(Label_compLabell3Heap, __c_7, __f_7)): int), (recInv((getreceiver(__c_7): ReceiverDomainType int), (loc(a_3, i3): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, j2).val := loc(a, j2).val + 1 -- arrayTestChainIrrel3.vpr@455.3--455.39 // -- Check definedness of loc(a, j2).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j2).val (arrayTestChainIrrel3.vpr@455.3--455.39) [582]"} HasDirectPerm(Mask, (loc(a_3, j2): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j2).val (arrayTestChainIrrel3.vpr@455.3--455.39) [583]"} FullPerm == Mask[(loc(a_3, j2): Ref), val]; Heap := Heap[(loc(a_3, j2): Ref), val:=Heap[(loc(a_3, j2): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell5 -- arrayTestChainIrrel3.vpr@456.3--456.21 _compLabell5: Label_compLabell5Mask := Mask; Label_compLabell5Heap := Heap; _compLabell5_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@457.3--470.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j2)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool) && (forall __ind_21: int :: { __f_8[__ind_21] } __f_8[__ind_21] ==> NoPerm < Mask[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_21): Ref), val] )) { if ((filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@467.45--467.77) [584]"} (filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool) || (forall __ind1_8: int, __ind2_8: int :: { __f_8[__ind1_8], __f_8[__ind2_8] } __f_8[__ind1_8] && (__f_8[__ind2_8] && __ind1_8 != __ind2_8) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind1_8): Ref) != (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind2_8): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@467.45--467.77) [585]"} (forall __ind_22: int :: { (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref) } { __f_8[__ind_22] } __f_8[__ind_22] && dummyFunction(Heap[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@467.45--467.77) [586]"} (forall __ind_22: int, __ind_22_1: int :: { neverTriggered18(__ind_22), neverTriggered18(__ind_22_1) } (((__ind_22 != __ind_22_1 && __f_8[__ind_22]) && __f_8[__ind_22_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref) != (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@467.45--467.77) [587]"} (forall __ind_22: int :: { (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref) } { __f_8[__ind_22] } __f_8[__ind_22] ==> Mask[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_22: int :: { (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref) } { __f_8[__ind_22] } __f_8[__ind_22] && NoPerm < 1 / 10 ==> qpRange18((recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref)) && invRecv18((recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_22): Ref)) == __ind_22 ); assume (forall o_3: Ref :: { invRecv18(o_3) } __f_8[invRecv18(o_3)] && (NoPerm < 1 / 10 && qpRange18(o_3)) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), invRecv18(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_8[invRecv18(o_3)] && (NoPerm < 1 / 10 && qpRange18(o_3)) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), invRecv18(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_8[invRecv18(o_3)] && (NoPerm < 1 / 10 && qpRange18(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c_8, __snap_Int_Int_Int_val(Heap, __c_8, __f_8)): int), (recInv((getreceiver(__c_8): ReceiverDomainType int), (loc(a_3, j2): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell4 required to evaluate old[_compLabell4]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@457.11--470.90) [588]"} _compLabell4_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell4Mask; ExhaleWellDef0Heap := Label_compLabell4Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@469.62--470.11) [589]"} (filterReceiverGood(__f_8, (getreceiver(__c_8): ReceiverDomainType int)): bool) || (forall __ind1_9: int, __ind2_9: int :: { __f_8[__ind1_9], __f_8[__ind2_9] } __f_8[__ind1_9] && (__f_8[__ind2_9] && __ind1_9 != __ind2_9) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind1_9): Ref) != (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind2_9): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@469.62--470.11) [590]"} (forall __ind_23: int :: { (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref) } { __f_8[__ind_23] } __f_8[__ind_23] && dummyFunction(Label_compLabell4Heap[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@469.62--470.11) [591]"} (forall __ind_23: int, __ind_23_1: int :: { neverTriggered19(__ind_23), neverTriggered19(__ind_23_1) } (((__ind_23 != __ind_23_1 && __f_8[__ind_23]) && __f_8[__ind_23_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref) != (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@469.62--470.11) [592]"} (forall __ind_23: int :: { (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref) } { __f_8[__ind_23] } __f_8[__ind_23] ==> Label_compLabell4Mask[(recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_23: int :: { (recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref) } { __f_8[__ind_23] } __f_8[__ind_23] && NoPerm < 1 / 10 ==> qpRange19((recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref)) && invRecv19((recApply((getreceiver(__c_8): ReceiverDomainType int), __ind_23): Ref)) == __ind_23 ); assume (forall o_3: Ref :: { invRecv19(o_3) } __f_8[invRecv19(o_3)] && (NoPerm < 1 / 10 && qpRange19(o_3)) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), invRecv19(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_8[invRecv19(o_3)] && (NoPerm < 1 / 10 && qpRange19(o_3)) ==> (recApply((getreceiver(__c_8): ReceiverDomainType int), invRecv19(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell4Mask[o_3, val] - 1 / 10) && (!(__f_8[invRecv19(o_3)] && (NoPerm < 1 / 10 && qpRange19(o_3))) ==> QPMask[o_3, val] == Label_compLabell4Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell4Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell4Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell4Heap, ExhaleHeap, Label_compLabell4Mask); Label_compLabell4Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_9: (FoldDomainType int int int), __f_9: (Set int) :: { (hfoldApply(__c_9, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell4Heap, __c_9, __f_9)), __c_9, __f_9)): int) } { (hfoldApply(__c_9, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_9, __f_9)), __c_9, __f_9)): int) } (filterReceiverGood(__f_9, (getreceiver(__c_9): ReceiverDomainType int)): bool) && (forall __ind_24: int :: { __f_9[__ind_24] } __f_9[__ind_24] ==> NoPerm < Mask[(recApply((getreceiver(__c_9): ReceiverDomainType int), __ind_24): Ref), val] ) ==> (filterReceiverGood(__f_9, (getreceiver(__c_9): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_9, __snap_Int_Int_Int_val(Heap, __c_9, __f_9)): int), (recInv((getreceiver(__c_9): ReceiverDomainType int), (loc(a_3, j2): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_9, __snap_Int_Int_Int_val(Label_compLabell4Heap, __c_9, __f_9)): int), (recInv((getreceiver(__c_9): ReceiverDomainType int), (loc(a_3, j2): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, i4).val := loc(a, i4).val + 1 -- arrayTestChainIrrel3.vpr@471.3--471.39 // -- Check definedness of loc(a, i4).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i4).val (arrayTestChainIrrel3.vpr@471.3--471.39) [593]"} HasDirectPerm(Mask, (loc(a_3, i4): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i4).val (arrayTestChainIrrel3.vpr@471.3--471.39) [594]"} FullPerm == Mask[(loc(a_3, i4): Ref), val]; Heap := Heap[(loc(a_3, i4): Ref), val:=Heap[(loc(a_3, i4): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell6 -- arrayTestChainIrrel3.vpr@472.3--472.21 _compLabell6: Label_compLabell6Mask := Mask; Label_compLabell6Heap := Heap; _compLabell6_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@473.3--486.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i4)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool) && (forall __ind_26: int :: { __f_10[__ind_26] } __f_10[__ind_26] ==> NoPerm < Mask[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_26): Ref), val] )) { if ((filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@483.45--483.77) [595]"} (filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool) || (forall __ind1_10: int, __ind2_10: int :: { __f_10[__ind1_10], __f_10[__ind2_10] } __f_10[__ind1_10] && (__f_10[__ind2_10] && __ind1_10 != __ind2_10) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind1_10): Ref) != (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind2_10): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@483.45--483.77) [596]"} (forall __ind_27: int :: { (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref) } { __f_10[__ind_27] } __f_10[__ind_27] && dummyFunction(Heap[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@483.45--483.77) [597]"} (forall __ind_27: int, __ind_27_1: int :: { neverTriggered20(__ind_27), neverTriggered20(__ind_27_1) } (((__ind_27 != __ind_27_1 && __f_10[__ind_27]) && __f_10[__ind_27_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref) != (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@483.45--483.77) [598]"} (forall __ind_27: int :: { (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref) } { __f_10[__ind_27] } __f_10[__ind_27] ==> Mask[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_27: int :: { (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref) } { __f_10[__ind_27] } __f_10[__ind_27] && NoPerm < 1 / 10 ==> qpRange20((recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref)) && invRecv20((recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_27): Ref)) == __ind_27 ); assume (forall o_3: Ref :: { invRecv20(o_3) } __f_10[invRecv20(o_3)] && (NoPerm < 1 / 10 && qpRange20(o_3)) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), invRecv20(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_10[invRecv20(o_3)] && (NoPerm < 1 / 10 && qpRange20(o_3)) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), invRecv20(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_10[invRecv20(o_3)] && (NoPerm < 1 / 10 && qpRange20(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c_10, __snap_Int_Int_Int_val(Heap, __c_10, __f_10)): int), (recInv((getreceiver(__c_10): ReceiverDomainType int), (loc(a_3, i4): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell5 required to evaluate old[_compLabell5]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@473.11--486.90) [599]"} _compLabell5_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell5Mask; ExhaleWellDef0Heap := Label_compLabell5Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@485.62--486.11) [600]"} (filterReceiverGood(__f_10, (getreceiver(__c_10): ReceiverDomainType int)): bool) || (forall __ind1_11: int, __ind2_11: int :: { __f_10[__ind1_11], __f_10[__ind2_11] } __f_10[__ind1_11] && (__f_10[__ind2_11] && __ind1_11 != __ind2_11) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind1_11): Ref) != (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind2_11): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@485.62--486.11) [601]"} (forall __ind_28: int :: { (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref) } { __f_10[__ind_28] } __f_10[__ind_28] && dummyFunction(Label_compLabell5Heap[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@485.62--486.11) [602]"} (forall __ind_28: int, __ind_28_1: int :: { neverTriggered21(__ind_28), neverTriggered21(__ind_28_1) } (((__ind_28 != __ind_28_1 && __f_10[__ind_28]) && __f_10[__ind_28_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref) != (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@485.62--486.11) [603]"} (forall __ind_28: int :: { (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref) } { __f_10[__ind_28] } __f_10[__ind_28] ==> Label_compLabell5Mask[(recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_28: int :: { (recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref) } { __f_10[__ind_28] } __f_10[__ind_28] && NoPerm < 1 / 10 ==> qpRange21((recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref)) && invRecv21((recApply((getreceiver(__c_10): ReceiverDomainType int), __ind_28): Ref)) == __ind_28 ); assume (forall o_3: Ref :: { invRecv21(o_3) } __f_10[invRecv21(o_3)] && (NoPerm < 1 / 10 && qpRange21(o_3)) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), invRecv21(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_10[invRecv21(o_3)] && (NoPerm < 1 / 10 && qpRange21(o_3)) ==> (recApply((getreceiver(__c_10): ReceiverDomainType int), invRecv21(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell5Mask[o_3, val] - 1 / 10) && (!(__f_10[invRecv21(o_3)] && (NoPerm < 1 / 10 && qpRange21(o_3))) ==> QPMask[o_3, val] == Label_compLabell5Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell5Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell5Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell5Heap, ExhaleHeap, Label_compLabell5Mask); Label_compLabell5Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_11: (FoldDomainType int int int), __f_11: (Set int) :: { (hfoldApply(__c_11, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell5Heap, __c_11, __f_11)), __c_11, __f_11)): int) } { (hfoldApply(__c_11, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_11, __f_11)), __c_11, __f_11)): int) } (filterReceiverGood(__f_11, (getreceiver(__c_11): ReceiverDomainType int)): bool) && (forall __ind_29: int :: { __f_11[__ind_29] } __f_11[__ind_29] ==> NoPerm < Mask[(recApply((getreceiver(__c_11): ReceiverDomainType int), __ind_29): Ref), val] ) ==> (filterReceiverGood(__f_11, (getreceiver(__c_11): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_11, __snap_Int_Int_Int_val(Heap, __c_11, __f_11)): int), (recInv((getreceiver(__c_11): ReceiverDomainType int), (loc(a_3, i4): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_11, __snap_Int_Int_Int_val(Label_compLabell5Heap, __c_11, __f_11)): int), (recInv((getreceiver(__c_11): ReceiverDomainType int), (loc(a_3, i4): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, i5).val := loc(a, i5).val + 1 -- arrayTestChainIrrel3.vpr@487.3--487.39 // -- Check definedness of loc(a, i5).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i5).val (arrayTestChainIrrel3.vpr@487.3--487.39) [604]"} HasDirectPerm(Mask, (loc(a_3, i5): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i5).val (arrayTestChainIrrel3.vpr@487.3--487.39) [605]"} FullPerm == Mask[(loc(a_3, i5): Ref), val]; Heap := Heap[(loc(a_3, i5): Ref), val:=Heap[(loc(a_3, i5): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell7 -- arrayTestChainIrrel3.vpr@488.3--488.21 _compLabell7: Label_compLabell7Mask := Mask; Label_compLabell7Heap := Heap; _compLabell7_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@489.3--502.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i5)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool) && (forall __ind_31: int :: { __f_12[__ind_31] } __f_12[__ind_31] ==> NoPerm < Mask[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_31): Ref), val] )) { if ((filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@499.45--499.77) [606]"} (filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool) || (forall __ind1_12: int, __ind2_12: int :: { __f_12[__ind1_12], __f_12[__ind2_12] } __f_12[__ind1_12] && (__f_12[__ind2_12] && __ind1_12 != __ind2_12) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind1_12): Ref) != (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind2_12): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@499.45--499.77) [607]"} (forall __ind_32: int :: { (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref) } { __f_12[__ind_32] } __f_12[__ind_32] && dummyFunction(Heap[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@499.45--499.77) [608]"} (forall __ind_32: int, __ind_32_1: int :: { neverTriggered22(__ind_32), neverTriggered22(__ind_32_1) } (((__ind_32 != __ind_32_1 && __f_12[__ind_32]) && __f_12[__ind_32_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref) != (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@499.45--499.77) [609]"} (forall __ind_32: int :: { (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref) } { __f_12[__ind_32] } __f_12[__ind_32] ==> Mask[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_32: int :: { (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref) } { __f_12[__ind_32] } __f_12[__ind_32] && NoPerm < 1 / 10 ==> qpRange22((recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref)) && invRecv22((recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_32): Ref)) == __ind_32 ); assume (forall o_3: Ref :: { invRecv22(o_3) } __f_12[invRecv22(o_3)] && (NoPerm < 1 / 10 && qpRange22(o_3)) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), invRecv22(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_12[invRecv22(o_3)] && (NoPerm < 1 / 10 && qpRange22(o_3)) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), invRecv22(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_12[invRecv22(o_3)] && (NoPerm < 1 / 10 && qpRange22(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c_12, __snap_Int_Int_Int_val(Heap, __c_12, __f_12)): int), (recInv((getreceiver(__c_12): ReceiverDomainType int), (loc(a_3, i5): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell6 required to evaluate old[_compLabell6]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@489.11--502.90) [610]"} _compLabell6_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell6Mask; ExhaleWellDef0Heap := Label_compLabell6Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@501.62--502.11) [611]"} (filterReceiverGood(__f_12, (getreceiver(__c_12): ReceiverDomainType int)): bool) || (forall __ind1_13: int, __ind2_13: int :: { __f_12[__ind1_13], __f_12[__ind2_13] } __f_12[__ind1_13] && (__f_12[__ind2_13] && __ind1_13 != __ind2_13) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind1_13): Ref) != (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind2_13): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@501.62--502.11) [612]"} (forall __ind_33: int :: { (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref) } { __f_12[__ind_33] } __f_12[__ind_33] && dummyFunction(Label_compLabell6Heap[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@501.62--502.11) [613]"} (forall __ind_33: int, __ind_33_1: int :: { neverTriggered23(__ind_33), neverTriggered23(__ind_33_1) } (((__ind_33 != __ind_33_1 && __f_12[__ind_33]) && __f_12[__ind_33_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref) != (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@501.62--502.11) [614]"} (forall __ind_33: int :: { (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref) } { __f_12[__ind_33] } __f_12[__ind_33] ==> Label_compLabell6Mask[(recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_33: int :: { (recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref) } { __f_12[__ind_33] } __f_12[__ind_33] && NoPerm < 1 / 10 ==> qpRange23((recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref)) && invRecv23((recApply((getreceiver(__c_12): ReceiverDomainType int), __ind_33): Ref)) == __ind_33 ); assume (forall o_3: Ref :: { invRecv23(o_3) } __f_12[invRecv23(o_3)] && (NoPerm < 1 / 10 && qpRange23(o_3)) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), invRecv23(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_12[invRecv23(o_3)] && (NoPerm < 1 / 10 && qpRange23(o_3)) ==> (recApply((getreceiver(__c_12): ReceiverDomainType int), invRecv23(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell6Mask[o_3, val] - 1 / 10) && (!(__f_12[invRecv23(o_3)] && (NoPerm < 1 / 10 && qpRange23(o_3))) ==> QPMask[o_3, val] == Label_compLabell6Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell6Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell6Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell6Heap, ExhaleHeap, Label_compLabell6Mask); Label_compLabell6Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_13: (FoldDomainType int int int), __f_13: (Set int) :: { (hfoldApply(__c_13, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell6Heap, __c_13, __f_13)), __c_13, __f_13)): int) } { (hfoldApply(__c_13, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_13, __f_13)), __c_13, __f_13)): int) } (filterReceiverGood(__f_13, (getreceiver(__c_13): ReceiverDomainType int)): bool) && (forall __ind_34: int :: { __f_13[__ind_34] } __f_13[__ind_34] ==> NoPerm < Mask[(recApply((getreceiver(__c_13): ReceiverDomainType int), __ind_34): Ref), val] ) ==> (filterReceiverGood(__f_13, (getreceiver(__c_13): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_13, __snap_Int_Int_Int_val(Heap, __c_13, __f_13)): int), (recInv((getreceiver(__c_13): ReceiverDomainType int), (loc(a_3, i5): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_13, __snap_Int_Int_Int_val(Label_compLabell6Heap, __c_13, __f_13)): int), (recInv((getreceiver(__c_13): ReceiverDomainType int), (loc(a_3, i5): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, j3).val := loc(a, j3).val + 1 -- arrayTestChainIrrel3.vpr@503.3--503.39 // -- Check definedness of loc(a, j3).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j3).val (arrayTestChainIrrel3.vpr@503.3--503.39) [615]"} HasDirectPerm(Mask, (loc(a_3, j3): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, j3).val (arrayTestChainIrrel3.vpr@503.3--503.39) [616]"} FullPerm == Mask[(loc(a_3, j3): Ref), val]; Heap := Heap[(loc(a_3, j3): Ref), val:=Heap[(loc(a_3, j3): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell8 -- arrayTestChainIrrel3.vpr@504.3--504.21 _compLabell8: Label_compLabell8Mask := Mask; Label_compLabell8Heap := Heap; _compLabell8_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@505.3--518.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, j3)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool) && (forall __ind_36: int :: { __f_14[__ind_36] } __f_14[__ind_36] ==> NoPerm < Mask[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_36): Ref), val] )) { if ((filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@515.45--515.77) [617]"} (filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool) || (forall __ind1_14: int, __ind2_14: int :: { __f_14[__ind1_14], __f_14[__ind2_14] } __f_14[__ind1_14] && (__f_14[__ind2_14] && __ind1_14 != __ind2_14) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind1_14): Ref) != (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind2_14): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@515.45--515.77) [618]"} (forall __ind_37: int :: { (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref) } { __f_14[__ind_37] } __f_14[__ind_37] && dummyFunction(Heap[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@515.45--515.77) [619]"} (forall __ind_37: int, __ind_37_1: int :: { neverTriggered24(__ind_37), neverTriggered24(__ind_37_1) } (((__ind_37 != __ind_37_1 && __f_14[__ind_37]) && __f_14[__ind_37_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref) != (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@515.45--515.77) [620]"} (forall __ind_37: int :: { (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref) } { __f_14[__ind_37] } __f_14[__ind_37] ==> Mask[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_37: int :: { (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref) } { __f_14[__ind_37] } __f_14[__ind_37] && NoPerm < 1 / 10 ==> qpRange24((recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref)) && invRecv24((recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_37): Ref)) == __ind_37 ); assume (forall o_3: Ref :: { invRecv24(o_3) } __f_14[invRecv24(o_3)] && (NoPerm < 1 / 10 && qpRange24(o_3)) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), invRecv24(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_14[invRecv24(o_3)] && (NoPerm < 1 / 10 && qpRange24(o_3)) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), invRecv24(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_14[invRecv24(o_3)] && (NoPerm < 1 / 10 && qpRange24(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c_14, __snap_Int_Int_Int_val(Heap, __c_14, __f_14)): int), (recInv((getreceiver(__c_14): ReceiverDomainType int), (loc(a_3, j3): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell7 required to evaluate old[_compLabell7]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@505.11--518.90) [621]"} _compLabell7_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell7Mask; ExhaleWellDef0Heap := Label_compLabell7Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@517.62--518.11) [622]"} (filterReceiverGood(__f_14, (getreceiver(__c_14): ReceiverDomainType int)): bool) || (forall __ind1_15: int, __ind2_15: int :: { __f_14[__ind1_15], __f_14[__ind2_15] } __f_14[__ind1_15] && (__f_14[__ind2_15] && __ind1_15 != __ind2_15) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind1_15): Ref) != (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind2_15): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@517.62--518.11) [623]"} (forall __ind_38: int :: { (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref) } { __f_14[__ind_38] } __f_14[__ind_38] && dummyFunction(Label_compLabell7Heap[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@517.62--518.11) [624]"} (forall __ind_38: int, __ind_38_1: int :: { neverTriggered25(__ind_38), neverTriggered25(__ind_38_1) } (((__ind_38 != __ind_38_1 && __f_14[__ind_38]) && __f_14[__ind_38_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref) != (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@517.62--518.11) [625]"} (forall __ind_38: int :: { (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref) } { __f_14[__ind_38] } __f_14[__ind_38] ==> Label_compLabell7Mask[(recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_38: int :: { (recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref) } { __f_14[__ind_38] } __f_14[__ind_38] && NoPerm < 1 / 10 ==> qpRange25((recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref)) && invRecv25((recApply((getreceiver(__c_14): ReceiverDomainType int), __ind_38): Ref)) == __ind_38 ); assume (forall o_3: Ref :: { invRecv25(o_3) } __f_14[invRecv25(o_3)] && (NoPerm < 1 / 10 && qpRange25(o_3)) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), invRecv25(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_14[invRecv25(o_3)] && (NoPerm < 1 / 10 && qpRange25(o_3)) ==> (recApply((getreceiver(__c_14): ReceiverDomainType int), invRecv25(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell7Mask[o_3, val] - 1 / 10) && (!(__f_14[invRecv25(o_3)] && (NoPerm < 1 / 10 && qpRange25(o_3))) ==> QPMask[o_3, val] == Label_compLabell7Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell7Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell7Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell7Heap, ExhaleHeap, Label_compLabell7Mask); Label_compLabell7Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_15: (FoldDomainType int int int), __f_15: (Set int) :: { (hfoldApply(__c_15, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell7Heap, __c_15, __f_15)), __c_15, __f_15)): int) } { (hfoldApply(__c_15, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_15, __f_15)), __c_15, __f_15)): int) } (filterReceiverGood(__f_15, (getreceiver(__c_15): ReceiverDomainType int)): bool) && (forall __ind_39: int :: { __f_15[__ind_39] } __f_15[__ind_39] ==> NoPerm < Mask[(recApply((getreceiver(__c_15): ReceiverDomainType int), __ind_39): Ref), val] ) ==> (filterReceiverGood(__f_15, (getreceiver(__c_15): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_15, __snap_Int_Int_Int_val(Heap, __c_15, __f_15)): int), (recInv((getreceiver(__c_15): ReceiverDomainType int), (loc(a_3, j3): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_15, __snap_Int_Int_Int_val(Label_compLabell7Heap, __c_15, __f_15)): int), (recInv((getreceiver(__c_15): ReceiverDomainType int), (loc(a_3, j3): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: loc(a, i6).val := loc(a, i6).val + 1 -- arrayTestChainIrrel3.vpr@519.3--519.39 // -- Check definedness of loc(a, i6).val + 1 assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i6).val (arrayTestChainIrrel3.vpr@519.3--519.39) [626]"} HasDirectPerm(Mask, (loc(a_3, i6): Ref), val); assert {:msg " Assignment might fail. There might be insufficient permission to access loc(a, i6).val (arrayTestChainIrrel3.vpr@519.3--519.39) [627]"} FullPerm == Mask[(loc(a_3, i6): Ref), val]; Heap := Heap[(loc(a_3, i6): Ref), val:=Heap[(loc(a_3, i6): Ref), val] + 1]; assume state(Heap, Mask); // -- Translating statement: label _compLabell9 -- arrayTestChainIrrel3.vpr@520.3--520.21 _compLabell9: Label_compLabell9Mask := Mask; Label_compLabell9Heap := Heap; _compLabell9_lblGuard := true; assume state(Heap, Mask); // -- Translating statement: inhale (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: // { old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } // { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // (forall __ind: Int :: // { (__ind in __f) } // (__ind in __f) ==> // perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > // none) ==> // (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && // ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), // (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool) && // (_triggerDeleteKey1(old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, // __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool))) -- arrayTestChainIrrel3.vpr@521.3--534.91 assume state(Heap, Mask); // -- Check definedness of (forall __c: Fold[Int, Int, Int], __f: Set[Int] :: { old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)) } { (hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int) } (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && (forall __ind: Int :: { (__ind in __f) } (__ind in __f) ==> perm((recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val) > none) ==> (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) && ((_triggerDeleteKey1((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool) && (_triggerDeleteKey1(old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)), (recInv((getreceiver(__c): Receiver[Int]), loc(a, i6)): Int)): Bool))) if (*) { if ((filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool)) { if (*) { assume false; } } if ((filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool) && (forall __ind_41: int :: { __f_16[__ind_41] } __f_16[__ind_41] ==> NoPerm < Mask[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_41): Ref), val] )) { if ((filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool)) { if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@531.45--531.77) [628]"} (filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool) || (forall __ind1_16: int, __ind2_16: int :: { __f_16[__ind1_16], __f_16[__ind2_16] } __f_16[__ind1_16] && (__f_16[__ind2_16] && __ind1_16 != __ind2_16) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind1_16): Ref) != (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind2_16): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@531.45--531.77) [629]"} (forall __ind_42: int :: { (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref) } { __f_16[__ind_42] } __f_16[__ind_42] && dummyFunction(Heap[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@531.45--531.77) [630]"} (forall __ind_42: int, __ind_42_1: int :: { neverTriggered26(__ind_42), neverTriggered26(__ind_42_1) } (((__ind_42 != __ind_42_1 && __f_16[__ind_42]) && __f_16[__ind_42_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref) != (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@531.45--531.77) [631]"} (forall __ind_42: int :: { (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref) } { __f_16[__ind_42] } __f_16[__ind_42] ==> Mask[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_42: int :: { (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref) } { __f_16[__ind_42] } __f_16[__ind_42] && NoPerm < 1 / 10 ==> qpRange26((recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref)) && invRecv26((recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_42): Ref)) == __ind_42 ); assume (forall o_3: Ref :: { invRecv26(o_3) } __f_16[invRecv26(o_3)] && (NoPerm < 1 / 10 && qpRange26(o_3)) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), invRecv26(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_16[invRecv26(o_3)] && (NoPerm < 1 / 10 && qpRange26(o_3)) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), invRecv26(o_3)): Ref) == o_3 && QPMask[o_3, val] == Mask[o_3, val] - 1 / 10) && (!(__f_16[invRecv26(o_3)] && (NoPerm < 1 / 10 && qpRange26(o_3))) ==> QPMask[o_3, val] == Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Mask[o_3, f_5] == QPMask[o_3, f_5] ); Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Heap, ExhaleHeap, Mask); Heap := ExhaleHeap; // Stop execution assume false; } if ((_triggerDeleteKey1((hfoldApply(__c_16, __snap_Int_Int_Int_val(Heap, __c_16, __f_16)): int), (recInv((getreceiver(__c_16): ReceiverDomainType int), (loc(a_3, i6): Ref)): int)): bool)) { assert {:msg " Inhale might fail. Did not reach labelled state _compLabell8 required to evaluate old[_compLabell8]((hfoldApply(__c, __snap_Int_Int_Int_val(__c, __f)): Int)). (arrayTestChainIrrel3.vpr@521.11--534.90) [632]"} _compLabell8_lblGuard; if (*) { // Exhale precondition of function application ExhaleWellDef0Mask := Label_compLabell8Mask; ExhaleWellDef0Heap := Label_compLabell8Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(__f, (getreceiver(__c): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in __f), (__ind2 in __f) } (__ind1 in __f) && ((__ind2 in __f) && __ind1 != __ind2) ==> (recApply((getreceiver(__c): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver(__c): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@533.62--534.11) [633]"} (filterReceiverGood(__f_16, (getreceiver(__c_16): ReceiverDomainType int)): bool) || (forall __ind1_17: int, __ind2_17: int :: { __f_16[__ind1_17], __f_16[__ind2_17] } __f_16[__ind1_17] && (__f_16[__ind2_17] && __ind1_17 != __ind2_17) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind1_17): Ref) != (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind2_17): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@533.62--534.11) [634]"} (forall __ind_43: int :: { (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref) } { __f_16[__ind_43] } __f_16[__ind_43] && dummyFunction(Label_compLabell8Heap[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@533.62--534.11) [635]"} (forall __ind_43: int, __ind_43_1: int :: { neverTriggered27(__ind_43), neverTriggered27(__ind_43_1) } (((__ind_43 != __ind_43_1 && __f_16[__ind_43]) && __f_16[__ind_43_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref) != (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@533.62--534.11) [636]"} (forall __ind_43: int :: { (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref) } { __f_16[__ind_43] } __f_16[__ind_43] ==> Label_compLabell8Mask[(recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver(__c): Receiver[Int]), __ind): Ref) assume (forall __ind_43: int :: { (recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref) } { __f_16[__ind_43] } __f_16[__ind_43] && NoPerm < 1 / 10 ==> qpRange27((recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref)) && invRecv27((recApply((getreceiver(__c_16): ReceiverDomainType int), __ind_43): Ref)) == __ind_43 ); assume (forall o_3: Ref :: { invRecv27(o_3) } __f_16[invRecv27(o_3)] && (NoPerm < 1 / 10 && qpRange27(o_3)) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), invRecv27(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (__f_16[invRecv27(o_3)] && (NoPerm < 1 / 10 && qpRange27(o_3)) ==> (recApply((getreceiver(__c_16): ReceiverDomainType int), invRecv27(o_3)): Ref) == o_3 && QPMask[o_3, val] == Label_compLabell8Mask[o_3, val] - 1 / 10) && (!(__f_16[invRecv27(o_3)] && (NoPerm < 1 / 10 && qpRange27(o_3))) ==> QPMask[o_3, val] == Label_compLabell8Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> Label_compLabell8Mask[o_3, f_5] == QPMask[o_3, f_5] ); Label_compLabell8Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(Label_compLabell8Heap, ExhaleHeap, Label_compLabell8Mask); Label_compLabell8Heap := ExhaleHeap; // Stop execution assume false; } } } } assume false; } assume (forall __c_17: (FoldDomainType int int int), __f_17: (Set int) :: { (hfoldApply(__c_17, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Label_compLabell8Heap, __c_17, __f_17)), __c_17, __f_17)): int) } { (hfoldApply(__c_17, __snap_Int_Int_Int_val#frame(FrameFragment(__snap_Int_Int_Int_val#condqp1(Heap, __c_17, __f_17)), __c_17, __f_17)): int) } (filterReceiverGood(__f_17, (getreceiver(__c_17): ReceiverDomainType int)): bool) && (forall __ind_44: int :: { __f_17[__ind_44] } __f_17[__ind_44] ==> NoPerm < Mask[(recApply((getreceiver(__c_17): ReceiverDomainType int), __ind_44): Ref), val] ) ==> (filterReceiverGood(__f_17, (getreceiver(__c_17): ReceiverDomainType int)): bool) && ((_triggerDeleteKey1((hfoldApply(__c_17, __snap_Int_Int_Int_val(Heap, __c_17, __f_17)): int), (recInv((getreceiver(__c_17): ReceiverDomainType int), (loc(a_3, i6): Ref)): int)): bool) && (_triggerDeleteKey1((hfoldApply(__c_17, __snap_Int_Int_Int_val(Label_compLabell8Heap, __c_17, __f_17)): int), (recInv((getreceiver(__c_17): ReceiverDomainType int), (loc(a_3, i6): Ref)): int)): bool)) ); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: inhale (js intersection is) == Set[Int]() -- arrayTestChainIrrel3.vpr@535.3--535.44 assume Set#Equal(Set#Intersection(js, vis), (Set#Empty(): Set int)); assume state(Heap, Mask); assume state(Heap, Mask); // -- Translating statement: assert (hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), // __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), // add()): Fold[Int, Int, Int]), js)): Int) == // old((hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), // __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), // add()): Fold[Int, Int, Int]), js)): Int)) + // 3 -- arrayTestChainIrrel3.vpr@536.3--542.6 ExhaleWellDef0Mask := Mask; ExhaleWellDef0Heap := Heap; // -- Check definedness of (hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int) == old((hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int)) + 3 if (*) { // Exhale precondition of function application ExhaleWellDef1Mask := ExhaleWellDef0Mask; ExhaleWellDef1Heap := ExhaleWellDef0Heap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(js, (getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in js), (__ind2 in js) } (__ind1 in js) && ((__ind2 in js) && __ind1 != __ind2) ==> (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@537.35--538.74) [637]"} (filterReceiverGood(js, (getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int)): bool) || (forall __ind1_18: int, __ind2_18: int :: { js[__ind1_18], js[__ind2_18] } js[__ind1_18] && (js[__ind2_18] && __ind1_18 != __ind2_18) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind1_18): Ref) != (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind2_18): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@537.35--538.74) [638]"} (forall __ind_45: int :: { js[__ind_45] } js[__ind_45] && dummyFunction(ExhaleWellDef0Heap[(recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@537.35--538.74) [639]"} (forall __ind_45: int, __ind_45_1: int :: { neverTriggered28(__ind_45), neverTriggered28(__ind_45_1) } (((__ind_45 != __ind_45_1 && js[__ind_45]) && js[__ind_45_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref) != (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@537.35--538.74) [640]"} (forall __ind_45: int :: { js[__ind_45] } js[__ind_45] ==> ExhaleWellDef0Mask[(recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref) assume (forall __ind_45: int :: { js[__ind_45] } js[__ind_45] && NoPerm < 1 / 10 ==> qpRange28((recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref)) && invRecv28((recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_45): Ref)) == __ind_45 ); assume (forall o_3: Ref :: { invRecv28(o_3) } js[invRecv28(o_3)] && (NoPerm < 1 / 10 && qpRange28(o_3)) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), invRecv28(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (js[invRecv28(o_3)] && (NoPerm < 1 / 10 && qpRange28(o_3)) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), invRecv28(o_3)): Ref) == o_3 && QPMask[o_3, val] == ExhaleWellDef0Mask[o_3, val] - 1 / 10) && (!(js[invRecv28(o_3)] && (NoPerm < 1 / 10 && qpRange28(o_3))) ==> QPMask[o_3, val] == ExhaleWellDef0Mask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> ExhaleWellDef0Mask[o_3, f_5] == QPMask[o_3, f_5] ); ExhaleWellDef0Mask := QPMask; // Finish exhale havoc ExhaleHeap; assume IdenticalOnKnownLocations(ExhaleWellDef0Heap, ExhaleHeap, ExhaleWellDef0Mask); ExhaleWellDef0Heap := ExhaleHeap; // Stop execution assume false; } if (*) { // Exhale precondition of function application ExhaleWellDef1Mask := oldMask; ExhaleWellDef1Heap := oldHeap; assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Assertion (filterReceiverGood(js, (getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int])): Bool) || (forall __ind1: Int, __ind2: Int :: { (__ind1 in js), (__ind2 in js) } (__ind1 in js) && ((__ind2 in js) && __ind1 != __ind2) ==> (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind1): Ref) != (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind2): Ref)) might not hold. (arrayTestChainIrrel3.vpr@540.35--541.74) [641]"} (filterReceiverGood(js, (getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int)): bool) || (forall __ind1_19: int, __ind2_19: int :: { js[__ind1_19], js[__ind2_19] } js[__ind1_19] && (js[__ind2_19] && __ind1_19 != __ind2_19) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind1_19): Ref) != (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind2_19): Ref) ); havoc QPMask; // -- check that the permission amount is positive assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Fraction 1 / 10 might be negative. (arrayTestChainIrrel3.vpr@540.35--541.74) [642]"} (forall __ind_46: int :: { js[__ind_46] } js[__ind_46] && dummyFunction(oldHeap[(recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref), val]) ==> 1 / 10 >= NoPerm ); // -- check if receiver (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref) is injective assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. Quantified resource (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref).val might not be injective. (arrayTestChainIrrel3.vpr@540.35--541.74) [643]"} (forall __ind_46: int, __ind_46_1: int :: { neverTriggered29(__ind_46), neverTriggered29(__ind_46_1) } (((__ind_46 != __ind_46_1 && js[__ind_46]) && js[__ind_46_1]) && NoPerm < 1 / 10) && NoPerm < 1 / 10 ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref) != (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46_1): Ref) ); // -- check if sufficient permission is held assert {:msg " Precondition of function __snap_Int_Int_Int_val might not hold. There might be insufficient permission to access (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref).val (arrayTestChainIrrel3.vpr@540.35--541.74) [644]"} (forall __ind_46: int :: { js[__ind_46] } js[__ind_46] ==> oldMask[(recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref), val] >= 1 / 10 ); // -- assumptions for inverse of receiver (recApply((getreceiver((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int])): Receiver[Int]), __ind): Ref) assume (forall __ind_46: int :: { js[__ind_46] } js[__ind_46] && NoPerm < 1 / 10 ==> qpRange29((recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref)) && invRecv29((recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), __ind_46): Ref)) == __ind_46 ); assume (forall o_3: Ref :: { invRecv29(o_3) } js[invRecv29(o_3)] && (NoPerm < 1 / 10 && qpRange29(o_3)) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), invRecv29(o_3)): Ref) == o_3 ); // -- assume permission updates for field val assume (forall o_3: Ref :: { QPMask[o_3, val] } (js[invRecv29(o_3)] && (NoPerm < 1 / 10 && qpRange29(o_3)) ==> (recApply((getreceiver((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int)): ReceiverDomainType int), invRecv29(o_3)): Ref) == o_3 && QPMask[o_3, val] == oldMask[o_3, val]) && (!(js[invRecv29(o_3)] && (NoPerm < 1 / 10 && qpRange29(o_3))) ==> QPMask[o_3, val] == oldMask[o_3, val]) ); // -- assume permission updates for independent locations assume (forall o_3: Ref, f_5: (Field A B) :: { QPMask[o_3, f_5] } f_5 != val ==> oldMask[o_3, f_5] == QPMask[o_3, f_5] ); oldMask := QPMask; // Finish exhale // Stop execution assume false; } assert {:msg " Assert might fail. Assertion (hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int) == old((hfoldApply((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), __snap_Int_Int_Int_val((hfold(arrayRec(a), (mapIdentity(): Mapping[Int, Int]), add()): Fold[Int, Int, Int]), js)): Int)) + 3 might not hold. (arrayTestChainIrrel3.vpr@536.10--542.6) [645]"} (hfoldApply((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int), __snap_Int_Int_Int_val(Heap, (hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int), js)): int) == (hfoldApply((hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int), __snap_Int_Int_Int_val(oldHeap, (hfold((arrayRec(a_3): ReceiverDomainType int), (mapIdentity(): MappingDomainType int int), (add(): OperatorDomainType int)): FoldDomainType int int int), js)): int) + 3; assume state(Heap, Mask); }