[typing] fix crash with casts from non-integral terms to integral-types

src/plugins/e-acsl/doc/Changelog

@@ -15,6 +15,8 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2017/02/24] Fix crash with casts from non-integral terms to
+	        integral types (bts #2284).
 -* E-ACSL       [2017/02/17] Fix bug with goto which points to a labeled
 	        statement which must be instrumented.
 -* E-ACSL       [2017/01/23] Fix bug #2252 about pointer arithmetic with

src/plugins/e-acsl/interval.ml

@@ -135,9 +135,22 @@ let rec infer t =
     Ival.bitwise_or i1 i2
   | TCastE (ty, t)
   | TCoerce (t, ty) ->
-    let it = infer t in
-    let ity = interv_of_typ ty in
-    Ival.meet it ity
+    (try
+       let it = infer t in
+       let ity = interv_of_typ ty in
+       Ival.meet it ity
+     with Not_an_integer ->
+       if Cil.isIntegralType ty then begin
+         (* heterogeneous cast from a non-integral term to an integral type:
+            consider that one eventually gets an integral type even if it is
+            not sure. *)
+         Options.warning
+           ~once:true "possibly unsafe cast from term '%a' to typ '%a'."
+           Printer.pp_term t
+           Printer.pp_typ ty;
+         interv_of_typ ty
+       end else
+         raise Not_an_integer)
   | Tif (_, t2, t3) ->
     let i2 = infer t2 in
     let i3 = infer t3 in

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

@@ -12,11 +12,15 @@ int main(void) {
 
   /*@ assert y == (int)0; */ ; // cast from integer to int
   /*@ assert (unsigned int) y == (unsigned int)0; */ ; /* cast from integer
-  						          to unsigned int */
+                                                          to unsigned int */
 
   /*@ assert y != (int)0xfffffffffffffff; */ ; // cast from integer to int
   /*@ assert (unsigned int) y != (unsigned int)0xfffffffffffffff; */ ;
   /* cast from integer to unsigned int */
 
+  /* heterogeneous casts from/to integers */
+  int t[2] = { 0, 1 };
+  /*@ assert (float)x == t[(int)0.1]; */
+
   return 0;
 }

src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle

 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] warning: possibly unsafe cast from term '0.1' to typ 'int'.
+tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -15,4 +17,5 @@ FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns cl
   __e_acsl_internal_heap ∈ [--..--]
   __e_acsl_heap_allocation_size ∈ [--..--]
 [value] using specification for function __e_acsl_assert
+[value] user error: type long double not implemented. Using double instead
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle

 [e-acsl] beginning translation.
 FRAMAC_SHARE/libc/stdlib.h:277:[kernel] warning: No code nor implicit assigns clause for function calloc, generating default assigns from the prototype
+[e-acsl] warning: possibly unsafe cast from term '0.1' to typ 'int'.
+tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -22,4 +24,7 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: preco
 [value] using specification for function __gmpz_clear
 [value] using specification for function __gmpz_get_ui
 [value] using specification for function __gmpz_init_set_ui
+[value] user error: type long double not implemented. Using double instead
+tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert 0 ≤ __gen_e_acsl_cast_9;
+tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert __gen_e_acsl_cast_9 < 2;
 [value] done for function main