[e-acsl] update TODO-list

src/plugins/e-acsl/TODO

-- enlever les skip inutiles
-- valid global literal string
-
-################
-# MEMORY MODEL #
-################
-
-- appel de full_init et consort sur des variables générées par e_acsl (at.i)
-- ne générer les instructions que si nécessaire
-- traduction constructions logiques modèle mémoire \valid, \init ...
-
 ################
 # NEXT RELEASE #
 ################
 
-- updater doc/Changelog
 - [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
   à appeler dès qu'un behavior est activé
 - utiliser Rte pour tous les overflows potentiels
@@ -54,8 +42,6 @@
 # TESTS #
 #########
 
-- améliorer test "integer_constant.i" quand bug fixed #745
 - inclure exemple du E-ACSL Reference Manual
 - test arith.i: mettre les exemples du ACSL manual about div and modulo
-- -val-verbose 0 dans les tests...
-- test intensif modèle mémoire
+- tests intensifs modèle mémoire

src/plugins/e-acsl/tests/e-acsl-runtime/integer_constant.i

 /* run.config
    COMMENT: integer constant + a stmt after the assertion
-   COMMENT: waiting for fixing BTS #745
    EXECNOW: LOG gen_integer_constant.c BIN gen_integer_constant.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant.c > /dev/null && ./gcc_test.sh integer_constant
    EXECNOW: LOG gen_integer_constant2.c BIN gen_integer_constant2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/integer_constant.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_integer_constant2.c > /dev/null && ./gcc_test.sh integer_constant2
 */
@@ -11,7 +10,7 @@ int main(void) {
   /*@ assert 0 != 1; */
   /*@ assert 1152921504606846975 == 0xfffffffffffffff; */
 
-  /* /\*@ assert 0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff; *\/ */
+  /*@ assert 0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff; */
 
   return 0;
 }

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant.c

@@ -22,6 +22,27 @@ typedef struct __fc_FILE FILE;
 /*@
 model __mpz_struct { ℤ n };
 */
+/*@ requires ¬\initialized(z);
+    ensures \valid(\old(z));
+    
+    ensures \initialized(\old(z));
+    allocates \old(z);
+    
+    assigns *z;
+    assigns *z \from str, base;
+  
+*/
+extern  __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
+                                                                char const *str,
+                                                                int base);
+/*@ requires \valid(x);
+    assigns *x;  */
+extern  __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+    requires \valid(z2);
+    assigns \nothing;  */
+extern  __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+                                                       __mpz_struct const * /*[1]*/ z2);
 int __fc_random_counter __attribute__((__unused__));
 unsigned long const __fc_rand_max = (unsigned long)2147483647;
 extern int __fc_heap_status;
@@ -58,14 +79,30 @@ int main(void)
   int __retres;
   int x;
   /*@ assert 0 ≡ 0; */
-  e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"0 == 0",9);
+  e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"0 == 0",8);
   x = 0;
   x ++;
   /*@ assert 0 ≢ 1; */
-  e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"0 != 1",11);
+  e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"0 != 1",10);
   /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
   e_acsl_assert(1152921504606846975 == 0xfffffffffffffff,(char *)"Assertion",
-                (char *)"1152921504606846975 == 0xfffffffffffffff",12);
+                (char *)"1152921504606846975 == 0xfffffffffffffff",11);
+  /*@ assert
+      0xffffffffffffffffffffffffffffffff ≡
+      0xffffffffffffffffffffffffffffffff;
+  */
+  {
+    mpz_t __e_acsl;
+    int __e_acsl_eq;
+    __gmpz_init_set_str(__e_acsl,"340282366920938463463374607431768211455",
+                        10);
+    __e_acsl_eq = __gmpz_cmp(__e_acsl,__e_acsl);
+    e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",
+                  (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
+                  13);
+    __gmpz_clear(__e_acsl);
+  }
+  
   __retres = 0;
   __clean();
   return (__retres);

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_integer_constant2.c

@@ -96,7 +96,7 @@ int main(void)
     int __e_acsl_eq;
     __gmpz_init_set_si(__e_acsl,(long)0);
     __e_acsl_eq = __gmpz_cmp(__e_acsl,__e_acsl);
-    e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",9);
+    e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",8);
     __gmpz_clear(__e_acsl);
   }
   
@@ -110,7 +110,7 @@ int main(void)
     __gmpz_init_set_si(__e_acsl_2,(long)0);
     __gmpz_init_set_si(__e_acsl_3,(long)1);
     __e_acsl_ne = __gmpz_cmp(__e_acsl_2,__e_acsl_3);
-    e_acsl_assert(__e_acsl_ne != 0,(char *)"Assertion",(char *)"0 != 1",11);
+    e_acsl_assert(__e_acsl_ne != 0,(char *)"Assertion",(char *)"0 != 1",10);
     __gmpz_clear(__e_acsl_2);
     __gmpz_clear(__e_acsl_3);
   }
@@ -122,10 +122,26 @@ int main(void)
     __gmpz_init_set_str(__e_acsl_4,"1152921504606846975",10);
     __e_acsl_eq_2 = __gmpz_cmp(__e_acsl_4,__e_acsl_4);
     e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",
-                  (char *)"1152921504606846975 == 0xfffffffffffffff",12);
+                  (char *)"1152921504606846975 == 0xfffffffffffffff",11);
     __gmpz_clear(__e_acsl_4);
   }
   
+  /*@ assert
+      0xffffffffffffffffffffffffffffffff ≡
+      0xffffffffffffffffffffffffffffffff;
+  */
+  {
+    mpz_t __e_acsl_5;
+    int __e_acsl_eq_3;
+    __gmpz_init_set_str(__e_acsl_5,"340282366920938463463374607431768211455",
+                        10);
+    __e_acsl_eq_3 = __gmpz_cmp(__e_acsl_5,__e_acsl_5);
+    e_acsl_assert(__e_acsl_eq_3 == 0,(char *)"Assertion",
+                  (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
+                  13);
+    __gmpz_clear(__e_acsl_5);
+  }
+  
   __retres = 0;
   __clean();
   return (__retres);

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle

@@ -25,70 +25,84 @@
                      [1].__fc_stdio_id ∈ [--..--]
         S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
         S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-tests/e-acsl-runtime/integer_constant.i:9:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:8:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:9.
+        Called from tests/e-acsl-runtime/integer_constant.i:8.
 [value] using specification for function __gmpz_init_set_si
 ./share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
 ./share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
 ./share/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: postcondition got status unknown.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_cmp <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:9.
+        Called from tests/e-acsl-runtime/integer_constant.i:8.
 [value] using specification for function __gmpz_cmp
 ./share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
 ./share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_assert <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:9.
+        Called from tests/e-acsl-runtime/integer_constant.i:8.
 ./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
 [value] computing for function __gmpz_clear <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:9.
+        Called from tests/e-acsl-runtime/integer_constant.i:8.
 [value] using specification for function __gmpz_clear
 ./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
 [value] Done for function __gmpz_clear
-tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:10:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:11.
+        Called from tests/e-acsl-runtime/integer_constant.i:10.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_init_set_si <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:11.
+        Called from tests/e-acsl-runtime/integer_constant.i:10.
 [value] Done for function __gmpz_init_set_si
 [value] computing for function __gmpz_cmp <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:11.
+        Called from tests/e-acsl-runtime/integer_constant.i:10.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_assert <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:11.
+        Called from tests/e-acsl-runtime/integer_constant.i:10.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
 [value] computing for function __gmpz_clear <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:11.
+        Called from tests/e-acsl-runtime/integer_constant.i:10.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_clear <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:11.
+        Called from tests/e-acsl-runtime/integer_constant.i:10.
 [value] Done for function __gmpz_clear
-tests/e-acsl-runtime/integer_constant.i:12:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid.
 [value] computing for function __gmpz_init_set_str <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:12.
+        Called from tests/e-acsl-runtime/integer_constant.i:11.
 [value] using specification for function __gmpz_init_set_str
 ./share/e-acsl/e_acsl_gmp.h:70:[value] Function __gmpz_init_set_str: precondition got status valid.
 ./share/e-acsl/e_acsl_gmp.h:72:[value] Function __gmpz_init_set_str: postcondition got status valid.
 ./share/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: postcondition got status unknown.
 [value] Done for function __gmpz_init_set_str
 [value] computing for function __gmpz_cmp <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:12.
+        Called from tests/e-acsl-runtime/integer_constant.i:11.
+[value] Done for function __gmpz_cmp
+[value] computing for function e_acsl_assert <- main.
+        Called from tests/e-acsl-runtime/integer_constant.i:11.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+        Called from tests/e-acsl-runtime/integer_constant.i:11.
+[value] Done for function __gmpz_clear
+tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
+[value] computing for function __gmpz_init_set_str <- main.
+        Called from tests/e-acsl-runtime/integer_constant.i:13.
+[value] Done for function __gmpz_init_set_str
+[value] computing for function __gmpz_cmp <- main.
+        Called from tests/e-acsl-runtime/integer_constant.i:13.
 [value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_assert <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:12.
+        Called from tests/e-acsl-runtime/integer_constant.i:13.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
 [value] computing for function __gmpz_clear <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:12.
+        Called from tests/e-acsl-runtime/integer_constant.i:13.
 [value] Done for function __gmpz_clear
 [value] computing for function __clean <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:16.
+        Called from tests/e-acsl-runtime/integer_constant.i:15.
 [value] using specification for function __clean
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] Done for function __clean
@@ -198,7 +212,7 @@ int main(void)
     int __e_acsl_eq;
     __gmpz_init_set_si(__e_acsl,(long)0);
     __e_acsl_eq = __gmpz_cmp(__e_acsl,__e_acsl);
-    e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",9);
+    e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"0 == 0",8);
     __gmpz_clear(__e_acsl);
   }
   
@@ -212,7 +226,7 @@ int main(void)
     __gmpz_init_set_si(__e_acsl_2,(long)0);
     __gmpz_init_set_si(__e_acsl_3,(long)1);
     __e_acsl_ne = __gmpz_cmp(__e_acsl_2,__e_acsl_3);
-    e_acsl_assert(__e_acsl_ne != 0,(char *)"Assertion",(char *)"0 != 1",11);
+    e_acsl_assert(__e_acsl_ne != 0,(char *)"Assertion",(char *)"0 != 1",10);
     __gmpz_clear(__e_acsl_2);
     __gmpz_clear(__e_acsl_3);
   }
@@ -224,10 +238,26 @@ int main(void)
     __gmpz_init_set_str(__e_acsl_4,"1152921504606846975",10);
     __e_acsl_eq_2 = __gmpz_cmp(__e_acsl_4,__e_acsl_4);
     e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",
-                  (char *)"1152921504606846975 == 0xfffffffffffffff",12);
+                  (char *)"1152921504606846975 == 0xfffffffffffffff",11);
     __gmpz_clear(__e_acsl_4);
   }
   
+  /*@ assert
+      0xffffffffffffffffffffffffffffffff ≡
+      0xffffffffffffffffffffffffffffffff;
+  */
+  {
+    mpz_t __e_acsl_5;
+    int __e_acsl_eq_3;
+    __gmpz_init_set_str(__e_acsl_5,"340282366920938463463374607431768211455",
+                        10);
+    __e_acsl_eq_3 = __gmpz_cmp(__e_acsl_5,__e_acsl_5);
+    e_acsl_assert(__e_acsl_eq_3 == 0,(char *)"Assertion",
+                  (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
+                  13);
+    __gmpz_clear(__e_acsl_5);
+  }
+  
   __retres = 0;
   __clean();
   return (__retres);

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle

@@ -25,24 +25,48 @@
                      [1].__fc_stdio_id ∈ [--..--]
         S___fc_stdio_buffer_0_S___fc_stdout[0..1] ∈ [--..--]
         S___fc_stdio_buffer_1_S___fc_stdout[0..1] ∈ [--..--]
-tests/e-acsl-runtime/integer_constant.i:9:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:8:[value] Assertion got status valid.
 [value] computing for function e_acsl_assert <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:9.
+        Called from tests/e-acsl-runtime/integer_constant.i:8.
 ./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status valid.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
+tests/e-acsl-runtime/integer_constant.i:10:[value] Assertion got status valid.
+[value] computing for function e_acsl_assert <- main.
+        Called from tests/e-acsl-runtime/integer_constant.i:10.
+[value] Recording results for e_acsl_assert
+[value] Done for function e_acsl_assert
 tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid.
 [value] computing for function e_acsl_assert <- main.
         Called from tests/e-acsl-runtime/integer_constant.i:11.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-tests/e-acsl-runtime/integer_constant.i:12:[value] Assertion got status valid.
+tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
+[value] computing for function __gmpz_init_set_str <- main.
+        Called from tests/e-acsl-runtime/integer_constant.i:13.
+[value] using specification for function __gmpz_init_set_str
+./share/e-acsl/e_acsl_gmp.h:70:[value] Function __gmpz_init_set_str: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:72:[value] Function __gmpz_init_set_str: postcondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: postcondition got status unknown.
+[value] Done for function __gmpz_init_set_str
+[value] computing for function __gmpz_cmp <- main.
+        Called from tests/e-acsl-runtime/integer_constant.i:13.
+[value] using specification for function __gmpz_cmp
+./share/e-acsl/e_acsl_gmp.h:115:[value] Function __gmpz_cmp: precondition got status valid.
+./share/e-acsl/e_acsl_gmp.h:116:[value] Function __gmpz_cmp: precondition got status valid.
+[value] Done for function __gmpz_cmp
 [value] computing for function e_acsl_assert <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:12.
+        Called from tests/e-acsl-runtime/integer_constant.i:13.
+./share/e-acsl/e_acsl.h:37:[value] Function e_acsl_assert: precondition got status unknown.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
+[value] computing for function __gmpz_clear <- main.
+        Called from tests/e-acsl-runtime/integer_constant.i:13.
+[value] using specification for function __gmpz_clear
+./share/e-acsl/e_acsl_gmp.h:105:[value] Function __gmpz_clear: precondition got status valid.
+[value] Done for function __gmpz_clear
 [value] computing for function __clean <- main.
-        Called from tests/e-acsl-runtime/integer_constant.i:16.
+        Called from tests/e-acsl-runtime/integer_constant.i:15.
 [value] using specification for function __clean
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
 [value] Done for function __clean
@@ -77,6 +101,27 @@ typedef struct __fc_FILE FILE;
 /*@
 model __mpz_struct { ℤ n };
 */
+/*@ requires ¬\initialized(z);
+    ensures \valid(\old(z));
+    
+    ensures \initialized(\old(z));
+    allocates \old(z);
+    
+    assigns *z;
+    assigns *z \from str, base;
+  
+*/
+extern  __attribute__((__FC_BUILTIN__)) int __gmpz_init_set_str(__mpz_struct * /*[1]*/ z,
+                                                                char const *str,
+                                                                int base);
+/*@ requires \valid(x);
+    assigns *x;  */
+extern  __attribute__((__FC_BUILTIN__)) void __gmpz_clear(__mpz_struct * /*[1]*/ x);
+/*@ requires \valid(z1);
+    requires \valid(z2);
+    assigns \nothing;  */
+extern  __attribute__((__FC_BUILTIN__)) int __gmpz_cmp(__mpz_struct const * /*[1]*/ z1,
+                                                       __mpz_struct const * /*[1]*/ z2);
 int __fc_random_counter __attribute__((__unused__));
 unsigned long const __fc_rand_max = (unsigned long)2147483647;
 extern int __fc_heap_status;
@@ -114,14 +159,30 @@ int main(void)
   int __retres;
   int x;
   /*@ assert 0 ≡ 0; */
-  e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"0 == 0",9);
+  e_acsl_assert(0 == 0,(char *)"Assertion",(char *)"0 == 0",8);
   x = 0;
   x ++;
   /*@ assert 0 ≢ 1; */
-  e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"0 != 1",11);
+  e_acsl_assert(0 != 1,(char *)"Assertion",(char *)"0 != 1",10);
   /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */
   e_acsl_assert(1152921504606846975 == 0xfffffffffffffff,(char *)"Assertion",
-                (char *)"1152921504606846975 == 0xfffffffffffffff",12);
+                (char *)"1152921504606846975 == 0xfffffffffffffff",11);
+  /*@ assert
+      0xffffffffffffffffffffffffffffffff ≡
+      0xffffffffffffffffffffffffffffffff;
+  */
+  {
+    mpz_t __e_acsl;
+    int __e_acsl_eq;
+    __gmpz_init_set_str(__e_acsl,"340282366920938463463374607431768211455",
+                        10);
+    __e_acsl_eq = __gmpz_cmp(__e_acsl,__e_acsl);
+    e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",
+                  (char *)"0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff",
+                  13);
+    __gmpz_clear(__e_acsl);
+  }
+  
   __retres = 0;
   __clean();
   return (__retres);