[tests] Fixed an issue where tests in bts and gmp folders were not run

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

@@ -4,13 +4,12 @@
 
 #include "stdlib.h"
 
-/*@ behavior exists:
-  assumes \exists integer i; 0 <= i < n && ((char*)buf)[i] == c;
-  ensures
-  \forall int j; 0 <= j < \offset((char*)\result) ==> ((char*)buf)[j] != c; 
+/*@behavior exists:
+    assumes \exists int i; 0 <= i < (int)n && ((char*)buf)[i] == c;
+    ensures \forall int j; 0 <= j < (int)\offset((char*)\result) ==> ((char*)buf)[j] != c;
   behavior not_exists:
-  assumes \forall integer k; 0 <= k < n ==> ((char*)buf)[k] != c;
-  ensures \result == (void*) 0; */
+    assumes \forall int k; 0 <= k < (int)n ==> ((char*)buf)[k] != c;
+    ensures \result == (void*) 0; */
 void *memchr(const void *buf, int c, size_t n) {
   int i;
   char *s = buf;

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

@@ -2,4 +2,6 @@
 FRAMAC_SHARE/libc/stdlib.h:160:[kernel] warning: No code nor implicit assigns clause for function calloc, 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.
-FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] warning: function __gmpz_add: precondition got status invalid.
+tests/bts/bts1390.c:12:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:12:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:17:[value] warning: out of bounds read. assert \valid_read(s);

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

@@ -2,27 +2,27 @@
 char *__gen_e_acsl_literal_string;
 char *__gen_e_acsl_literal_string_2;
 /*@ behavior exists:
-      assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
+      assumes ∃ int i; 0 ≤ i < (int)n ∧ (int)*((char *)buf+i) ≡ c;
       ensures
         ∀ int j;
-          0 ≤ j < \offset((char *)\result) ⇒
+          0 ≤ j < (int)\offset((char *)\result) ⇒
           (int)*((char *)\old(buf)+j) ≢ \old(c);
     
     behavior not_exists:
-      assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+      assumes ∀ int k; 0 ≤ k < (int)n ⇒ (int)*((char *)buf+k) ≢ c;
       ensures \result ≡ (void *)0;
  */
 void *__gen_e_acsl_memchr(void const *buf, int c, size_t n);
 
 /*@ behavior exists:
-      assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
+      assumes ∃ int i; 0 ≤ i < (int)n ∧ (int)*((char *)buf+i) ≡ c;
       ensures
         ∀ int j;
-          0 ≤ j < \offset((char *)\result) ⇒
+          0 ≤ j < (int)\offset((char *)\result) ⇒
           (int)*((char *)\old(buf)+j) ≢ \old(c);
     
     behavior not_exists:
-      assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+      assumes ∀ int k; 0 ≤ k < (int)n ⇒ (int)*((char *)buf+k) ≢ c;
       ensures \result ≡ (void *)0;
  */
 void *memchr(void const *buf, int c, size_t n)
@@ -37,6 +37,7 @@ void *memchr(void const *buf, int c, size_t n)
   s = (char *)buf;
   i = 0;
   while ((size_t)i < n) {
+    /*@ assert Value: mem_access: \valid_read(s); */
     if ((int)*s == c) {
       __e_acsl_full_init((void *)(& __retres));
       __retres = (void *)s;
@@ -56,14 +57,14 @@ void *memchr(void const *buf, int c, size_t n)
 }
 
 /*@ behavior exists:
-      assumes ∃ ℤ i; 0 ≤ i < n ∧ (int)*((char *)buf+i) ≡ c;
+      assumes ∃ int i; 0 ≤ i < (int)n ∧ (int)*((char *)buf+i) ≡ c;
       ensures
         ∀ int j;
-          0 ≤ j < \offset((char *)\result) ⇒
+          0 ≤ j < (int)\offset((char *)\result) ⇒
           (int)*((char *)\old(buf)+j) ≢ \old(c);
     
     behavior not_exists:
-      assumes ∀ ℤ k; 0 ≤ k < n ⇒ (int)*((char *)buf+k) ≢ c;
+      assumes ∀ int k; 0 ≤ k < (int)n ⇒ (int)*((char *)buf+k) ≢ c;
       ensures \result ≡ (void *)0;
  */
 void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
@@ -79,9 +80,9 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
     int __gen_e_acsl_forall_2;
     unsigned long __gen_e_acsl_k;
     __gen_e_acsl_forall_2 = 1;
-    __gen_e_acsl_k = 0UL;
+    __gen_e_acsl_k = 0;
     while (1) {
-      if (__gen_e_acsl_k < n) ; else break;
+      if (__gen_e_acsl_k < (unsigned int)((int)n)) ; else break;
       {
         int __gen_e_acsl_valid_read_3;
         __gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_k),
@@ -89,26 +90,14 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
         __e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",
                         (char *)"memchr",
                         (char *)"mem_access: \\valid_read((char *)buf+__gen_e_acsl_k)",
-                        12);
+                        11);
         if ((int)*((char *)buf + __gen_e_acsl_k) != c) ;
         else {
           __gen_e_acsl_forall_2 = 0;
           goto e_acsl_end_loop3;
         }
       }
-      {
-        mpz_t __gen_e_acsl__5;
-        mpz_t __gen_e_acsl_add_3;
-        unsigned long __gen_e_acsl__6;
-        __gmpz_init_set_si(__gen_e_acsl__5,1L);
-        __gmpz_init(__gen_e_acsl_add_3);
-        __gmpz_add(__gen_e_acsl_add_3,(__mpz_struct const *)__gen_e_acsl_k,
-                   (__mpz_struct const *)(__gen_e_acsl__5));
-        __gen_e_acsl__6 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add_3));
-        __gen_e_acsl_k = __gen_e_acsl__6;
-        __gmpz_clear(__gen_e_acsl__5);
-        __gmpz_clear(__gen_e_acsl_add_3);
-      }
+      __gen_e_acsl_k ++;
     }
     e_acsl_end_loop3: ;
     __gen_e_acsl_at_4 = __gen_e_acsl_forall_2;
@@ -119,9 +108,9 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
     int __gen_e_acsl_exists;
     unsigned long __gen_e_acsl_i;
     __gen_e_acsl_exists = 0;
-    __gen_e_acsl_i = 0UL;
+    __gen_e_acsl_i = 0;
     while (1) {
-      if (__gen_e_acsl_i < n) ; else break;
+      if (__gen_e_acsl_i < (unsigned int)((int)n)) ; else break;
       {
         int __gen_e_acsl_valid_read;
         __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)((char *)buf + __gen_e_acsl_i),
@@ -136,19 +125,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
           goto e_acsl_end_loop1;
         }
       }
-      {
-        mpz_t __gen_e_acsl_;
-        mpz_t __gen_e_acsl_add;
-        unsigned long __gen_e_acsl__2;
-        __gmpz_init_set_si(__gen_e_acsl_,1L);
-        __gmpz_init(__gen_e_acsl_add);
-        __gmpz_add(__gen_e_acsl_add,(__mpz_struct const *)__gen_e_acsl_i,
-                   (__mpz_struct const *)(__gen_e_acsl_));
-        __gen_e_acsl__2 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add));
-        __gen_e_acsl_i = __gen_e_acsl__2;
-        __gmpz_clear(__gen_e_acsl_);
-        __gmpz_clear(__gen_e_acsl_add);
-      }
+      __gen_e_acsl_i ++;
     }
     e_acsl_end_loop1: ;
     __gen_e_acsl_at = __gen_e_acsl_exists;
@@ -167,7 +144,8 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
         {
           int __gen_e_acsl_offset;
           __gen_e_acsl_offset = __e_acsl_offset(__retres);
-          if (__gen_e_acsl_j < __gen_e_acsl_offset) ; else break;
+          if (__gen_e_acsl_j < (unsigned int)__gen_e_acsl_offset) ;
+          else break;
         }
         {
           int __gen_e_acsl_valid_read_2;
@@ -176,7 +154,7 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
           __e_acsl_assert(__gen_e_acsl_valid_read_2,(char *)"RTE",
                           (char *)"memchr",
                           (char *)"mem_access: \\valid_read((char *)__gen_e_acsl_at_2+__gen_e_acsl_j)",
-                          10);
+                          9);
           if ((int)*((char *)__gen_e_acsl_at_2 + __gen_e_acsl_j) != __gen_e_acsl_at_3) 
             ;
           else {
@@ -184,33 +162,21 @@ void *__gen_e_acsl_memchr(void const *buf, int c, size_t n)
             goto e_acsl_end_loop2;
           }
         }
-        {
-          mpz_t __gen_e_acsl__3;
-          mpz_t __gen_e_acsl_add_2;
-          unsigned long __gen_e_acsl__4;
-          __gmpz_init_set_si(__gen_e_acsl__3,1L);
-          __gmpz_init(__gen_e_acsl_add_2);
-          __gmpz_add(__gen_e_acsl_add_2,(__mpz_struct const *)__gen_e_acsl_j,
-                     (__mpz_struct const *)(__gen_e_acsl__3));
-          __gen_e_acsl__4 = __gmpz_get_ui((__mpz_struct const *)(__gen_e_acsl_add_2));
-          __gen_e_acsl_j = __gen_e_acsl__4;
-          __gmpz_clear(__gen_e_acsl__3);
-          __gmpz_clear(__gen_e_acsl_add_2);
-        }
+        __gen_e_acsl_j ++;
       }
       e_acsl_end_loop2: ;
       __gen_e_acsl_implies = __gen_e_acsl_forall;
     }
     __e_acsl_assert(__gen_e_acsl_implies,(char *)"Postcondition",
                     (char *)"memchr",
-                    (char *)"\\old(\\exists integer i; 0 <= i < n && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n   0 <= j < \\offset((char *)\\result) ==>\n   (int)*((char *)\\old(buf)+j) != \\old(c))",
-                    10);
+                    (char *)"\\old(\\exists int i; 0 <= i < (int)n && (int)*((char *)buf+i) == c) ==>\n(\\forall int j;\n   0 <= j < (int)\\offset((char *)\\result) ==>\n   (int)*((char *)\\old(buf)+j) != \\old(c))",
+                    9);
     if (! __gen_e_acsl_at_4) __gen_e_acsl_implies_2 = 1;
     else __gen_e_acsl_implies_2 = __retres == (void *)0;
     __e_acsl_assert(__gen_e_acsl_implies_2,(char *)"Postcondition",
                     (char *)"memchr",
-                    (char *)"\\old(\\forall integer k; 0 <= k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
-                    13);
+                    (char *)"\\old(\\forall int k; 0 <= k < (int)n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
+                    12);
     __e_acsl_delete_block((void *)(& buf));
     __e_acsl_delete_block((void *)(& __retres));
     return __retres;

src/plugins/e-acsl/tests/bts/test_config

 LOG: gen_@PTEST_NAME@.c
 OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/bts/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -value-verbose 0
-EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@"
+EXEC: ./scripts/testrun.sh @PTEST_NAME@ bts "" "--frama-c=@frama-c@"

src/plugins/e-acsl/tests/gmp/test_config

 LOG: gen_@PTEST_NAME@.c
 OPT: -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results
-EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
+EXEC: ./scripts/testrun.sh @PTEST_NAME@ gmp "1" "--frama-c=@frama-c@"
 LOG: gen_@PTEST_NAME@2.c
 OPT: -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/gmp/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -val -no-val-print -no-val-show-progress -no-results