[tests] add test case for BTS #2191 which is solved by the new type system

src/plugins/e-acsl/doc/Changelog

@@ -15,6 +15,10 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-  E-ACSL       [2016/05/23] Re-implementation of the type system which
+	        improves the efficiency of the generated code over integers.
+-* E-ACSL       [2016/05/23] Fix bug #2191 about complicate structs and
+	        literate string.
 -* E-ACSL       [2016/05/23] Fix bug #1395 about recursive functions.
 -* E-ACSL       [2016/04/07] Fix 'make install' when executed within Frama-C.
 -* E-ACSL       [2016/03/31] Improve performance of Patricia Trie memory model.

src/plugins/e-acsl/tests/bts/bts2191.c

+struct ST {
+    char *str;
+    int num;
+};
+
+struct ST _G[] = {
+    {
+        .str = "Struct_G[0]",
+        .num = 99
+    },
+    {
+        .str = "Struct_G[1]",
+        .num = 147
+    }
+};
+
+int main(int argc, char **argv) {
+    /*@ assert \valid_read(_G[0].str); */
+    return 0;
+}

src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle

+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c

+/* Generated by Frama-C */
+char *__gen_e_acsl_literal_string;
+char *__gen_e_acsl_literal_string_2;
+struct ST {
+   char *str ;
+   int num ;
+};
+struct ST _G[2] =
+  {{.str = (char *)"Struct_G[0]", .num = 99},
+   {.str = (char *)"Struct_G[1]", .num = 147}};
+void __e_acsl_globals_init(void)
+{
+  __gen_e_acsl_literal_string = "Struct_G[1]";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+                       sizeof("Struct_G[1]"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
+  __gen_e_acsl_literal_string_2 = "Struct_G[0]";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string_2,
+                       sizeof("Struct_G[0]"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string_2);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string_2);
+  __e_acsl_store_block((void *)(_G),32UL);
+  __e_acsl_full_init((void *)(& _G));
+  return;
+}
+
+int main(int argc, char **argv)
+{
+  int __retres;
+  __e_acsl_memory_init(& argc,& argv,8UL);
+  __e_acsl_globals_init();
+  /*@ assert \valid_read(_G[0].str); */
+  {
+    int __gen_e_acsl_initialized;
+    int __gen_e_acsl_and;
+    __gen_e_acsl_initialized = __e_acsl_initialized((void *)(& _G[0].str),
+                                                    sizeof(char *));
+    if (__gen_e_acsl_initialized) {
+      int __gen_e_acsl_valid_read;
+      __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)_G[0].str,
+                                                    sizeof(char));
+      __gen_e_acsl_and = __gen_e_acsl_valid_read;
+    }
+    else __gen_e_acsl_and = 0;
+    __e_acsl_assert(__gen_e_acsl_and,(char *)"Assertion",(char *)"main",
+                    (char *)"\\valid_read(_G[0].str)",18);
+  }
+  __retres = 0;
+  __e_acsl_delete_block((void *)(_G));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+