Merge pull request #790 from Dudeldu/fix-get-ikind-master

Fix `get_ikind` in `eval_rv_ask_mustbeequal` and `is_safe_cast`

Author: michael-schwarz

src/analyses/base.ml

@@ -664,7 +664,7 @@ struct
     in
     let r =
     match exp with
-    | BinOp (op,arg1,arg2,_) -> binop op arg1 arg2
+    | BinOp (op,arg1,arg2,_) when Cil.isIntegralType (Cilfacade.typeOf exp) -> binop op arg1 arg2
     | _ -> eval_next ()
     in
     if M.tracing then M.traceu "evalint" "base eval_rv_ask_mustbeequal %a -> %a\n" d_exp exp VD.pretty r;

src/cdomains/valueDomain.ml

@@ -259,8 +259,9 @@ struct
     | TInt (ik,_), TFloat (fk,_) (* does a1 fit into ik's range? *)
     | TFloat (fk,_), TInt (ik,_) (* can a1 be represented as fk? *)
       -> false (* TODO precision *)
-    | _ -> IntDomain.Size.is_cast_injective ~from_type:t1 ~to_type:t2 && bitsSizeOf t2 >= bitsSizeOf t1
-  (*| _ -> false*)
+    | (TInt _ | TEnum _ | TPtr _) , (TInt _ | TEnum _ | TPtr _) ->
+      IntDomain.Size.is_cast_injective ~from_type:t1 ~to_type:t2 && bitsSizeOf t2 >= bitsSizeOf t1
+    | _ -> false
 
   let ptr_ikind () = match !upointType with TInt (ik,_) -> ik | _ -> assert false