From ce1c2de044c91624370411e23acab13b0381949b Mon Sep 17 00:00:00 2001 From: mikebarnett Date: Wed, 15 Jul 2009 21:03:41 +0000 Subject: Initial set of files. --- Test/test2/Answer | 359 +++++++++++++++ Test/test2/Arrays.bpl | 180 ++++++++ Test/test2/AssumeEnsures.bpl | 69 +++ Test/test2/Axioms.bpl | 29 ++ Test/test2/B.bpl | 86 ++++ Test/test2/Call.bpl | 60 +++ Test/test2/CallForall.bpl | 134 ++++++ Test/test2/CutBackEdge.bpl | 14 + Test/test2/Ensures.bpl | 75 +++ Test/test2/False.bpl | 16 + Test/test2/FormulaTerm.bpl | 139 ++++++ Test/test2/FormulaTerm2.bpl | 49 ++ Test/test2/Implies.bpl | 16 + Test/test2/LoopInvAssume.bpl | 20 + Test/test2/NeverPattern.bpl | 29 ++ Test/test2/NullaryMaps.bpl | 57 +++ Test/test2/Old.bpl | 132 ++++++ Test/test2/OldIllegal.bpl | 16 + Test/test2/Output | 359 +++++++++++++++ Test/test2/Passification.bpl | 169 +++++++ Test/test2/Quantifiers.bpl | 154 +++++++ Test/test2/Structured.bpl | 327 +++++++++++++ Test/test2/UpdateExpr.bpl | 81 ++++ Test/test2/Where.bpl | 163 +++++++ Test/test2/runtest.bat | 26 ++ Test/test2/sk_hack.bpl | 32 ++ Test/test2/strings-no-where.bpl | 995 ++++++++++++++++++++++++++++++++++++++++ Test/test2/strings-where.bpl | 995 ++++++++++++++++++++++++++++++++++++++++ 28 files changed, 4781 insertions(+) create mode 100644 Test/test2/Answer create mode 100644 Test/test2/Arrays.bpl create mode 100644 Test/test2/AssumeEnsures.bpl create mode 100644 Test/test2/Axioms.bpl create mode 100644 Test/test2/B.bpl create mode 100644 Test/test2/Call.bpl create mode 100644 Test/test2/CallForall.bpl create mode 100644 Test/test2/CutBackEdge.bpl create mode 100644 Test/test2/Ensures.bpl create mode 100644 Test/test2/False.bpl create mode 100644 Test/test2/FormulaTerm.bpl create mode 100644 Test/test2/FormulaTerm2.bpl create mode 100644 Test/test2/Implies.bpl create mode 100644 Test/test2/LoopInvAssume.bpl create mode 100644 Test/test2/NeverPattern.bpl create mode 100644 Test/test2/NullaryMaps.bpl create mode 100644 Test/test2/Old.bpl create mode 100644 Test/test2/OldIllegal.bpl create mode 100644 Test/test2/Output create mode 100644 Test/test2/Passification.bpl create mode 100644 Test/test2/Quantifiers.bpl create mode 100644 Test/test2/Structured.bpl create mode 100644 Test/test2/UpdateExpr.bpl create mode 100644 Test/test2/Where.bpl create mode 100644 Test/test2/runtest.bat create mode 100644 Test/test2/sk_hack.bpl create mode 100644 Test/test2/strings-no-where.bpl create mode 100644 Test/test2/strings-where.bpl (limited to 'Test/test2') diff --git a/Test/test2/Answer b/Test/test2/Answer new file mode 100644 index 00000000..7876d732 --- /dev/null +++ b/Test/test2/Answer @@ -0,0 +1,359 @@ + +-------------------- FormulaTerm.bpl -------------------- +FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold at this return statement. +FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold. +Execution trace: + FormulaTerm.bpl(8,1): start + +Boogie program verifier finished with 11 verified, 1 error + +-------------------- FormulaTerm2.bpl -------------------- +FormulaTerm2.bpl(39,5): Error BP5001: This assertion might not hold. +Execution trace: + FormulaTerm2.bpl(36,3): start +FormulaTerm2.bpl(47,5): Error BP5001: This assertion might not hold. +Execution trace: + FormulaTerm2.bpl(45,3): start + +Boogie program verifier finished with 2 verified, 2 errors + +-------------------- Passification.bpl -------------------- +Passification.bpl(44,3): Error BP5003: A postcondition might not hold at this return statement. +Passification.bpl(36,3): Related location: This is the postcondition that might not hold. +Execution trace: + Passification.bpl(39,1): A +Passification.bpl(116,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(106,1): L0 + Passification.bpl(111,1): L1 + Passification.bpl(115,1): L2 +Passification.bpl(151,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(144,1): L0 + Passification.bpl(150,1): L2 +Passification.bpl(165,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(158,1): L0 + Passification.bpl(161,1): L1 + Passification.bpl(164,1): L2 + +Boogie program verifier finished with 7 verified, 4 errors + +-------------------- B.bpl -------------------- + +Boogie program verifier finished with 4 verified, 0 errors + +-------------------- Ensures.bpl -------------------- +Ensures.bpl(30,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(28,3): start +Ensures.bpl(35,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(34,3): start +Ensures.bpl(41,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(39,3): start +Ensures.bpl(47,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(45,3): start +Ensures.bpl(72,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(70,3): start + +Boogie program verifier finished with 5 verified, 5 errors + +-------------------- Old.bpl -------------------- +Old.bpl(29,5): Error BP5003: A postcondition might not hold at this return statement. +Old.bpl(26,3): Related location: This is the postcondition that might not hold. +Execution trace: + Old.bpl(28,3): start + +Boogie program verifier finished with 7 verified, 1 error + +-------------------- OldIllegal.bpl -------------------- +OldIllegal.bpl(7,11): Error: old expressions allowed only in two-state contexts +OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts +2 name resolution errors detected in OldIllegal.bpl + +-------------------- Arrays.bpl -------------------- +Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement. +Arrays.bpl(38,3): Related location: This is the postcondition that might not hold. +Execution trace: + Arrays.bpl(42,3): start +Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement. +Arrays.bpl(119,3): Related location: This is the postcondition that might not hold. +Execution trace: + Arrays.bpl(123,3): start + +Boogie program verifier finished with 8 verified, 2 errors + +-------------------- Axioms.bpl -------------------- +Axioms.bpl(19,5): Error BP5001: This assertion might not hold. +Execution trace: + Axioms.bpl(18,3): start + +Boogie program verifier finished with 2 verified, 1 error + +-------------------- Quantifiers.bpl -------------------- +Quantifiers.bpl(20,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(19,3): start +Quantifiers.bpl(43,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(42,3): start +Quantifiers.bpl(65,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(64,3): start +Quantifiers.bpl(73,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(71,3): start +Quantifiers.bpl(125,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(124,3): start +Quantifiers.bpl(150,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(149,3): start + +Boogie program verifier finished with 8 verified, 6 errors + +-------------------- Call.bpl -------------------- +Call.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Call.bpl(9,3): entry +Call.bpl(46,5): Error BP5001: This assertion might not hold. +Execution trace: + Call.bpl(45,3): start +Call.bpl(55,5): Error BP5003: A postcondition might not hold at this return statement. +Call.bpl(20,3): Related location: This is the postcondition that might not hold. +Execution trace: + Call.bpl(53,3): start + +Boogie program verifier finished with 2 verified, 3 errors + +-------------------- AssumeEnsures.bpl -------------------- +AssumeEnsures.bpl(28,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(26,5): entry +AssumeEnsures.bpl(47,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(46,5): entry +AssumeEnsures.bpl(62,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(60,5): entry + +Boogie program verifier finished with 4 verified, 3 errors + +-------------------- CutBackEdge.bpl -------------------- +CutBackEdge.bpl(10,5): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + CutBackEdge.bpl(5,3): entry + CutBackEdge.bpl(9,3): block850 + +Boogie program verifier finished with 0 verified, 1 error + +-------------------- False.bpl -------------------- + +Boogie program verifier finished with 2 verified, 0 errors + +-------------------- LoopInvAssume.bpl -------------------- +LoopInvAssume.bpl(18,7): Error BP5001: This assertion might not hold. +Execution trace: + LoopInvAssume.bpl(8,4): entry + LoopInvAssume.bpl(16,4): exit + +Boogie program verifier finished with 0 verified, 1 error + +-------------------- strings-no-where.bpl -------------------- +strings-no-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) +strings-no-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) +strings-no-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) +strings-no-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any) +strings-no-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator == +18 type checking errors detected in strings-no-where.bpl + +-------------------- strings-where.bpl -------------------- +strings-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) +strings-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) +strings-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) +strings-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any) +strings-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator == +18 type checking errors detected in strings-where.bpl + +-------------------- Structured.bpl -------------------- +Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement. +Structured.bpl(243,3): Related location: This is the postcondition that might not hold. +Execution trace: + Structured.bpl(245,3): anon0 + Structured.bpl(245,3): anon6_LoopHead + Structured.bpl(246,5): anon6_LoopBody + Structured.bpl(247,7): anon7_LoopBody + Structured.bpl(252,5): anon4 + Structured.bpl(252,14): anon9_Then +Structured.bpl(303,3): Error BP5001: This assertion might not hold. +Execution trace: + Structured.bpl(299,5): anon0 + Structured.bpl(300,3): anon3_Else + Structured.bpl(303,3): anon2 +Structured.bpl(311,7): Error BP5001: This assertion might not hold. +Execution trace: + Structured.bpl(308,3): anon0 + Structured.bpl(308,3): anon1_Then + Structured.bpl(309,5): A + +Boogie program verifier finished with 15 verified, 3 errors + +-------------------- Where.bpl -------------------- +Where.bpl(8,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(6,3): anon0 +Where.bpl(22,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(16,5): anon0 +Where.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(30,3): anon0 +Where.bpl(44,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(40,5): anon0 +Where.bpl(57,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(52,3): anon0 +Where.bpl(111,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(102,5): anon0 + Where.bpl(104,3): anon3_LoopHead + Where.bpl(110,3): anon2 +Where.bpl(128,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(121,5): anon0 + Where.bpl(122,3): anon3_LoopHead + Where.bpl(125,3): anon2 +Where.bpl(145,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(138,5): anon0 + Where.bpl(139,3): anon3_LoopHead + Where.bpl(142,3): anon2 +Where.bpl(162,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(155,5): anon0 + Where.bpl(156,3): anon3_LoopHead + Where.bpl(159,3): anon2 + +Boogie program verifier finished with 2 verified, 9 errors + +-------------------- UpdateExpr.bpl -------------------- +UpdateExpr.bpl(14,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(14,3): anon0 +UpdateExpr.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(19,3): anon0 +UpdateExpr.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(32,3): anon0 +UpdateExpr.bpl(38,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(38,3): anon0 +UpdateExpr.bpl(52,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(51,5): anon0 + +Boogie program verifier finished with 5 verified, 5 errors + +-------------------- NeverPattern.bpl -------------------- +NeverPattern.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(15,3): anon0 +NeverPattern.bpl(22,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(21,3): anon0 +NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(27,3): anon0 + +Boogie program verifier finished with 1 verified, 3 errors + +-------------------- NullaryMaps.bpl -------------------- +NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(28,3): anon0 +NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(28,3): anon0 +NullaryMaps.bpl(36,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(36,3): anon0 + +Boogie program verifier finished with 2 verified, 3 errors + +-------------------- Implies.bpl -------------------- +Implies.bpl(12,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(11,3): anon0 +Implies.bpl(15,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(11,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors +-------------------- sk_hack.bpl -------------------- + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- CallForall.bpl -------------------- +CallForall.bpl(17,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(17,3): anon0 +CallForall.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(28,3): anon0 +CallForall.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(40,3): anon0 +CallForall.bpl(47,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(46,3): anon0 +CallForall.bpl(75,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(75,3): anon0 +CallForall.bpl(111,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(109,3): anon0 +CallForall.bpl(118,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(117,3): anon0 +CallForall.bpl(125,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(124,3): anon0 + +Boogie program verifier finished with 10 verified, 8 errors diff --git a/Test/test2/Arrays.bpl b/Test/test2/Arrays.bpl new file mode 100644 index 00000000..d0f712c9 --- /dev/null +++ b/Test/test2/Arrays.bpl @@ -0,0 +1,180 @@ +// -------------------- 1-dimensional arrays -------------------- + +var A: [ref]int; + +procedure P0(o: ref, q: ref, y: int) + requires o != q; + modifies A; + ensures A[o] == old(A[o]) + y; + ensures (forall p: ref :: A[p] == old(A[p]) || p == o); +{ + var k: int; + + start: + k := A[q]; + A[o] := y + A[o]; + A[q] := k; + return; +} + +procedure P1(o: ref, q: ref, y: int) + // This procedure does not have the assumption that o != q. + modifies A; + // It also does not ensures anything about A[o] + ensures (forall p: ref :: A[p] == old(A[p]) || p == o); +{ + var k: int; + + start: + k := A[q]; + A[o] := y + A[o]; + A[q] := k; + return; +} + +procedure P2(o: ref, q: ref, y: int) + // This procedure does not have the assumption that o != q. + modifies A; + ensures A[o] == old(A[o]) + y; +{ + var k: int; + + start: + k := A[q]; + A[o] := y + A[o]; + A[q] := k; + return; +} // error: postcondition violated (if o == q) + +// -------------------- 2-dimensional arrays -------------------- + +var B: [ref,name]int; +const F: name; + +procedure Q0(o: ref, q: ref, y: int, G: name) + requires o != q && F != G; + modifies B; + ensures B[o,F] == old(B[o,F]) + y; + ensures (forall p: ref, f: name :: B[p,f] == old(B[p,f]) || + (p == o && f == F)); +{ + var k: int; + + start: + k := B[q,G]; + B[o,F] := y + B[o,F]; + B[q,G] := k; + return; +} + +procedure Q1(o: ref, q: ref, y: int, G: name) + // This procedure does not have the assumption that o != q && F != G. + modifies B; + // It also does not ensures anything about B[o,F] + ensures (forall p: ref, f: name :: B[p,f] == old(B[p,f]) || + (p == o && f == F)); +{ + var k: int; + + start: + k := B[q,G]; + B[o,F] := y + B[o,F]; + B[q,G] := k; + return; +} + +procedure Q2(o: ref, q: ref, y: int, G: name) + requires F != G; + // This procedure does not have the assumption that o != q. + modifies B; + ensures B[o,F] == old(B[o,F]) + y; +{ + var k: int; + + start: + k := B[q,G]; + B[o,F] := y + B[o,F]; + B[q,G] := k; + return; +} + +procedure Q3(o: ref, q: ref, y: int, G: name) + requires o != q; + // This procedure does not have the assumption that F != G. + modifies B; + ensures B[o,F] == old(B[o,F]) + y; +{ + var k: int; + + start: + k := B[q,G]; + B[o,F] := y + B[o,F]; + B[q,G] := k; + return; +} + +procedure Q4(o: ref, q: ref, y: int, G: name) + // This procedure does not have either of the assumptions o != q and F != G. + modifies B; + ensures B[o,F] == old(B[o,F]) + y; +{ + var k: int; + + start: + k := B[q,G]; + B[o,F] := y + B[o,F]; + B[q,G] := k; + return; +} // error: postcondition violated + +// -------------------- more tests -------------------- + +procedure Skip0(o: ref, q: ref, G: name, H: name) + modifies A,B; + ensures (forall p: ref :: A[p] == old(A[p])); + ensures (forall p: ref, g: name :: B[p,g] == old(B[p,g])); +{ + start: + return; +} + +procedure Skip1(o: ref, q: ref, G: name, H: name) + modifies A,B; + ensures (forall p: ref :: A[p] == old(A[p])); + ensures (forall p: ref, g: name :: B[p,g] == old(B[p,g])); +{ + var k: int; + var l: int; + + start: + k := A[o]; + l := A[q]; + goto oneWay, theOtherWay; + + oneWay: + A[o] := k; + A[q] := l; + goto next; + + theOtherWay: + A[q] := l; + A[o] := k; + goto next; + + next: + k := B[o,G]; + l := B[q,H]; + goto Lx, Ly; + + Lx: + B[o,G] := k; + B[q,H] := l; + return; + + Ly: + B[q,H] := l; + B[o,G] := k; + return; +} + +type name, ref; diff --git a/Test/test2/AssumeEnsures.bpl b/Test/test2/AssumeEnsures.bpl new file mode 100644 index 00000000..901c06c8 --- /dev/null +++ b/Test/test2/AssumeEnsures.bpl @@ -0,0 +1,69 @@ +var g: int; + +procedure Foo() returns (); + modifies g; + free ensures 0 <= g; + +implementation Foo() returns () +{ + entry: + g := g + 1; + return; +} + +procedure BarGood() returns () + modifies g; +{ + entry: + call Foo(); + assert 0 <= g; + return; +} + +procedure BarBad() returns () + modifies g; +{ + entry: + call Foo(); + assert 0 < g; + return; +} + +// ----- Free preconditions + +procedure Proc() returns (); + free requires g == 15; + +implementation Proc() returns () +{ + entry: + assert g > 10; // yes, this condition can be used here + return; +} + +implementation Proc() returns () +{ + entry: + assert g < 10; // error + return; +} + +procedure Caller0() returns () +{ + entry: + call Proc(); // yes, legal, since the precondition is not checked + return; +} + +procedure Caller1() returns () +{ + entry: + call Proc(); + assert g > 10; // error, because: + // Free preconditions are ignored (that is, treated as "skip") for the caller. + // This is a BoogiePL design choice. Another alternative would be to treat free + // preconditions as assume commands also on the caller side, either in the order + // that all preconditions are given, or before or after all the checked preconditions + // have been checked. + return; +} diff --git a/Test/test2/Axioms.bpl b/Test/test2/Axioms.bpl new file mode 100644 index 00000000..4fe7a8a7 --- /dev/null +++ b/Test/test2/Axioms.bpl @@ -0,0 +1,29 @@ +const Seven: int; +axiom Seven == 7; + +function inc(int) returns (int); +axiom (forall j: int :: inc(j) == j+1); + +procedure P() +{ + start: + assert 4 <= Seven; + assert Seven < inc(Seven); + assert inc(5) + inc(inc(2)) == Seven + 3; + return; +} + +procedure Q() +{ + start: + assert inc(5) + inc(inc(2)) == Seven; // error + return; +} + +function inc2(x:int) returns(int) { x + 2 } + +procedure ExpandTest() +{ + var q:int; + assert inc(inc(q)) == inc2(q); +} diff --git a/Test/test2/B.bpl b/Test/test2/B.bpl new file mode 100644 index 00000000..553d5002 --- /dev/null +++ b/Test/test2/B.bpl @@ -0,0 +1,86 @@ +// ----------- BEGIN PRELUDE + +var Heap: [ref, name]int; +const N: name; + +procedure Q0() +{ + var h: int; + + entry: + goto Else; + + Then: + h := 15; + goto end; + + Else: + assume h == 0; + goto end; + + end: + assert 0 <= h; + return; +} + +procedure Q1() +{ + var h: int; + + entry: + goto Else; + + Then: + h := -15; + goto end; + + Else: + assume h == 0; + goto end; + + end: + h := -h; + assert 0 <= h; + return; +} + +procedure P0(this: ref) + modifies Heap; +{ + entry: + goto Else; + + Then: + Heap[this, N] := 15; + goto end; + + Else: + assume Heap[this, N] == 0; + goto end; + + end: + assert 0 <= Heap[this, N]; + return; +} + +procedure P1(this: ref) + modifies Heap; +{ + entry: + goto Else; + + Then: + Heap[this, N] := -15; + goto end; + + Else: + assume Heap[this, N] == 0; + goto end; + + end: + Heap[this, N] := -Heap[this, N]; + assert 0 <= Heap[this, N]; + return; +} + +type name, ref; diff --git a/Test/test2/Call.bpl b/Test/test2/Call.bpl new file mode 100644 index 00000000..c1de1e71 --- /dev/null +++ b/Test/test2/Call.bpl @@ -0,0 +1,60 @@ +procedure Bar() returns (barresult: ref); + +procedure Foo(); + +implementation Foo() +{ + var x: ref; + + entry: + call x := Bar(); + assume x == null; + call x := Bar(); + assert x == null; + return; + +} + +procedure DifferentFormalNames(x: int, y: int) returns (z: int); + requires x < y; + ensures z == x; + +implementation DifferentFormalNames(x: int, y: int) returns (z: int) +{ + start: + assert x < y; + z := x; + return; +} + +implementation DifferentFormalNames(y: int, x: int) returns (w: int) +{ + start: + goto A, B; + A: + assert y < x; + assume false; + return; + B: + w := y; + return; +} + +implementation DifferentFormalNames(y: int, x: int) returns (w: int) +{ + start: + assert x < y; // error + w := y; + return; +} + +implementation DifferentFormalNames(y: int, x: int) returns (w: int) +{ + start: + w := x; + return; // error: postcondition violation +} + +type ref; + +const null : ref; diff --git a/Test/test2/CallForall.bpl b/Test/test2/CallForall.bpl new file mode 100644 index 00000000..98a62103 --- /dev/null +++ b/Test/test2/CallForall.bpl @@ -0,0 +1,134 @@ +function G(int) returns (int); +axiom (forall x: int :: { G(x) } 0 <= x ==> G(x) == x); + +function F(int) returns (int); +axiom (forall x: int :: { F(G(x)) } 0 <= x ==> F(G(x)) == 5); + +procedure Lemma(y: int) + requires 0 <= y; + ensures F(y) == 5; +{ + // proof: + assert G(y) == y; +} + +procedure Main0() +{ + assert F(2) == 5; // error: cannot prove this directly, because of the trigger +} + +procedure Main1() +{ + call Lemma(2); + assert F(2) == 5; +} + +procedure Main2() +{ + call Lemma(3); + assert F(2) == 5; // error: Lemma was instantiated the wrong way +} + +procedure Main3() +{ + call forall Lemma(*); + assert F(2) == 5; +} + +procedure Main4() +{ + call forall Lemma(*); + assert false; // error +} + +procedure Main5(z: int) +{ + call forall Lemma(*); + assert F(z) == 5; // error: z might be negative +} + +procedure Main6(z: int) + requires 0 <= z; +{ + call forall Lemma(*); + assert F(z) == 5; +} + +// ------------ several parameters + +function K(int, int) returns (int); +axiom (forall x: int, y: int :: { K(G(x), G(y)) } 0 <= x && 0 <= y ==> K(G(x), G(y)) == 25); + +procedure MultivarLemma(x: int, y: int) + requires 0 <= x; + requires 0 <= y; + ensures K(x,y) == 25; +{ + // proof: + assert G(x) == x; + assert G(y) == y; +} + +procedure Multi0(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + assert K(x,y) == 25; // error +} + +procedure Multi1(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + call MultivarLemma(x, y); + assert K(x,y) == 25; +} + +procedure Multi2(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + call forall MultivarLemma(x, y); + assert K(x,y) == 25; +} + +procedure Multi3(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + call forall MultivarLemma(*, y); + assert K(x,y) == 25; +} + +procedure Multi4(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + call forall MultivarLemma(x, *); + assert K(x,y) == 25; +} + +procedure Multi5(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + call forall MultivarLemma(2 + 100, *); + assert K(102, y) == 25; + assert false; // error +} + +procedure Multi6(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + call forall MultivarLemma(*, y); + assert K(x+2,y+2) == 25; // error +} + +procedure Multi7(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + call forall MultivarLemma(x, *); + assert K(x+2,y+2) == 25; // error +} + +procedure Multi8(x: int, y: int) + requires 0 <= x && 0 <= y; +{ + call forall MultivarLemma(*, *); + assert K(x+2,y+2) == 25; // that's the ticket! +} + diff --git a/Test/test2/CutBackEdge.bpl b/Test/test2/CutBackEdge.bpl new file mode 100644 index 00000000..934974aa --- /dev/null +++ b/Test/test2/CutBackEdge.bpl @@ -0,0 +1,14 @@ +procedure Test() +{ + var i: int; + + entry: + i := 0; + goto block850; + + block850: + assert i == 0; + havoc i; + goto block850; + +} diff --git a/Test/test2/Ensures.bpl b/Test/test2/Ensures.bpl new file mode 100644 index 00000000..4e36c108 --- /dev/null +++ b/Test/test2/Ensures.bpl @@ -0,0 +1,75 @@ +var H: [ref,name]int; +var that: ref; + +const X: name; +const Y: name; + +procedure P(this: ref); + modifies H; + ensures H[this,X] == 5; + +implementation P(this: ref) { + start: + H[this,X] := 5; + return; +} + +procedure Q(this: ref); + modifies H; + ensures (forall o: ref, F: name :: o == this && F == X ==> H[o,F] == 5); + +implementation Q(this: ref) { + start: + H[this,X] := 5; + return; +} + +implementation Q(this: ref) { + start: + H[this,X] := 7; + return; // error +} + +implementation Q(this: ref) { + start: + return; // error +} + +implementation Q(this: ref) { + start: + H[that,X] := 5; + return; // error +} + +implementation Q(this: ref) { + start: + H[this,Y] := 5; + return; // error +} + +implementation Q(this: ref) { + start: + call P(this); + return; +} + +implementation Q(this: ref) { + start: + call Q(this); + return; +} + +implementation Q(this: ref) { + start: + call P(this); + call Q(this); + return; +} + +implementation Q(this: ref) { + start: + call P(that); + return; // error +} + +type name, ref; diff --git a/Test/test2/False.bpl b/Test/test2/False.bpl new file mode 100644 index 00000000..3fe14865 --- /dev/null +++ b/Test/test2/False.bpl @@ -0,0 +1,16 @@ +procedure Test1() +{ + entry: + assert !true == false; + return; +} + +procedure Test2() +{ + var b: bool; + + entry: + assume b != false; + assert b; + return; +} diff --git a/Test/test2/FormulaTerm.bpl b/Test/test2/FormulaTerm.bpl new file mode 100644 index 00000000..e14707cb --- /dev/null +++ b/Test/test2/FormulaTerm.bpl @@ -0,0 +1,139 @@ +// Test formula-term distinction in Simplify + +procedure plus(x: int, y: int) returns (z: int); + ensures z == x + y; + +implementation plus(x: int, y: int) returns (z: int) +{ +start: + assume z == 3; + return; // ERROR: postcondition possibly violated +} + +implementation plus(x: int, y: int) returns (z: int) +{ +start: + z := x + y; + return; +} + +implementation plus(x: int, y: int) returns (z: int) +{ +start: + z := x + y; + z := 0 + z; + return; +} + +procedure plus2(x: int, y: int) returns (z: int) + ensures z == x + y; +{ +start: + z := x + y; + return; +} + +procedure or(x: int, y: int, a: int, b: int) returns (z: int) + requires a == b; +{ +var t: bool; +start: + t := (x < y || x > y || x == y || x != y) && a >= b && a <= b; + assert (x < y || x > y || x == y || x != y) && a >= b && a <= b; + assert t; + return; +} + +procedure less(x: int, y: int) returns (z: bool); + requires x < y; + ensures z == (x < y); + +implementation less(x: int, y: int) returns (z: bool) +{ +start: + z := x < y; + return; +} + +implementation less(x: int, y: int) returns (z: bool) +{ +start: + goto yes, no; +yes: + assume x < y; + z := true; + return; +no: + assume !(x < y); + z := false; + return; +} + +implementation less(x: int, y: int) returns (z: bool) +{ +start: + goto yes, no; +yes: + assume x < y; + z := true; + return; +no: + assume x >= y; + z := false; + return; +} + +procedure LESS(x: int, y: int) returns (z: bool); + requires x < y; + ensures z <==> (x < y); + +implementation LESS(x: int, y: int) returns (z: bool) +{ +start: + z := x < y; + return; +} + +implementation LESS(x: int, y: int) returns (z: bool) +{ +start: + goto yes, no; +yes: + assume x < y; + z := true; + return; +no: + assume !(x < y); + z := false; + return; +} + +implementation LESS(x: int, y: int) returns (z: bool) +{ +start: + goto yes, no; +yes: + assume x < y; + z := true; + return; +no: + assume x >= y; + z := false; + return; +} + +procedure Assignments() +{ + var b: bool; + var c: bool; + var d: bool; + var x: bool, y: bool; + + entry: + b := c || d; + b := c && d; + x := c <==> d; + y := c ==> d; + assert x ==> y; + return; +} diff --git a/Test/test2/FormulaTerm2.bpl b/Test/test2/FormulaTerm2.bpl new file mode 100644 index 00000000..6c5e4bf3 --- /dev/null +++ b/Test/test2/FormulaTerm2.bpl @@ -0,0 +1,49 @@ +// This file has been created to test some of the formula/term issues in Zap. +// However, the test harness does not specify any particular prover to be used, +// since these tests should pass regardless of which prover is used. + +procedure P() +{ + var a: int, b: int, t: bool; + + start: + assume a == b; + t := a == b; + assert t; + return; +} + +function f(bool) returns (int); +const A: int; +const B: int; + +axiom f(A < B) == 5; + +procedure Q() +{ + start: + assume A < B; + assert f(true) == 5; + return; +} + +// ----- and now some erroneous procedures + +procedure PX() +{ + var a: int, b: int, t: bool; + + start: + assume a == b; + t := a == b; + assert !t; // error + return; +} + +procedure QX() +{ + start: + assume A < B; + assert f(true) < 2; // error + return; +} diff --git a/Test/test2/Implies.bpl b/Test/test2/Implies.bpl new file mode 100644 index 00000000..3034f973 --- /dev/null +++ b/Test/test2/Implies.bpl @@ -0,0 +1,16 @@ + +const a:bool; +const b:bool; +const c:bool; +const d:bool; + +function f(int) returns (bool); +axiom (forall x:int :: f(x) <== x >= 0); + +procedure P() { + assert (a ==> (b ==> c) ==> d) == (d <== (c <== b) <== a); + assert (a ==> b ==> c) == (c <== (a ==> b)); // error + + assert f(23); + assert f(-5); // error +} \ No newline at end of file diff --git a/Test/test2/LoopInvAssume.bpl b/Test/test2/LoopInvAssume.bpl new file mode 100644 index 00000000..1304e668 --- /dev/null +++ b/Test/test2/LoopInvAssume.bpl @@ -0,0 +1,20 @@ +// Check that assumes in loop invariants are handled correctly + +var x : int; + +procedure Test() + modifies x; +{ + entry: + goto loophead, exit; + + loophead: + assume x >= 0; + x := 0; + goto loophead, exit; + + exit: + assume x < 0; + assert false; + return; +} diff --git a/Test/test2/NeverPattern.bpl b/Test/test2/NeverPattern.bpl new file mode 100644 index 00000000..f0478077 --- /dev/null +++ b/Test/test2/NeverPattern.bpl @@ -0,0 +1,29 @@ +function {:never_pattern true} f1(x:int) returns(int); +function {:never_pattern false} f2(x:int) returns(int); +function f3(x:int) returns(int); + + +procedure foo() +{ + assume (forall x : int :: f1(x) > 0 && f2(x) > 0 && f3(x) > 0); + assert f2(3) > 0; + assert f3(4) > 0; +} + +procedure bar() +{ + assume (forall x : int :: f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); + assert f1(3) > 0; +} + +procedure bar1() +{ + assume (forall x : int :: {:nopats f2(x)} f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); + assert f1(3) > 0; +} + +procedure bar2() +{ + assume (forall x : int :: {:nopats f2(x)} f1(x) > 0 && f2(x) > 0 && f3(x) > 0 && f1(7) == 3); + assert f2(3) > 0; +} diff --git a/Test/test2/NullaryMaps.bpl b/Test/test2/NullaryMaps.bpl new file mode 100644 index 00000000..1bc18c41 --- /dev/null +++ b/Test/test2/NullaryMaps.bpl @@ -0,0 +1,57 @@ +// aren't these cool! + +var m: []int; +var p: []a; + +type ref; +const null: ref; + +procedure P() + requires m[] == 5; + modifies m; + modifies p; + ensures m[] == 30; + ensures p[] == null; +{ + m[] := 12; + p[] := 12; + p[] := true; + assert p[] == m[]; + assert p[]; + m := m[:= 30]; + p := p[:=null]; +} + +procedure Q() + modifies m; +{ + assert m[] == 5; // error + m[] := 30; + assert m[] == 5; // error +} + +procedure R() + modifies p; +{ + assert p[] < 3; // error +} + +// ---- + +type Field a; +type HeapType = [ref, Field a]a; +const F0: Field int; +const F1: Field bool; +const alloc: Field bool; +var Heap: HeapType; +procedure FrameCondition(this: ref) + modifies Heap; + ensures (forall o: ref, f: Field a :: + Heap[o,f] == old(Heap)[o,f] || + !old(Heap)[o,alloc] || + (o == this && f == F0) || + (o == this && f == F1) + ); +{ +} + diff --git a/Test/test2/Old.bpl b/Test/test2/Old.bpl new file mode 100644 index 00000000..00f798bc --- /dev/null +++ b/Test/test2/Old.bpl @@ -0,0 +1,132 @@ +var x: int; +var y: int; + +procedure P() + modifies x; + ensures x == old(x) + 1; +{ + start: + x := 1 + x; + return; +} + +procedure Q(); + modifies x; + ensures x == old(x) + 1; + +implementation Q() +{ + start: + x := 1 + x; + return; +} + +procedure R() + modifies x; + ensures x == old(x) + 1; +{ + start: + return; +} // error: does not establish postcondition + +procedure Swap() + modifies x, y; + ensures x == old(y) && y == old(x); +{ + var t: int; + + start: + goto A, B; + A: + t := x; + x := y; + y := t; + goto end; + B: + x := x - y; // x == old(x) - old(y) + y := y + x; // y == old(y) + (old(x) - old(y)) == old(x) + x := y - x; // x == old(x) - (old(x) - old(y)) == old(y) + goto end; + end: + return; +} + +procedure OutParam0(x: int) returns (y: int) + ensures y == x + 1; +{ + start: + y := x + 1; + return; +} + +// OutParam1 is like OutParam0, except that there's now a separate +// implementation declaration, which means that the specification +// and body use different AST nodes for the formal parameters. This +// may make a difference in the various substitutions going on. +// (Indeed, a previous bug caused OutParam0 to verify but not OutParam1.) +procedure OutParam1(x: int) returns (y: int); + ensures y == x + 1; +implementation OutParam1(x: int) returns (y: int) +{ + start: + y := x + 1; + return; +} + +var a: [ref]int; +var b: [ref]int; + +procedure SwapElems(o: ref) returns (p: ref) + modifies a, b; + ensures a[o] == old(b[p]) && b[o] == old(a[p]); +{ + var ta: int, tb: int; + + start: + goto A, B, C; + A: + havoc p; + goto B, C; + B: + ta := a[p]; + tb := b[p]; + a[o] := tb; + b[o] := ta; + return; + C: + assume a[o] == b[o];assume false; + + p := o; + return; +} + + + +//------------------------------------------------------------------------- +// Test old in Boogie PL code +//------------------------------------------------------------------------- + +var Global0: int; + +// Good +procedure OldInCode0() + requires Global0 >= 0; + ensures Global0 <= old(Global0) + 1; + modifies Global0; +{ + var local0: int; + + start: + goto A,B; + A: + assert Global0 == old(Global0); + return; + + B: + local0 := Global0 + 1; + local0 := local0 - 1; + Global0 := old(local0 + 1); + return; +} + +type ref; diff --git a/Test/test2/OldIllegal.bpl b/Test/test2/OldIllegal.bpl new file mode 100644 index 00000000..342c5b19 --- /dev/null +++ b/Test/test2/OldIllegal.bpl @@ -0,0 +1,16 @@ +// Test old appearing in illegal locations + +var Global0: int; + +// Bad +procedure OldInCode1() + requires old(Global0) == 0; +{ + start: + return; +} + +// Bad +axiom (forall o:ref :: old(o) == o); + +type ref; diff --git a/Test/test2/Output b/Test/test2/Output new file mode 100644 index 00000000..7876d732 --- /dev/null +++ b/Test/test2/Output @@ -0,0 +1,359 @@ + +-------------------- FormulaTerm.bpl -------------------- +FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold at this return statement. +FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold. +Execution trace: + FormulaTerm.bpl(8,1): start + +Boogie program verifier finished with 11 verified, 1 error + +-------------------- FormulaTerm2.bpl -------------------- +FormulaTerm2.bpl(39,5): Error BP5001: This assertion might not hold. +Execution trace: + FormulaTerm2.bpl(36,3): start +FormulaTerm2.bpl(47,5): Error BP5001: This assertion might not hold. +Execution trace: + FormulaTerm2.bpl(45,3): start + +Boogie program verifier finished with 2 verified, 2 errors + +-------------------- Passification.bpl -------------------- +Passification.bpl(44,3): Error BP5003: A postcondition might not hold at this return statement. +Passification.bpl(36,3): Related location: This is the postcondition that might not hold. +Execution trace: + Passification.bpl(39,1): A +Passification.bpl(116,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(106,1): L0 + Passification.bpl(111,1): L1 + Passification.bpl(115,1): L2 +Passification.bpl(151,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(144,1): L0 + Passification.bpl(150,1): L2 +Passification.bpl(165,3): Error BP5001: This assertion might not hold. +Execution trace: + Passification.bpl(158,1): L0 + Passification.bpl(161,1): L1 + Passification.bpl(164,1): L2 + +Boogie program verifier finished with 7 verified, 4 errors + +-------------------- B.bpl -------------------- + +Boogie program verifier finished with 4 verified, 0 errors + +-------------------- Ensures.bpl -------------------- +Ensures.bpl(30,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(28,3): start +Ensures.bpl(35,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(34,3): start +Ensures.bpl(41,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(39,3): start +Ensures.bpl(47,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(45,3): start +Ensures.bpl(72,5): Error BP5003: A postcondition might not hold at this return statement. +Ensures.bpl(19,3): Related location: This is the postcondition that might not hold. +Execution trace: + Ensures.bpl(70,3): start + +Boogie program verifier finished with 5 verified, 5 errors + +-------------------- Old.bpl -------------------- +Old.bpl(29,5): Error BP5003: A postcondition might not hold at this return statement. +Old.bpl(26,3): Related location: This is the postcondition that might not hold. +Execution trace: + Old.bpl(28,3): start + +Boogie program verifier finished with 7 verified, 1 error + +-------------------- OldIllegal.bpl -------------------- +OldIllegal.bpl(7,11): Error: old expressions allowed only in two-state contexts +OldIllegal.bpl(14,23): Error: old expressions allowed only in two-state contexts +2 name resolution errors detected in OldIllegal.bpl + +-------------------- Arrays.bpl -------------------- +Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement. +Arrays.bpl(38,3): Related location: This is the postcondition that might not hold. +Execution trace: + Arrays.bpl(42,3): start +Arrays.bpl(127,5): Error BP5003: A postcondition might not hold at this return statement. +Arrays.bpl(119,3): Related location: This is the postcondition that might not hold. +Execution trace: + Arrays.bpl(123,3): start + +Boogie program verifier finished with 8 verified, 2 errors + +-------------------- Axioms.bpl -------------------- +Axioms.bpl(19,5): Error BP5001: This assertion might not hold. +Execution trace: + Axioms.bpl(18,3): start + +Boogie program verifier finished with 2 verified, 1 error + +-------------------- Quantifiers.bpl -------------------- +Quantifiers.bpl(20,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(19,3): start +Quantifiers.bpl(43,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(42,3): start +Quantifiers.bpl(65,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(64,3): start +Quantifiers.bpl(73,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(71,3): start +Quantifiers.bpl(125,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(124,3): start +Quantifiers.bpl(150,5): Error BP5001: This assertion might not hold. +Execution trace: + Quantifiers.bpl(149,3): start + +Boogie program verifier finished with 8 verified, 6 errors + +-------------------- Call.bpl -------------------- +Call.bpl(13,5): Error BP5001: This assertion might not hold. +Execution trace: + Call.bpl(9,3): entry +Call.bpl(46,5): Error BP5001: This assertion might not hold. +Execution trace: + Call.bpl(45,3): start +Call.bpl(55,5): Error BP5003: A postcondition might not hold at this return statement. +Call.bpl(20,3): Related location: This is the postcondition that might not hold. +Execution trace: + Call.bpl(53,3): start + +Boogie program verifier finished with 2 verified, 3 errors + +-------------------- AssumeEnsures.bpl -------------------- +AssumeEnsures.bpl(28,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(26,5): entry +AssumeEnsures.bpl(47,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(46,5): entry +AssumeEnsures.bpl(62,9): Error BP5001: This assertion might not hold. +Execution trace: + AssumeEnsures.bpl(60,5): entry + +Boogie program verifier finished with 4 verified, 3 errors + +-------------------- CutBackEdge.bpl -------------------- +CutBackEdge.bpl(10,5): Error BP5005: This loop invariant might not be maintained by the loop. +Execution trace: + CutBackEdge.bpl(5,3): entry + CutBackEdge.bpl(9,3): block850 + +Boogie program verifier finished with 0 verified, 1 error + +-------------------- False.bpl -------------------- + +Boogie program verifier finished with 2 verified, 0 errors + +-------------------- LoopInvAssume.bpl -------------------- +LoopInvAssume.bpl(18,7): Error BP5001: This assertion might not hold. +Execution trace: + LoopInvAssume.bpl(8,4): entry + LoopInvAssume.bpl(16,4): exit + +Boogie program verifier finished with 0 verified, 1 error + +-------------------- strings-no-where.bpl -------------------- +strings-no-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) +strings-no-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) +strings-no-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-no-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) +strings-no-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-no-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator == +strings-no-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any) +strings-no-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator == +18 type checking errors detected in strings-no-where.bpl + +-------------------- strings-where.bpl -------------------- +strings-where.bpl(201,103): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(203,105): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(209,106): Error: invalid type for argument 1 in application of IsAllocated: struct (expected: any) +strings-where.bpl(211,72): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(211,108): Error: invalid type for argument 1 in application of IsAllocated: elements (expected: any) +strings-where.bpl(211,130): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(213,78): Error: invalid type for argument 1 in application of IsAllocated: ref (expected: any) +strings-where.bpl(235,98): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(249,118): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(699,34): Error: invalid type for argument 1 in application of IsAllocated: int (expected: any) +strings-where.bpl(728,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(737,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(751,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(760,9): Error: mismatched types in assignment command (cannot assign bool to any) +strings-where.bpl(926,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(949,36): Error: invalid argument types (any and name) to binary operator == +strings-where.bpl(975,9): Error: mismatched types in assignment command (cannot assign name to any) +strings-where.bpl(990,36): Error: invalid argument types (any and name) to binary operator == +18 type checking errors detected in strings-where.bpl + +-------------------- Structured.bpl -------------------- +Structured.bpl(252,14): Error BP5003: A postcondition might not hold at this return statement. +Structured.bpl(243,3): Related location: This is the postcondition that might not hold. +Execution trace: + Structured.bpl(245,3): anon0 + Structured.bpl(245,3): anon6_LoopHead + Structured.bpl(246,5): anon6_LoopBody + Structured.bpl(247,7): anon7_LoopBody + Structured.bpl(252,5): anon4 + Structured.bpl(252,14): anon9_Then +Structured.bpl(303,3): Error BP5001: This assertion might not hold. +Execution trace: + Structured.bpl(299,5): anon0 + Structured.bpl(300,3): anon3_Else + Structured.bpl(303,3): anon2 +Structured.bpl(311,7): Error BP5001: This assertion might not hold. +Execution trace: + Structured.bpl(308,3): anon0 + Structured.bpl(308,3): anon1_Then + Structured.bpl(309,5): A + +Boogie program verifier finished with 15 verified, 3 errors + +-------------------- Where.bpl -------------------- +Where.bpl(8,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(6,3): anon0 +Where.bpl(22,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(16,5): anon0 +Where.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(30,3): anon0 +Where.bpl(44,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(40,5): anon0 +Where.bpl(57,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(52,3): anon0 +Where.bpl(111,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(102,5): anon0 + Where.bpl(104,3): anon3_LoopHead + Where.bpl(110,3): anon2 +Where.bpl(128,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(121,5): anon0 + Where.bpl(122,3): anon3_LoopHead + Where.bpl(125,3): anon2 +Where.bpl(145,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(138,5): anon0 + Where.bpl(139,3): anon3_LoopHead + Where.bpl(142,3): anon2 +Where.bpl(162,3): Error BP5001: This assertion might not hold. +Execution trace: + Where.bpl(155,5): anon0 + Where.bpl(156,3): anon3_LoopHead + Where.bpl(159,3): anon2 + +Boogie program verifier finished with 2 verified, 9 errors + +-------------------- UpdateExpr.bpl -------------------- +UpdateExpr.bpl(14,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(14,3): anon0 +UpdateExpr.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(19,3): anon0 +UpdateExpr.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(32,3): anon0 +UpdateExpr.bpl(38,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(38,3): anon0 +UpdateExpr.bpl(52,3): Error BP5001: This assertion might not hold. +Execution trace: + UpdateExpr.bpl(51,5): anon0 + +Boogie program verifier finished with 5 verified, 5 errors + +-------------------- NeverPattern.bpl -------------------- +NeverPattern.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(15,3): anon0 +NeverPattern.bpl(22,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(21,3): anon0 +NeverPattern.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + NeverPattern.bpl(27,3): anon0 + +Boogie program verifier finished with 1 verified, 3 errors + +-------------------- NullaryMaps.bpl -------------------- +NullaryMaps.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(28,3): anon0 +NullaryMaps.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(28,3): anon0 +NullaryMaps.bpl(36,3): Error BP5001: This assertion might not hold. +Execution trace: + NullaryMaps.bpl(36,3): anon0 + +Boogie program verifier finished with 2 verified, 3 errors + +-------------------- Implies.bpl -------------------- +Implies.bpl(12,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(11,3): anon0 +Implies.bpl(15,3): Error BP5001: This assertion might not hold. +Execution trace: + Implies.bpl(11,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors +-------------------- sk_hack.bpl -------------------- + +Boogie program verifier finished with 1 verified, 0 errors + +-------------------- CallForall.bpl -------------------- +CallForall.bpl(17,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(17,3): anon0 +CallForall.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(28,3): anon0 +CallForall.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(40,3): anon0 +CallForall.bpl(47,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(46,3): anon0 +CallForall.bpl(75,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(75,3): anon0 +CallForall.bpl(111,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(109,3): anon0 +CallForall.bpl(118,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(117,3): anon0 +CallForall.bpl(125,3): Error BP5001: This assertion might not hold. +Execution trace: + CallForall.bpl(124,3): anon0 + +Boogie program verifier finished with 10 verified, 8 errors diff --git a/Test/test2/Passification.bpl b/Test/test2/Passification.bpl new file mode 100644 index 00000000..e13d3e49 --- /dev/null +++ b/Test/test2/Passification.bpl @@ -0,0 +1,169 @@ +// VC generation tests: passification + +procedure good0(x: int) returns (y: int, z: int) + ensures z == 4 || z == 4+x; +{ +var t: int; +A: + t := y; + z := 3; + goto B, C; +B: + z := z + x; + goto D; +C: + goto D; +D: + z := z + 1; + y := t; + return; +} + +procedure good1(x: int) returns (y: int, z: int) + ensures z == x + 4; +{ +var t: int; +A: + t := y; + z := 3; + z := z + x; + z := z + 1; + y := t; + return; +} + +procedure bad0(x: int) returns (y: int, z: int) + ensures y == 4; // ERROR: postcondition violation +{ +var t: int; +A: + t := z; + z := 3; + z := z + 1; + y := t; + return; +} + +procedure Loop() +{ +start: + goto start; +} + +procedure UnreachableBlock() +{ +start: + return; +notReached: + goto start; +reallyNeverReached: + goto reallyNeverReached; +} + +procedure Loop0() returns (z: int) + ensures 10 <= z; +{ +var x: int; +A: + goto B, C; +B: + assume x < 10; + x := x + 1; + goto A; +C: + assume !(x < 10); + z := x; + return; +} + +const unique A0: name; +const unique A1: name; +const unique A2: name; + +procedure Array0() returns (z: int) + ensures z >= 5; +{ +var a: [name,name]int; +L0: + a[A0,A2] := 5; + a[A0,A1] := 20; + assert a[A0,A1] == 20; + goto L1,L2; +L1: + a[A0,A2] := 18; + assert a[A0,A2] == 18; + goto L2; +L2: + assert a[A0,A1] == 20; + z := a[A0,A2]; + return; +} + +procedure Array1(o0: ref, o1: ref) returns (z: int) + ensures z >= 5; +{ +var a: [ref,name]int; +L0: + a[o1,A0] := 5; + a[o0,A0] := 20; + assert a[o0,A0] == 20; + goto L1,L2; +L1: + a[o1,A0] := 18; + assert a[o1,A0] == 18; + goto L2; +L2: + assert a[o0,A0] == 20; // ERROR: assertion failure + z := a[o1,A0]; + return; +} + +procedure Array2(o0: ref, o1: ref) returns (z: int) + ensures z >= 5; +{ +var a: [ref,name]int; +L0: + assume o1 != o0; + a[o1,A0] := 5; + a[o0,A0] := 20; + assert a[o0,A0] == 20; + goto L1,L2; +L1: + a[o1,A0] := 18; + assert a[o1,A0] == 18; + goto L2; +L2: + assert a[o0,A0] == 20; + z := a[o1,A0]; + return; +} + +procedure P() +{ +var t: int; +L0: + t := 0; + goto L1, L2; +L1: + t := 1; + goto L2; +L2: + assert t == 1; // ERROR: assert failure + return; +} + +procedure Q() +{ +var t: int; +L0: + t := 0; + goto L1, L2; +L1: + t := 1; + goto L2; +L2: + assert t == 0; // ERROR: assert failure + return; +} + +type name, ref; diff --git a/Test/test2/Quantifiers.bpl b/Test/test2/Quantifiers.bpl new file mode 100644 index 00000000..d368fe1f --- /dev/null +++ b/Test/test2/Quantifiers.bpl @@ -0,0 +1,154 @@ +// ----------------------------------------------------------------------- single trigger + +function f(int, int) returns (int); + +axiom (forall x: int, y: int :: f(x,y) < x+y); +axiom (forall x: int :: { f(x,10) } f(x,10) == 3); + +procedure P(a: int, b: int) + requires a <= 25 && b <= 30; +{ + start: + assert f(a,b) <= 100; + return; +} + +procedure Q(a: int, b: int) + requires a + 2 <= b; +{ + start: + assert f(a,b) == 3; // not provable with the trigger given above + return; +} + +procedure R(a: int, b: int) + requires a + 2 <= b; +{ + start: + assume b <= 10 && 8 <= a; + assert f(a,b) == 3; // now, the trigger should fire + return; +} + +// ----------------------------------------------------------------------- multi trigger + +function g(int, int) returns (int); + +axiom (forall x: int, y: int :: { g(x,10),g(x,y) } g(x,y) == 3); // multi-trigger + +procedure S(a: int, b: int) + requires a + 2 <= b; +{ + start: + assert g(a,b) == 3; // not provable with the trigger given above + return; +} + +procedure T(a: int, b: int) + requires a + 2 <= b; +{ + start: + assume b <= 10 && 8 <= a; + assert g(a,b) == 3; // this should trigger + return; +} + +// ----------------------------------------------------------------------- several triggers + +function h(int, int) returns (int); + +axiom (forall y: int :: { g(y,y) } { h(y,h(y,10)) } h(y, h(y,y)) == y); // several triggers + +procedure U0(a: int) +{ + start: + assert h(a,h(a,a)) == a; // not provable with the triggers given above + return; +} + +procedure U1(a: int, b: int) +{ + start: + assume g(a,b) == 5; + assert h(a,h(a,a)) == a; // not provable with the triggers given above + return; +} + +procedure V0(a: int, b: int) + requires a == b; +{ + start: + assume g(a,b) == 5; + assert h(a,h(a,a)) == a; // this should trigger + return; +} + +procedure V1(a: int, b: int) +{ + start: + assume a == 10; + assert h(a,h(a,a)) == a; // this should trigger + return; +} + +procedure V2(a: int, b: int) +{ + start: + assume 0 <= h(a,h(a,10)); + assume a == 17; + assert h(a,h(a,a)) == a; // this should trigger + return; +} + +// ----------------------------------------------------------------------- negated triggers + +function ka(ref) returns (int); +function kb(ref) returns (int); +function kbSynonym(ref) returns (int); +function isA(ref, name) returns (bool); +function isB(ref, name) returns (bool); +const $T: name; + +axiom (forall o: ref :: + isA(o, $T) ==> ka(o) < ka(o)); // automatically inferred triggers can be both isA(o,$T) and ka(o) + +axiom (forall o: ref :: + {:nopats isB(o, $T) } + isB(o, $T) ==> kb(o) < kbSynonym(o)); // prevent isB(o,$T) from being used as a trigger + +axiom (forall o: ref :: kb(o) == kbSynonym(o)); + +procedure W(o: ref, e: int) + requires isB(o, $T); +{ + start: + assert e > 20; // the isB axiom should not trigger, so this cannot be proved + return; +} + +procedure X0(o: ref, e: int) + requires isA(o, $T); +{ + start: + assert e > 20; // this should trigger the isA axiom, so anything is provable + return; +} + +procedure X1(o: ref, e: int, u: int) + requires isB(o, $T); +{ + start: + assume f(kb(o), kb(o)) == u; + assert e > 20; // this should now trigger the isB axiom, so anything is provable + return; +} + +procedure X2(o: ref, e: int, u: int) + requires isB(o, $T); +{ + start: + assert e > 20; // error is report here, providing evidence that the isB axiom has not been triggered + return; +} + +type name, ref; diff --git a/Test/test2/Structured.bpl b/Test/test2/Structured.bpl new file mode 100644 index 00000000..ce97b145 --- /dev/null +++ b/Test/test2/Structured.bpl @@ -0,0 +1,327 @@ + +const K: int; + +function f(int) returns (int); + +axiom (exists k: int :: f(k) == K); + +procedure Find(a: int, b: int) returns (k: int); + requires a <= b && (forall j: int :: a < j && j < b ==> f(j) != K); + ensures f(k) == K; + +// nondeterministic, unstructured, recursive version +implementation Find(a: int, b: int) returns (k: int) +{ + entry: + goto A, B, C; + + A: + assume f(a) == K; + k := a; + return; + + B: + assume f(b) == K; + k := b; + return; + + C: + assume f(a) != K && f(b) != K; + call k := Find(a-1, b+1); + return; +} + +// nondeterministic, recursive version +implementation Find(a: int, b: int) returns (k: int) +{ + if (*) { + assume f(a) == K; + k := a; + } else if (*) { + assume f(b) == K; + k := b; + } else { + assume f(a) != K && f(b) != K; + call k := Find(a-1, b+1); + } +} + +// deterministic, structured, recursive version +implementation Find(a: int, b: int) returns (k: int) +{ + if (f(a) == K) { + k := a; + } else if (f(b) == K) { + k := b; + } else { + call k := Find(a-1, b+1); + } +} + +// deterministic, structured, iterative version +implementation Find(a: int, b: int) returns (k: int) +{ + var x: int, y: int; + + x := a; + y := b; + + while (f(x) != K && f(y) != K) + invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K); + { + x := x-1; + y := y+1; + } + + if (f(x) == K) { + k := x; + } else { + k := y; + } +} + +// deterministic, structured, iterative version with breaks +implementation Find(a: int, b: int) returns (k: int) +{ + var x: int, y: int; + + x := a; + y := b; + + while (true) + invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K); + { + if (f(x) == K) { + k := x; + break; + } else if (f(y) == K) { + k := y; + break; + } + x := x-1; + y := y+1; + } +} + +// deterministic, somewhat structured, iterative version +implementation Find(a: int, b: int) returns (k: int) +{ + var x: int, y: int; + + x := a; + y := b; + + while (true) + invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K); + { + if (f(x) == K) { + goto FoundX; + } else if (f(y) == K) { + goto FoundY; + } + x := x-1; + y := y+1; + } + + FoundX: + k := x; + return; + + FoundY: + k := y; + return; +} + +// deterministic, structured, iterative version with breaks +implementation Find(a: int, b: int) returns (k: int) +{ + var x: int, y: int; + + x := a; + y := b; + + outer: + if (true) { + inner: + while (true) + invariant x <= y && (forall j: int :: x < j && j < y ==> f(j) != K); + { + if (f(x) == K) { + break inner; + } else if (f(y) == K) { + break outer; + } + x := x-1; + y := y+1; + } + + k := x; + return; + } + k := y; +} + +// ----- free invariant ----- + +function Teal(int) returns (bool); +function ShadeOfGreen(int) returns (bool); +axiom (forall w: int :: Teal(w) ==> ShadeOfGreen(w)); + +procedure P(x: int) returns (y: int) + requires Teal(x); + ensures ShadeOfGreen(y); +{ + y := x; + while (y < 100) + free invariant Teal(y); + { + y := y + 5; + } +} + +// ----- run off the end of the BigBlock ----- + +procedure RunOffEnd0() returns (x: int) + ensures x == 3; +{ + x := 0; + Label0: + x := x + 1; + Label1: + x := x + 1; + Label2: + Label3: + Label4: + x := x + 1; +} + +procedure RunOffEnd1() returns (x: int) + ensures x == 4; +{ + x := 0; + Label0: + x := x + 1; + Label1: + if (*) { + Label2: + x := x + 2; + } else if (*) { + Label3: + x := 2; + x := x + 2; + Label4: + Label5: + x := x - 1; + } else { + if (*) { + x := 0; + while (x < 3) + invariant x <= 3; + { x := x + 1; } + } else { + x := x + 2; + } + } + x := x + 1; +} + +procedure RunOffEnd2() returns (x: int) + ensures x == 10; +{ + while (true) { + while (true) { + if (*) { + x := 10; + break; + } + } + if (*) { break; } + } +} + +procedure RunOffEnd3() returns (x: int) + ensures x == 9; +{ + while (true) { + while (true) { + if (*) { + x := 10; + break; + } + } + if (*) { break; } + } // error: violated postcondition +} + +procedure RunOffEnd4() returns (x: int) +{ + var y: int; + var bad: bool; + + while (true) { + y := x; + bad := false; + if (*) { + x := x + 1; + bad := true; + } + if (x == y) { break; } + } + assert !bad; +} + +procedure RunOffEnd5() returns (x: int) +{ + while (true) { + if (x == 5) { } + } + assert false; +} + +procedure RunOffEnd6() returns (x: int) +{ + x := 7; + while (true) + invariant x == 7; + { + x := 5; + MyLabel: + x := 7; + } +} + +// ----- jump optimizations ----- + +procedure Q0() +{ + var x: int; + + x := 0; + if (*) { + x := 1; + } + assert x == 1; // error +} + +procedure Q1() returns (x: int) +{ + if (x == 0) { + A: + x := x + 0; + assert x == 0; // error + B: + x := x + 1; + goto A; + } +} + +procedure Q2() returns (x: int) +{ + if (x == 0) { + while (x < 10) + invariant x <= 10; + { + x := x + 1; + } + } +} diff --git a/Test/test2/UpdateExpr.bpl b/Test/test2/UpdateExpr.bpl new file mode 100644 index 00000000..8f950073 --- /dev/null +++ b/Test/test2/UpdateExpr.bpl @@ -0,0 +1,81 @@ + +const a: [int]bool; + +// element 5 of a stores the value true +axiom a == a[5 := true]; + +procedure P() +{ + assert a[5]; +} + +procedure Q() +{ + assert a[4]; // error +} + +procedure R() +{ + assert !a[5]; // error +} + +procedure S(y: int, t: bool) + requires y <= 5; +{ + if (a[y := t][5] == false) { + assert y == 5; + } +} + +procedure T0(aa: [int,ref]bool) +{ + assert aa[5,null := true] != aa[2,null := false]; // error +} + +procedure T1(aa: [int,ref]bool) + requires aa[5,null] && !aa[2,null]; +{ + assert aa[5,null := true] == aa[2,null := false]; // error, because we have no extensionality +} + +procedure T2(aa: [int,ref]bool) + requires aa[5,null] && !aa[2,null]; +{ + assert (forall x: int, y: ref :: aa[5,null := true][x,y] == aa[2,null := false][x,y]); +} + +procedure U0(a: [int]int) +{ + var b: [int]int; + + b := a[5 := 12]; + assert a == b; // error +} + +procedure U1() returns (a: [int]int) +{ + var b: [int]int; + + b := a[5 := 12]; + a[5] := 12; + assert a == b; +} + +type Field a; +const unique IntField: Field int; +const unique RefField: Field ref; +const unique SomeField: Field int; + +procedure FieldProc(H: [ref,Field a]a, this: ref) +{ + var i: int, r: ref, y: any; + var K: [ref,Field a]a; + + K := H[this, IntField := 5][this, RefField := null][this, SomeField := 100][this, IntField := 7]; + assert K[this, IntField] == 7; + assert K[this, RefField] == null; + assert K[this, SomeField] == 100; +} + +type ref, any; +const null : ref; diff --git a/Test/test2/Where.bpl b/Test/test2/Where.bpl new file mode 100644 index 00000000..96ffcf04 --- /dev/null +++ b/Test/test2/Where.bpl @@ -0,0 +1,163 @@ +procedure P0() +{ + var x: int where 0 <= x; + var y: int where x <= y; + + assert 0 <= x; + assert x <= y; + assert y < 5; // error +} + +procedure P1() +{ + var x: int where 0 <= x; + var y: int where x <= y; + + x := 5; + havoc y; + assert 5 <= y; + + havoc x; + assert 0 <= x; + assert x <= y; // error +} + +procedure P2() +{ + var x: int where 0 <= x; + var y: int where x <= y; + + havoc y; // y first + havoc x; + assert x <= y; // error +} + +procedure P3() +{ + var x: int where 0 <= x; + var y: int where x <= y; + + x := 5; + havoc x; // this time, x first + havoc y; + assert x <= y; // yeah! + assert 5 <= y; // error +} + +procedure P4() +{ + var x: int where 0 <= x; + var y: int where x <= y; + + havoc x, y; // both at the same time + assert 0 <= x && x <= y; + havoc y, x; // or in the other order + assert 0 <= x && x <= y; + + assert x == 7; // error +} + +procedure R0() returns (wProc: int where wProc == xProc, + xProc: int where 0 <= xProc, + yProc: int where xProc <= yProc); +implementation R0() returns (w: int, x: int, y: int) +{ + while (*) { + assert w == x; + assert 0 <= x; + assert x <= y; + } + while (*) { + assert w == x; + assert 0 <= x; + assert x <= y; + // the following makes w, x, y loop targets + w := w + 1; + havoc x; + y := w; + } + assert w == x; + assert 0 <= x; + assert x <= y; +} + +procedure R1() +{ + var a: int; + var b: int; + var c: int; + + call a, b, c := R0(); + assert a == b; + assert 0 <= b; + assert b <= c; +} + +procedure R2() +{ + var w: int where w == x; + var x: int where 0 <= x; + var y: int where x <= y; + + x := 5; + y := 10; + while (*) { + w := w + 1; + assert w == 6; + y := y + 2; + assert 7 <= y; + } + assert x == 5 && 0 <= y - w; + assert y == 10; // error +} + +procedure R3() +{ + var w: int where w == x; + var x: int where 0 <= x; + var y: int where x <= y; + + // change w and x + y := 10; + while (*) { + w := w; x := x; + } + assert w == x; + assert 0 <= x; + assert y == 10; + assert w <= 10; // error +} + +procedure R4() +{ + var w: int where w == x; + var x: int where 0 <= x; + var y: int where x <= y; + + // change x and y + w := 12; + while (*) { + x := x; y := y; + } + assert 0 <= x; + assert x <= y; + assert w == 12; + assert 8 <= y; // error +} + +procedure R5(K: int) +{ + var w: int where w == x; + var x: int where 0 <= x; + var y: int where x <= y; + + // change w and y + x := K; + while (*) { + w := w; y := y; + } + assert w == K; + assert K <= y; + assert x == K; + assert 0 <= x; // error +} diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat new file mode 100644 index 00000000..5f48a799 --- /dev/null +++ b/Test/test2/runtest.bat @@ -0,0 +1,26 @@ +@echo off +setlocal + +set BGEXE=..\..\Binaries\Boogie.exe +rem set BGEXE=mono ..\..\Binaries\Boogie.exe + +for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl + Ensures.bpl Old.bpl OldIllegal.bpl Arrays.bpl Axioms.bpl + Quantifiers.bpl Call.bpl AssumeEnsures.bpl + CutBackEdge.bpl False.bpl LoopInvAssume.bpl + strings-no-where.bpl strings-where.bpl + Structured.bpl Where.bpl UpdateExpr.bpl + NeverPattern.bpl NullaryMaps.bpl Implies.bpl) do ( + echo. + echo -------------------- %%f -------------------- + %BGEXE% %* /noinfer %%f +) + +echo -------------------- sk_hack.bpl -------------------- +%BGEXE% %* /noinfer /bv:z sk_hack.bpl + +for %%f in (CallForall.bpl) do ( + echo. + echo -------------------- %%f -------------------- + %BGEXE% %* %%f +) diff --git a/Test/test2/sk_hack.bpl b/Test/test2/sk_hack.bpl new file mode 100644 index 00000000..df942317 --- /dev/null +++ b/Test/test2/sk_hack.bpl @@ -0,0 +1,32 @@ +function in_set(int) returns(bool); +function next(int) returns(int); +function f(int) returns(bool); +function g(int) returns(bool); + +// this function is treated specially by Z3 when used in triggers +// sk_hack(f(x)) means to activate the e-node f(x0) when trying to prove +// !(forall x : T :: {sk_hack(f(x))} p(x)) by proving !p(x0) +// (i.e., after skolemization of x to x0). +function sk_hack(bool) returns(bool); + +// PR: sk_hack cannot be defined as a polymorphic function +// when using /quantifierTypePremisses:a, because then it would +// get an additional explicit type parameter, and Z3 would +// no longer recognise it. + +procedure foo() +{ + assume (forall x:int :: {in_set(next(x))} + in_set(x) ==> in_set(next(x))); + + assume (forall x:int :: {in_set(x)} + in_set(x) ==> f(x)); + + assume (forall x:int :: {f(next(x))} + f(next(x)) ==> g(x)); + + assert (forall x:int :: + { sk_hack(in_set(next(x))) } + in_set(x) ==> g(x)); + } + diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl new file mode 100644 index 00000000..ff723db2 --- /dev/null +++ b/Test/test2/strings-no-where.bpl @@ -0,0 +1,995 @@ +type real; + +type elements; + +type struct; + +var $Heap: [ref,name]any; +function cast(S) returns (T); +function IsHeap(h: [ref,name]any) returns (bool); + +const unique $allocated: name; + +const unique $elements: name; + +const unique $inv: name; + +const unique $writable: name; + +const unique $sharingMode: name; + +const unique $SharingMode_Unshared: name; + +const unique $SharingMode_LockProtected: name; + +function ClassRepr(class: name) returns (ref); + +axiom (forall c0: name, c1: name :: c0 != c1 ==> ClassRepr(c0) != ClassRepr(c1)); + +axiom (forall T: name :: !($typeof(ClassRepr(T)) <: System.Object)); + +axiom (forall T: name :: ClassRepr(T) != null); + +axiom (forall T: name, h: [ref,name]any :: { h[ClassRepr(T), $writable] } IsHeap(h) ==> cast(h[ClassRepr(T), $writable]):bool); + +function IsDirectlyModifiableField(f: name) returns (bool); + +axiom !IsDirectlyModifiableField($allocated); + +axiom IsDirectlyModifiableField($elements); + +axiom !IsDirectlyModifiableField($inv); + +axiom !IsDirectlyModifiableField($writable); + +function IsStaticField(f: name) returns (bool); + +axiom !IsStaticField($allocated); + +axiom !IsStaticField($elements); + +axiom !IsStaticField($inv); + +axiom !IsStaticField($writable); + +function ValueArrayGet(elements, int) returns (any); + +function ValueArraySet(elements, int, any) returns (elements); + +function RefArrayGet(elements, int) returns (ref); + +function RefArraySet(elements, int, ref) returns (elements); + +axiom (forall A: elements, i: int, x: any :: ValueArrayGet(ValueArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: any :: i != j ==> ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j)); + +axiom (forall A: elements, i: int, x: ref :: RefArrayGet(RefArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: ref :: i != j ==> RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j)); + +function ArrayIndex(arr: ref, dim: int, indexAtDim: int, remainingIndexContribution: int) returns (int); + +axiom (forall a: ref, d: int, x: int, y: int, x': int, y': int :: ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y') ==> x == x' && y == y'); + +axiom (forall a: ref, T: name, i: int, r: int, heap: [ref,name]any :: $typeof(a) <: RefArray(T, r) ==> $Is(RefArrayGet(cast(heap[a, $elements]):elements, i), T)); + +function $Rank(ref) returns (int); + +axiom (forall a: ref :: 1 <= $Rank(a)); + +axiom (forall a: ref, T: name, r: int :: { $Is(a, ValueArray(T, r)) } $Is(a, ValueArray(T, r)) ==> $Rank(a) == r); + +axiom (forall a: ref, T: name, r: int :: { $Is(a, RefArray(T, r)) } $Is(a, RefArray(T, r)) ==> $Rank(a) == r); + +function $Length(ref) returns (int); + +axiom (forall a: ref :: { $Length(a) } 0 <= $Length(a)); + +function $DimLength(ref, int) returns (int); + +axiom (forall a: ref, i: int :: 0 <= $DimLength(a, i)); + +axiom (forall a: ref :: $Rank(a) == 1 ==> $DimLength(a, 0) == $Length(a)); + +function $LBound(ref, int) returns (int); + +function $UBound(ref, int) returns (int); + +axiom (forall a: ref, i: int :: { $LBound(a, i) } $LBound(a, i) == 0); + +axiom (forall a: ref, i: int :: { $UBound(a, i) } $UBound(a, i) == $DimLength(a, i) - 1); + +const unique System.Array: name; + +axiom $IsClass(System.Array); + +axiom System.Array <: System.Object; + +function $ElementType(name) returns (name); + +function ValueArray(elementType: name, rank: int) returns (name); + +axiom (forall T: name, r: int :: { ValueArray(T, r) } ValueArray(T, r) <: System.Array); + +function RefArray(elementType: name, rank: int) returns (name); + +axiom (forall T: name, r: int :: { RefArray(T, r) } RefArray(T, r) <: System.Array); + +axiom (forall T: name, U: name, r: int :: U <: T ==> RefArray(U, r) <: RefArray(T, r)); + +axiom (forall A: name, r: int :: $ElementType(ValueArray(A, r)) == A); + +axiom (forall A: name, r: int :: $ElementType(RefArray(A, r)) == A); + +axiom (forall A: name, r: int, T: name :: { T <: RefArray(A, r) } T <: RefArray(A, r) ==> T == RefArray($ElementType(T), r) && $ElementType(T) <: A); + +axiom (forall A: name, r: int, T: name :: { T <: ValueArray(A, r) } T <: ValueArray(A, r) ==> T == ValueArray(A, r)); + +axiom (forall A: name, r: int, T: name :: RefArray(A, r) <: T ==> System.Array <: T || (T == RefArray($ElementType(T), r) && A <: $ElementType(T))); + +axiom (forall A: name, r: int, T: name :: ValueArray(A, r) <: T ==> System.Array <: T || T == ValueArray(A, r)); + +function $ArrayPtr(elementType: name) returns (name); + +function $StructGet(struct, name) returns (any); + +function $StructSet(struct, name, any) returns (struct); + +axiom (forall s: struct, f: name, x: any :: $StructGet($StructSet(s, f, x), f) == x); + +axiom (forall s: struct, f: name, f': name, x: any :: f != f' ==> $StructGet($StructSet(s, f, x), f') == $StructGet(s, f')); + +function ZeroInit(s: struct, typ: name) returns (bool); + +function $typeof(ref) returns (name); + +function Implements(class: name, interface: name) returns (bool); + +axiom (forall T: name, J: name :: { Implements(T, J) } Implements(T, J) ==> T <: J); + +function InterfaceExtends(subIntf: name, superIntf: name) returns (bool); + +axiom (forall J: name, K: name :: { InterfaceExtends(J, K) } InterfaceExtends(J, K) ==> J <: K); + +function $IsClass(name) returns (bool); + +axiom (forall C: name :: { $IsClass(C) } $IsClass(C) ==> C <: C); + +function AsDirectSubClass(sub: name, base: name) returns (sub': name); + +function OneClassDown(sub: name, base: name) returns (directSub: name); + +axiom (forall A: name, B: name, C: name :: { C <: AsDirectSubClass(B, A) } C <: AsDirectSubClass(B, A) ==> OneClassDown(C, A) == B); + +function $IsInterface(name) returns (bool); + +axiom (forall J: name :: { $IsInterface(J) } $IsInterface(J) ==> J <: System.Object); + +function $IsValueType(name) returns (bool); + +axiom (forall T: name :: $IsValueType(T) ==> (forall U: name :: T <: U ==> T == U) && (forall U: name :: U <: T ==> T == U)); + +const unique System.Object: name; + +axiom $IsClass(System.Object); + +function $IsTokenForType(struct, name) returns (bool); + +function TypeObject(name) returns (ref); + +const unique System.Type: name; + +axiom System.Type <: System.Object; + +axiom (forall T: name :: { TypeObject(T) } $IsNotNull(TypeObject(T), System.Type)); + +function $Is(ref, name) returns (bool); + +axiom (forall o: ref, T: name :: { $Is(o, T) } $Is(o, T) <==> o == null || $typeof(o) <: T); + +function $IsNotNull(ref, name) returns (bool); + +axiom (forall o: ref, T: name :: { $IsNotNull(o, T) } $IsNotNull(o, T) <==> o != null && $Is(o, T)); + +function $As(ref, name) returns (ref); + +axiom (forall o: ref, T: name :: $Is(o, T) ==> $As(o, T) == o); + +axiom (forall o: ref, T: name :: !$Is(o, T) ==> $As(o, T) == null); + +axiom (forall heap: [ref,name]any, o: ref, A: name, r: int :: $Is(o, RefArray(A, r)) ==> heap[o, $inv] == $typeof(o)); + +axiom (forall heap: [ref,name]any, o: ref, A: name, r: int :: $Is(o, ValueArray(A, r)) ==> heap[o, $inv] == $typeof(o)); + +function IsAllocated(h: [ref,name]any, o: any) returns (bool); + +axiom (forall h: [ref,name]any, o: ref, f: name :: { IsAllocated(h, h[o, f]) } IsHeap(h) ==> IsAllocated(h, h[o, f])); + +axiom (forall h: [ref,name]any, s: struct, f: name :: { IsAllocated(h, $StructGet(s, f)) } IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))); + +axiom (forall h: [ref,name]any, e: elements, i: int :: { IsAllocated(h, RefArrayGet(e, i)) } IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))); + +axiom (forall h: [ref,name]any, o: ref :: { h[o, $allocated] } IsAllocated(h, o) ==> cast(h[o, $allocated]):bool); + +axiom (forall h: [ref,name]any, c: name :: { h[ClassRepr(c), $allocated] } IsHeap(h) ==> cast(h[ClassRepr(c), $allocated]):bool); + +function DeclType(field: name) returns (class: name); + +function AsNonNullRefField(field: name, T: name) returns (f: name); + +function AsRefField(field: name, T: name) returns (f: name); + +function AsRangeField(field: name, T: name) returns (f: name); + +axiom (forall f: name, T: name :: { AsNonNullRefField(f, T) } AsNonNullRefField(f, T) == f ==> AsRefField(f, T) == f); + +axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsRefField(f, T)] } IsHeap(h) ==> $Is(cast(h[o, AsRefField(f, T)]):ref, T)); + +axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsNonNullRefField(f, T)] } IsHeap(h) ==> cast(h[o, AsNonNullRefField(f, T)]):ref != null); + +axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsRangeField(f, T)] } IsHeap(h) ==> InRange(cast(h[o, AsRangeField(f, T)]):int, T)); + +const unique System.String: name; + +axiom (forall h: [ref,name]any, s: ref :: IsHeap(h) && $typeof(s) == System.String ==> h[s, $inv] == $typeof(s) && cast(h[s, $writable]):bool); + +function AsOwnedField(f: name) returns (name); + +axiom (forall h: [ref,name]any, o: ref, f: name :: { h[o, AsOwnedField(f)] } IsHeap(h) && cast(h[o, $inv]):name <: DeclType(AsOwnedField(f)) ==> cast(h[o, AsOwnedField(f)]):ref == null || $typeof(cast(h[o, AsOwnedField(f)]):ref) == System.String || !cast(h[cast(h[o, AsOwnedField(f)]):ref, $writable]):bool); + +axiom (forall h: [ref,name]any, o: ref :: { h[o, $writable] } IsHeap(h) && !cast(h[o, $writable]):bool ==> cast(h[o, $inv]):name == $typeof(o)); + +function Box(any, ref) returns (ref); + +function Unbox(ref) returns (any); + +axiom (forall x: any, p: ref :: { Unbox(Box(x, p)) } Unbox(Box(x, p)) == x); + +axiom (forall heap: [ref,name]any, x: any, p: ref :: { heap[Box(x, p), $inv] } IsHeap(heap) ==> heap[Box(x, p), $inv] == $typeof(Box(x, p))); + +function UnboxedType(ref) returns (name); + +function BoxTester(p: ref, typ: name) returns (ref); + +axiom (forall p: ref, typ: name :: { BoxTester(p, typ) } UnboxedType(p) == typ <==> BoxTester(p, typ) != null); + +const unique System.Int16: name; + +axiom $IsValueType(System.Int16); + +const unique System.Int32: name; + +axiom $IsValueType(System.Int32); + +const unique System.Int64: name; + +axiom $IsValueType(System.Int64); + +const unique System.Byte: name; + +axiom $IsValueType(System.Byte); + +const unique System.Int16.MinValue: int; + +const unique System.Int16.MaxValue: int; + +const unique System.Int32.MinValue: int; + +const unique System.Int32.MaxValue: int; + +const unique System.Int64.MinValue: int; + +const unique System.Int64.MaxValue: int; + +axiom System.Int64.MinValue < System.Int32.MinValue; + +axiom System.Int32.MinValue < System.Int16.MinValue; + +axiom System.Int16.MinValue < System.Int16.MaxValue; + +axiom System.Int16.MaxValue < System.Int32.MaxValue; + +axiom System.Int32.MaxValue < System.Int64.MaxValue; + +function InRange(i: int, T: name) returns (bool); + +axiom (forall i: int :: InRange(i, System.Int16) <==> System.Int16.MinValue <= i && i <= System.Int16.MaxValue); + +axiom (forall i: int :: InRange(i, System.Int32) <==> System.Int32.MinValue <= i && i <= System.Int32.MaxValue); + +axiom (forall i: int :: InRange(i, System.Int64) <==> System.Int64.MinValue <= i && i <= System.Int64.MaxValue); + +axiom (forall i: int :: { InRange(i, System.Byte) } InRange(i, System.Byte) <==> 0 <= i && i < 256); + +function $RealToInt(real) returns (int); + +function $IntToReal(int) returns (real); + +function $SizeIs(name, int) returns (bool); + +function $IfThenElse(bool, any, any) returns (any); + +axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } b ==> $IfThenElse(b, x, y) == x); + +axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } !b ==> $IfThenElse(b, x, y) == y); + +function #neg(int) returns (int); + +function #rneg(real) returns (real); + +function #rdiv(real, real) returns (real); + +function #and(int, int) returns (int); + +function #or(int, int) returns (int); + +function #xor(int, int) returns (int); + +function #shl(int, int) returns (int); + +function #shr(int, int) returns (int); + +axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y); + +axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y); + +axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y); + +axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0); + +axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0); + +axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y); + +axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y); + +axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y); + +axiom (forall a: int, b: int, d: int :: { a % d,b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b); + +axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i); + +axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2); + +axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i); + +axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) / 2); + +const unique $UnknownRef: ref; + +const unique System.IComparable: name; + +const unique Microsoft.Singularity.Applications.ThreadTest: name; + +const unique System.Threading.Thread: name; + +const unique System.Collections.IEnumerable: name; + +const unique System.Threading.ThreadStart: name; + +const unique System.ICloneable: name; + +const unique System.MulticastDelegate: name; + +const unique System.Delegate: name; + +const unique $stringLiteral0: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral0, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral0, $allocated]):bool) && $IsNotNull($stringLiteral0, System.String) && $Length($stringLiteral0) == 13; + +const unique $stringLiteral1: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral1, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral1, $allocated]):bool) && $IsNotNull($stringLiteral1, System.String) && $Length($stringLiteral1) == 14; + +const unique $stringLiteral2: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral2, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral2, $allocated]):bool) && $IsNotNull($stringLiteral2, System.String) && $Length($stringLiteral2) == 11; + +const unique $stringLiteral3: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral3, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral3, $allocated]):bool) && $IsNotNull($stringLiteral3, System.String) && $Length($stringLiteral3) == 18; + +const unique $stringLiteral4: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral4, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral4, $allocated]):bool) && $IsNotNull($stringLiteral4, System.String) && $Length($stringLiteral4) == 19; + +const unique $stringLiteral5: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral5, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral5, $allocated]):bool) && $IsNotNull($stringLiteral5, System.String) && $Length($stringLiteral5) == 14; + +const unique $stringLiteral6: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral6, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral6, $allocated]):bool) && $IsNotNull($stringLiteral6, System.String) && $Length($stringLiteral6) == 15; + +const unique $stringLiteral7: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral7, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral7, $allocated]):bool) && $IsNotNull($stringLiteral7, System.String) && $Length($stringLiteral7) == 11; + +const unique $stringLiteral8: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral8, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral8, $allocated]):bool) && $IsNotNull($stringLiteral8, System.String) && $Length($stringLiteral8) == 19; + +const unique $stringLiteral9: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral9, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral9, $allocated]):bool) && $IsNotNull($stringLiteral9, System.String) && $Length($stringLiteral9) == 20; + +const unique $stringLiteral10: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral10, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral10, $allocated]):bool) && $IsNotNull($stringLiteral10, System.String) && $Length($stringLiteral10) == 22; + +const unique $stringLiteral11: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral11, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral11, $allocated]):bool) && $IsNotNull($stringLiteral11, System.String) && $Length($stringLiteral11) == 21; + +const unique $stringLiteral12: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral12, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral12, $allocated]):bool) && $IsNotNull($stringLiteral12, System.String) && $Length($stringLiteral12) == 23; + +const unique $stringLiteral13: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral13, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral13, $allocated]):bool) && $IsNotNull($stringLiteral13, System.String) && $Length($stringLiteral13) == 22; + +axiom $IsClass(Microsoft.Singularity.Applications.ThreadTest); + +axiom Microsoft.Singularity.Applications.ThreadTest <: System.Object && AsDirectSubClass(Microsoft.Singularity.Applications.ThreadTest, System.Object) == Microsoft.Singularity.Applications.ThreadTest; + +axiom (forall $K: name :: { Microsoft.Singularity.Applications.ThreadTest <: $K } Microsoft.Singularity.Applications.ThreadTest <: $K <==> Microsoft.Singularity.Applications.ThreadTest == $K || System.Object <: $K); + +function Inv_Microsoft.Singularity.Applications.ThreadTest(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_Microsoft.Singularity.Applications.ThreadTest(this, heap) } Inv_Microsoft.Singularity.Applications.ThreadTest(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: Microsoft.Singularity.Applications.ThreadTest } { Inv_Microsoft.Singularity.Applications.ThreadTest($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: Microsoft.Singularity.Applications.ThreadTest ==> Inv_Microsoft.Singularity.Applications.ThreadTest($o, heap)); + +procedure Microsoft.Singularity.Applications.ThreadTest.FirstThreadMethod(); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Microsoft.Singularity.Applications.ThreadTest.FirstThreadMethod() +{ + var stack0o: ref, i: int, stack0i: int, stack0b: bool, local1: int, $Heap$block1513$LoopPreheader: [ref,name]any; + + entry: + assume IsHeap($Heap); + goto block1479; + + block1479: + goto block1496; + + block1496: + // ----- load constant First thread! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(21,13) + stack0o := $stringLiteral0; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(21,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant First thread! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(22,13) + stack0o := $stringLiteral1; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(22,13) + call Microsoft.Singularity.DebugStub.Print$System.String(stack0o); + // ----- load constant 0 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,18) + i := 0; + goto block1513$LoopPreheader; + + block1513: + // ----- default loop invariant: $inv field ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29) + assert (forall $o: ref :: $Heap$block1513$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block1513$LoopPreheader[$o, $allocated]):bool != true); + assert (forall $o: ref :: cast($Heap$block1513$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + // ----- load constant 10 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29) + stack0i := 10; + // ----- binary operator ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29) + stack0b := i >= stack0i; + // ----- branch ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29) + goto true1513to1547, false1513to1530; + + true1513to1547: + assume stack0b == true; + goto block1547; + + false1513to1530: + assume stack0b == false; + goto block1530; + + block1547: + // ----- load constant First thread done! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(29,13) + stack0o := $stringLiteral3; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(29,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant First thread done! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(30,13) + stack0o := $stringLiteral4; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(30,13) + call Microsoft.Singularity.DebugStub.Print$System.String(stack0o); + // ----- return ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(31,10) + return; + + block1530: + // ----- load constant [0] ... ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(25,17) + stack0o := $stringLiteral2; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(25,17) + // Commented out, to avoid problems with the theorem prover nondeterministically choosing this error over the one 12 lines above: call System.Console.WriteLine$System.String(stack0o); + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(26,17) + call System.Threading.Thread.Yield(); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,37) + local1 := i; + // ----- load constant 1 + stack0i := 1; + // ----- binary operator + stack0i := local1 + stack0i; + // ----- copy + i := stack0i; + // ----- copy + stack0i := local1; + // ----- branch + goto block1513; + + block1513$LoopPreheader: + $Heap$block1513$LoopPreheader := $Heap; + goto block1513; + +} + + + +axiom $IsClass(System.String); + +axiom System.String <: System.Object && AsDirectSubClass(System.String, System.Object) == System.String; + +axiom $IsInterface(System.IComparable); + +axiom (forall $K: name :: { System.IComparable <: $K } System.IComparable <: $K <==> System.IComparable == $K || System.Object == $K); + +axiom Implements(System.String, System.IComparable); + +axiom $IsInterface(System.ICloneable); + +axiom (forall $K: name :: { System.ICloneable <: $K } System.ICloneable <: $K <==> System.ICloneable == $K || System.Object == $K); + +axiom Implements(System.String, System.ICloneable); + +axiom $IsInterface(System.Collections.IEnumerable); + +axiom (forall $K: name :: { System.Collections.IEnumerable <: $K } System.Collections.IEnumerable <: $K <==> System.Collections.IEnumerable == $K || System.Object == $K); + +axiom Implements(System.String, System.Collections.IEnumerable); + +axiom (forall $K: name :: { System.String <: $K } System.String <: $K <==> System.String == $K || System.Object <: $K || System.IComparable <: $K || System.ICloneable <: $K || System.Collections.IEnumerable <: $K); + +axiom (forall $U: name :: { $U <: System.String } $U <: System.String ==> $U == System.String); + +function Inv_System.String(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.String(this, heap) } Inv_System.String(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.String } { Inv_System.String($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.String ==> Inv_System.String($o, heap)); + +procedure System.Console.WriteLine$System.String(value$in: ref); + requires value$in == null || (cast($Heap[value$in, $writable]):bool == true && cast($Heap[value$in, $inv]):name == $typeof(value$in)); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure Microsoft.Singularity.DebugStub.Print$System.String(value$in: ref); + requires value$in == null || (cast($Heap[value$in, $writable]):bool == true && cast($Heap[value$in, $inv]):name == $typeof(value$in)); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure System.Threading.Thread.Yield(); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure Microsoft.Singularity.Applications.ThreadTest.SecondThreadMethod(); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Microsoft.Singularity.Applications.ThreadTest.SecondThreadMethod() +{ + var stack0o: ref, i: int, stack0i: int, stack0b: bool, local1: int, $Heap$block2516$LoopPreheader: [ref,name]any; + + entry: + assume IsHeap($Heap); + goto block2482; + + block2482: + goto block2499; + + block2499: + // ----- load constant Second thread! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(35,13) + stack0o := $stringLiteral5; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(35,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant Second thread! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(36,13) + stack0o := $stringLiteral6; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(36,13) + call Microsoft.Singularity.DebugStub.Print$System.String(stack0o); + // ----- load constant 0 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,18) + i := 0; + goto block2516$LoopPreheader; + + block2516: + // ----- default loop invariant: $inv field ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29) + assert (forall $o: ref :: $Heap$block2516$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block2516$LoopPreheader[$o, $allocated]):bool != true); + assert (forall $o: ref :: cast($Heap$block2516$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + // ----- load constant 10 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29) + stack0i := 10; + // ----- binary operator ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29) + stack0b := i >= stack0i; + // ----- branch ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29) + goto true2516to2550, false2516to2533; + + true2516to2550: + assume stack0b == true; + goto block2550; + + false2516to2533: + assume stack0b == false; + goto block2533; + + block2550: + // ----- load constant Second thread done! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(44,13) + stack0o := $stringLiteral8; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(44,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant Second thread done! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(45,13) + stack0o := $stringLiteral9; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(45,13) + call Microsoft.Singularity.DebugStub.Print$System.String(stack0o); + // ----- return ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(46,10) + return; + + block2533: + // ----- load constant ... [1] ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(40,17) + stack0o := $stringLiteral7; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(40,17) + // Commented out, to avoid problems with the theorem prover nondeterministically choosing this error over the one 12 lines above: call System.Console.WriteLine$System.String(stack0o); + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(41,17) + call System.Threading.Thread.Yield(); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,37) + local1 := i; + // ----- load constant 1 + stack0i := 1; + // ----- binary operator + stack0i := local1 + stack0i; + // ----- copy + i := stack0i; + // ----- copy + stack0i := local1; + // ----- branch + goto block2516; + + block2516$LoopPreheader: + $Heap$block2516$LoopPreheader := $Heap; + goto block2516; + +} + + + +procedure Microsoft.Singularity.Applications.ThreadTest.Main$System.String.array(args$in: ref) returns ($result: int); + requires args$in == null || (cast($Heap[args$in, $writable]):bool == true && cast($Heap[args$in, $inv]):name == $typeof(args$in)); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures IsAllocated($Heap, $result); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Microsoft.Singularity.Applications.ThreadTest.Main$System.String.array(args$in: ref) returns ($result: int) +{ + var args: ref, stack0o: ref, stack1o: ref, stack50000o: ref, t1: ref, t2: ref, i: int, stack0i: int, stack0b: bool, local3: int, return.value: int, SS$Display.Return.Local: int, $Heap$block3825$LoopPreheader: [ref,name]any; + + entry: + assume IsHeap($Heap); + args := args$in; + assume $Is(args, RefArray(System.String, 1)); + assume cast($Heap[args$in, $allocated]):bool == true; + goto block3791; + + block3791: + goto block3808; + + block3808: + stack0o := null; + // ----- load function ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + havoc stack1o; + // ----- new object ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + havoc stack50000o; + assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.ThreadStart; + $Heap[stack50000o, $allocated] := true; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + assert stack50000o != null; + call System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(stack50000o, stack0o, stack1o); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + stack0o := stack50000o; + // ----- new object ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + havoc stack50000o; + assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.Thread; + $Heap[stack50000o, $allocated] := true; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + assert stack50000o != null; + call System.Threading.Thread..ctor$System.Threading.ThreadStart(stack50000o, stack0o); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + stack0o := stack50000o; + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + t1 := stack0o; + stack0o := null; + // ----- load function ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + havoc stack1o; + // ----- new object ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + havoc stack50000o; + assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.ThreadStart; + $Heap[stack50000o, $allocated] := true; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + assert stack50000o != null; + call System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(stack50000o, stack0o, stack1o); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + stack0o := stack50000o; + // ----- new object ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + havoc stack50000o; + assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.Thread; + $Heap[stack50000o, $allocated] := true; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + assert stack50000o != null; + call System.Threading.Thread..ctor$System.Threading.ThreadStart(stack50000o, stack0o); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + stack0o := stack50000o; + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + t2 := stack0o; + // ----- load constant Starting first thread. ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(54,13) + stack0o := $stringLiteral10; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(54,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(55,13) + assert t1 != null; + call System.Threading.Thread.Start(t1); + // ----- load constant Started first thread. ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(56,13) + stack0o := $stringLiteral11; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(56,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant Starting second thread. ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(58,13) + stack0o := $stringLiteral12; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(58,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(59,13) + assert t2 != null; + call System.Threading.Thread.Start(t2); + // ----- load constant Started second thread. ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(60,13) + stack0o := $stringLiteral13; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(60,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant 0 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,18) + i := 0; + goto block3825$LoopPreheader; + + block3825: + // ----- default loop invariant: $inv field ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29) + assert (forall $o: ref :: $Heap$block3825$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block3825$LoopPreheader[$o, $allocated]):bool != true); + assert (forall $o: ref :: cast($Heap$block3825$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + // ----- load constant 30 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29) + stack0i := 30; + // ----- binary operator ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29) + stack0b := i >= stack0i; + // ----- branch ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29) + goto true3825to3859, false3825to3842; + + true3825to3859: + assume stack0b == true; + goto block3859; + + false3825to3842: + assume stack0b == false; + goto block3842; + + block3859: + // ----- load constant 0 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(66,13) + return.value := 0; + // ----- branch + goto block3876; + + block3842: + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(64,17) + call System.Threading.Thread.Yield(); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,37) + local3 := i; + // ----- load constant 1 + stack0i := 1; + // ----- binary operator + stack0i := local3 + stack0i; + // ----- copy + i := stack0i; + // ----- copy + stack0i := local3; + // ----- branch + goto block3825; + + block3876: + // ----- copy + SS$Display.Return.Local := return.value; + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(67,10) + stack0i := return.value; + // ----- return ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(67,10) + $result := stack0i; + return; + + block3825$LoopPreheader: + $Heap$block3825$LoopPreheader := $Heap; + goto block3825; + +} + + + +axiom $IsClass(System.Threading.ThreadStart); + +axiom $IsClass(System.MulticastDelegate); + +axiom $IsClass(System.Delegate); + +axiom System.Delegate <: System.Object && AsDirectSubClass(System.Delegate, System.Object) == System.Delegate; + +axiom Implements(System.Delegate, System.ICloneable); + +axiom (forall $K: name :: { System.Delegate <: $K } System.Delegate <: $K <==> System.Delegate == $K || System.Object <: $K || System.ICloneable <: $K); + +function Inv_System.Delegate(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Delegate(this, heap) } Inv_System.Delegate(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Delegate } { Inv_System.Delegate($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Delegate ==> Inv_System.Delegate($o, heap)); + +axiom System.MulticastDelegate <: System.Delegate && AsDirectSubClass(System.MulticastDelegate, System.Delegate) == System.MulticastDelegate; + +axiom (forall $K: name :: { System.MulticastDelegate <: $K } System.MulticastDelegate <: $K <==> System.MulticastDelegate == $K || System.Delegate <: $K); + +function Inv_System.MulticastDelegate(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.MulticastDelegate(this, heap) } Inv_System.MulticastDelegate(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.MulticastDelegate } { Inv_System.MulticastDelegate($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.MulticastDelegate ==> Inv_System.MulticastDelegate($o, heap)); + +axiom System.Threading.ThreadStart <: System.MulticastDelegate && AsDirectSubClass(System.Threading.ThreadStart, System.MulticastDelegate) == System.Threading.ThreadStart; + +axiom (forall $K: name :: { System.Threading.ThreadStart <: $K } System.Threading.ThreadStart <: $K <==> System.Threading.ThreadStart == $K || System.MulticastDelegate <: $K); + +axiom (forall $U: name :: { $U <: System.Threading.ThreadStart } $U <: System.Threading.ThreadStart ==> $U == System.Threading.ThreadStart); + +function Inv_System.Threading.ThreadStart(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Threading.ThreadStart(this, heap) } Inv_System.Threading.ThreadStart(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Threading.ThreadStart } { Inv_System.Threading.ThreadStart($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Threading.ThreadStart ==> Inv_System.Threading.ThreadStart($o, heap)); + +procedure System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(this: ref, object$in: ref, method$in: ref); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Threading.ThreadStart; + + + +axiom $IsClass(System.Threading.Thread); + +axiom System.Threading.Thread <: System.Object && AsDirectSubClass(System.Threading.Thread, System.Object) == System.Threading.Thread; + +axiom (forall $K: name :: { System.Threading.Thread <: $K } System.Threading.Thread <: $K <==> System.Threading.Thread == $K || System.Object <: $K); + +axiom (forall $U: name :: { $U <: System.Threading.Thread } $U <: System.Threading.Thread ==> $U == System.Threading.Thread); + +function Inv_System.Threading.Thread(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Threading.Thread(this, heap) } Inv_System.Threading.Thread(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Threading.Thread } { Inv_System.Threading.Thread($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Threading.Thread ==> Inv_System.Threading.Thread($o, heap)); + +procedure System.Threading.Thread..ctor$System.Threading.ThreadStart(this: ref, start$in: ref); + requires start$in == null || (cast($Heap[start$in, $writable]):bool == true && cast($Heap[start$in, $inv]):name == $typeof(start$in)); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(System.Threading.Thread <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Threading.Thread; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + + + +procedure System.Threading.Thread.Start(this: ref); + requires cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == $typeof(this); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure Microsoft.Singularity.Applications.ThreadTest..ctor(this: ref); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(Microsoft.Singularity.Applications.ThreadTest <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == Microsoft.Singularity.Applications.ThreadTest; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + + + +implementation Microsoft.Singularity.Applications.ThreadTest..ctor(this: ref) +{ + + entry: + assume IsHeap($Heap); + assume $IsNotNull(this, Microsoft.Singularity.Applications.ThreadTest); + assume cast($Heap[this, $allocated]):bool == true; + assume cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object; + goto block4777; + + block4777: + goto block4794; + + block4794: + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(17,18) + assert this != null; + call System.Object..ctor(this); + // ----- return ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(17,28) + assert this != null; + assert cast($Heap[this, $writable]):bool == true && System.Object <: cast($Heap[this, $inv]):name; + assert cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object; + assert Inv_Microsoft.Singularity.Applications.ThreadTest(this, $Heap); + $Heap[this, $inv] := Microsoft.Singularity.Applications.ThreadTest; + return; + +} + + + +procedure System.Object..ctor(this: ref); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(System.Object <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + + + +type ref, name, any; +const null : ref; diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl new file mode 100644 index 00000000..da529b84 --- /dev/null +++ b/Test/test2/strings-where.bpl @@ -0,0 +1,995 @@ +type real; + +type elements; + +type struct; + +var $Heap: [ref,name]any where IsHeap($Heap); +function cast(S) returns (T); +function IsHeap(h: [ref,name]any) returns (bool); + +const unique $allocated: name; + +const unique $elements: name; + +const unique $inv: name; + +const unique $writable: name; + +const unique $sharingMode: name; + +const unique $SharingMode_Unshared: name; + +const unique $SharingMode_LockProtected: name; + +function ClassRepr(class: name) returns (ref); + +axiom (forall c0: name, c1: name :: c0 != c1 ==> ClassRepr(c0) != ClassRepr(c1)); + +axiom (forall T: name :: !($typeof(ClassRepr(T)) <: System.Object)); + +axiom (forall T: name :: ClassRepr(T) != null); + +axiom (forall T: name, h: [ref,name]any :: { h[ClassRepr(T), $writable] } IsHeap(h) ==> cast(h[ClassRepr(T), $writable]):bool); + +function IsDirectlyModifiableField(f: name) returns (bool); + +axiom !IsDirectlyModifiableField($allocated); + +axiom IsDirectlyModifiableField($elements); + +axiom !IsDirectlyModifiableField($inv); + +axiom !IsDirectlyModifiableField($writable); + +function IsStaticField(f: name) returns (bool); + +axiom !IsStaticField($allocated); + +axiom !IsStaticField($elements); + +axiom !IsStaticField($inv); + +axiom !IsStaticField($writable); + +function ValueArrayGet(elements, int) returns (any); + +function ValueArraySet(elements, int, any) returns (elements); + +function RefArrayGet(elements, int) returns (ref); + +function RefArraySet(elements, int, ref) returns (elements); + +axiom (forall A: elements, i: int, x: any :: ValueArrayGet(ValueArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: any :: i != j ==> ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(A, j)); + +axiom (forall A: elements, i: int, x: ref :: RefArrayGet(RefArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: ref :: i != j ==> RefArrayGet(RefArraySet(A, i, x), j) == RefArrayGet(A, j)); + +function ArrayIndex(arr: ref, dim: int, indexAtDim: int, remainingIndexContribution: int) returns (int); + +axiom (forall a: ref, d: int, x: int, y: int, x': int, y': int :: ArrayIndex(a, d, x, y) == ArrayIndex(a, d, x', y') ==> x == x' && y == y'); + +axiom (forall a: ref, T: name, i: int, r: int, heap: [ref,name]any :: $typeof(a) <: RefArray(T, r) ==> $Is(RefArrayGet(cast(heap[a, $elements]):elements, i), T)); + +function $Rank(ref) returns (int); + +axiom (forall a: ref :: 1 <= $Rank(a)); + +axiom (forall a: ref, T: name, r: int :: { $Is(a, ValueArray(T, r)) } $Is(a, ValueArray(T, r)) ==> $Rank(a) == r); + +axiom (forall a: ref, T: name, r: int :: { $Is(a, RefArray(T, r)) } $Is(a, RefArray(T, r)) ==> $Rank(a) == r); + +function $Length(ref) returns (int); + +axiom (forall a: ref :: { $Length(a) } 0 <= $Length(a)); + +function $DimLength(ref, int) returns (int); + +axiom (forall a: ref, i: int :: 0 <= $DimLength(a, i)); + +axiom (forall a: ref :: $Rank(a) == 1 ==> $DimLength(a, 0) == $Length(a)); + +function $LBound(ref, int) returns (int); + +function $UBound(ref, int) returns (int); + +axiom (forall a: ref, i: int :: { $LBound(a, i) } $LBound(a, i) == 0); + +axiom (forall a: ref, i: int :: { $UBound(a, i) } $UBound(a, i) == $DimLength(a, i) - 1); + +const unique System.Array: name; + +axiom $IsClass(System.Array); + +axiom System.Array <: System.Object; + +function $ElementType(name) returns (name); + +function ValueArray(elementType: name, rank: int) returns (name); + +axiom (forall T: name, r: int :: { ValueArray(T, r) } ValueArray(T, r) <: System.Array); + +function RefArray(elementType: name, rank: int) returns (name); + +axiom (forall T: name, r: int :: { RefArray(T, r) } RefArray(T, r) <: System.Array); + +axiom (forall T: name, U: name, r: int :: U <: T ==> RefArray(U, r) <: RefArray(T, r)); + +axiom (forall A: name, r: int :: $ElementType(ValueArray(A, r)) == A); + +axiom (forall A: name, r: int :: $ElementType(RefArray(A, r)) == A); + +axiom (forall A: name, r: int, T: name :: { T <: RefArray(A, r) } T <: RefArray(A, r) ==> T == RefArray($ElementType(T), r) && $ElementType(T) <: A); + +axiom (forall A: name, r: int, T: name :: { T <: ValueArray(A, r) } T <: ValueArray(A, r) ==> T == ValueArray(A, r)); + +axiom (forall A: name, r: int, T: name :: RefArray(A, r) <: T ==> System.Array <: T || (T == RefArray($ElementType(T), r) && A <: $ElementType(T))); + +axiom (forall A: name, r: int, T: name :: ValueArray(A, r) <: T ==> System.Array <: T || T == ValueArray(A, r)); + +function $ArrayPtr(elementType: name) returns (name); + +function $StructGet(struct, name) returns (any); + +function $StructSet(struct, name, any) returns (struct); + +axiom (forall s: struct, f: name, x: any :: $StructGet($StructSet(s, f, x), f) == x); + +axiom (forall s: struct, f: name, f': name, x: any :: f != f' ==> $StructGet($StructSet(s, f, x), f') == $StructGet(s, f')); + +function ZeroInit(s: struct, typ: name) returns (bool); + +function $typeof(ref) returns (name); + +function Implements(class: name, interface: name) returns (bool); + +axiom (forall T: name, J: name :: { Implements(T, J) } Implements(T, J) ==> T <: J); + +function InterfaceExtends(subIntf: name, superIntf: name) returns (bool); + +axiom (forall J: name, K: name :: { InterfaceExtends(J, K) } InterfaceExtends(J, K) ==> J <: K); + +function $IsClass(name) returns (bool); + +axiom (forall C: name :: { $IsClass(C) } $IsClass(C) ==> C <: C); + +function AsDirectSubClass(sub: name, base: name) returns (sub': name); + +function OneClassDown(sub: name, base: name) returns (directSub: name); + +axiom (forall A: name, B: name, C: name :: { C <: AsDirectSubClass(B, A) } C <: AsDirectSubClass(B, A) ==> OneClassDown(C, A) == B); + +function $IsInterface(name) returns (bool); + +axiom (forall J: name :: { $IsInterface(J) } $IsInterface(J) ==> J <: System.Object); + +function $IsValueType(name) returns (bool); + +axiom (forall T: name :: $IsValueType(T) ==> (forall U: name :: T <: U ==> T == U) && (forall U: name :: U <: T ==> T == U)); + +const unique System.Object: name; + +axiom $IsClass(System.Object); + +function $IsTokenForType(struct, name) returns (bool); + +function TypeObject(name) returns (ref); + +const unique System.Type: name; + +axiom System.Type <: System.Object; + +axiom (forall T: name :: { TypeObject(T) } $IsNotNull(TypeObject(T), System.Type)); + +function $Is(ref, name) returns (bool); + +axiom (forall o: ref, T: name :: { $Is(o, T) } $Is(o, T) <==> o == null || $typeof(o) <: T); + +function $IsNotNull(ref, name) returns (bool); + +axiom (forall o: ref, T: name :: { $IsNotNull(o, T) } $IsNotNull(o, T) <==> o != null && $Is(o, T)); + +function $As(ref, name) returns (ref); + +axiom (forall o: ref, T: name :: $Is(o, T) ==> $As(o, T) == o); + +axiom (forall o: ref, T: name :: !$Is(o, T) ==> $As(o, T) == null); + +axiom (forall heap: [ref,name]any, o: ref, A: name, r: int :: $Is(o, RefArray(A, r)) ==> heap[o, $inv] == $typeof(o)); + +axiom (forall heap: [ref,name]any, o: ref, A: name, r: int :: $Is(o, ValueArray(A, r)) ==> heap[o, $inv] == $typeof(o)); + +function IsAllocated(h: [ref,name]any, o: any) returns (bool); + +axiom (forall h: [ref,name]any, o: ref, f: name :: { IsAllocated(h, h[o, f]) } IsHeap(h) ==> IsAllocated(h, h[o, f])); + +axiom (forall h: [ref,name]any, s: struct, f: name :: { IsAllocated(h, $StructGet(s, f)) } IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))); + +axiom (forall h: [ref,name]any, e: elements, i: int :: { IsAllocated(h, RefArrayGet(e, i)) } IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))); + +axiom (forall h: [ref,name]any, o: ref :: { h[o, $allocated] } IsAllocated(h, o) ==> cast(h[o, $allocated]):bool); + +axiom (forall h: [ref,name]any, c: name :: { h[ClassRepr(c), $allocated] } IsHeap(h) ==> cast(h[ClassRepr(c), $allocated]):bool); + +function DeclType(field: name) returns (class: name); + +function AsNonNullRefField(field: name, T: name) returns (f: name); + +function AsRefField(field: name, T: name) returns (f: name); + +function AsRangeField(field: name, T: name) returns (f: name); + +axiom (forall f: name, T: name :: { AsNonNullRefField(f, T) } AsNonNullRefField(f, T) == f ==> AsRefField(f, T) == f); + +axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsRefField(f, T)] } IsHeap(h) ==> $Is(cast(h[o, AsRefField(f, T)]):ref, T)); + +axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsNonNullRefField(f, T)] } IsHeap(h) ==> cast(h[o, AsNonNullRefField(f, T)]):ref != null); + +axiom (forall h: [ref,name]any, o: ref, f: name, T: name :: { h[o, AsRangeField(f, T)] } IsHeap(h) ==> InRange(cast(h[o, AsRangeField(f, T)]):int, T)); + +const unique System.String: name; + +axiom (forall h: [ref,name]any, s: ref :: IsHeap(h) && $typeof(s) == System.String ==> h[s, $inv] == $typeof(s) && cast(h[s, $writable]):bool); + +function AsOwnedField(f: name) returns (name); + +axiom (forall h: [ref,name]any, o: ref, f: name :: { h[o, AsOwnedField(f)] } IsHeap(h) && cast(h[o, $inv]):name <: DeclType(AsOwnedField(f)) ==> cast(h[o, AsOwnedField(f)]):ref == null || $typeof(cast(h[o, AsOwnedField(f)]):ref) == System.String || !cast(h[cast(h[o, AsOwnedField(f)]):ref, $writable]):bool); + +axiom (forall h: [ref,name]any, o: ref :: { h[o, $writable] } IsHeap(h) && !cast(h[o, $writable]):bool ==> cast(h[o, $inv]):name == $typeof(o)); + +function Box(any, ref) returns (ref); + +function Unbox(ref) returns (any); + +axiom (forall x: any, p: ref :: { Unbox(Box(x, p)) } Unbox(Box(x, p)) == x); + +axiom (forall heap: [ref,name]any, x: any, p: ref :: { heap[Box(x, p), $inv] } IsHeap(heap) ==> heap[Box(x, p), $inv] == $typeof(Box(x, p))); + +function UnboxedType(ref) returns (name); + +function BoxTester(p: ref, typ: name) returns (ref); + +axiom (forall p: ref, typ: name :: { BoxTester(p, typ) } UnboxedType(p) == typ <==> BoxTester(p, typ) != null); + +const unique System.Int16: name; + +axiom $IsValueType(System.Int16); + +const unique System.Int32: name; + +axiom $IsValueType(System.Int32); + +const unique System.Int64: name; + +axiom $IsValueType(System.Int64); + +const unique System.Byte: name; + +axiom $IsValueType(System.Byte); + +const unique System.Int16.MinValue: int; + +const unique System.Int16.MaxValue: int; + +const unique System.Int32.MinValue: int; + +const unique System.Int32.MaxValue: int; + +const unique System.Int64.MinValue: int; + +const unique System.Int64.MaxValue: int; + +axiom System.Int64.MinValue < System.Int32.MinValue; + +axiom System.Int32.MinValue < System.Int16.MinValue; + +axiom System.Int16.MinValue < System.Int16.MaxValue; + +axiom System.Int16.MaxValue < System.Int32.MaxValue; + +axiom System.Int32.MaxValue < System.Int64.MaxValue; + +function InRange(i: int, T: name) returns (bool); + +axiom (forall i: int :: InRange(i, System.Int16) <==> System.Int16.MinValue <= i && i <= System.Int16.MaxValue); + +axiom (forall i: int :: InRange(i, System.Int32) <==> System.Int32.MinValue <= i && i <= System.Int32.MaxValue); + +axiom (forall i: int :: InRange(i, System.Int64) <==> System.Int64.MinValue <= i && i <= System.Int64.MaxValue); + +axiom (forall i: int :: { InRange(i, System.Byte) } InRange(i, System.Byte) <==> 0 <= i && i < 256); + +function $RealToInt(real) returns (int); + +function $IntToReal(int) returns (real); + +function $SizeIs(name, int) returns (bool); + +function $IfThenElse(bool, any, any) returns (any); + +axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } b ==> $IfThenElse(b, x, y) == x); + +axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } !b ==> $IfThenElse(b, x, y) == y); + +function #neg(int) returns (int); + +function #rneg(real) returns (real); + +function #rdiv(real, real) returns (real); + +function #and(int, int) returns (int); + +function #or(int, int) returns (int); + +function #xor(int, int) returns (int); + +function #shl(int, int) returns (int); + +function #shr(int, int) returns (int); + +axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y); + +axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y); + +axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y); + +axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0); + +axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0); + +axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y); + +axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y); + +axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y); + +axiom (forall a: int, b: int, d: int :: { a % d,b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b); + +axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i); + +axiom (forall i: int, j: int :: 0 <= j ==> #shl(i, j + 1) == #shl(i, j) * 2); + +axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i); + +axiom (forall i: int, j: int :: 0 <= j ==> #shr(i, j + 1) == #shr(i, j) / 2); + +const unique $UnknownRef: ref; + +const unique System.IComparable: name; + +const unique Microsoft.Singularity.Applications.ThreadTest: name; + +const unique System.Threading.Thread: name; + +const unique System.Collections.IEnumerable: name; + +const unique System.Threading.ThreadStart: name; + +const unique System.ICloneable: name; + +const unique System.MulticastDelegate: name; + +const unique System.Delegate: name; + +const unique $stringLiteral0: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral0, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral0, $allocated]):bool) && $IsNotNull($stringLiteral0, System.String) && $Length($stringLiteral0) == 13; + +const unique $stringLiteral1: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral1, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral1, $allocated]):bool) && $IsNotNull($stringLiteral1, System.String) && $Length($stringLiteral1) == 14; + +const unique $stringLiteral2: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral2, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral2, $allocated]):bool) && $IsNotNull($stringLiteral2, System.String) && $Length($stringLiteral2) == 11; + +const unique $stringLiteral3: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral3, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral3, $allocated]):bool) && $IsNotNull($stringLiteral3, System.String) && $Length($stringLiteral3) == 18; + +const unique $stringLiteral4: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral4, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral4, $allocated]):bool) && $IsNotNull($stringLiteral4, System.String) && $Length($stringLiteral4) == 19; + +const unique $stringLiteral5: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral5, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral5, $allocated]):bool) && $IsNotNull($stringLiteral5, System.String) && $Length($stringLiteral5) == 14; + +const unique $stringLiteral6: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral6, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral6, $allocated]):bool) && $IsNotNull($stringLiteral6, System.String) && $Length($stringLiteral6) == 15; + +const unique $stringLiteral7: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral7, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral7, $allocated]):bool) && $IsNotNull($stringLiteral7, System.String) && $Length($stringLiteral7) == 11; + +const unique $stringLiteral8: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral8, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral8, $allocated]):bool) && $IsNotNull($stringLiteral8, System.String) && $Length($stringLiteral8) == 19; + +const unique $stringLiteral9: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral9, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral9, $allocated]):bool) && $IsNotNull($stringLiteral9, System.String) && $Length($stringLiteral9) == 20; + +const unique $stringLiteral10: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral10, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral10, $allocated]):bool) && $IsNotNull($stringLiteral10, System.String) && $Length($stringLiteral10) == 22; + +const unique $stringLiteral11: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral11, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral11, $allocated]):bool) && $IsNotNull($stringLiteral11, System.String) && $Length($stringLiteral11) == 21; + +const unique $stringLiteral12: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral12, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral12, $allocated]):bool) && $IsNotNull($stringLiteral12, System.String) && $Length($stringLiteral12) == 23; + +const unique $stringLiteral13: ref; + +axiom (forall heap: [ref,name]any :: { cast(heap[$stringLiteral13, $allocated]):bool } IsHeap(heap) ==> cast(heap[$stringLiteral13, $allocated]):bool) && $IsNotNull($stringLiteral13, System.String) && $Length($stringLiteral13) == 22; + +axiom $IsClass(Microsoft.Singularity.Applications.ThreadTest); + +axiom Microsoft.Singularity.Applications.ThreadTest <: System.Object && AsDirectSubClass(Microsoft.Singularity.Applications.ThreadTest, System.Object) == Microsoft.Singularity.Applications.ThreadTest; + +axiom (forall $K: name :: { Microsoft.Singularity.Applications.ThreadTest <: $K } Microsoft.Singularity.Applications.ThreadTest <: $K <==> Microsoft.Singularity.Applications.ThreadTest == $K || System.Object <: $K); + +function Inv_Microsoft.Singularity.Applications.ThreadTest(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_Microsoft.Singularity.Applications.ThreadTest(this, heap) } Inv_Microsoft.Singularity.Applications.ThreadTest(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: Microsoft.Singularity.Applications.ThreadTest } { Inv_Microsoft.Singularity.Applications.ThreadTest($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: Microsoft.Singularity.Applications.ThreadTest ==> Inv_Microsoft.Singularity.Applications.ThreadTest($o, heap)); + +procedure Microsoft.Singularity.Applications.ThreadTest.FirstThreadMethod(); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Microsoft.Singularity.Applications.ThreadTest.FirstThreadMethod() +{ + var stack0o: ref, i: int, stack0i: int, stack0b: bool, local1: int, $Heap$block1513$LoopPreheader: [ref,name]any; + + entry: + assume IsHeap($Heap); + goto block1479; + + block1479: + goto block1496; + + block1496: + // ----- load constant First thread! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(21,13) + stack0o := $stringLiteral0; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(21,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant First thread! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(22,13) + stack0o := $stringLiteral1; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(22,13) + call Microsoft.Singularity.DebugStub.Print$System.String(stack0o); + // ----- load constant 0 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,18) + i := 0; + goto block1513$LoopPreheader; + + block1513: + // ----- default loop invariant: $inv field ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29) + assert (forall $o: ref :: $Heap$block1513$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block1513$LoopPreheader[$o, $allocated]):bool != true); + assert (forall $o: ref :: cast($Heap$block1513$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + // ----- load constant 10 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29) + stack0i := 10; + // ----- binary operator ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29) + stack0b := i >= stack0i; + // ----- branch ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,29) + goto true1513to1547, false1513to1530; + + true1513to1547: + assume stack0b == true; + goto block1547; + + false1513to1530: + assume stack0b == false; + goto block1530; + + block1547: + // ----- load constant First thread done! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(29,13) + stack0o := $stringLiteral3; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(29,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant First thread done! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(30,13) + stack0o := $stringLiteral4; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(30,13) + call Microsoft.Singularity.DebugStub.Print$System.String(stack0o); + // ----- return ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(31,10) + return; + + block1530: + // ----- load constant [0] ... ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(25,17) + stack0o := $stringLiteral2; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(25,17) + call System.Console.WriteLine$System.String(stack0o); + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(26,17) + call System.Threading.Thread.Yield(); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(24,37) + local1 := i; + // ----- load constant 1 + stack0i := 1; + // ----- binary operator + stack0i := local1 + stack0i; + // ----- copy + i := stack0i; + // ----- copy + stack0i := local1; + // ----- branch + goto block1513; + + block1513$LoopPreheader: + $Heap$block1513$LoopPreheader := $Heap; + goto block1513; + +} + + + +axiom $IsClass(System.String); + +axiom System.String <: System.Object && AsDirectSubClass(System.String, System.Object) == System.String; + +axiom $IsInterface(System.IComparable); + +axiom (forall $K: name :: { System.IComparable <: $K } System.IComparable <: $K <==> System.IComparable == $K || System.Object == $K); + +axiom Implements(System.String, System.IComparable); + +axiom $IsInterface(System.ICloneable); + +axiom (forall $K: name :: { System.ICloneable <: $K } System.ICloneable <: $K <==> System.ICloneable == $K || System.Object == $K); + +axiom Implements(System.String, System.ICloneable); + +axiom $IsInterface(System.Collections.IEnumerable); + +axiom (forall $K: name :: { System.Collections.IEnumerable <: $K } System.Collections.IEnumerable <: $K <==> System.Collections.IEnumerable == $K || System.Object == $K); + +axiom Implements(System.String, System.Collections.IEnumerable); + +axiom (forall $K: name :: { System.String <: $K } System.String <: $K <==> System.String == $K || System.Object <: $K || System.IComparable <: $K || System.ICloneable <: $K || System.Collections.IEnumerable <: $K); + +axiom (forall $U: name :: { $U <: System.String } $U <: System.String ==> $U == System.String); + +function Inv_System.String(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.String(this, heap) } Inv_System.String(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.String } { Inv_System.String($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.String ==> Inv_System.String($o, heap)); + +procedure System.Console.WriteLine$System.String(value$in: ref); + requires value$in == null || (cast($Heap[value$in, $writable]):bool == true && cast($Heap[value$in, $inv]):name == $typeof(value$in)); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure Microsoft.Singularity.DebugStub.Print$System.String(value$in: ref); + requires value$in == null || (cast($Heap[value$in, $writable]):bool == true && cast($Heap[value$in, $inv]):name == $typeof(value$in)); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure System.Threading.Thread.Yield(); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure Microsoft.Singularity.Applications.ThreadTest.SecondThreadMethod(); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Microsoft.Singularity.Applications.ThreadTest.SecondThreadMethod() +{ + var stack0o: ref, i: int, stack0i: int, stack0b: bool, local1: int, $Heap$block2516$LoopPreheader: [ref,name]any; + + entry: + assume IsHeap($Heap); + goto block2482; + + block2482: + goto block2499; + + block2499: + // ----- load constant Second thread! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(35,13) + stack0o := $stringLiteral5; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(35,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant Second thread! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(36,13) + stack0o := $stringLiteral6; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(36,13) + call Microsoft.Singularity.DebugStub.Print$System.String(stack0o); + // ----- load constant 0 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,18) + i := 0; + goto block2516$LoopPreheader; + + block2516: + // ----- default loop invariant: $inv field ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29) + assert (forall $o: ref :: $Heap$block2516$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block2516$LoopPreheader[$o, $allocated]):bool != true); + assert (forall $o: ref :: cast($Heap$block2516$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + // ----- load constant 10 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29) + stack0i := 10; + // ----- binary operator ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29) + stack0b := i >= stack0i; + // ----- branch ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,29) + goto true2516to2550, false2516to2533; + + true2516to2550: + assume stack0b == true; + goto block2550; + + false2516to2533: + assume stack0b == false; + goto block2533; + + block2550: + // ----- load constant Second thread done! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(44,13) + stack0o := $stringLiteral8; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(44,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant Second thread done! ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(45,13) + stack0o := $stringLiteral9; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(45,13) + call Microsoft.Singularity.DebugStub.Print$System.String(stack0o); + // ----- return ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(46,10) + return; + + block2533: + // ----- load constant ... [1] ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(40,17) + stack0o := $stringLiteral7; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(40,17) + call System.Console.WriteLine$System.String(stack0o); + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(41,17) + call System.Threading.Thread.Yield(); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(38,37) + local1 := i; + // ----- load constant 1 + stack0i := 1; + // ----- binary operator + stack0i := local1 + stack0i; + // ----- copy + i := stack0i; + // ----- copy + stack0i := local1; + // ----- branch + goto block2516; + + block2516$LoopPreheader: + $Heap$block2516$LoopPreheader := $Heap; + goto block2516; + +} + + + +procedure Microsoft.Singularity.Applications.ThreadTest.Main$System.String.array(args$in: ref) returns ($result: int); + requires args$in == null || (cast($Heap[args$in, $writable]):bool == true && cast($Heap[args$in, $inv]):name == $typeof(args$in)); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures IsAllocated($Heap, $result); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Microsoft.Singularity.Applications.ThreadTest.Main$System.String.array(args$in: ref) returns ($result: int) +{ + var args: ref, stack0o: ref, stack1o: ref, stack50000o: ref, t1: ref, t2: ref, i: int, stack0i: int, stack0b: bool, local3: int, return.value: int, SS$Display.Return.Local: int, $Heap$block3825$LoopPreheader: [ref,name]any; + + entry: + assume IsHeap($Heap); + args := args$in; + assume $Is(args, RefArray(System.String, 1)); + assume cast($Heap[args$in, $allocated]):bool == true; + goto block3791; + + block3791: + goto block3808; + + block3808: + stack0o := null; + // ----- load function ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + havoc stack1o; + // ----- new object ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + havoc stack50000o; + assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.ThreadStart; + $Heap[stack50000o, $allocated] := true; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + assert stack50000o != null; + call System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(stack50000o, stack0o, stack1o); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + stack0o := stack50000o; + // ----- new object ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + havoc stack50000o; + assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.Thread; + $Heap[stack50000o, $allocated] := true; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + assert stack50000o != null; + call System.Threading.Thread..ctor$System.Threading.ThreadStart(stack50000o, stack0o); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + stack0o := stack50000o; + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(51,13) + t1 := stack0o; + stack0o := null; + // ----- load function ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + havoc stack1o; + // ----- new object ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + havoc stack50000o; + assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.ThreadStart; + $Heap[stack50000o, $allocated] := true; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + assert stack50000o != null; + call System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(stack50000o, stack0o, stack1o); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + stack0o := stack50000o; + // ----- new object ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + havoc stack50000o; + assume cast($Heap[stack50000o, $allocated]):bool == false && stack50000o != null && $typeof(stack50000o) == System.Threading.Thread; + $Heap[stack50000o, $allocated] := true; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + assert stack50000o != null; + call System.Threading.Thread..ctor$System.Threading.ThreadStart(stack50000o, stack0o); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + stack0o := stack50000o; + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(52,13) + t2 := stack0o; + // ----- load constant Starting first thread. ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(54,13) + stack0o := $stringLiteral10; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(54,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(55,13) + assert t1 != null; + call System.Threading.Thread.Start(t1); + // ----- load constant Started first thread. ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(56,13) + stack0o := $stringLiteral11; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(56,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant Starting second thread. ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(58,13) + stack0o := $stringLiteral12; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(58,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(59,13) + assert t2 != null; + call System.Threading.Thread.Start(t2); + // ----- load constant Started second thread. ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(60,13) + stack0o := $stringLiteral13; + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(60,13) + call System.Console.WriteLine$System.String(stack0o); + // ----- load constant 0 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,18) + i := 0; + goto block3825$LoopPreheader; + + block3825: + // ----- default loop invariant: $inv field ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29) + assert (forall $o: ref :: $Heap$block3825$LoopPreheader[$o, $inv] == $Heap[$o, $inv] || cast($Heap$block3825$LoopPreheader[$o, $allocated]):bool != true); + assert (forall $o: ref :: cast($Heap$block3825$LoopPreheader[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + // ----- load constant 30 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29) + stack0i := 30; + // ----- binary operator ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29) + stack0b := i >= stack0i; + // ----- branch ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,29) + goto true3825to3859, false3825to3842; + + true3825to3859: + assume stack0b == true; + goto block3859; + + false3825to3842: + assume stack0b == false; + goto block3842; + + block3859: + // ----- load constant 0 ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(66,13) + return.value := 0; + // ----- branch + goto block3876; + + block3842: + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(64,17) + call System.Threading.Thread.Yield(); + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(62,37) + local3 := i; + // ----- load constant 1 + stack0i := 1; + // ----- binary operator + stack0i := local3 + stack0i; + // ----- copy + i := stack0i; + // ----- copy + stack0i := local3; + // ----- branch + goto block3825; + + block3876: + // ----- copy + SS$Display.Return.Local := return.value; + // ----- copy ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(67,10) + stack0i := return.value; + // ----- return ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(67,10) + $result := stack0i; + return; + + block3825$LoopPreheader: + $Heap$block3825$LoopPreheader := $Heap; + goto block3825; + +} + + + +axiom $IsClass(System.Threading.ThreadStart); + +axiom $IsClass(System.MulticastDelegate); + +axiom $IsClass(System.Delegate); + +axiom System.Delegate <: System.Object && AsDirectSubClass(System.Delegate, System.Object) == System.Delegate; + +axiom Implements(System.Delegate, System.ICloneable); + +axiom (forall $K: name :: { System.Delegate <: $K } System.Delegate <: $K <==> System.Delegate == $K || System.Object <: $K || System.ICloneable <: $K); + +function Inv_System.Delegate(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Delegate(this, heap) } Inv_System.Delegate(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Delegate } { Inv_System.Delegate($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Delegate ==> Inv_System.Delegate($o, heap)); + +axiom System.MulticastDelegate <: System.Delegate && AsDirectSubClass(System.MulticastDelegate, System.Delegate) == System.MulticastDelegate; + +axiom (forall $K: name :: { System.MulticastDelegate <: $K } System.MulticastDelegate <: $K <==> System.MulticastDelegate == $K || System.Delegate <: $K); + +function Inv_System.MulticastDelegate(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.MulticastDelegate(this, heap) } Inv_System.MulticastDelegate(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.MulticastDelegate } { Inv_System.MulticastDelegate($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.MulticastDelegate ==> Inv_System.MulticastDelegate($o, heap)); + +axiom System.Threading.ThreadStart <: System.MulticastDelegate && AsDirectSubClass(System.Threading.ThreadStart, System.MulticastDelegate) == System.Threading.ThreadStart; + +axiom (forall $K: name :: { System.Threading.ThreadStart <: $K } System.Threading.ThreadStart <: $K <==> System.Threading.ThreadStart == $K || System.MulticastDelegate <: $K); + +axiom (forall $U: name :: { $U <: System.Threading.ThreadStart } $U <: System.Threading.ThreadStart ==> $U == System.Threading.ThreadStart); + +function Inv_System.Threading.ThreadStart(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Threading.ThreadStart(this, heap) } Inv_System.Threading.ThreadStart(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Threading.ThreadStart } { Inv_System.Threading.ThreadStart($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Threading.ThreadStart ==> Inv_System.Threading.ThreadStart($o, heap)); + +procedure System.Threading.ThreadStart..ctor$System.Object$System.IntPtr(this: ref, object$in: ref, method$in: ref); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Threading.ThreadStart; + + + +axiom $IsClass(System.Threading.Thread); + +axiom System.Threading.Thread <: System.Object && AsDirectSubClass(System.Threading.Thread, System.Object) == System.Threading.Thread; + +axiom (forall $K: name :: { System.Threading.Thread <: $K } System.Threading.Thread <: $K <==> System.Threading.Thread == $K || System.Object <: $K); + +axiom (forall $U: name :: { $U <: System.Threading.Thread } $U <: System.Threading.Thread ==> $U == System.Threading.Thread); + +function Inv_System.Threading.Thread(object: ref, heap: [ref,name]any) returns (result: bool); + +axiom (forall this: ref, heap: [ref,name]any :: { Inv_System.Threading.Thread(this, heap) } Inv_System.Threading.Thread(this, heap) <==> true); + +axiom (forall $o: ref, heap: [ref,name]any :: { cast(heap[$o, $inv]):name <: System.Threading.Thread } { Inv_System.Threading.Thread($o, heap) } IsHeap(heap) && cast(heap[$o, $inv]):name <: System.Threading.Thread ==> Inv_System.Threading.Thread($o, heap)); + +procedure System.Threading.Thread..ctor$System.Threading.ThreadStart(this: ref, start$in: ref); + requires start$in == null || (cast($Heap[start$in, $writable]):bool == true && cast($Heap[start$in, $inv]):name == $typeof(start$in)); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(System.Threading.Thread <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Threading.Thread; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + + + +procedure System.Threading.Thread.Start(this: ref); + requires cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == $typeof(this); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure Microsoft.Singularity.Applications.ThreadTest..ctor(this: ref); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(Microsoft.Singularity.Applications.ThreadTest <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == Microsoft.Singularity.Applications.ThreadTest; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + + + +implementation Microsoft.Singularity.Applications.ThreadTest..ctor(this: ref) +{ + + entry: + assume IsHeap($Heap); + assume $IsNotNull(this, Microsoft.Singularity.Applications.ThreadTest); + assume cast($Heap[this, $allocated]):bool == true; + assume cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object; + goto block4777; + + block4777: + goto block4794; + + block4794: + // ----- call ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(17,18) + assert this != null; + call System.Object..ctor(this); + // ----- return ----- C:\Maf\Singularity\base\Applications\Tests\ThreadTest\ThreadTest.cs(17,28) + assert this != null; + assert cast($Heap[this, $writable]):bool == true && System.Object <: cast($Heap[this, $inv]):name; + assert cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object; + assert Inv_Microsoft.Singularity.Applications.ThreadTest(this, $Heap); + $Heap[this, $inv] := Microsoft.Singularity.Applications.ThreadTest; + return; + +} + + + +procedure System.Object..ctor(this: ref); + modifies $Heap; + free ensures IsHeap($Heap); + free ensures (forall $o: ref, $f: name :: $f != $inv && $o != null && cast(old($Heap)[$o, $allocated]):bool == true && cast(old($Heap)[$o, $writable]):bool == true && (!IsStaticField($f) || !IsDirectlyModifiableField($f)) && ($o != this || !(System.Object <: DeclType($f))) ==> old($Heap[$o, $f]) == $Heap[$o, $f]); + free ensures (forall $o: ref :: $o == this || old($Heap)[$o, $inv] == $Heap[$o, $inv] || cast(old($Heap)[$o, $allocated]):bool != true); + free ensures (forall $o: ref :: cast(old($Heap)[$o, $allocated]):bool ==> cast($Heap[$o, $allocated]):bool); + free ensures (forall $o: ref :: $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + ensures cast($Heap[this, $writable]):bool == true && cast($Heap[this, $inv]):name == System.Object; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + + + +type ref, name, any; +const null : ref; -- cgit v1.2.3