remove incorrect tests about sizeof(literal_string)

src/plugins/e-acsl/TODO

@@ -20,6 +20,7 @@
 # KNOWN BUGS #
 ##############
 
+- sizeof("literal_string") (voir sizeof.i)
 - Bernard's bug avec un requires global et un ensures dans un behavior
 - \at incorrect si StmtLabel faisant référence au stmt courant (voir test at.i)
 - incorrect d'utiliser un \old dans le post-state si pre-state == post-state

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

@@ -34,9 +34,6 @@ int main(void)
   /*@ assert sizeof(int) ≡ sizeof(x); */ ;
   e_acsl_assert(4 == 4,(char *)"Assertion",
                 (char *)"(sizeof(int) == sizeof(x))",9);
-  /*@ assert sizeof("totototototo") ≡ sizeof(char *); */ ;
-  e_acsl_assert(4 == 4,(char *)"Assertion",
-                (char *)"(sizeof(\"totototototo\") == sizeof(char *))",10);
   __retres = 0;
   return (__retres);
 }

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

@@ -64,21 +64,6 @@ int main(void)
     __gmpz_clear((__mpz_struct *)(__e_acsl_sizeof_2));
   }
   
-  /*@ assert sizeof("totototototo") ≡ sizeof(char *); */ ;
-  {
-    mpz_t __e_acsl_sizeof_3;
-    mpz_t __e_acsl_sizeof_4;
-    int __e_acsl_eq_2;
-    __gmpz_init_set_si((__mpz_struct *)(__e_acsl_sizeof_3),(long)4);
-    __gmpz_init_set_si((__mpz_struct *)(__e_acsl_sizeof_4),(long)4);
-    __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_sizeof_3),
-                               (__mpz_struct const *)(__e_acsl_sizeof_4));
-    e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",
-                  (char *)"(sizeof(\"totototototo\") == sizeof(char *))",10);
-    __gmpz_clear((__mpz_struct *)(__e_acsl_sizeof_3));
-    __gmpz_clear((__mpz_struct *)(__e_acsl_sizeof_4));
-  }
-  
   __retres = 0;
   return (__retres);
 }

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

@@ -30,26 +30,6 @@ PROJECT_FILE.i:120:[value] Function __gmpz_clear: precondition got status valid.
 [value] computing for function __gmpz_clear <- main.
         Called from PROJECT_FILE.i:257.
 [value] Done for function __gmpz_clear
-PROJECT_FILE.i:261:[value] Assertion got status valid.
-[value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:266.
-[value] Done for function __gmpz_init_set_si
-[value] computing for function __gmpz_init_set_si <- main.
-        Called from PROJECT_FILE.i:267.
-[value] Done for function __gmpz_init_set_si
-[value] computing for function __gmpz_cmp <- main.
-        Called from PROJECT_FILE.i:268.
-[value] Done for function __gmpz_cmp
-[value] computing for function e_acsl_assert <- main.
-        Called from PROJECT_FILE.i:269.
-[value] Recording results for e_acsl_assert
-[value] Done for function e_acsl_assert
-[value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:271.
-[value] Done for function __gmpz_clear
-[value] computing for function __gmpz_clear <- main.
-        Called from PROJECT_FILE.i:272.
-[value] Done for function __gmpz_clear
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
@@ -126,21 +106,6 @@ int main(void)
     __gmpz_clear((__mpz_struct *)(__e_acsl_sizeof_2));
   }
   
-  /*@ assert sizeof("totototototo") ≡ sizeof(char *); */ ;
-  {
-    mpz_t __e_acsl_sizeof_3;
-    mpz_t __e_acsl_sizeof_4;
-    int __e_acsl_eq_2;
-    __gmpz_init_set_si((__mpz_struct *)(__e_acsl_sizeof_3),(long)4);
-    __gmpz_init_set_si((__mpz_struct *)(__e_acsl_sizeof_4),(long)4);
-    __e_acsl_eq_2 = __gmpz_cmp((__mpz_struct const *)(__e_acsl_sizeof_3),
-                               (__mpz_struct const *)(__e_acsl_sizeof_4));
-    e_acsl_assert(__e_acsl_eq_2 == 0,(char *)"Assertion",
-                  (char *)"(sizeof(\"totototototo\") == sizeof(char *))",10);
-    __gmpz_clear((__mpz_struct *)(__e_acsl_sizeof_3));
-    __gmpz_clear((__mpz_struct *)(__e_acsl_sizeof_4));
-  }
-  
   __retres = 0;
   return (__retres);
 }

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

@@ -8,11 +8,6 @@ PROJECT_FILE.i:246:[value] Assertion got status valid.
 PROJECT_FILE.i:231:[value] Function e_acsl_assert: precondition got status valid.
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
-PROJECT_FILE.i:249:[value] Assertion got status valid.
-[value] computing for function e_acsl_assert <- main.
-        Called from PROJECT_FILE.i:250.
-[value] Recording results for e_acsl_assert
-[value] Done for function e_acsl_assert
 [value] Recording results for main
 [value] done for function main
 [value] ====== VALUES COMPUTED ======
@@ -56,9 +51,6 @@ int main(void)
   /*@ assert sizeof(int) ≡ sizeof(x); */ ;
   e_acsl_assert(4 == 4,(char *)"Assertion",
                 (char *)"(sizeof(int) == sizeof(x))",9);
-  /*@ assert sizeof("totototototo") ≡ sizeof(char *); */ ;
-  e_acsl_assert(4 == 4,(char *)"Assertion",
-                (char *)"(sizeof(\"totototototo\") == sizeof(char *))",10);
   __retres = 0;
   return (__retres);
 }

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

@@ -7,6 +7,6 @@
 int main(void) {
   int x = 0;
   /*@ assert sizeof(int) == sizeof(x); */ ;
-  /*@ assert sizeof("totototototo") == sizeof(char *); */ ;
+  //  /*@ assert sizeof("totototototo") == sizeof(char *); */ ;
   return 0;
 }