Classify all castkinds in Goblint

Author: sim642

src/analyses/base.ml

@@ -2368,7 +2368,8 @@ struct
                     |> AD.type_of in
       (* when src and destination type coincide, take value from the source, otherwise use top *)
       let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then
-          let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~kind:None ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
+          (* TODO: why cast if types coincide? *)
+          let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~kind:Internal ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
           eval_rv ~man st (Lval src_cast_lval)
         else
           VD.top_value (unrollType dest_typ)

src/cdomain/value/cdomains/intDomain0.ml

@@ -161,7 +161,7 @@ struct
   let name () = "IntDomLifter(" ^ (I.name ()) ^ ")"
   let to_yojson x = I.to_yojson x.v
   let invariant e x =
-    let e' = Cilfacade.mkCast ~kind:None ~e ~newt:(TInt (x.ikind, [])) in
+    let e' = Cilfacade.mkCast ~kind:Explicit ~e ~newt:(TInt (x.ikind, [])) in
     I.invariant_ikind e' x.ikind x.v
   let tag x = I.tag x.v
   let arbitrary ik = failwith @@ "Arbitrary not implement for " ^ (name ()) ^ "."

src/cdomain/value/cdomains/offset.ml

@@ -27,7 +27,7 @@ struct
       | CastE (_, TInt (ik, []), Const (CStr ("any_index", No_encoding))) when CilType.Ikind.equal ik (Cilfacade.ptrdiff_ikind ()) -> true
       | _ -> false
 
-    let all = lazy (CastE (Internal, TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index"))
+    let all = lazy (CastE (Explicit, TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index"))
     let is_all = function
       | CastE (_, TInt (ik, []), Const (CStr ("all_index", No_encoding))) when CilType.Ikind.equal ik (Cilfacade.ptrdiff_ikind ()) -> true
       | _ -> false

src/cdomain/value/cdomains/valueDomain.ml

@@ -1361,7 +1361,7 @@ struct
           let offset = Addr.Offs.to_cil offs in
 
           let cast_to_void_ptr e =
-            Cilfacade.mkCast ~kind:None ~e ~newt:(TPtr (TVoid [], []))
+            Cilfacade.mkCast ~kind:Explicit ~e ~newt:(TPtr (TVoid [], []))
           in
           let i =
             if InvariantCil.(exp_is_suitable ~scope c_exp && var_is_suitable ~scope vi && not (var_is_heap vi)) then
@@ -1384,7 +1384,7 @@ struct
               (* Address set for a void* variable contains pointers to values of non-void type,
                   so insert pointer cast to make invariant expression valid (no field/index on void). *)
               let newt = TPtr (typ, []) in
-              let c_exp = Cilfacade.mkCast ~kind:None ~e:c_exp ~newt in
+              let c_exp = Cilfacade.mkCast ~kind:Explicit ~e:c_exp ~newt in
               deref_invariant ~vs vi ~offset ~lval:(Mem c_exp, NoOffset)
             | exception Cilfacade.TypeOfError _ (* typeOffset: Index on a non-array on calloc-ed alloc variables *)
             | _ ->

src/cdomains/apron/sharedFunctions.apron.ml

@@ -300,7 +300,7 @@ struct
   let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =
     match V.to_cil_varinfo v with
     | Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[]))   ->
-      let var = Cilfacade.mkCast ~kind:None ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
+      let var = Cilfacade.mkCast ~kind:Explicit ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
       let i = int_of_coeff_warn ~scalewith c in
       if Z.equal i Z.one then
         false, var

src/cdomains/unionFind.ml

@@ -463,7 +463,7 @@ module T = struct
           | _ ->
             let void_ptr_type = TPtr(TVoid [], []) in
             let offset_plus_exp =  to_cil_sum offset exp in
-            Lval (Mem (CastE (Internal, void_ptr_type, offset_plus_exp)), NoOffset)
+            Lval (Mem (CastE (Internal, void_ptr_type, offset_plus_exp)), NoOffset) (* TODO: how can void* be dereferenced? *)
       in
       if check_valid_pointer res then
         res

src/common/util/cilfacade.ml

@@ -424,7 +424,6 @@ let mkCast ~kind ~(e: exp) ~(newt: typ) =
     with TypeOfError _ -> (* e might involve alloc variables, weird offsets, etc *)
       Cil.voidType (* oldt is only used for avoiding duplicate cast, so this falls back to adding cast *)
   in
-  let kind = Option.value kind ~default:Internal in
   Cil.mkCastT ~kind ~e ~oldt ~newt
 
 (** @raise TypeOfError
@@ -806,4 +805,4 @@ let add_function_declarations (file: Cil.file): unit =
 (** Special index expression for some unknown index.
     Weakly updates array in assignment.
     Used for [exp.fast_global_inits]. *)
-let any_index_exp = lazy (CastE (Internal, TInt (ptrdiff_ikind (), []), mkString "any_index")) (* TODO: move back to Offset *)
+let any_index_exp = lazy (CastE (Explicit, TInt (ptrdiff_ikind (), []), mkString "any_index")) (* TODO: move back to Offset *)