Store null-pointer-is-zero in pointer_logict

This keeps configurable aspects out of bv_pointerst.

Author: tautschnig

src/solvers/flattening/pointer_logic.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/invariant.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
@@ -159,6 +160,8 @@ pointer_logict::pointer_logict(const namespacet &_ns):ns(_ns)
 
   // add INVALID
   invalid_object=objects.number(exprt("INVALID"));
+
+  null_is_zero_address = config.ansi_c.NULL_is_zero;
 }
 
 pointer_logict::~pointer_logict()

src/solvers/flattening/pointer_logic.h

@@ -70,9 +70,15 @@ class pointer_logict
 
   void get_dynamic_objects(std::vector<std::size_t> &objects) const;
 
+  bool get_null_is_zero() const
+  {
+    return null_is_zero_address;
+  }
+
 protected:
   const namespacet &ns;
   std::size_t null_object, invalid_object;
+  bool null_is_zero_address;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H