From 2736b6c79cdd12947b43311f015ca80a8ab9351f Mon Sep 17 00:00:00 2001
From: Zafer Esen <zafer.esen@it.uu.se>
Date: Wed, 15 May 2024 13:44:07 +0200
Subject: [PATCH] Fixes printing of struct fields in ACSL contracts.

---
 regression-tests/horn-contracts/Answers           | 13 +++++++++++++
 regression-tests/horn-contracts/runtests          |  3 ++-
 .../horn-contracts/struct-name-bug.hcc            | 15 +++++++++++++++
 src/tricera/postprocessor/ACSLLineariser.scala    |  2 +-
 4 files changed, 31 insertions(+), 2 deletions(-)
 create mode 100644 regression-tests/horn-contracts/struct-name-bug.hcc

diff --git a/regression-tests/horn-contracts/Answers b/regression-tests/horn-contracts/Answers
index 19bbbc1..5eb1f27 100644
--- a/regression-tests/horn-contracts/Answers
+++ b/regression-tests/horn-contracts/Answers
@@ -119,3 +119,16 @@ UNSAFE
 
 stackptr.hcc
 UNKNOWN (Unsupported C fragment. Function contracts are currently not supported together with stack pointers (10:5))
+
+struct-name-bug.hcc
+
+Inferred ACSL annotations
+================================================================================
+/* contracts for foo */
+/*@
+  requires s.f == 21;
+  ensures \old(s).f == 21 && 2*21 == \result;
+*/
+================================================================================
+
+SAFE
diff --git a/regression-tests/horn-contracts/runtests b/regression-tests/horn-contracts/runtests
index 993190e..493cd17 100755
--- a/regression-tests/horn-contracts/runtests
+++ b/regression-tests/horn-contracts/runtests
@@ -9,7 +9,8 @@ TESTS="contract1.hcc \
        takeuchi.hcc  \
        assert.hcc \
        fib.hcc \
-       stackptr.hcc"
+       stackptr.hcc \
+       struct-name-bug.hcc"
 
 for name in $TESTS; do
     echo
diff --git a/regression-tests/horn-contracts/struct-name-bug.hcc b/regression-tests/horn-contracts/struct-name-bug.hcc
new file mode 100644
index 0000000..1c4394c
--- /dev/null
+++ b/regression-tests/horn-contracts/struct-name-bug.hcc
@@ -0,0 +1,15 @@
+struct S {
+  int f;
+};
+
+/*@ contract @*/
+int foo(struct S s) {
+  return s.f*2;
+}
+
+int main() {
+  struct S s;
+  s.f = 21;
+  assert(foo(s) == 42);
+  return 0;
+}
diff --git a/src/tricera/postprocessor/ACSLLineariser.scala b/src/tricera/postprocessor/ACSLLineariser.scala
index 8f50449..15e3fcf 100644
--- a/src/tricera/postprocessor/ACSLLineariser.scala
+++ b/src/tricera/postprocessor/ACSLLineariser.scala
@@ -83,7 +83,7 @@ object ACSLLineariser {
   def asString(e : IExpression) : String =
     ap.DialogUtil.asString { printExpression(e) }
 
-  private def fun2Identifier(fun : IFunction) = fun.name
+  private def fun2Identifier(fun : IFunction) = fun.name.split("::").last
 
   //////////////////////////////////////////////////////////////////////////////