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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
#include <assert.h>
#include <stdio.h>
class base
{
public:
virtual ~base() {}
virtual int func(void)
{
printf ("In base, returning 1");
return 1;
}
};
class derived : public base
{
public:
virtual ~derived() {}
virtual int func(void)
{
printf ("In derived, returning 2");
return 2;
}
};
int main (void)
{
base* D = new derived;
int a = D->func();
delete D;
assert(a == 2);
return a;
}
/*
CBMC Error
C:\FormalMethods\CBMC5_1>cbmc.exe C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp
CBMC version 5.1 32-bit i386 windows
Parsing C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp
inheritance_1.cpp
Converting
Type-checking inheritance_1
Generating GOTO Program
Adding CPROVER library
tmp.stdin45548.KyVaaa.c
file <built-in-additions> line 9 function __CPROVER_size_t: syntax error before `__CPROVER_zero_string_length'
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
**** WARNING: no body for function __new
**** WARNING: no body for function __delete
size of program expression: 125 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
1044 variables, 879 clauses
SAT checker: negated claim is SATISFIABLE, i.e., does not hold
Runtime decision procedure: 0.004s
Building error trace
Counterexample:
State 19 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 26 function main thread 0
----------------------------------------------------
D=((class *)NULL) (00000000000000000000000000000000)
State 27 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 26 function main thread 0
----------------------------------------------------
this=((class *)NULL) (00000000000000000000000000000000)
State 28 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 26 function main thread 0
----------------------------------------------------
this=((class *)NULL) (00000000000000000000000000000000)
State 30 thread 0
----------------------------------------------------
this=((class *)NULL) (00000000000000000000000000000000)
State 31 thread 0
----------------------------------------------------
this=((class *)NULL) (00000000000000000000000000000000)
State 32 thread 0
----------------------------------------------------
this$object.base@vtable_pointer=&tag.base@tag.base.@dtor (00001000000000000000000000000000)
State 34 thread 0
----------------------------------------------------
this$object.base@vtable_pointer=&tag.base@tag.derived.@dtor (00001001000000000000000000000000)
State 35 thread 0
----------------------------------------------------
this$object.derived@vtable_pointer=&tag.derived@tag.derived.@dtor (00001010000000000000000000000000)
State 37 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 26 function main thread 0
----------------------------------------------------
D=((class *)NULL) (00000000000000000000000000000000)
State 38 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 27 function main thread 0
----------------------------------------------------
a=0 (00000000000000000000000000000000)
State 41 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 27 function main thread 0
----------------------------------------------------
this=((class *)NULL) (00000000000000000000000000000000)
State 42 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 27 function main thread 0
----------------------------------------------------
this=((class *)NULL) (00000000000000000000000000000000)
In base, returning 1
State 44 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 9 function func thread 0
----------------------------------------------------
a=1 (00000000000000000000000000000001)
State 48 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 28 function main thread 0
----------------------------------------------------
this=((class *)NULL) (00000000000000000000000000000000)
State 49 file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 28 function main thread 0
----------------------------------------------------
this=((class *)NULL) (00000000000000000000000000000000)
State 50 thread 0
----------------------------------------------------
this$object.base@vtable_pointer=&tag.base@tag.base.@dtor (00001000000000000000000000000000)
Violated property:
file C:\FormalMethods\Projects\CPP_Tests\inheritance_1.cpp line 29 function main
Property 1
a == 2
VERIFICATION FAILED
C:\FormalMethods\CBMC5_1>
*/
|
