add __CPROVER_is_list(p)

This adds a builtin to the C frontend that indicates that the given pointer
points to a singly linked null-terminated dynamically allocated list.

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2289,6 +2289,33 @@ exprt c_typecheck_baset::do_special_functions(
 
     return buffer_size_expr;
   }
+  else if(identifier == CPROVER_PREFIX "is_list")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      error().source_location = f_op.source_location();
+      error() << "is_list expects one operand" << eom;
+      throw 0;
+    }
+
+    typecheck_function_call_arguments(expr);
+
+    if(
+      expr.arguments()[0].type().id() != ID_pointer ||
+      to_pointer_type(expr.arguments()[0].type()).base_type().id() !=
+        ID_struct_tag)
+    {
+      error().source_location = expr.arguments()[0].source_location();
+      error() << "is_list expects a struct-pointer operand" << eom;
+      throw 0;
+    }
+
+    predicate_exprt is_list_expr("is_list");
+    is_list_expr.operands() = expr.arguments();
+    is_list_expr.add_source_location() = source_location;
+
+    return std::move(is_list_expr);
+  }
   else if(identifier==CPROVER_PREFIX "is_zero_string")
   {
     if(expr.arguments().size()!=1)

src/ansi-c/cprover_builtin_headers.h

@@ -10,6 +10,8 @@ __CPROVER_bool __CPROVER_equal();
 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
 __CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
 _Bool __CPROVER_is_zero_string(const void *);
+// a singly-linked null-terminated dynamically-allocated list
+__CPROVER_bool __CPROVER_is_list();
 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
 __CPROVER_size_t __CPROVER_buffer_size(const void *);
 __CPROVER_bool __CPROVER_r_ok();