object_size can now do objects with variable size

Author: Daniel Kroening

regression/cbmc/dynamic_size1/stack_object.c

@@ -0,0 +1,24 @@
+struct S
+{
+  __CPROVER_size_t size;
+  char *p;
+};
+
+void func(struct S *s)
+{
+  char *p = s->p;
+  __CPROVER_size_t size = __CPROVER_OBJECT_SIZE(p);
+  __CPROVER_assert(size == s->size, "size ok");
+  p[80] = 123; // should be safe
+}
+
+int main()
+{
+  __CPROVER_size_t buffer_size;
+  __CPROVER_assume(buffer_size >= 100);
+  char buffer[buffer_size];
+  struct S s;
+  s.size = buffer_size;
+  s.p = buffer;
+  func(&s);
+}

regression/cbmc/dynamic_size1/stack_object.desc

@@ -0,0 +1,8 @@
+CORE
+stack_object.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/solvers/flattening/bv_pointers.cpp

@@ -786,24 +786,17 @@ void bv_pointerst::do_postponed(
     {
       const exprt &expr=*it;
 
-      mp_integer object_size;
-
-      if(expr.id()==ID_symbol)
-      {
-        // just get the type
-        const typet &type=ns.follow(expr.type());
-
-        exprt size_expr=size_of_expr(type, ns);
+      if(expr.id() != ID_symbol)
+        continue;
 
-        if(size_expr.is_nil())
-          continue;
+      const exprt size_expr = size_of_expr(expr.type(), ns);
 
-        if(to_integer(size_expr, object_size))
-          continue;
-      }
-      else
+      if(size_expr.is_nil())
         continue;
 
+      const exprt object_size =
+        typecast_exprt::conditional_cast(size_expr, postponed.expr.type());
+
       // only compare object part
       bvt bv;
       encode(number, bv);
@@ -813,12 +806,13 @@ void bv_pointerst::do_postponed(
       bvt saved_bv=postponed.op;
       saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
 
+      bvt size_bv = convert_bv(object_size);
+
       POSTCONDITION(bv.size()==saved_bv.size());
       PRECONDITION(postponed.bv.size()>=1);
+      PRECONDITION(size_bv.size() == postponed.bv.size());
 
       literalt l1=bv_utils.equal(bv, saved_bv);
-
-      bvt size_bv=bv_utils.build_constant(object_size, postponed.bv.size());
       literalt l2=bv_utils.equal(postponed.bv, size_bv);
 
       prop.l_set_to(prop.limplies(l1, l2), true);