Merge pull request #7858 from tautschnig/features/objects-bits-set-up

Permit re-setting --object-bits

Author: kroening

doc/cprover-manual/goto-cc.md

@@ -132,9 +132,6 @@ most important architectural parameters are:
     `sizeof(long int)` on various machines.
 -   The width of pointers; for example, compare the value of `sizeof(int *)` on
     various machines.
--   The number of bits in a pointer which are used to differentiate between
-    different objects. The remaining bits of a pointer are used for offsets
-    within objects.
 -   The [endianness](http://en.wikipedia.org/wiki/Endianness) of
     the architecture.
 
@@ -152,8 +149,6 @@ following command-line arguments can be passed to the CPROVER tools:
 -   The word-width can be set with `--16`, `--32`, `--64`.
 -   The endianness can be defined with `--little-endian` and
     `--big-endian`.
--   The number of bits in a pointer used to differentiate between different
-    objects can be set using `--object-bits x`. Where `x` is the number of bits.
 
 When using a goto binary, CBMC and the other tools read the
 configuration from the binary. The setting when running goto-cc is

doc/man/goto-cc.1

@@ -96,9 +96,10 @@ files.
 .TP
 \fB\-\-print\-rejected\-preprocessed\-source\fR \fIfile\fR
 Copy failing (preprocessed) source to \fIfile\fR.
-.TP
-\fB\-\-object\-bits\fR \fIN\fR
-Configure the number of bits used for object numbering in CBMC's pointer encoding.
+.SH BACKWARD COMPATIBILITY
+.B goto\-cc
+will warn and ignore the use of \fB\-\-object\-bits\fR, which previous versions
+processed. This option now instead needs to be passed to \fBcbmc\fR(1).
 .SH ENVIRONMENT
 All tools honor the TMPDIR environment variable when generating temporary
 files and directories.

regression/CMakeLists.txt

@@ -63,7 +63,6 @@ else()
   add_subdirectory(goto-cl)
 endif()
 add_subdirectory(goto-cc-cbmc)
-add_subdirectory(goto-cc-cbmc-shared-options)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(goto-analyzer-simplify)

regression/Makefile

@@ -36,7 +36,6 @@ DIRS = cbmc-shadow-memory \
        goto-gcc \
        goto-cl \
        goto-cc-cbmc \
-       goto-cc-cbmc-shared-options \
        cbmc-cpp \
        goto-cc-goto-analyzer \
        goto-analyzer-simplify \

regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c

@@ -5,8 +5,6 @@
 #include <stdlib.h>
 #include <stdint.h>
 
-extern size_t __CPROVER_max_malloc_size;
-
 #if defined(_WIN32) && defined(_M_X64)
 int __builtin_clzll(unsigned long long);
 #define __nof_symex_objects                                                    \

regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc

@@ -1,4 +1,4 @@
-CORE dfcc-only
+THOROUGH dfcc-only
 main.c
 --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
 ^EXIT=0$