Fixes a bug in uninterpreted predicate declarations.

Unnamed pointer parameters were raising an exception.

regression-tests/uninterpreted-predicates/Answers

@@ -36,3 +36,7 @@ Other Error: 5:3 Unsupported operation: stack pointer argument to uninterpreted
 
 unint-pred-simple-ptr-true.c
 SAFE
+
+unint-pred-unnamed-ptr-arg-bug.c
+Warning: no definition of function "nondet_ptr" available
+SAFE

regression-tests/uninterpreted-predicates/runtests

@@ -4,7 +4,8 @@ LAZABS=../../tri
 
 TESTS="pred-hint.c pred-hint-loop.c \
        unint-pred-simple-false.c unint-pred-simple-true.c \
-       unint-pred-stack-ptr-unsupported.c unint-pred-simple-ptr-true.c"
+       unint-pred-stack-ptr-unsupported.c unint-pred-simple-ptr-true.c
+       unint-pred-unnamed-ptr-arg-bug.c"
 
 for name in $TESTS; do
     echo

regression-tests/uninterpreted-predicates/unint-pred-unnamed-ptr-arg-bug.c

@@ -0,0 +1,13 @@
+/*$ P(int *) $*/
+
+int* nondet_ptr();
+
+void main() {
+  int *p = 0;
+  assert(P(p));
+
+  int *q = nondet_ptr();
+  assume(P(q));
+
+  assert(p == q);
+}

src/tricera/concurrency/CCReader.scala

@@ -1474,6 +1474,16 @@ class CCReader private (prog              : Program,
           processHints(argDec.listannotation_) // todo: does this work??
           (actualType, name)
         }
+        case argDec : Abstract => {
+          val typ  = getType(argDec.listdeclaration_specifier_)
+          val actualType = argDec.abstract_declarator_ match {
+            case p : PointerStart => createHeapPointer(p, typ)
+            case _ => throw new TranslationException(
+              s"Unsupported declaration inside predicate declaration: ${printer.print(argDec)}")
+          }
+          val argName = declName + "_" + ind
+          (actualType, argName)
+        }
       }
     }
   }
@@ -4033,6 +4043,9 @@ private def collectVarDecls(dec                    : Dec,
   private def createHeapPointer(decl : BeginPointer, typ : CCType) :
   CCHeapPointer = createHeapPointerHelper(decl.pointer_, typ)
 
+  private def createHeapPointer(decl : PointerStart, typ : CCType) :
+  CCHeapPointer = createHeapPointerHelper(decl.pointer_, typ)
+
   private def createHeapPointerHelper(decl : Pointer, typ : CCType) :
   CCHeapPointer = decl match {
       case pp : PointPoint =>