[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

@@ -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);
+}