[e-acsl] minor code+tests improvements

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

@@ -7,7 +7,7 @@ int main(void) {
   int x;
   /*@ assert 0 == 0; */ x = 0;
   /*@ assert 0 != 1; */
-  /*@ assert 0xfffffffffffffff == 0xfffffffffffffff; */
+  /*@ assert 1152921504606846975 == 0xfffffffffffffff; */
 
   /* /\*@ assert 0xffffffffffffffffffffffffffffffff == 0xffffffffffffffffffffffffffffffff; *\/ */
 

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

@@ -593,14 +593,14 @@ int main(void)
     __gmpz_clear((__mpz_struct *)(e_acsl_5));
   }
   
-  /*@ assert 0xfffffffffffffff ≡ 0xfffffffffffffff; */ ;
+  /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */ ;
   { mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
     __gmpz_init_set_str((__mpz_struct *)(e_acsl_7),"1152921504606846975",10);
     __gmpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
     e_acsl_9 = __gmpz_cmp((__mpz_struct const *)(e_acsl_7),
                           (__mpz_struct const *)(e_acsl_8));
     if (! (e_acsl_9 == 0)) {
-      e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
+      e_acsl_fail((char *)"(1152921504606846975 == 0xfffffffffffffff)");
     } __gmpz_clear((__mpz_struct *)(e_acsl_7));
     __gmpz_clear((__mpz_struct *)(e_acsl_8));
   }

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

@@ -175,14 +175,14 @@ int main(void)
     mpz_clear((__mpz_struct *)(e_acsl_5));
   }
   
-  /*@ assert 0xfffffffffffffff ≡ 0xfffffffffffffff; */ ;
+  /*@ assert 1152921504606846975 ≡ 0xfffffffffffffff; */ ;
   { mpz_t e_acsl_7; mpz_t e_acsl_8; int e_acsl_9;
     mpz_init_set_str((__mpz_struct *)(e_acsl_7),"1152921504606846975",10);
     mpz_init_set_str((__mpz_struct *)(e_acsl_8),"1152921504606846975",10);
     e_acsl_9 = mpz_cmp((__mpz_struct const *)(e_acsl_7),
                        (__mpz_struct const *)(e_acsl_8));
     if (! (e_acsl_9 == 0)) {
-      e_acsl_fail((char *)"(0xfffffffffffffff == 0xfffffffffffffff)");
+      e_acsl_fail((char *)"(1152921504606846975 == 0xfffffffffffffff)");
     } mpz_clear((__mpz_struct *)(e_acsl_7));
     mpz_clear((__mpz_struct *)(e_acsl_8));
   }

src/plugins/e-acsl/visit.ml

@@ -230,14 +230,17 @@ end
 (* ************************************************************************** *)
 
 let constant_to_exp ?(loc=Location.unknown) = function
-  | CInt64(n, k, s) ->
-    (match k with
-    | IBool | IChar | IUChar | IUInt | IUShort | IULong
-    | ISChar | IShort | IInt | ILong ->
-      kinteger64_repr ?loc k n s
-    | ILongLong | IULongLong ->
-      mkString ?loc (Int64.to_string n))
-  | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c -> new_exp ?loc (Const c)
+  | CInt64(n, 
+	   (IBool | IChar | IUChar | IUInt | IUShort | IULong
+	       | ISChar | IShort | IInt | ILong as k), 
+	   s) ->
+    kinteger64_repr ?loc k n s
+  | CInt64(n, (ILongLong | IULongLong), _s) -> 
+    (* cannot use the string [s] if any since we do not know the base in which
+       it is written. Such a base is required by GMP. *)
+    mkString ?loc (Int64.to_string n)
+  | CStr _ | CWStr _ | CChr _ | CReal _ | CEnum _ as c -> 
+    new_exp ?loc (Const c)
 
 let tlval_to_lval = function
   | TVar { lv_origin = Some v }, TNoOffset -> Var v, NoOffset
@@ -536,7 +539,8 @@ class e_acsl_visitor prj generate = object (self)
 	stmt 
 	Env.empty
     in
-    if Env.is_empty env then DoChildren
+    if Env.is_empty env then 
+      DoChildren
     else begin
       assert generate;
       let mk_block stmt =
@@ -548,7 +552,6 @@ class e_acsl_visitor prj generate = object (self)
 
   initializer Env.register_actions_queue self#get_filling_actions
 
-
 end
 
 let do_visit ?(prj=Project.current ()) generate =