From e15a60ed857c349018bf4980aa479e378c0ef949 Mon Sep 17 00:00:00 2001
From: Zafer Esen <zafer.esen@it.uu.se>
Date: Mon, 13 Jan 2025 13:57:18 +0100
Subject: [PATCH] Fixes a bug in uninterpreted predicate declarations. Unnamed
 pointer parameters were raising an exception.

---
 regression-tests/uninterpreted-predicates/Answers   |  4 ++++
 regression-tests/uninterpreted-predicates/runtests  |  3 ++-
 .../unint-pred-unnamed-ptr-arg-bug.c                | 13 +++++++++++++
 src/tricera/concurrency/CCReader.scala              | 13 +++++++++++++
 4 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 regression-tests/uninterpreted-predicates/unint-pred-unnamed-ptr-arg-bug.c

diff --git a/regression-tests/uninterpreted-predicates/Answers b/regression-tests/uninterpreted-predicates/Answers
index 39a68f9..47a7f3c 100644
--- a/regression-tests/uninterpreted-predicates/Answers
+++ b/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
\ No newline at end of file
diff --git a/regression-tests/uninterpreted-predicates/runtests b/regression-tests/uninterpreted-predicates/runtests
index aa65b23..f163620 100755
--- a/regression-tests/uninterpreted-predicates/runtests
+++ b/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
diff --git a/regression-tests/uninterpreted-predicates/unint-pred-unnamed-ptr-arg-bug.c b/regression-tests/uninterpreted-predicates/unint-pred-unnamed-ptr-arg-bug.c
new file mode 100644
index 0000000..e9b9a8a
--- /dev/null
+++ b/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);
+}
diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala
index beef2b0..2c34ab9 100644
--- a/src/tricera/concurrency/CCReader.scala
+++ b/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 =>