Adds a one-argument points_to_valid_memory

This commit adds support for a one-argument form of
__CPROVER_points_to_valid_memory, taking only a pointer, with no size.

If ptr has type T*, then __CPROVER_points_to_valid_memory(ptr) is
equivalent to __CPROVER_points_to_valid_memory(ptr, sizeof(T)).

Author: klaas

src/ansi-c/c_typecheck_expr.cpp

@@ -2113,10 +2113,10 @@ exprt c_typecheck_baset::do_special_functions(
   }
   else if(identifier == CPROVER_PREFIX "points_to_valid_memory")
   {
-    if(expr.arguments().size() != 2)
+    if(expr.arguments().size() != 2 && expr.arguments().size() != 1)
     {
       error().source_location = f_op.source_location();
-      error() << "points_to_valid_memory expects two operands" << eom;
+      error() << "points_to_valid_memory expects one or two operands" << eom;
       throw 0;
     }
     if(!is_lvalue(expr.arguments().front()))
@@ -2142,6 +2142,24 @@ exprt c_typecheck_baset::do_special_functions(
       same_object_expr =
         points_to_valid_memory(expr.arguments()[0], expr.arguments()[1]);
     }
+    else if(expr.arguments().size() == 1)
+    {
+      PRECONDITION(expr.arguments()[0].type().id() == ID_pointer);
+
+      const typet &base_type = expr.arguments()[0].type().subtype();
+      auto expr_size = size_of_expr(base_type, *this);
+      if(!expr_size)
+      {
+        error().source_location = expr.source_location();
+        error() << "cannot determine size of pointed-to memory region" << eom;
+        throw 0;
+      }
+
+      expr_size->add(ID_C_c_sizeof_type) = base_type;
+
+      same_object_expr =
+        points_to_valid_memory(expr.arguments()[0], *expr_size);
+    }
     else
     {
       UNREACHABLE;

src/ansi-c/cprover_builtin_headers.h

@@ -6,7 +6,7 @@ void __CPROVER_havoc_object(void *);
 __CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
 __CPROVER_bool __CPROVER_invalid_pointer(const void *);
-__CPROVER_bool __CPROVER_points_to_valid_memory(const void *, __CPROVER_size_t);
+__CPROVER_bool __CPROVER_points_to_valid_memory(const void *, ...);
 __CPROVER_bool __CPROVER_is_zero_string(const void *);
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);