From 2ea357b6585263fd29d03c8a1ae6472653a6a657 Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Sun, 1 Sep 2024 13:38:16 +0200
Subject: [PATCH] [e-acsl] pathological example for bad scoping
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
bin/test.sh -c dev fails for this example.
GCC complains that a.out.frama.c:277:13: error: ‘__gen_e_acsl_v_2’ undeclared
The translation doesn't take into account the scenario that the same
logic function needs to be translated twice. This is due to different
call sites requiring different signatures.
The authors of the translation must worked with the assumption that
uniqueness of logic variables is a strong enough guarantee to be able to
reuse the translation of a logic variable can always be re-used.
This is wrong, since the translation of a logic variable can be re-used
within the context of one function translation, but escapes its scope if
it is re-used in another translation of the same function.
---
src/plugins/e-acsl/tests/constructs/let.c | 18 ++++
.../e-acsl/tests/constructs/oracle/gen_let.c | 85 +++++++++++++++++++
.../tests/constructs/oracle/let.res.oracle | 4 +
3 files changed, 107 insertions(+)
create mode 100644 src/plugins/e-acsl/tests/constructs/let.c
create mode 100644 src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
create mode 100644 src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
diff --git a/src/plugins/e-acsl/tests/constructs/let.c b/src/plugins/e-acsl/tests/constructs/let.c
new file mode 100644
index 00000000000..eef3a376cf1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/let.c
@@ -0,0 +1,18 @@
+/* run.config
+ COMMENT: The same function is translated twice with different signatures.
+ COMMENT: This regression test ensures that translations of sub-terms do not
+ COMMENT: spill over from one translation to the other, falling out of scope.
+*/
+
+/*@
+
+logic ℤ f(ℤ x) =
+ x ≡ 0 ? 0 :
+ \let v = f(0);
+ 0 ≡ v ? x - 1 : 0;
+
+*/
+
+int main() {
+ /*@ assert f(1) == 0; */
+}
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
new file mode 100644
index 00000000000..60957b9d31a
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle/gen_let.c
@@ -0,0 +1,85 @@
+/* Generated by Frama-C */
+#include "pthread.h"
+#include "sched.h"
+#include "signal.h"
+#include "stddef.h"
+#include "stdint.h"
+#include "stdio.h"
+#include "time.h"
+extern __attribute__((__FC_BUILTIN__)) int __e_acsl_sound_verdict;
+
+/*@
+logic integer f(integer x) = x == 0? 0: (\let v = f(0); 0 == v? x - 1: 0);
+
+*/
+long __gen_e_acsl_f_2(int x);
+
+int __gen_e_acsl_f(int x);
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,8UL);
+ {
+ int __gen_e_acsl_f_6;
+ __e_acsl_assert_data_t __gen_e_acsl_assert_data = {.values = (void *)0};
+ __gen_e_acsl_f_6 = __gen_e_acsl_f(1);
+ __e_acsl_assert_register_int(& __gen_e_acsl_assert_data,"f(1)",0,
+ __gen_e_acsl_f_6);
+ __gen_e_acsl_assert_data.blocking = 1;
+ __gen_e_acsl_assert_data.kind = "Assertion";
+ __gen_e_acsl_assert_data.pred_txt = "f(1) == 0";
+ __gen_e_acsl_assert_data.file = "let.c";
+ __gen_e_acsl_assert_data.fct = "main";
+ __gen_e_acsl_assert_data.line = 17;
+ __e_acsl_assert(__gen_e_acsl_f_6 == 0,& __gen_e_acsl_assert_data);
+ __e_acsl_assert_clean(& __gen_e_acsl_assert_data);
+ }
+ /*@ assert f(1) == 0; */ ;
+ __retres = 0;
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+/*@ assigns \result;
+ assigns \result \from x; */
+int __gen_e_acsl_f(int x)
+{
+ long __gen_e_acsl_if_4;
+ if (x == 0) __gen_e_acsl_if_4 = 0L;
+ else {
+ long __gen_e_acsl_v;
+ long __gen_e_acsl_f_5;
+ long __gen_e_acsl_if_3;
+ __gen_e_acsl_f_5 = __gen_e_acsl_f_2(0);
+ __gen_e_acsl_v = __gen_e_acsl_f_5;
+ /*@ assert Eva: initialization: \initialized(&__gen_e_acsl_v_2); */
+ if (0L == __gen_e_acsl_v_2) __gen_e_acsl_if_3 = x - 1L;
+ else __gen_e_acsl_if_3 = 0L;
+ __gen_e_acsl_if_4 = __gen_e_acsl_if_3;
+ }
+ int __retres = (int)__gen_e_acsl_if_4;
+ return __retres;
+}
+
+/*@ assigns \result;
+ assigns \result \from x; */
+long __gen_e_acsl_f_2(int x)
+{
+ long __gen_e_acsl_if_2;
+ if (x == 0) __gen_e_acsl_if_2 = 0L;
+ else {
+ long __gen_e_acsl_v_2;
+ long __gen_e_acsl_f_4;
+ long __gen_e_acsl_if;
+ __gen_e_acsl_f_4 = __gen_e_acsl_f_2(0);
+ __gen_e_acsl_v_2 = __gen_e_acsl_f_4;
+ if (0L == __gen_e_acsl_v_2) __gen_e_acsl_if = x - 1L;
+ else __gen_e_acsl_if = 0L;
+ __gen_e_acsl_if_2 = __gen_e_acsl_if;
+ }
+ long __retres = (int)__gen_e_acsl_if_2;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
new file mode 100644
index 00000000000..d3f26b8698b
--- /dev/null
+++ b/src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] let.c:12: Warning:
+ accessing uninitialized left-value. assert \initialized(&__gen_e_acsl_v_2);
--
GitLab