upgrading oracles according to bug fixed #744

src/plugins/e-acsl/TODO

 
+- guarde pour les divisions/modulos
+
 - tester les opérations binaires sur les pointeurs (requiert complex left value)
 
 - amélioration des locs quand possible (genre Prel)
 
-- amliorer test "comparison.i" quand bug fixed #744
-- remettre test "cast.i" quand bug fixed #744
 - améliorer test "integer_constant.i" quand bug fixed #745
-- amliorer test "arith.i" quand bug fixed #744
+- améliorer test "arith.i" quand bug fixed #751
 
 en lien avec bts #743:
 - make distrib

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

 /* run.config
-   COMMENT: arithmetic operations */
+   COMMENT: arithmetic operations
+   COMMENT: add the last assertion when fixing BTS #751 */
 
 void main() {
   int x = -3;
@@ -22,7 +23,7 @@ void main() {
   /*@ assert (0 >= -1) == (0 <= 0); */ ;
   /*@ assert (0 != 1) == !(0 != 0); */ ;
 
-  //  /*@ assert 0 == !1; */ ;
+  //   /*@ assert 0 == !1; */ ;
   /* subtyping relation: 0 should be promoted to boolean below
-     How to handle this? */
+     How to handle this? See BTS #751 */
 }

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

 /* run.config
-   DONTRUN:
-   COMMENT: cast
-   COMMENT: waiting for fixing bts #744 */
+   COMMENT: cast */
 
 void main() {
   long x = 0;

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

 /* run.config
-   COMMENT: comparison operators
-   COMMENT: will be improved by fixing BTS #744 */
+   COMMENT: comparison operators */
 
 void main() {
   int x = 0, y = 1;

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

@@ -2,91 +2,17 @@
 [value] Computing initial state
 [value] Initial state computed
 [value] Values of globals at initialization
-PROJECT_FILE:77:[value] Assertion got status valid.
-[value] computing for function mpz_init <-main.
-        Called from PROJECT_FILE:79.
-PROJECT_FILE:79:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
-        Called from PROJECT_FILE:79.
-PROJECT_FILE:79:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_init <-main.
-        Called from PROJECT_FILE:80.
-PROJECT_FILE:80:[value] Function mpz_init: postcondition got status unknown
-[value] Done for function mpz_init
-[value] computing for function mpz_set_si <-main.
-        Called from PROJECT_FILE:80.
-PROJECT_FILE:80:[value] Function mpz_set_si: precondition got status valid
-[value] Done for function mpz_set_si
-[value] computing for function mpz_cmp <-main.
-        Called from PROJECT_FILE:81.
-PROJECT_FILE:81:[value] Function mpz_cmp: precondition got status valid
-[value] Done for function mpz_cmp
-[value] computing for function e_acsl_fail <-main.
-        Called from PROJECT_FILE:82.
-[value] computing for function eprintf <-e_acsl_fail <-main.
-        Called from PROJECT_FILE:69.
-[value] Done for function eprintf
-[value] computing for function exit <-e_acsl_fail <-main.
-        Called from PROJECT_FILE:69.
-PROJECT_FILE:69:[value] Function exit: postcondition got status invalid
-[value] Done for function exit
-[value] Recording results for e_acsl_fail
-[value] Done for function e_acsl_fail
-[value] computing for function mpz_clear <-main.
-        Called from PROJECT_FILE:83.
-PROJECT_FILE:83:[value] Function mpz_clear: precondition got status valid
-[value] Done for function mpz_clear
-[value] computing for function mpz_clear <-main.
-        Called from PROJECT_FILE:83.
-[value] Done for function mpz_clear
+PROJECT_FILE:123:[value] Assertion got status valid.
+PROJECT_FILE:126:[value] Assertion got status valid.
 [value] Recording results for main
 [value] done for function main
-[from] Computing for function mpz_init
-[from] Done for function mpz_init
-[from] Computing for function mpz_set_si
-[from] Done for function mpz_set_si
-[from] Computing for function mpz_cmp
-[from] Done for function mpz_cmp
-[from] Computing for function e_acsl_fail
-[from] Computing for function eprintf <-e_acsl_fail
-[from] Done for function eprintf
-[from] Computing for function exit <-e_acsl_fail
-[from] Done for function exit
-PROJECT_FILE:69:[from] Non terminating function (no dependencies)
-[from] Done for function e_acsl_fail
-[from] Computing for function mpz_clear
-[from] Done for function mpz_clear
 [dominators] computing for function main
 [dominators] done for function main
 [value] ====== VALUES COMPUTED ======
-[value] Values for function e_acsl_fail:
-          NON TERMINATING FUNCTION
 [value] Values for function main:
           x ∈ {0; }
           y ∈ {0; }
 /* Generated by Frama-C */
-struct __anonstruct___mpz_struct_1 {
-   int _mp_alloc ;
-   int _mp_size ;
-   unsigned long *_mp_d ;
-};
-typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
-typedef __mpz_struct mpz_t[1];
-/*@ ensures \valid(\at(x,Old));
-    assigns *x;  */
-extern void mpz_init(__mpz_struct * /*[1]*/  x ) ;
-/*@ requires \valid(x);
-    assigns *x;  */
-extern void mpz_clear(__mpz_struct * /*[1]*/  x ) ;
-/*@ requires \valid(z);
-    assigns *z;  */
-extern void mpz_set_si(__mpz_struct * /*[1]*/  z , long n ) ;
-/*@ requires \valid(z1);
-    requires \valid(z2);
-    assigns \nothing;  */
-extern int mpz_cmp(__mpz_struct * /*[1]*/  z1 , __mpz_struct * /*[1]*/  z2 ) ;
 /*@ terminates \false;
     ensures \false;
     assigns \nothing;  */
@@ -106,19 +32,10 @@ void main(void)
   int y ;
   x = (long )0;
   y = 0;
-  /*@ assert ((int )x ≡ y); */ ;
-  { mpz_t e_acsl_cst_1 ; mpz_t e_acsl_cst_2 ; int e_acsl_cst_3 ;
-    mpz_init((__mpz_struct *)(e_acsl_cst_1));
-    mpz_set_si((__mpz_struct *)(e_acsl_cst_1),(long )((int )x));
-    mpz_init((__mpz_struct *)(e_acsl_cst_2));
-    mpz_set_si((__mpz_struct *)(e_acsl_cst_2),(long )y);
-    e_acsl_cst_3 = mpz_cmp((__mpz_struct *)(e_acsl_cst_1),
-                           (__mpz_struct *)(e_acsl_cst_2));
-    if (e_acsl_cst_3 != 0) { e_acsl_fail((char *)"(((int )x == y))"); }
-    mpz_clear((__mpz_struct *)(e_acsl_cst_2));
-    mpz_clear((__mpz_struct *)(e_acsl_cst_1));
-  }
-  
+  /*@ assert (int )x ≡ y; */ ;
+  if ((int )x != y) { e_acsl_fail((char *)"((int )x == y)"); }
+  /*@ assert x ≡ (long )y; */ ;
+  if (x != (long )y) { e_acsl_fail((char *)"(x == (long )y)"); }
   return;
 }