Change bts2252 test case to the original program from ITC benchmark

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

@@ -2,12 +2,24 @@
    COMMENT: bts #2252, failures due to typing of offsets
 */
 
-int *p;
-int main(void) {
-  int i = -1;
-  int t[10];
-  /*@ assert ! \valid_read(t+i); */
-  p = t;
-  /*@ assert ! \valid_read(p+i); */
-  return 0;
+#include <stdlib.h>
+
+int main() {
+  char* srcbuf = "Test Code";
+  int i, loc = 1;
+
+  char * destbuf = (char*)malloc(10*sizeof(char));
+  char ch = 'o';
+
+  if (destbuf != NULL) {
+    for (i = -1; i < 0; i++) {
+      /*@ assert ! \valid_read(srcbuf + i); */
+      if (srcbuf[i] == ch) { /* ERROR: Buffer Underrun */
+        loc = i;
+      }
+    }
+
+    strncpy (&destbuf[loc], &srcbuf[loc], 1);
+    free(destbuf);
+  }
 }

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

+tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Old style K&R code?
 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:276:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
 [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.
+tests/bts/bts2252.c:17:[value] warning: out of bounds read. assert \valid_read(srcbuf + i);

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

 /* Generated by Frama-C */
-int *p;
+char *__gen_e_acsl_literal_string;
+/*@ assigns \result, *(x_0 + (0 ..)), *(x_1 + (0 ..));
+    assigns \result \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2;
+    assigns *(x_0 + (0 ..)) \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2;
+    assigns *(x_1 + (0 ..)) \from *(x_0 + (0 ..)), *(x_1 + (0 ..)), x_2;
+ */
+extern int ( /* missing proto */ strncpy)(char *x_0, char *x_1, int x_2);
+
 void __e_acsl_globals_init(void)
 {
-  __e_acsl_store_block((void *)(& p),8UL);
-  __e_acsl_full_init((void *)(& p));
+  __gen_e_acsl_literal_string = "Test Code";
+  __e_acsl_store_block((void *)__gen_e_acsl_literal_string,
+                       sizeof("Test Code"));
+  __e_acsl_full_init((void *)__gen_e_acsl_literal_string);
+  __e_acsl_readonly((void *)__gen_e_acsl_literal_string);
   return;
 }
 
 int main(void)
 {
   int __retres;
+  char *srcbuf;
   int i;
-  int t[10];
+  int loc;
+  char *destbuf;
+  char ch;
   __e_acsl_memory_init((int *)0,(char ***)0,8UL);
   __e_acsl_globals_init();
-  __e_acsl_store_block((void *)(t),40UL);
-  i = -1;
-  /*@ assert ¬\valid_read(&t[i]); */
-  {
-    {
-      int __gen_e_acsl_valid_read;
-      __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(& t[i]),
-                                                    sizeof(int));
-      __e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion",
-                      (char *)"main",(char *)"!\\valid_read(&t[i])",9);
-    }
-  }
-  p = t;
-  /*@ assert ¬\valid_read(p + i); */
-  {
-    {
-      int __gen_e_acsl_valid_read_2;
-      __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)(p + i),
-                                                      sizeof(int));
-      __e_acsl_assert(! __gen_e_acsl_valid_read_2,(char *)"Assertion",
-                      (char *)"main",(char *)"!\\valid_read(p + i)",11);
+  __e_acsl_store_block((void *)(& srcbuf),8UL);
+  __e_acsl_full_init((void *)(& srcbuf));
+  srcbuf = (char *)__gen_e_acsl_literal_string;
+  loc = 1;
+  destbuf = (char *)malloc((unsigned long)10 * sizeof(char));
+  ch = (char)'o';
+  if (destbuf != (char *)0) {
+    i = -1;
+    while (i < 0) {
+      /*@ assert ¬\valid_read(srcbuf + i); */
+      {
+        {
+          int __gen_e_acsl_valid_read;
+          __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)(srcbuf + i),
+                                                        sizeof(char));
+          __e_acsl_assert(! __gen_e_acsl_valid_read,(char *)"Assertion",
+                          (char *)"main",(char *)"!\\valid_read(srcbuf + i)",
+                          16);
+        }
+      }
+      /*@ assert Value: mem_access: \valid_read(srcbuf + i); */
+      if ((int)*(srcbuf + i) == (int)ch) loc = i;
+      i ++;
     }
+    strncpy(destbuf + loc,srcbuf + loc,1);
+    free((void *)destbuf);
   }
   __retres = 0;
-  __e_acsl_delete_block((void *)(& p));
-  __e_acsl_delete_block((void *)(t));
+  __e_acsl_delete_block((void *)(& srcbuf));
   __e_acsl_memory_clean();
   return __retres;
 }