File tree 1 file changed +5
-0
lines changed 1 file changed +5
-0
lines changed Original file line number Diff line number Diff line change @@ -112,6 +112,9 @@ most important architectural parameters are:
112
112
` sizeof(long int) ` on various machines.
113
113
- The width of pointers; for example, compare the value of ` sizeof(int *) ` on
114
114
various machines.
115
+ - The number of bits in a pointer which are used to differentiate between
116
+ different objects. The remaining bits of a pointer are used for offsets
117
+ within objects.
115
118
- The [ endianness] ( http://en.wikipedia.org/wiki/Endianness ) of
116
119
the architecture.
117
120
@@ -129,6 +132,8 @@ following command-line arguments can be passed to the CPROVER tools:
129
132
- The word-width can be set with ` --16 ` , ` --32 ` , ` --64 ` .
130
133
- The endianness can be defined with ` --little-endian ` and
131
134
` --big-endian ` .
135
+ - The number of bits in a pointer used to differentiate between different
136
+ objects can be set using ` --object-bits x ` . Where ` x ` is the number of bits.
132
137
133
138
When using a goto binary, CBMC and the other tools read the
134
139
configuration from the binary. The setting when running goto-cc is
You can’t perform that action at this time.
0 commit comments