From 0d4e53140f1ee6df696c23849f734f10ce74d0dd Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Tue, 12 Nov 2024 11:52:28 +0100
Subject: [PATCH] Fixed parsing derefs

---
 subprojects/common/grammar/src/main/antlr/CommonTokens.g4 | 8 ++++----
 .../test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt    | 6 ++++++
 2 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/subprojects/common/grammar/src/main/antlr/CommonTokens.g4 b/subprojects/common/grammar/src/main/antlr/CommonTokens.g4
index 132737fe5c..7bc61ee23d 100644
--- a/subprojects/common/grammar/src/main/antlr/CommonTokens.g4
+++ b/subprojects/common/grammar/src/main/antlr/CommonTokens.g4
@@ -101,9 +101,6 @@ MINUS
 	:	'-'
 	;
 
-MUL	:	'*'
-	;
-
 DIV	:	'div'
 	;
 
@@ -406,7 +403,10 @@ SIGN:	PLUS | MINUS
 DOT	:	'.'
 	;
 
-ID	:	(LETTER | UNDERSCORE) (LETTER | UNDERSCORE | '$' | DIGIT | COLON)*
+ID	:	(LETTER | UNDERSCORE) (LETTER | UNDERSCORE | '$' | '*' | DIGIT | COLON)*
+	;
+
+MUL	:	'*'
 	;
 
 UNDERSCORE
diff --git a/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt b/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt
index f0c9e82b4f..a93ef5340c 100644
--- a/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt
+++ b/subprojects/common/grammar/src/test/java/hu/bme/mit/theta/grammar/dsl/ExprTest.kt
@@ -65,6 +65,7 @@ class ExprTest {
     fun data(): Collection<Array<Any>> {
       val x = Var("x", Int())
       val p = Param("p", Int())
+      val casret = Var("thr1::casret*", Int())
 
       val bvLit1 = Bv(BooleanArray(4) { it % 2 == 0 })
       val bvLit2 = Bv(BooleanArray(4) { it % 2 == 1 })
@@ -286,6 +287,11 @@ class ExprTest {
           emptyMap<Symbol, Decl<*>>(),
         ),
         arrayOf(Dereference(Int(0), Int(1), Int()), "(deref 0 1 Int)", emptyMap<Symbol, Decl<*>>()),
+        arrayOf(
+          Dereference(casret.ref, Int(0), Int()),
+          "(deref thr1::casret* 0 Int)",
+          mapOf(Pair(NamedSymbol("thr1::casret*"), casret)),
+        ),
       )
     }
   }