Merge pull request #470 from smowton/fix_address_space_size_check

Fix address space size check

Author: peterschrammel

regression/cbmc/address_space_size_limit1/test.c

@@ -0,0 +1,16 @@
+
+#include <stdlib.h>
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+
+  int i;
+  char* c;
+  for(i=0; i<300; ++i)
+  {
+    c=(char*)malloc(1);
+    assert(c!=(char*)0);
+  }
+
+}

regression/cbmc/address_space_size_limit1/test.desc

@@ -0,0 +1,5 @@
+CORE
+test.c
+--no-simplify --unwind 300
+too many variables
+--

src/solvers/flattening/bv_pointers.cpp

@@ -795,7 +795,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))
+  if(a==(std::size_t(1)<<object_bits))
     throw "too many variables";
 
   encode(a, bv);