From 66742f494a6481a7621281fa95543747da7a2e96 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Thu, 19 Sep 2024 18:17:28 +0200
Subject: [PATCH] [e-acsl] pathological example exposing translation error
[kernel] functions.c:120: Failure:
mkBinOp: unsupported operator for such operands 2L == __gen_e_acsl_at
(type of e1: long, type of e2: __e_acsl_mpz_t)
This occurs notable for code using stdlib.h unless the flag
"-keep-unused-functions none" is given.
The reason for this is a memoisation issue. In the example there are two
occurrences of j, in two terms of the form \at(j, Old).
They are typed differently according to their context. However the
memoisation in Translate_ats does not take into account the typing.
More specifically it uses Analyses_datatype.At_data for memoising the
translations, which relies on structural equivalence of terms.
---
src/plugins/e-acsl/tests/arith/functions.c | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/src/plugins/e-acsl/tests/arith/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
index b02c5f9baca..66e0968c071 100644
--- a/src/plugins/e-acsl/tests/arith/functions.c
+++ b/src/plugins/e-acsl/tests/arith/functions.c
@@ -111,3 +111,16 @@ int main(void) {
void test_f4() {
/*@ assert f4 (0) ≡ 0; */
}
+
+// same term \at(j, Old) twice in different typing contexts
+/*@
+ behavior a:
+ ensures 1 == -j;
+ behavior b:
+ ensures 2 == j;
+ */
+int f5(long int j) {}
+
+int test_f5() {
+ f5(1);
+}
--
GitLab