[eacsl] Add test for struct comparison

src/plugins/e-acsl/tests/bts/issue-eacsl-139.c

+/* run.config_ci, run.config_dev
+   COMMENT: While unsupported, struct comparison should fail gracefully instead
+   COMMENT: of crashing Frama-C (issue frama-c/e-acsl#139).
+ */
+struct X {
+    int i ;
+};
+
+/*@ ensures *\old(item) == \old(*item); */
+void f(struct X *item){
+}
+
+int main() {
+    struct X x = {.i = 1};
+    f(&x);
+    return 0;
+}

src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-139.c

+/* Generated by Frama-C */
+#include "stddef.h"
+#include "stdio.h"
+extern int __e_acsl_sound_verdict;
+
+struct X {
+   int i ;
+};
+/*@ ensures *\old(item) ≡ \old(*item); */
+void __gen_e_acsl_f(struct X *item);
+
+void f(struct X *item)
+{
+  __e_acsl_store_block((void *)(& item),(size_t)8);
+  __e_acsl_delete_block((void *)(& item));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+  struct X x = {.i = 1};
+  __e_acsl_store_block((void *)(& x),(size_t)4);
+  __e_acsl_full_init((void *)(& x));
+  __gen_e_acsl_f(& x);
+  __retres = 0;
+  __e_acsl_delete_block((void *)(& x));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+/*@ ensures *\old(item) ≡ \old(*item); */
+void __gen_e_acsl_f(struct X *item)
+{
+  struct X __gen_e_acsl_at_2;
+  struct X *__gen_e_acsl_at;
+  __e_acsl_store_block((void *)(& item),(size_t)8);
+  {
+    int __gen_e_acsl_valid_read;
+    __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)item,
+                                                  sizeof(struct X),
+                                                  (void *)item,
+                                                  (void *)(& item));
+    __e_acsl_assert(__gen_e_acsl_valid_read,"RTE","f",
+                    "mem_access: \\valid_read(item)",
+                    "tests/bts/issue-eacsl-139.c",9);
+    __gen_e_acsl_at_2 = *item;
+  }
+  __gen_e_acsl_at = item;
+  f(item);
+  __e_acsl_delete_block((void *)(& item));
+  return;
+}
+
+

src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-139.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] tests/bts/issue-eacsl-139.c:9: Warning: 
+  E-ACSL construct `comparison between two structs or unions'
+  is not yet supported.
+  Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/bts/issue-eacsl-139.c:9: Warning: 
+  function __gen_e_acsl_f: postcondition got status unknown.