File tree Expand file tree Collapse file tree 1 file changed +5
-0
lines changed
Expand file tree Collapse file tree 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:
112112 ` sizeof(long int) ` on various machines.
113113- The width of pointers; for example, compare the value of ` sizeof(int *) ` on
114114 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.
115118- The [ endianness] ( http://en.wikipedia.org/wiki/Endianness ) of
116119 the architecture.
117120
@@ -129,6 +132,8 @@ following command-line arguments can be passed to the CPROVER tools:
129132- The word-width can be set with ` --16 ` , ` --32 ` , ` --64 ` .
130133- The endianness can be defined with ` --little-endian ` and
131134 ` --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.
132137
133138When using a goto binary, CBMC and the other tools read the
134139configuration from the binary. The setting when running goto-cc is
You can’t perform that action at this time.
0 commit comments