From b5d41873bfc330cf343e5380acbadb42203029c9 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Tue, 25 Jul 2017 15:02:14 +0200
Subject: [PATCH 01/10] Make configt::set_classpath private

It's only called from within configt.
---
 src/util/config.h | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/util/config.h b/src/util/config.h
index 6fb4a5a2376..992fac2e6bd 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -152,10 +152,11 @@ class configt
 
   bool set(const cmdlinet &cmdline);
 
-  void set_classpath(const std::string &cp);
-
   static irep_idt this_architecture();
   static irep_idt this_operating_system();
+
+private:
+  void set_classpath(const std::string &cp);
 };
 
 extern configt config;

From 549443baadca359dfca9033db2a1c21d35735219 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Tue, 25 Jul 2017 14:53:25 +0200
Subject: [PATCH 02/10] Factorize setting config from symbol table when reading
 goto binaries

---
 src/cbmc/cbmc_parse_options.cpp                       | 3 ---
 src/clobber/clobber_parse_options.cpp                 | 2 --
 src/goto-diff/goto_diff_parse_options.cpp             | 1 -
 src/goto-instrument/goto_instrument_parse_options.cpp | 1 -
 src/goto-programs/initialize_goto_model.cpp           | 3 ---
 src/goto-programs/read_goto_binary.cpp                | 4 ++++
 src/musketeer/musketeer_parse_options.cpp             | 2 --
 7 files changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 65a4386077b..5eca0edfe0b 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -659,9 +659,6 @@ int cbmc_parse_optionst::get_goto_program(
       }
     }
 
-    if(!binaries.empty())
-      config.set_from_symbol_table(symbol_table);
-
     if(cmdline.isset("show-symbol-table"))
     {
       show_symbol_table();
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 36cc3e49abc..c9278673a7c 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -209,8 +209,6 @@ bool clobber_parse_optionst::get_goto_program(
            symbol_table, goto_functions, get_message_handler()))
         return true;
 
-      config.set_from_symbol_table(symbol_table);
-
       if(cmdline.isset("show-symbol-table"))
       {
         show_symbol_table();
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
index 146fe27eb1c..1bfb9152c50 100644
--- a/src/goto-diff/goto_diff_parse_options.cpp
+++ b/src/goto-diff/goto_diff_parse_options.cpp
@@ -347,7 +347,6 @@ int goto_diff_parse_optionst::get_goto_program(
       return 6;
 
     config.set(cmdline);
-    config.set_from_symbol_table(goto_model.symbol_table);
 
     // This one is done.
     cmdline.args.erase(cmdline.args.begin());
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 888853c6dc4..e2a67dce2b7 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -867,7 +867,6 @@ void goto_instrument_parse_optionst::get_goto_program()
     throw 0;
 
   config.set(cmdline);
-  config.set_from_symbol_table(symbol_table);
 }
 
 void goto_instrument_parse_optionst::instrument_goto_program()
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index d284bc403c9..9b877fb20b7 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -131,9 +131,6 @@ bool initialize_goto_model(
         return true;
     }
 
-    if(!binaries.empty())
-      config.set_from_symbol_table(goto_model.symbol_table);
-
     msg.status() << "Generating GOTO Program" << messaget::eom;
 
     goto_convert(
diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp
index 1a4887cf0e9..58eafda8fb2 100644
--- a/src/goto-programs/read_goto_binary.cpp
+++ b/src/goto-programs/read_goto_binary.cpp
@@ -28,6 +28,7 @@ Module: Read Goto Programs
 #include <util/tempfile.h>
 #include <util/rename_symbol.h>
 #include <util/base_type.h>
+#include <util/config.h>
 
 #include <langapi/language_ui.h>
 
@@ -383,6 +384,9 @@ bool read_object_and_link(
       linking.object_type_updates))
     return true;
 
+  // reading successful, let's update config
+  config.set_from_symbol_table(symbol_table);
+
   return false;
 }
 
diff --git a/src/musketeer/musketeer_parse_options.cpp b/src/musketeer/musketeer_parse_options.cpp
index ace73687432..fabb89a3add 100644
--- a/src/musketeer/musketeer_parse_options.cpp
+++ b/src/musketeer/musketeer_parse_options.cpp
@@ -139,8 +139,6 @@ void goto_fence_inserter_parse_optionst::get_goto_program(
   if(read_goto_binary(cmdline.args[0],
     symbol_table, goto_functions, get_message_handler()))
     throw 0;
-
-  config.set_from_symbol_table(symbol_table);
 }
 
 void goto_fence_inserter_parse_optionst::instrument_goto_program(

From c624d2478c6fead1fa2552c7ed2ed08cea8f6d80 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 20 Jul 2017 22:46:22 +0100
Subject: [PATCH 03/10] Replace BV_ADDR_BITS by config setting

---
 src/solvers/flattening/bv_pointers.cpp |  2 +-
 src/solvers/flattening/pointer_logic.h |  2 --
 src/solvers/smt1/smt1_conv.cpp         | 34 ++++++++++++++-----------
 src/solvers/smt2/smt2_conv.cpp         | 35 +++++++++++++++-----------
 src/util/config.cpp                    |  2 ++
 src/util/config.h                      |  6 +++++
 6 files changed, 48 insertions(+), 33 deletions(-)

diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 9ecb81c9846..35cf5968c87 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -95,7 +95,7 @@ bv_pointerst::bv_pointerst(
   boolbvt(_ns, _prop),
   pointer_logic(_ns)
 {
-  object_bits=BV_ADDR_BITS;
+  object_bits=config.bv_encoding.object_bits;
   offset_bits=config.ansi_c.pointer_width-object_bits;
   bits=config.ansi_c.pointer_width;
 }
diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h
index 07193819358..d094dbd8523 100644
--- a/src/solvers/flattening/pointer_logic.h
+++ b/src/solvers/flattening/pointer_logic.h
@@ -16,8 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr.h>
 #include <util/numbering.h>
 
-#define BV_ADDR_BITS 8
-
 class namespacet;
 
 class pointer_logict
diff --git a/src/solvers/smt1/smt1_conv.cpp b/src/solvers/smt1/smt1_conv.cpp
index ee85dfc63a0..78c5d32d163 100644
--- a/src/solvers/smt1/smt1_conv.cpp
+++ b/src/solvers/smt1/smt1_conv.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ieee_float.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 
 #include <ansi-c/string_constant.h>
 
@@ -153,10 +154,11 @@ exprt smt1_convt::ce_value(
     pointer_logict::pointert p;
     p.object=integer2unsigned(
       binary2integer(
-        value.substr(0, BV_ADDR_BITS), false));
+        value.substr(0, config.bv_encoding.object_bits), false));
 
     p.offset=
-      binary2integer(value.substr(BV_ADDR_BITS, std::string::npos), true);
+      binary2integer(
+        value.substr(config.bv_encoding.object_bits, std::string::npos), true);
 
     result.copy_to_operands(pointer_logic.pointer_expr(p, type));
 
@@ -260,8 +262,10 @@ void smt1_convt::convert_address_of_rec(
   {
     out
       << "(concat"
-      << " bv" << pointer_logic.add_object(expr) << "[" << BV_ADDR_BITS << "]"
-      << " bv0[" << boolbv_width(result_type)-BV_ADDR_BITS << "]"
+      << " bv" << pointer_logic.add_object(expr) << "["
+      << config.bv_encoding.object_bits << "]"
+      << " bv0["
+      << boolbv_width(result_type)-config.bv_encoding.object_bits << "]"
       << ")";
   }
   else if(expr.id()==ID_index)
@@ -889,8 +893,8 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
     std::size_t op_width=boolbv_width(expr.op0().type());
-    out << "(zero_extend[" << BV_ADDR_BITS << "] (extract["
-        << (op_width-1-BV_ADDR_BITS)
+    out << "(zero_extend[" << config.bv_encoding.object_bits << "] (extract["
+        << (op_width-1-config.bv_encoding.object_bits)
         << ":0] ";
     convert_expr(expr.op0(), true);
     out << "))";
@@ -901,7 +905,7 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
     std::size_t op_width=boolbv_width(expr.op0().type());
-    signed int ext=boolbv_width(expr.type())-BV_ADDR_BITS;
+    signed int ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
 
     if(ext>0)
       out << "(zero_extend[" << ext << "] ";
@@ -909,7 +913,7 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
     out << "(extract["
         << (op_width-1)
         << ":"
-        << op_width-1-BV_ADDR_BITS << "] ";
+        << op_width-1-config.bv_encoding.object_bits << "] ";
     convert_expr(expr.op0(), true);
     out << ")";
 
@@ -933,10 +937,10 @@ void smt1_convt::convert_expr(const exprt &expr, bool bool_as_bv)
 
     out << "(= (extract["
         << (op_width-1)
-        << ":" << op_width-BV_ADDR_BITS << "] ";
+        << ":" << op_width-config.bv_encoding.object_bits << "] ";
     convert_expr(expr.op0(), true);
     out << ") bv" << pointer_logic.get_invalid_object()
-        << "[" << BV_ADDR_BITS << "])";
+        << "[" << config.bv_encoding.object_bits << "])";
 
     // this may have to be converted
     from_bool_end(type, bool_as_bv);
@@ -1853,8 +1857,8 @@ void smt1_convt::convert_constant(
       assert(boolbv_width(expr.type())!=0);
       out << "(concat"
           << " bv" << pointer_logic.get_null_object()
-          << "[" << BV_ADDR_BITS << "]"
-          << " bv0[" << boolbv_width(expr.type())-BV_ADDR_BITS
+          << "[" << config.bv_encoding.object_bits << "]"
+          << " bv0[" << boolbv_width(expr.type())-config.bv_encoding.object_bits
           << "]"
           << ")"; // concat
     }
@@ -1945,14 +1949,14 @@ void smt1_convt::convert_is_dynamic_object(
 
     out << "(let (?obj (extract["
         << (op_width-1)
-        << ":" << op_width-BV_ADDR_BITS << "] ";
+        << ":" << op_width-config.bv_encoding.object_bits << "] ";
     convert_expr(expr.op0(), true);
     out << ")) ";
 
     if(dynamic_objects.size()==1)
     {
       out << "(= bv" << dynamic_objects.front()
-          << "[" << BV_ADDR_BITS << "] ?obj)";
+          << "[" << config.bv_encoding.object_bits << "] ?obj)";
     }
     else
     {
@@ -1960,7 +1964,7 @@ void smt1_convt::convert_is_dynamic_object(
 
       for(const auto &obj : dynamic_objects)
         out << " (= bv" << obj
-            << "[" << BV_ADDR_BITS << "] ?obj)";
+            << "[" << config.bv_encoding.object_bits << "] ?obj)";
 
       out << ")"; // or
     }
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index ccf6087379f..023b83adb5d 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
+#include <util/config.h>
 
 #include <ansi-c/string_constant.h>
 
@@ -142,7 +143,7 @@ void smt2_convt::define_object_size(
   std::size_t pointer_width = boolbv_width(ptr.type());
   std::size_t number = 0;
   std::size_t h=pointer_width-1;
-  std::size_t l=pointer_width-BV_ADDR_BITS;
+  std::size_t l=pointer_width-config.bv_encoding.object_bits;
 
   for(const auto &o : pointer_logic.objects)
   {
@@ -161,9 +162,10 @@ void smt2_convt::define_object_size(
     out << "(assert (implies (= " <<
       "((_ extract " << h << " " << l << ") ";
     convert_expr(ptr);
-    out << ") (_ bv" << number << " " << BV_ADDR_BITS << "))" <<
-      "(= " << id << " (_ bv" << object_size.to_ulong() << " " <<
-      size_width << "))))\n";
+    out << ") (_ bv" << number << " "
+        << config.bv_encoding.object_bits << "))"
+        << "(= " << id << " (_ bv" << object_size.to_ulong() << " "
+        << size_width << "))))\n";
 
     ++number;
   }
@@ -454,7 +456,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
     to_integer(bv_expr, v);
 
     // split into object and offset
-    mp_integer pow=power(2, width-BV_ADDR_BITS);
+    mp_integer pow=power(2, width-config.bv_encoding.object_bits);
     pointer_logict::pointert ptr;
     ptr.object=integer2size_t(v/pow);
     ptr.offset=v%pow;
@@ -487,8 +489,10 @@ void smt2_convt::convert_address_of_rec(
   {
     out
       << "(concat (_ bv"
-      << pointer_logic.add_object(expr) << " " << BV_ADDR_BITS << ")"
-      << " (_ bv0 " << boolbv_width(result_type)-BV_ADDR_BITS << "))";
+      << pointer_logic.add_object(expr) << " "
+      << config.bv_encoding.object_bits << ")"
+      << " (_ bv0 "
+      << boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
   }
   else if(expr.id()==ID_index)
   {
@@ -1308,7 +1312,8 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
-    std::size_t offset_bits=boolbv_width(expr.op0().type())-BV_ADDR_BITS;
+    std::size_t offset_bits=
+      boolbv_width(expr.op0().type())-config.bv_encoding.object_bits;
     std::size_t result_width=boolbv_width(expr.type());
 
     // max extract width
@@ -1330,7 +1335,7 @@ void smt2_convt::convert_expr(const exprt &expr)
   {
     assert(expr.operands().size()==1);
     assert(expr.op0().type().id()==ID_pointer);
-    std::size_t ext=boolbv_width(expr.type())-BV_ADDR_BITS;
+    std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
     std::size_t pointer_width=boolbv_width(expr.op0().type());
 
     if(ext>0)
@@ -1338,7 +1343,7 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     out << "((_ extract "
         << pointer_width-1 << " "
-        << pointer_width-BV_ADDR_BITS << ") ";
+        << pointer_width-config.bv_encoding.object_bits << ") ";
     convert_expr(expr.op0());
     out << ")";
 
@@ -1356,10 +1361,10 @@ void smt2_convt::convert_expr(const exprt &expr)
     std::size_t pointer_width=boolbv_width(expr.op0().type());
     out << "(= ((_ extract "
         << pointer_width-1 << " "
-        << pointer_width-BV_ADDR_BITS << ") ";
+        << pointer_width-config.bv_encoding.object_bits << ") ";
     convert_expr(expr.op0());
     out << ") (_ bv" << pointer_logic.get_invalid_object()
-        << " " << BV_ADDR_BITS << "))";
+        << " " << config.bv_encoding.object_bits << "))";
   }
   else if(expr.id()=="pointer_object_has_type")
   {
@@ -2725,14 +2730,14 @@ void smt2_convt::convert_is_dynamic_object(const exprt &expr)
 
     out << "(let ((?obj ((_ extract "
         << pointer_width-1 << " "
-        << pointer_width-BV_ADDR_BITS << ") ";
+        << pointer_width-config.bv_encoding.object_bits << ") ";
     convert_expr(expr.op0());
     out << "))) ";
 
     if(dynamic_objects.size()==1)
     {
       out << "(= (_ bv" << dynamic_objects.front()
-          << " " << BV_ADDR_BITS << ") ?obj)";
+          << " " << config.bv_encoding.object_bits << ") ?obj)";
     }
     else
     {
@@ -2740,7 +2745,7 @@ void smt2_convt::convert_is_dynamic_object(const exprt &expr)
 
       for(const auto &object : dynamic_objects)
         out << " (= (_ bv" << object
-            << " " << BV_ADDR_BITS << ") ?obj)";
+            << " " << config.bv_encoding.object_bits << ") ?obj)";
 
       out << ")"; // or
     }
diff --git a/src/util/config.cpp b/src/util/config.cpp
index ee24ab7b0f7..978993f980c 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -730,6 +730,8 @@ bool configt::set(const cmdlinet &cmdline)
 
   cpp.cpp_standard=cppt::default_cpp_standard();
 
+  bv_encoding.object_bits=8;
+
   ansi_c.single_precision_constant=false;
   ansi_c.for_has_scope=true; // C99 or later
   ansi_c.c_standard=ansi_ct::default_c_standard();
diff --git a/src/util/config.h b/src/util/config.h
index 992fac2e6bd..22f8de1df08 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -143,6 +143,12 @@ class configt
     irep_idt main_class;
   } java;
 
+  struct bv_encodingt
+  {
+    // number of bits to encode heap object addresses
+    unsigned object_bits;
+  } bv_encoding;
+
   // this is the function to start executing
   std::string main;
 

From c29bf8cfbf554005c24efe3badada311e610bac1 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 20 Jul 2017 23:49:51 +0100
Subject: [PATCH 04/10] Better error message when too many dynamic objects

---
 regression/cbmc/address_space_size_limit1/test.desc | 2 +-
 src/solvers/flattening/bv_pointers.cpp              | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
index 9dcfb8970aa..1cb3a86cd65 100644
--- a/regression/cbmc/address_space_size_limit1/test.desc
+++ b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,5 +1,5 @@
 CORE
 test.c
 --no-simplify --unwind 300
-too many variables
+too many addressed objects
 --
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 35cf5968c87..56c5ce01ce5 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -682,7 +682,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
   std::size_t a=pointer_logic.add_object(expr);
 
   if(a==(std::size_t(1)<<object_bits))
-    throw "too many variables";
+    throw "too many addressed objects";
 
   encode(a, bv);
 }

From 18f30a652dafccea00521f14e936e1e99ee4ec15 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Thu, 20 Jul 2017 23:44:56 +0100
Subject: [PATCH 05/10] Allow specifying object-bits via command line and
 language defaults

---
 .../cbmc/address_space_size_limit1/test.desc  |  2 +-
 src/cbmc/cbmc_parse_options.cpp               |  1 +
 src/cbmc/cbmc_parse_options.h                 |  1 +
 src/langapi/language_ui.cpp                   |  3 ++
 src/solvers/flattening/bv_pointers.cpp        |  8 ++-
 src/util/config.cpp                           | 49 ++++++++++++++++++-
 src/util/config.h                             | 11 +++++
 7 files changed, 71 insertions(+), 4 deletions(-)

diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
index 1cb3a86cd65..d0d0ed3c04e 100644
--- a/regression/cbmc/address_space_size_limit1/test.desc
+++ b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,5 +1,5 @@
 CORE
 test.c
---no-simplify --unwind 300
+--no-simplify --unwind 300 --object-bits 8
 too many addressed objects
 --
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 5eca0edfe0b..f871b8603a8 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -1057,6 +1057,7 @@ void cbmc_parse_optionst::help()
     " --graphml-witness filename   write the witness in GraphML format to filename\n" // NOLINT(*)
     "\n"
     "Backend options:\n"
+    " --object-bits n              number of bits used for object addresses\n"
     " --dimacs                     generate CNF in DIMACS format\n"
     " --beautify                   beautify the counterexample (greedy heuristic)\n" // NOLINT(*)
     " --localize-faults            localize faults (experimental)\n"
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index d95e60eb25b..5dd2ed1e4af 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -31,6 +31,7 @@ class optionst;
   "(debug-level):(no-propagation)(no-simplify-if)" \
   "(document-subgoals)(outfile):(test-preprocessor)" \
   "D:I:(c89)(c99)(c11)(cpp89)(cpp99)(cpp11)" \
+  "(object-bits):" \
   "(classpath):(cp):(main-class):" \
   "(depth):(partial-loops)(no-unwinding-assertions)(unwinding-assertions)" \
   OPT_GOTO_CHECK \
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index ddd774f2c4b..ebd5cb9180a 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 #include <util/namespace.h>
 #include <util/language.h>
 #include <util/cmdline.h>
+#include <util/config.h>
 #include <util/unicode.h>
 
 #include "mode.h"
@@ -121,6 +122,8 @@ bool language_uit::final()
     return true;
   }
 
+  config.set_object_bits_from_symbol_table(symbol_table);
+
   return false;
 }
 
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 56c5ce01ce5..6d86b506fcb 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -681,8 +681,12 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 {
   std::size_t a=pointer_logic.add_object(expr);
 
-  if(a==(std::size_t(1)<<object_bits))
-    throw "too many addressed objects";
+  const std::size_t max_objects=std::size_t(1)<<object_bits;
+  if(a==max_objects)
+    throw
+      "too many addressed objects: maximum number of objects is set to 2^n="+
+      std::to_string(max_objects)+" (with n="+std::to_string(object_bits)+"); "+
+      "use the `--object-bits n` option to increase the maximum number";
 
   encode(a, bv);
 }
diff --git a/src/util/config.cpp b/src/util/config.cpp
index 978993f980c..348c15e05f0 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "simplify_expr.h"
 #include "std_expr.h"
 #include "cprover_prefix.h"
+#include "string2int.h"
 
 configt config;
 
@@ -730,7 +731,9 @@ bool configt::set(const cmdlinet &cmdline)
 
   cpp.cpp_standard=cppt::default_cpp_standard();
 
-  bv_encoding.object_bits=8;
+  bv_encoding.object_bits=bv_encoding.default_object_bits;
+  // This will allow us to override by language defaults later.
+  bv_encoding.is_object_bits_default=true;
 
   ansi_c.single_precision_constant=false;
   ansi_c.for_has_scope=true; // C99 or later
@@ -1012,6 +1015,20 @@ bool configt::set(const cmdlinet &cmdline)
   if(cmdline.isset("round-to-zero"))
     ansi_c.rounding_mode=ieee_floatt::ROUND_TO_ZERO;
 
+  if(cmdline.isset("object-bits"))
+  {
+    bv_encoding.object_bits=
+      unsafe_string2unsigned(cmdline.get_value("object-bits"));
+    bv_encoding.is_object_bits_default=false;
+
+    if(!(0<bv_encoding.object_bits &&
+         bv_encoding.object_bits<ansi_c.pointer_width))
+    {
+      throw "object-bits must be positive and less than the pointer width ("+
+        std::to_string(ansi_c.pointer_width)+") ";
+    }
+  }
+
   return false;
 }
 
@@ -1145,6 +1162,36 @@ void configt::set_from_symbol_table(
 
   // mode, preprocessor (and all preprocessor command line options),
   // lib, string_abstraction not stored in namespace
+
+  set_object_bits_from_symbol_table(symbol_table);
+}
+
+/// Sets the number of bits used for object addresses
+/// \param symbol_table The symbol table
+void configt::set_object_bits_from_symbol_table(
+  const symbol_tablet &symbol_table)
+{
+  // has been overridden by command line option,
+  //   thus do not apply language defaults
+  if(!bv_encoding.is_object_bits_default)
+    return;
+
+  // set object_bits according to entry point language
+  if(symbol_table.has_symbol(CPROVER_PREFIX "_start"))
+  {
+    const symbolt &entry_point_symbol=
+      symbol_table.lookup(CPROVER_PREFIX "_start");
+
+    if(entry_point_symbol.mode==ID_java)
+      bv_encoding.object_bits=java.default_object_bits;
+    else if(entry_point_symbol.mode==ID_C)
+      bv_encoding.object_bits=ansi_c.default_object_bits;
+    else if(entry_point_symbol.mode==ID_cpp)
+      bv_encoding.object_bits=cpp.default_object_bits;
+    DATA_INVARIANT(
+      0<bv_encoding.object_bits && bv_encoding.object_bits<ansi_c.pointer_width,
+      "object_bits should fit into pointer width");
+  }
 }
 
 irep_idt configt::this_architecture()
diff --git a/src/util/config.h b/src/util/config.h
index 22f8de1df08..30903aa2f2e 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -118,6 +118,8 @@ class configt
     libt lib;
 
     bool string_abstraction;
+
+    static const unsigned default_object_bits=8;
   } ansi_c;
 
   struct cppt
@@ -129,6 +131,8 @@ class configt
     void set_cpp03() { cpp_standard=cpp_standardt::CPP03; }
     void set_cpp11() { cpp_standard=cpp_standardt::CPP11; }
     void set_cpp14() { cpp_standard=cpp_standardt::CPP14; }
+
+    static const unsigned default_object_bits=8;
   } cpp;
 
   struct verilogt
@@ -141,12 +145,17 @@ class configt
     typedef std::list<std::string> classpatht;
     classpatht classpath;
     irep_idt main_class;
+
+    static const unsigned default_object_bits=16;
   } java;
 
   struct bv_encodingt
   {
     // number of bits to encode heap object addresses
     unsigned object_bits;
+    bool is_object_bits_default;
+
+    static const unsigned default_object_bits=8;
   } bv_encoding;
 
   // this is the function to start executing
@@ -158,6 +167,8 @@ class configt
 
   bool set(const cmdlinet &cmdline);
 
+  void set_object_bits_from_symbol_table(const symbol_tablet &);
+
   static irep_idt this_architecture();
   static irep_idt this_operating_system();
 

From d7715c772341671431b9ef6c76dcb8b306c6b03e Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 2 Aug 2017 15:28:43 +0100
Subject: [PATCH 06/10] Catch command line parsing exceptions

---
 src/cbmc/cbmc_parse_options.cpp | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index f871b8603a8..25d8f595232 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -435,7 +435,23 @@ int cbmc_parse_optionst::doit()
   //
 
   optionst options;
-  get_command_line_options(options);
+  try
+  {
+    get_command_line_options(options);
+  }
+
+  catch(const char *error_msg)
+  {
+    error() << error_msg << eom;
+    return 6; // should contemplate EX_SOFTWARE from sysexits.h
+  }
+
+  catch(const std::string error_msg)
+  {
+    error() << error_msg << eom;
+    return 6; // should contemplate EX_SOFTWARE from sysexits.h
+  }
+
   eval_verbosity();
 
   //

From f4a6dd192f65a9a8ee0f547fb541e0f6e7ce8f80 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Fri, 21 Jul 2017 00:15:35 +0100
Subject: [PATCH 07/10] Add java address space limits tests

---
 .../address_space_size_limit1/Test.class          | Bin 0 -> 640 bytes
 .../cbmc-java/address_space_size_limit1/Test.java |  13 +++++++++++++
 .../cbmc-java/address_space_size_limit1/test.desc |   5 +++++
 .../address_space_size_limit2/Test.class          | Bin 0 -> 640 bytes
 .../cbmc-java/address_space_size_limit2/Test.java |  13 +++++++++++++
 .../cbmc-java/address_space_size_limit2/test.desc |   8 ++++++++
 6 files changed, 39 insertions(+)
 create mode 100644 regression/cbmc-java/address_space_size_limit1/Test.class
 create mode 100644 regression/cbmc-java/address_space_size_limit1/Test.java
 create mode 100644 regression/cbmc-java/address_space_size_limit1/test.desc
 create mode 100644 regression/cbmc-java/address_space_size_limit2/Test.class
 create mode 100644 regression/cbmc-java/address_space_size_limit2/Test.java
 create mode 100644 regression/cbmc-java/address_space_size_limit2/test.desc

diff --git a/regression/cbmc-java/address_space_size_limit1/Test.class b/regression/cbmc-java/address_space_size_limit1/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..5f81fc826ffa983a71fe170b00828a9d1b6ffa96
GIT binary patch
literal 640
zcmYL{T~8B16o%ikv)yU83zV<6bhQW~Rzf5(B%06|3~EAB<f6m`xZ1W8GElZ=cWd|o
z{0eSNyy4o<CKC1D-@;$;<IGy^#q60m=bh)gXR<$jefb7p9d}*iP{~2Sm$>0_ylD<q
ziFp?eDlTqeL1K|WXS}uv(@Q}dt0>XEFn+4zpw(3!t{f1Yx(;>nm|)ko@4e)()$1t2
zL_>$_MgO#=qCKPL!fBvGLa}z(I1XM1Yuz9`T5Bee4v#j>#j$1*v`=<|SE*j&HX&PY
zcZYOQGa9$q>ql+%TpM6+PsPc7!}2hWk_Q)gZey}0G2y|(7@<7s_T=9T&!VUoNi2D|
zgJnWtB-w2pt9C+=hYbVT;7LZstuDU;kI+%Ej#TGAj-4lcF0jc1EbvR__?azU><B27
zjS)TxUhE6pkavr$NHr@1(2D;F);rD;Ci&}d1Z?I^VS1?VBa;#y6{=q$c0}DTRNrD|
z)xUz+_Xn_>=R}vkuiqncfmwf5JopIf4f0oT_6LyP4c$uV73PE44*MHtZ*v^ydH0aL
z&2S|T@e^5+m@Sr&MG>W;h4s`HFgYbYBYOd9U&0n2kQuT6I;WJAf#q%TUxISldhQRu
C&~X6(

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/address_space_size_limit1/Test.java b/regression/cbmc-java/address_space_size_limit1/Test.java
new file mode 100644
index 00000000000..4f60b51e973
--- /dev/null
+++ b/regression/cbmc-java/address_space_size_limit1/Test.java
@@ -0,0 +1,13 @@
+public class Test {
+    int x;
+    Test(int x) { this.x = x; }
+
+    public static void main(String[] args) {
+        int i;
+        Test[] tests = new Test[30];
+        for(i = 0; i < 30; ++i) {
+            tests[i] = new Test(i);
+        }
+        assert i == tests[0].x;
+    }
+}
diff --git a/regression/cbmc-java/address_space_size_limit1/test.desc b/regression/cbmc-java/address_space_size_limit1/test.desc
new file mode 100644
index 00000000000..d08ff5b05c1
--- /dev/null
+++ b/regression/cbmc-java/address_space_size_limit1/test.desc
@@ -0,0 +1,5 @@
+CORE
+Test.class
+--object-bits 4
+too many addressed objects
+--
diff --git a/regression/cbmc-java/address_space_size_limit2/Test.class b/regression/cbmc-java/address_space_size_limit2/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..5f81fc826ffa983a71fe170b00828a9d1b6ffa96
GIT binary patch
literal 640
zcmYL{T~8B16o%ikv)yU83zV<6bhQW~Rzf5(B%06|3~EAB<f6m`xZ1W8GElZ=cWd|o
z{0eSNyy4o<CKC1D-@;$;<IGy^#q60m=bh)gXR<$jefb7p9d}*iP{~2Sm$>0_ylD<q
ziFp?eDlTqeL1K|WXS}uv(@Q}dt0>XEFn+4zpw(3!t{f1Yx(;>nm|)ko@4e)()$1t2
zL_>$_MgO#=qCKPL!fBvGLa}z(I1XM1Yuz9`T5Bee4v#j>#j$1*v`=<|SE*j&HX&PY
zcZYOQGa9$q>ql+%TpM6+PsPc7!}2hWk_Q)gZey}0G2y|(7@<7s_T=9T&!VUoNi2D|
zgJnWtB-w2pt9C+=hYbVT;7LZstuDU;kI+%Ej#TGAj-4lcF0jc1EbvR__?azU><B27
zjS)TxUhE6pkavr$NHr@1(2D;F);rD;Ci&}d1Z?I^VS1?VBa;#y6{=q$c0}DTRNrD|
z)xUz+_Xn_>=R}vkuiqncfmwf5JopIf4f0oT_6LyP4c$uV73PE44*MHtZ*v^ydH0aL
z&2S|T@e^5+m@Sr&MG>W;h4s`HFgYbYBYOd9U&0n2kQuT6I;WJAf#q%TUxISldhQRu
C&~X6(

literal 0
HcmV?d00001

diff --git a/regression/cbmc-java/address_space_size_limit2/Test.java b/regression/cbmc-java/address_space_size_limit2/Test.java
new file mode 100644
index 00000000000..4f60b51e973
--- /dev/null
+++ b/regression/cbmc-java/address_space_size_limit2/Test.java
@@ -0,0 +1,13 @@
+public class Test {
+    int x;
+    Test(int x) { this.x = x; }
+
+    public static void main(String[] args) {
+        int i;
+        Test[] tests = new Test[30];
+        for(i = 0; i < 30; ++i) {
+            tests[i] = new Test(i);
+        }
+        assert i == tests[0].x;
+    }
+}
diff --git a/regression/cbmc-java/address_space_size_limit2/test.desc b/regression/cbmc-java/address_space_size_limit2/test.desc
new file mode 100644
index 00000000000..9cf9d12a7f7
--- /dev/null
+++ b/regression/cbmc-java/address_space_size_limit2/test.desc
@@ -0,0 +1,8 @@
+CORE
+Test.class
+--object-bits 8
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\[java::Test.main:\(\[Ljava/lang/String;\)V.assertion.1\] .*: FAILURE$
+--

From 12e280f1fc5a5479d1e07c38dd51e482e533c01e Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Fri, 21 Jul 2017 00:35:28 +0100
Subject: [PATCH 08/10] Tests for overflows in pointer arithmetic

One is detected with --pointer-check enabled,
the other one is currently not detected.
---
 .../cbmc/address_space_size_limit2/test.c     |  10 ++
 .../cbmc/address_space_size_limit2/test.desc  |   5 +
 .../cbmc/address_space_size_limit3/main.c     | 136 ++++++++++++++++++
 .../cbmc/address_space_size_limit3/test.desc  |  11 ++
 4 files changed, 162 insertions(+)
 create mode 100644 regression/cbmc/address_space_size_limit2/test.c
 create mode 100644 regression/cbmc/address_space_size_limit2/test.desc
 create mode 100644 regression/cbmc/address_space_size_limit3/main.c
 create mode 100644 regression/cbmc/address_space_size_limit3/test.desc

diff --git a/regression/cbmc/address_space_size_limit2/test.c b/regression/cbmc/address_space_size_limit2/test.c
new file mode 100644
index 00000000000..c35cc13da7f
--- /dev/null
+++ b/regression/cbmc/address_space_size_limit2/test.c
@@ -0,0 +1,10 @@
+#include <stdlib.h>
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+  char* c=(char*)malloc(10);
+  char* d=c;
+  for(char i=0; i<10; i++, d++);
+  assert((size_t)d==(size_t)c+10);
+}
diff --git a/regression/cbmc/address_space_size_limit2/test.desc b/regression/cbmc/address_space_size_limit2/test.desc
new file mode 100644
index 00000000000..63d05de2268
--- /dev/null
+++ b/regression/cbmc/address_space_size_limit2/test.desc
@@ -0,0 +1,5 @@
+KNOWNBUG
+test.c
+--32 --object-bits 31 --unwind 11 --no-simplify
+dynamic object too large
+--
diff --git a/regression/cbmc/address_space_size_limit3/main.c b/regression/cbmc/address_space_size_limit3/main.c
new file mode 100644
index 00000000000..6c62d538ee5
--- /dev/null
+++ b/regression/cbmc/address_space_size_limit3/main.c
@@ -0,0 +1,136 @@
+// copy of Pointer_Arithmetic12
+
+#include <stdint.h>
+
+#include <assert.h>
+
+uint32_t __stack[32];
+
+uint32_t eax;
+uint32_t ebp;
+uint32_t ebx;
+uint32_t ecx;
+uint32_t edi;
+uint32_t edx;
+uint32_t esi;
+uint32_t esp=(uint32_t)&(__stack[31]);
+uint32_t var0;
+uint32_t var1;
+uint32_t var10;
+uint32_t var11;
+uint32_t var12;
+uint32_t var13;
+uint32_t var14;
+uint32_t var15;
+uint32_t var16;
+uint32_t var2;
+uint32_t var3;
+uint32_t var4;
+uint32_t var5;
+uint32_t var6;
+uint32_t var7;
+uint32_t var8;
+uint32_t var9;
+
+void g__L_0x3b4_0()
+{
+  L_0x3b4_0: esp-=0x4;
+  L_0x3b4_1: *(uint32_t*)(esp)=ebp;
+  L_0x3b5_0: ebp=esp;
+  L_0x3b7_0: var4=ebp;
+  L_0x3b7_1: var4+=0xc;
+  L_0x3b7_2: eax=*(uint32_t*)(var4);
+  L_0x3ba_0: edx=eax;
+  L_0x3bc_0: edx&=0x3;
+  L_0x3bf_0: var5=ebp;
+  L_0x3bf_1: var5+=0x8;
+  L_0x3bf_2: eax=*(uint32_t*)(var5);
+  L_0x3c2_0: *(uint32_t*)(eax)=edx;
+  L_0x3c4_0: ebp=*(uint32_t*)(esp);
+  L_0x3c4_1: esp+=0x4;
+  L_0x3c5_0: return;
+}
+
+void f__L_0x3c6_0()
+{
+  L_0x3c6_0: esp-=0x4;
+  L_0x3c6_1: *(uint32_t*)(esp)=ebp;
+  L_0x3c7_0: ebp=esp;
+  L_0x3c9_0: esp-=0x18;
+  L_0x3cc_0: var6=ebp;
+  L_0x3cc_1: var6-=0x4;
+  L_0x3cc_2: *(uint32_t*)(var6)=0x0;
+  L_0x3d3_0: var7=ebp;
+  L_0x3d3_1: var7-=0x8;
+  L_0x3d3_2: *(uint32_t*)(var7)=0x0;
+  L_0x3da_0: var8=ebp;
+  L_0x3da_1: var8+=0x8;
+  L_0x3da_2: eax=*(uint32_t*)(var8);
+  L_0x3dd_0: var9=ebp;
+  L_0x3dd_1: var9-=0x4;
+  L_0x3dd_2: *(uint32_t*)(var9)=eax;
+  L_0x3e0_0: var10=ebp;
+  L_0x3e0_1: var10-=0x4;
+  L_0x3e0_2: eax=*(uint32_t*)(var10);
+  L_0x3e3_0: var11=esp;
+  L_0x3e3_1: var11+=0x4;
+  L_0x3e3_2: *(uint32_t*)(var11)=eax;
+  L_0x3e7_0: var12=ebp;
+  L_0x3e7_1: var12-=0x8;
+  L_0x3e7_2: eax=(uint32_t)&*(uint32_t*)(var12);
+  L_0x3ea_0: *(uint32_t*)(esp)=eax;
+  L_0x3ed_0: esp-=4; g__L_0x3b4_0(); esp+=4;
+  L_0x3f2_0: var13=ebp;
+  L_0x3f2_1: var13-=0x4;
+  L_0x3f2_2: *(uint32_t*)(var13)=0x5;
+  L_0x3f9_0: var14=ebp;
+  L_0x3f9_1: var14-=0x8;
+  L_0x3f9_2: eax=*(uint32_t*)(var14);
+  L_0x3fc_0: esp=ebp;
+  L_0x3fc_1: ebp=*(uint32_t*)(esp);
+  L_0x3fc_2: esp+=0x4;
+  L_0x3fd_0: return;
+}
+
+int main()
+{
+  L_0x3fe_0: esp-=0x4;
+  L_0x3fe_1: *(uint32_t*)(esp)=ebp;
+  L_0x3ff_0: ebp=esp;
+  L_0x401_0: esp-=0x14;
+  L_0x404_0: var15=ebp;
+  L_0x404_1: var15-=0x4;
+#ifdef NONDET
+  L_0x404_2: *(uint32_t*)(var15)=nondet_uint();
+#else
+  L_0x404_2: *(uint32_t*)(var15)=0xffffffff;
+#endif
+  L_0x40b_0: var16=ebp;
+  L_0x40b_1: var16-=0x4;
+  L_0x40b_2: eax=*(uint32_t*)(var16);
+  L_0x40e_0: *(uint32_t*)(esp)=eax;
+  L_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
+#if 1
+             uint32_t eax1=eax;
+  C_0x3ff_0: ebp=esp;
+  C_0x401_0: esp-=0x14;
+  C_0x404_0: var15=ebp;
+  C_0x404_1: var15-=0x4;
+#ifdef NONDET
+  C_0x404_2: *(uint32_t*)(var15)=nondet_uint();
+#else
+  C_0x404_2: *(uint32_t*)(var15)=0xffffffff;
+#endif
+  C_0x40b_0: var16=ebp;
+  C_0x40b_1: var16-=0x4;
+  C_0x40b_2: eax=*(uint32_t*)(var16);
+  C_0x40e_0: *(uint32_t*)(esp)=eax;
+  C_0x411_0: esp-=4; f__L_0x3c6_0(); esp+=4;
+             uint32_t eax2=eax;
+             assert(eax2==eax1);
+#endif
+  L_0x416_0: esp=ebp;
+  L_0x416_1: ebp=*(uint32_t*)(esp);
+  L_0x416_2: esp+=0x4;
+  L_0x417_0: return 0;
+}
diff --git a/regression/cbmc/address_space_size_limit3/test.desc b/regression/cbmc/address_space_size_limit3/test.desc
new file mode 100644
index 00000000000..ee7b4e94ab8
--- /dev/null
+++ b/regression/cbmc/address_space_size_limit3/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--32 --little-endian --object-bits 25 --pointer-check
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^.* dereference failure: pointer outside object bounds in .*: FAILURE$
+--
+^warning: ignoring
+--
+requires at least 8 offset bits

From e9b9dd8e5e852ccd1c03e4a2ff7110139834860c Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sat, 22 Jul 2017 21:19:27 +0100
Subject: [PATCH 09/10] Fix getting model for object address (unsigned ->
 size_t)

Bug exhibited by cbmc-java/iterator2 when run with --object-bits 35
---
 src/solvers/flattening/bv_pointers.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 6d86b506fcb..cf5ebfdb243 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -600,7 +600,7 @@ exprt bv_pointerst::bv_get_rec(
   result.set_value(value);
 
   pointer_logict::pointert pointer;
-  pointer.object=integer2unsigned(binary2integer(value_addr, false));
+  pointer.object=integer2size_t(binary2integer(value_addr, false));
   pointer.offset=binary2integer(value_offset, true);
 
   // we add the elaborated expression as operand

From ded2d1c85bab8ae64bcd872c6148ae95add70212 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Wed, 26 Jul 2017 11:27:10 +0200
Subject: [PATCH 10/10] Output message about used object bits settings

---
 src/cbmc/cbmc_parse_options.cpp |  2 ++
 src/util/config.cpp             | 10 ++++++++++
 src/util/config.h               |  1 +
 3 files changed, 13 insertions(+)

diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 25d8f595232..d360c7140de 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -702,6 +702,8 @@ int cbmc_parse_optionst::get_goto_program(
       show_goto_functions(ns, get_ui(), goto_functions);
       return 0;
     }
+
+    status() << config.object_bits_info() << eom;
   }
 
   catch(const char *e)
diff --git a/src/util/config.cpp b/src/util/config.cpp
index 348c15e05f0..436a99d140d 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -1194,6 +1194,16 @@ void configt::set_object_bits_from_symbol_table(
   }
 }
 
+std::string configt::object_bits_info()
+{
+  return "Running with "+std::to_string(bv_encoding.object_bits)+
+    " object bits, "+
+    std::to_string(ansi_c.pointer_width-bv_encoding.object_bits)+
+    " offset bits ("+
+    (bv_encoding.is_object_bits_default ? "default" : "user-specified")+
+    ")";
+}
+
 irep_idt configt::this_architecture()
 {
   irep_idt this_arch;
diff --git a/src/util/config.h b/src/util/config.h
index 30903aa2f2e..4b1b39c1402 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -168,6 +168,7 @@ class configt
   bool set(const cmdlinet &cmdline);
 
   void set_object_bits_from_symbol_table(const symbol_tablet &);
+  std::string object_bits_info();
 
   static irep_idt this_architecture();
   static irep_idt this_operating_system();