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
|
<!--#include virtual="header.inc" -->
<p><a href="./">CPROVER Manual TOC</a></p>
<h2>Pointer Model</h2>
<h3>Pointers in C</h3>
<p class="justified">C programs (and sometimes C++ programs as well) make
intensive use of pointers in order to decouple program code from specific
data. A pointer variable does not store data such as numbers or letters,
but instead points to a location in memory that hold the relevant data.
This section describes the way the CPROVER tools model pointers.
</p>
<h3>Objects and Offsets</h3>
<p class="justified">The CPROVER tools represent pointers as a pair. The
first member of the pair is the <i>object</i> the pointer points to, and the
second is the offset within the object.</p>
<p class="justified">In C, objects are simply continuous fragments of memory
(this definition of "object" is not to be confused with the use of the term
in object-oriented programming). Variables of any type are guaranteed to be
stored as one object, irrespectively of their type. As an example, all
members of a struct or array belong to the same object. CPROVER simply
assigns a number to each active object. The object number of a pointer
<code>p</code> can be extracted using the expression
<code>__CPROVER_POINTER_OBJECT(p)</code>. As a consequence, pointers to
different objects are always different, which is not sound.
</p>
<p class="justified">The offset (the second member of the pair that forms a
pointer) is relative to the beginning of the object; it uses byte
granularity. As an example, the code fragment
</p>
<code>
unsigned array[10];<br>
char *p;<br>
<br>
p=(char *)(array+1);<br>
p++;
</code>
<p class="justified">will result in a pointer with offset 5. The offset of
a pointer <code>p</code> can be extracted using the expression
<code>__CPROVER_POINTER_OFFSET(p)</code>.</p>
<h3>Dereferencing Pointers</h3>
<p class="justified">The CPROVER tools require that pointers that
are dereferenced point to a valid object. Assertions that check
this requirement can be generated using the option --pointer-check
and, if desired, --bounds-check. These options will ensure
that NULL pointers are not dereferenced, and that dynamically
allocated objects have not yet been deallocated.</p>
<p class="justified">Furthermore, the CPROVER
tools check that dynamically allocated memory is not
deallocated twice. The goto-instrument tool is also able
to add checks for memory leaks, i.e., it detects dynamically
allocated objects that are not deallocated once the program
terminates.</p>
<p class="justified">The CPROVER tools support pointer typecasts. Most
casts are supported, with the following exceptions:
</p>
<ol>
<li><p class="justified">
One notable exception is that pointers can only be
accessed using a pointer type. The conversion of a pointer into an
integer-type using a pointer typecast is not supported.
</p></li>
<li><p class="justified">
Casts from integers to pointers yield a pointer that is either
NULL (if the integer is zero) or that point into a special
array for modeling <a href="http://en.wikipedia.org/wiki/Memory-mapped_I/O">
memory-mapped I/O</a>. Such pointers are assumed not to
overlap with any other objects. This is, of course, only sound if
a corresponding range check is instrumented.
</p></li>
<li><p class="justified">
Accesses to arrays via pointers that have the array subtype need
to be well-aligned.
</p></li>
</ol>
<h3>Pointers in Open Programs</h3>
<p class="justified">It is frequently desired to validate an open program,
i.e., a fragment of a program. Some variables are left undefined. In case
an undefined pointer is dereferenced, CBMC assumes that the pointer
points to a separate object of appropriate type with unbounded size.
The object is assumed not to alias with any other object.
This assumption may obviously be wrong in specific extensions
of the program.
</p>
<!--#include virtual="footer.inc" -->
|
