Merge pull request #8156 from tautschnig/features/__builtin_dynamic_object_size

Support __builtin_dynamic_object_size

Author: tautschnig

Diff for: src/ansi-c/c_typecheck_expr.cpp

@@ -3519,11 +3519,15 @@ exprt c_typecheck_baset::do_special_functions(
 
     return typecast_exprt(expr.arguments()[0], expr.type());
   }
-  else if(identifier=="__builtin_object_size")
+  else if(
+    identifier == "__builtin_object_size" ||
+    identifier == "__builtin_dynamic_object_size")
   {
-    // this is a gcc extension to provide information about
+    // These are gcc extensions to provide information about
     // object sizes at compile time
     // http://gcc.gnu.org/onlinedocs/gcc/Object-Size-Checking.html
+    // Our behavior is as if it was never possible to determine the object that
+    // the pointer pointed to.
 
     if(expr.arguments().size()!=2)
     {

Diff for: src/ansi-c/compiler_headers/gcc_builtin_headers_mem_string.h

@@ -119,6 +119,7 @@ void* __builtin_memmove(void*, const void*, __CPROVER_size_t);
 void* __builtin_mempcpy(void*, const void*, __CPROVER_size_t);
 void* __builtin_memset(void*, int, __CPROVER_size_t);
 __CPROVER_size_t __builtin_object_size(const void*, int);
+__CPROVER_size_t __builtin_dynamic_object_size(const void*, int);
 int __builtin_popcount(unsigned);
 int __builtin_popcountimax(uintmax_t);
 int __builtin_popcountll(unsigned long long int x);