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,7 +786,7 @@ void bv_pointerst::do_postponed(
     {
       const exprt &expr=*it;
 
-      mp_integer object_size;
+      exprt object_size;
 
       if(expr.id()==ID_symbol)
       {
@@ -798,8 +798,8 @@ void bv_pointerst::do_postponed(
         if(size_expr.is_nil())
           continue;
 
-        if(to_integer(size_expr, object_size))
-          continue;
+        object_size =
+          typecast_exprt::conditional_cast(size_expr, postponed.expr.type());
       }
       else
         continue;
@@ -813,12 +813,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);