blob: 6939fee46b65e7cb34e43e63c9287c9db0485847 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
|
CaptureState.bpl(29,1): Error BP5003: A postcondition might not hold on this return path.
CaptureState.bpl(10,3): Related location: This is the postcondition that might not hold.
Execution trace:
CaptureState.bpl(14,3): anon0
CaptureState.bpl(18,5): anon4_Then
CaptureState.bpl(26,5): anon3
*** MODEL
$mv_state_const -> 3
%lbl%@293 -> false
%lbl%+112 -> true
%lbl%+114 -> true
%lbl%+118 -> true
%lbl%+148 -> true
F -> T@FieldName!val!0
Heap -> |T@[Ref,FieldName]Int!val!0|
m -> **m
m@0 -> (- 2)
m@1 -> (- 1)
m@3 -> (- 1)
r -> **r
r@0 -> (- 2)
this -> T@Ref!val!0
x -> 719
y -> **y
Select_[Ref,FieldName]$int -> {
|T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2)
else -> (- 2)
}
$mv_state -> {
3 0 -> true
3 1 -> true
3 2 -> true
3 5 -> true
else -> true
}
tickleBool -> {
true -> true
false -> true
else -> true
}
*** STATE <initial>
Heap -> |T@[Ref,FieldName]Int!val!0|
this -> T@Ref!val!0
x -> 719
y -> **y
r -> **r
m -> **m
*** END_STATE
*** STATE top
*** END_STATE
*** STATE then
m -> (- 2)
*** END_STATE
*** STATE postUpdate0
m -> (- 1)
*** END_STATE
*** STATE end
r -> (- 2)
m -> 7
*** END_STATE
*** END_MODEL
Boogie program verifier finished with 0 verified, 1 error
|
