Fix get_ikind in eval_rv_ask_mustbeequal and is_safe_cast

goblint · Jul 21, 2022 · b12015a · b12015a
1 parent 4f57a8d
commit b12015a
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/src/analyses/base.ml b/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;

diff --git a/src/cdomains/valueDomain.ml b/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