diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-27 15:18:47 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-27 15:18:47 -0700 |
| commit | 7cc79726ea246593f4a903ad89b55aa0949fc915 (patch) | |
| tree | 1e94082e49e1965510993b93f35b3779d168e9a5 /Test/prover | |
| parent | 43b80b13bd24bb789849aac3385df6ac4a8233be (diff) | |
Boogie and Dafny: adjustments to the test suite expected output (and a temporary hack in FloydCycleDetect.dfy to be corrected shortly)
Diffstat (limited to 'Test/prover')
| -rw-r--r-- | Test/prover/Answer | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/Test/prover/Answer b/Test/prover/Answer index 1ca6407c..688e6e6a 100644 --- a/Test/prover/Answer +++ b/Test/prover/Answer @@ -4,7 +4,7 @@ z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(14,1): L3
+ z3mutl.bpl(8,1): L1
z3mutl.bpl(20,1): L5
z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
@@ -14,7 +14,7 @@ Execution trace: z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(8,1): L1
+ z3mutl.bpl(14,1): L3
z3mutl.bpl(20,1): L5
Boogie program verifier finished with 0 verified, 3 errors
@@ -24,19 +24,19 @@ EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hol EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
Execution trace:
EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
- EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2
EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
- EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2
- EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2
EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.
EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
Execution trace:
EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
- EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2
EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
- EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2
- EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2
EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
EQ_v2.Eval__v4.Eval_out.bpl(2152,5): Error BP5003: A postcondition might not hold on this return path.
EQ_v2.Eval__v4.Eval_out.bpl(2120,3): Related location: This is the postcondition that might not hold.
|