Check 1st arg to points_to_valid_memory is pointer

This commit ensures that the first argument to the
__CPROVER_points_to_valid_memory directive is a pointer, and adds a test
to check for the failing case.

Author: karkhaz

regression/contracts/argument_sanity/main.c renamed to regression/contracts/argument_sanity_1/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  int r;
+  __CPROVER_points_to_valid_memory(r, 2);
+}

regression/contracts/argument_sanity/main.mod renamed to regression/contracts/argument_sanity_1/main.mod

@@ -0,0 +1,9 @@
+CORE
+main.c
+--apply-code-contracts
+^EXIT=1$
+^SIGNAL=0$
+^main.c:\d+:\d+: error: first argument to points_to_valid_memory must be a pointer$
+^CONVERSION ERROR$
+--
+--

regression/contracts/argument_sanity/test.desc renamed to regression/contracts/argument_sanity_1/test.desc

@@ -2126,6 +2126,13 @@ exprt c_typecheck_baset::do_special_functions(
               << " must be an lvalue" << eom;
       throw 0;
     }
+    if(expr.arguments()[0].type().id() != ID_pointer)
+    {
+      error().source_location = f_op.source_location();
+      error() << "first argument to points_to_valid_memory must be a pointer"
+              << eom;
+      throw 0;
+    }
 
     exprt same_object_expr;
     if(expr.arguments().size() == 2)