diff options
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/codeexpr/Answer | 2 | ||||
| -rw-r--r-- | Test/inline/Answer | 124 | ||||
| -rw-r--r-- | Test/lazyinline/Answer | 4 | ||||
| -rw-r--r-- | Test/stratifiedinline/Answer | 4 | ||||
| -rw-r--r-- | Test/test2/Answer | 30 |
5 files changed, 82 insertions, 82 deletions
diff --git a/Test/codeexpr/Answer b/Test/codeexpr/Answer index 55709034..9c22ca61 100644 --- a/Test/codeexpr/Answer +++ b/Test/codeexpr/Answer @@ -13,7 +13,7 @@ Execution trace: Boogie program verifier finished with 3 verified, 3 errors
------------------------------ CodeExpr1.bpl ---------------------
-CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold at this return statement.
+CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold on this return path.
CodeExpr1.bpl(40,3): Related location: This is the postcondition that might not hold.
Execution trace:
CodeExpr1.bpl(42,3): start
diff --git a/Test/inline/Answer b/Test/inline/Answer index 12cb5960..0820093a 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -1,8 +1,8 @@ -------------------- test0.bpl --------------------
test0.bpl(30,5): Error BP5001: This assertion might not hold.
Execution trace:
- test0.bpl(26,3): anon0
- test0.bpl(30,5): anon3_Then
+ test0.bpl(26,3): anon0
+ test0.bpl(30,5): anon3_Then
Boogie program verifier finished with 1 verified, 1 error
-------------------- test1.bpl --------------------
@@ -819,44 +819,44 @@ implementation find(A: [int]int, size: int, x: int) returns (ret: int, found: bo }
-<console>(68,4): Error BP5003: A postcondition might not hold at this return statement.
+<console>(68,4): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(19,0): anon0
- <console>(28,0): inline$find$0$anon0
- <console>(38,0): inline$find$0$anon4_LoopBody
- <console>(42,0): inline$check$0$Entry
- <console>(57,0): inline$check$0$anon4_Else
- <console>(62,0): inline$check$0$anon3
- <console>(65,0): inline$check$0$Return
+ <console>(19,0): anon0
+ <console>(28,0): inline$find$0$anon0
+ <console>(38,0): inline$find$0$anon4_LoopBody
+ <console>(42,0): inline$check$0$Entry
+ <console>(57,0): inline$check$0$anon4_Else
+ <console>(62,0): inline$check$0$anon3
+ <console>(65,0): inline$check$0$Return
<console>(100,4): Error BP5001: This assertion might not hold.
Execution trace:
- <console>(19,0): anon0
- <console>(28,0): inline$find$0$anon0
- <console>(38,0): inline$find$0$anon4_LoopBody
- <console>(42,0): inline$check$0$Entry
- <console>(52,0): inline$check$0$anon4_Then
- <console>(65,0): inline$check$0$Return
- <console>(73,0): inline$find$0$anon5_Then
- <console>(87,0): inline$find$0$anon3
- <console>(90,0): inline$find$0$Return
- <console>(95,0): anon0$1
- <console>(98,0): anon3_Then
-<console>(50,4): Error BP5003: A postcondition might not hold at this return statement.
+ <console>(19,0): anon0
+ <console>(28,0): inline$find$0$anon0
+ <console>(38,0): inline$find$0$anon4_LoopBody
+ <console>(42,0): inline$check$0$Entry
+ <console>(52,0): inline$check$0$anon4_Then
+ <console>(65,0): inline$check$0$Return
+ <console>(73,0): inline$find$0$anon5_Then
+ <console>(87,0): inline$find$0$anon3
+ <console>(90,0): inline$find$0$Return
+ <console>(95,0): anon0$1
+ <console>(98,0): anon3_Then
+<console>(50,4): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(10,0): anon0
- <console>(20,0): anon4_LoopBody
- <console>(24,0): inline$check$0$Entry
- <console>(39,0): inline$check$0$anon4_Else
- <console>(44,0): inline$check$0$anon3
- <console>(47,0): inline$check$0$Return
-<console>(99,0): Error BP5003: A postcondition might not hold at this return statement.
+ <console>(10,0): anon0
+ <console>(20,0): anon4_LoopBody
+ <console>(24,0): inline$check$0$Entry
+ <console>(39,0): inline$check$0$anon4_Else
+ <console>(44,0): inline$check$0$anon3
+ <console>(47,0): inline$check$0$Return
+<console>(99,0): Error BP5003: A postcondition might not hold on this return path.
<console>(78,2): Related location: This is the postcondition that might not hold.
Execution trace:
- <console>(85,0): anon0
- <console>(93,0): anon4_Else
- <console>(98,0): anon3
+ <console>(85,0): anon0
+ <console>(93,0): anon4_Else
+ <console>(98,0): anon3
Boogie program verifier finished with 0 verified, 4 errors
-------------------- test6.bpl --------------------
@@ -1442,10 +1442,10 @@ Boogie program verifier finished with 5 verified, 0 errors -------------------- test5.bpl --------------------
test5.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- test5.bpl(34,10): anon0
- test5.bpl(28,10): inline$P$0$anon0
- test5.bpl(28,10): inline$P$1$anon0
- test5.bpl(34,10): anon0$2
+ test5.bpl(34,10): anon0
+ test5.bpl(28,10): inline$P$0$anon0
+ test5.bpl(28,10): inline$P$1$anon0
+ test5.bpl(34,10): anon0$2
Boogie program verifier finished with 4 verified, 1 error
-------------------- expansion.bpl --------------------
@@ -1465,37 +1465,37 @@ expansion.bpl(33,22): Error: expansion: an identifier was used more than once *** more than one possible expansion for x1
expansion3.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- expansion3.bpl(18,3): anon0
+ expansion3.bpl(18,3): anon0
Boogie program verifier finished with 1 verified, 1 error
-------------------- Elevator.bpl --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- Elevator.bpl(15,3): anon0
- Elevator.bpl(15,3): anon0$1
- Elevator.bpl(16,3): anon10_LoopHead
- Elevator.bpl(19,5): anon10_LoopBody
- Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
- Elevator.bpl(24,7): anon13_Then$1
+ Elevator.bpl(15,3): anon0
+ Elevator.bpl(15,3): anon0$1
+ Elevator.bpl(16,3): anon10_LoopHead
+ Elevator.bpl(19,5): anon10_LoopBody
+ Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(24,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
-------------------- Elevator.bpl with empty blocks --------------------
Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
Execution trace:
- Elevator.bpl(15,3): anon0
- Elevator.bpl(68,23): inline$Initialize$0$Entry
- Elevator.bpl(71,13): inline$Initialize$0$anon0
- Elevator.bpl(68,23): inline$Initialize$0$Return
- Elevator.bpl(15,3): anon0$1
- Elevator.bpl(16,3): anon10_LoopHead
- Elevator.bpl(19,5): anon10_LoopBody
- Elevator.bpl(19,5): anon11_Else
- Elevator.bpl(19,5): anon12_Else
- Elevator.bpl(24,7): anon13_Then
- Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
- Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
- Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
- Elevator.bpl(24,7): anon13_Then$1
+ Elevator.bpl(15,3): anon0
+ Elevator.bpl(68,23): inline$Initialize$0$Entry
+ Elevator.bpl(71,13): inline$Initialize$0$anon0
+ Elevator.bpl(68,23): inline$Initialize$0$Return
+ Elevator.bpl(15,3): anon0$1
+ Elevator.bpl(16,3): anon10_LoopHead
+ Elevator.bpl(19,5): anon10_LoopBody
+ Elevator.bpl(19,5): anon11_Else
+ Elevator.bpl(19,5): anon12_Else
+ Elevator.bpl(24,7): anon13_Then
+ Elevator.bpl(94,23): inline$MoveDown_Error$0$Entry
+ Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+ Elevator.bpl(94,23): inline$MoveDown_Error$0$Return
+ Elevator.bpl(24,7): anon13_Then$1
Boogie program verifier finished with 1 verified, 1 error
-------------------- expansion2.bpl --------------------
@@ -1528,7 +1528,7 @@ axiom (forall x: int :: { foo3(x): bool } foo3(x): bool == (x > 0)); Boogie program verifier finished with 0 verified, 0 errors
fundef2.bpl(6,3): Error BP5001: This assertion might not hold.
Execution trace:
- fundef2.bpl(5,3): anon0
+ fundef2.bpl(5,3): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- polyInline.bpl --------------------
@@ -1537,10 +1537,10 @@ polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(20,3): anon0
+ polyInline.bpl(20,3): anon0
polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(27,3): anon0
+ polyInline.bpl(27,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
polyInline.bpl(27,9): Warning: type parameter alpha is ambiguous, instantiating to int
@@ -1548,9 +1548,9 @@ polyInline.bpl(31,9): Warning: type parameter alpha is ambiguous, instantiating polyInline.bpl(35,9): Warning: type parameter alpha is ambiguous, instantiating to int
polyInline.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(20,3): anon0
+ polyInline.bpl(20,3): anon0
polyInline.bpl(39,3): Error BP5001: This assertion might not hold.
Execution trace:
- polyInline.bpl(27,3): anon0
+ polyInline.bpl(27,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
diff --git a/Test/lazyinline/Answer b/Test/lazyinline/Answer index ecb258a2..1feac694 100644 --- a/Test/lazyinline/Answer +++ b/Test/lazyinline/Answer @@ -1,5 +1,5 @@ ----- Running regression test bar1.bpl
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold at this return statement.
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar1.bpl(24,3): anon0
@@ -31,7 +31,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar3.bpl
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold at this return statement.
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar3.bpl(38,3): anon0
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index aa83b37c..290059d6 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -1,5 +1,5 @@ ----- Running regression test bar1.bpl
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold at this return statement.
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar1.bpl(24,3): anon0
@@ -31,7 +31,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar3.bpl
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold at this return statement.
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar3.bpl(38,3): anon0
diff --git a/Test/test2/Answer b/Test/test2/Answer index 5cea9721..ae27fa94 100644 --- a/Test/test2/Answer +++ b/Test/test2/Answer @@ -1,6 +1,6 @@ -------------------- FormulaTerm.bpl --------------------
-FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold at this return statement.
+FormulaTerm.bpl(10,3): Error BP5003: A postcondition might not hold on this return path.
FormulaTerm.bpl(4,3): Related location: This is the postcondition that might not hold.
Execution trace:
FormulaTerm.bpl(8,1): start
@@ -18,7 +18,7 @@ Execution trace: 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(44,3): Error BP5003: A postcondition might not hold on this return path.
Passification.bpl(36,3): Related location: This is the postcondition that might not hold.
Execution trace:
Passification.bpl(39,1): A
@@ -44,23 +44,23 @@ Boogie program verifier finished with 7 verified, 4 errors 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(30,5): Error BP5003: A postcondition might not hold on this return path.
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(35,5): Error BP5003: A postcondition might not hold on this return path.
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(41,5): Error BP5003: A postcondition might not hold on this return path.
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(47,5): Error BP5003: A postcondition might not hold on this return path.
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(72,5): Error BP5003: A postcondition might not hold on this return path.
Ensures.bpl(19,3): Related location: This is the postcondition that might not hold.
Execution trace:
Ensures.bpl(70,3): start
@@ -68,7 +68,7 @@ Execution trace: 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(29,5): Error BP5003: A postcondition might not hold on this return path.
Old.bpl(26,3): Related location: This is the postcondition that might not hold.
Execution trace:
Old.bpl(28,3): start
@@ -81,11 +81,11 @@ 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(46,5): Error BP5003: A postcondition might not hold on this return path.
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(127,5): Error BP5003: A postcondition might not hold on this return path.
Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.
Execution trace:
Arrays.bpl(123,3): start
@@ -128,7 +128,7 @@ Execution trace: 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(55,5): Error BP5003: A postcondition might not hold on this return path.
Call.bpl(20,3): Related location: This is the postcondition that might not hold.
Execution trace:
Call.bpl(53,3): start
@@ -211,7 +211,7 @@ strings-where.bpl(990,36): Error: invalid argument types (any and name) to binar 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(252,14): Error BP5003: A postcondition might not hold on this return path.
Structured.bpl(243,3): Related location: This is the postcondition that might not hold.
Execution trace:
Structured.bpl(244,5): anon0
@@ -382,11 +382,11 @@ Execution trace: Boogie program verifier finished with 1 verified, 3 errors
-------------------- Arrays.bpl /typeEncoding:m --------------------
-Arrays.bpl(46,5): Error BP5003: A postcondition might not hold at this return statement.
+Arrays.bpl(46,5): Error BP5003: A postcondition might not hold on this return path.
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(127,5): Error BP5003: A postcondition might not hold on this return path.
Arrays.bpl(119,3): Related location: This is the postcondition that might not hold.
Execution trace:
Arrays.bpl(123,3): start
@@ -442,7 +442,7 @@ Execution trace: Boogie program verifier finished with 10 verified, 8 errors
-------------------- ContractEvaluationOrder.bpl --------------------
-ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold at this return statement.
+ContractEvaluationOrder.bpl(8,1): Error BP5003: A postcondition might not hold on this return path.
ContractEvaluationOrder.bpl(3,3): Related location: This is the postcondition that might not hold.
Execution trace:
ContractEvaluationOrder.bpl(7,5): anon0
|