Fixes printing of struct fields in ACSL contracts.

uuverifiers · May 15, 2024 · 2736b6c · 2736b6c
1 parent 0aad60c
commit 2736b6c
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
 
   //////////////////////////////////////////////////////////////////////////////