[e-acsl] pathological example for bad scoping

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

+/* 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; */
+}

src/plugins/e-acsl/tests/constructs/oracle/gen_let.c

+/* 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;
+}
+
+

src/plugins/e-acsl/tests/constructs/oracle/let.res.oracle

+[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);