Check 2nd arg to points_to_valid_memory is size_t

This commit ensures that the second argument to the
__CPROVER_points_to_valid_memory directive can be coerced to a size_t,
and adds a test to check for the failing case.

Author: karkhaz

regression/contracts/argument_sanity/main.c

@@ -0,0 +1,5 @@
+int main()
+{
+  int *r;
+  __CPROVER_points_to_valid_memory(r, "huh?");
+}

regression/contracts/argument_sanity/main.mod

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

regression/contracts/argument_sanity/test.desc

@@ -2131,10 +2131,10 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size() == 2)
     {
       if(
-        expr.arguments()[1].type() != ID_unsignedbv &&
-        expr.arguments()[1].type() != ID_signedbv)
+        expr.arguments()[1].type().id() != ID_unsignedbv &&
+        expr.arguments()[1].type().id() != ID_signedbv)
       {
-        err_location(f_op);
+        error().source_location = f_op.source_location();
         error() << "size argument to points_to_valid_memory"
                 << " must be coercible to size_t" << eom;
         throw 0;