[typing] fix bug when mixing integers and floats in annotations while -e-acsl-gmp-only is activated

src/plugins/e-acsl/src/analyses/typing.ml

@@ -292,10 +292,13 @@ let ty_of_logic_ty ?term lty =
 (* generate a context [c]. Take --e-acsl-gmp-only into account iff [use_gmp_opt]
    is true. *)
 let mk_ctx ~use_gmp_opt = function
+  | C_float _ as f ->
+    if use_gmp_opt && Options.Gmp_only.get () then Rational
+    else f
   | C_integer _ as c ->
     if use_gmp_opt && Options.Gmp_only.get () then Gmpz
     else c
-  | C_float _ | Gmpz | Rational | Real | Nan as c -> c
+  | Gmpz | Rational | Real | Nan as c -> c
 
 (* the number_ty corresponding to [t] whenever use as an offset.
    In that case, it cannot be a GMP, so it must be coerced to an integral type

src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle

@@ -28,6 +28,6 @@
 [eva:alarm] tests/gmp-only/functions.c:25: Warning: 
   function __e_acsl_assert: precondition got status unknown.
 [eva:alarm] tests/gmp-only/functions.c:68: Warning: 
-  non-finite double value. assert \is_finite(__gen_e_acsl__15);
+  non-finite double value. assert \is_finite(__gen_e_acsl_cast);
 [eva:alarm] tests/gmp-only/functions.c:68: Warning: 
   function __e_acsl_assert: precondition got status unknown.

src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c

@@ -255,9 +255,20 @@ int main(void)
   double d = 2.0;
   {
     double __gen_e_acsl_f2_2;
+    __e_acsl_mpq_t __gen_e_acsl__15;
+    __e_acsl_mpq_t __gen_e_acsl__16;
+    int __gen_e_acsl_gt_5;
     __gen_e_acsl_f2_2 = __gen_e_acsl_f2(d);
-    __e_acsl_assert(__gen_e_acsl_f2_2 > 0.,"Assertion","main","f2(d) > 0",
+    __gmpq_init(__gen_e_acsl__15);
+    __gmpq_set_str(__gen_e_acsl__15,"0",10);
+    __gmpq_init(__gen_e_acsl__16);
+    __gmpq_set_d(__gen_e_acsl__16,__gen_e_acsl_f2_2);
+    __gen_e_acsl_gt_5 = __gmpq_cmp((__e_acsl_mpq_struct const *)(__gen_e_acsl__16),
+                                   (__e_acsl_mpq_struct const *)(__gen_e_acsl__15));
+    __e_acsl_assert(__gen_e_acsl_gt_5 > 0,"Assertion","main","f2(d) > 0",
                     "tests/gmp-only/functions.c",68);
+    __gmpq_clear(__gen_e_acsl__15);
+    __gmpq_clear(__gen_e_acsl__16);
   }
   /*@ assert f2(d) > 0; */ ;
   __retres = 0;
@@ -406,7 +417,7 @@ double __gen_e_acsl_f2(double x)
   __e_acsl_mpq_t __gen_e_acsl__13;
   __e_acsl_mpq_t __gen_e_acsl__14;
   __e_acsl_mpq_t __gen_e_acsl_div;
-  double __gen_e_acsl__15;
+  double __gen_e_acsl_cast;
   __gmpq_init(__gen_e_acsl__13);
   __gmpq_set_str(__gen_e_acsl__13,"1",10);
   __gmpq_init(__gen_e_acsl__14);
@@ -415,12 +426,12 @@ double __gen_e_acsl_f2(double x)
   __gmpq_div(__gen_e_acsl_div,
              (__e_acsl_mpq_struct const *)(__gen_e_acsl__13),
              (__e_acsl_mpq_struct const *)(__gen_e_acsl__14));
-  __gen_e_acsl__15 = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
+  __gen_e_acsl_cast = __gmpq_get_d((__e_acsl_mpq_struct const *)(__gen_e_acsl_div));
   __gmpq_clear(__gen_e_acsl__13);
   __gmpq_clear(__gen_e_acsl__14);
   __gmpq_clear(__gen_e_acsl_div);
-  /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl__15); */
-  return __gen_e_acsl__15;
+  /*@ assert Eva: is_nan_or_infinite: \is_finite(__gen_e_acsl_cast); */
+  return __gen_e_acsl_cast;
 }
 
 int __gen_e_acsl_g(int x)