Add cast kinds in CIL

goblint.opam

@@ -101,7 +101,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#6360600542d9c297b87e41db92991209f52f5176" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

goblint.opam.locked

@@ -147,7 +147,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.9"
-    "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e"
+    "git+https://github.com/goblint/cil.git#6360600542d9c297b87e41db92991209f52f5176"
   ]
   [
     "apron.v0.9.15"

goblint.opam.template

@@ -3,7 +3,7 @@
 x-maintenance-intent: ["(latest)" "(latest).(latest-1)"] # also keep previous minor version (with two releases per year, always keep a SV-COMP release)
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#1b48fc0ce4f3576a51618305251121ffedd0bf1e" ]
+  [ "goblint-cil.2.0.9" "git+https://github.com/goblint/cil.git#6360600542d9c297b87e41db92991209f52f5176" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release
   [ "apron.v0.9.15" "git+https://github.com/antoinemine/apron.git#418a217c7a70dae3f422678f3aaba38ae374d91a" ]
 ]

src/analyses/apron/relationAnalysis.apron.ml

@@ -216,7 +216,7 @@ struct
       | Const x -> e
       | UnOp (unop, e, typ) -> UnOp(unop, inner e, typ)
       | BinOp (binop, e1, e2, typ) -> BinOp (binop, inner e1, inner e2, typ)
-      | CastE (t,e) -> CastE (t, inner e)
+      | CastE (k,t,e) -> CastE (k, t, inner e)
       | Lval (Var v, off) -> Lval (Var v, off)
       | Lval (Mem e, NoOffset) ->
         begin match ask (Queries.MayPointTo e) with

src/analyses/base.ml

@@ -819,7 +819,7 @@ struct
         eval_rv_base_lval ~eval_lv ~man st exp lv
       (* Binary operators *)
       (* Eq/Ne when both values are equal and casted to the same type *)
-      | BinOp ((Eq | Ne) as op, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
+      | BinOp ((Eq | Ne) as op, (CastE (_, t1, e1) as c1), (CastE (_, t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
         let a1 = eval_rv ~man st e1 in
         let a2 = eval_rv ~man st e2 in
         let extra_is_safe =
@@ -836,7 +836,7 @@ struct
         (* split nested LOr Eqs to equality pairs, if possible *)
         let rec split = function
           (* copied from above to support pointer equalities with implicit casts inserted *)
-          | BinOp (Eq, (CastE (t1, e1) as c1), (CastE (t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
+          | BinOp (Eq, (CastE (_, t1, e1) as c1), (CastE (_, t2, e2) as c2), typ) when typeSig t1 = typeSig t2 ->
             Some [binop_remove_same_casts ~extra_is_safe:false ~e1 ~e2 ~t1 ~t2 ~c1 ~c2]
           | BinOp (Eq, arg1, arg2, _) ->
             Some [(arg1, arg2)]
@@ -921,8 +921,8 @@ struct
         let array_ofs = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in
         let array_start = add_offset_varinfo array_ofs in
         Address (AD.map array_start (eval_lv ~man st lval))
-      | CastE (t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
-      | CastE  (t, exp) ->
+      | CastE (_, t, Const (CStr (x,e))) -> (* VD.top () *) eval_rv ~man st (Const (CStr (x,e))) (* TODO safe? *)
+      | CastE (_, t, exp) ->
         (let v = eval_rv ~man st exp in
          try
            VD.cast ~torg:(Cilfacade.typeOf exp) t v
@@ -1066,7 +1066,7 @@ struct
     match ofs with
     | NoOffset -> `NoOffset
     | Field (fld, ofs) -> `Field (fld, convert_offset ~man st ofs)
-    | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
+    | Index (exp, ofs) when Offset.Index.Exp.is_any exp -> (* special offset added by convertToQueryLval *)
       `Index (IdxDom.top (), convert_offset ~man st ofs)
     | Index (exp, ofs) ->
       match eval_rv ~man st exp with
@@ -1383,7 +1383,7 @@ struct
         | Imag e
         | SizeOfE e
         | AlignOfE e
-        | CastE (_, e) -> exp_may_signed_overflow man e
+        | CastE (_, _, e) -> exp_may_signed_overflow man e
         | UnOp (unop, e, _) ->
           (* check if the current operation causes a signed overflow *)
           begin match unop with
@@ -2368,7 +2368,7 @@ 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 ~e:src ~newt:(TPtr (dest_typ, []))) ~off:NoOffset in
+          let src_cast_lval = mkMem ~addr:(Cilfacade.mkCast ~kind:Unknown ~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/analyses/baseInvariant.ml

@@ -245,9 +245,9 @@ struct
         else
           `NotUnderstood
       | BinOp(op, rval, Lval x, typ) -> derived_invariant (BinOp(switchedOp op, Lval x, rval, typ)) tv
-      | BinOp(op, CastE (t1, c1), CastE (t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
+      | BinOp(op, CastE (_, t1, c1), CastE (_, t2, c2), t) when (op = Eq || op = Ne) && typeSig t1 = typeSig t2 && VD.is_statically_safe_cast t1 (Cilfacade.typeOf c1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf c2)
         -> derived_invariant (BinOp (op, c1, c2, t)) tv
-      | BinOp(op, CastE (t1, Lval x), rval, typ) when Cil.isIntegralType t1 ->
+      | BinOp(op, CastE (_, t1, Lval x), rval, typ) when Cil.isIntegralType t1 ->
         begin match eval_rv ~man st (Lval x) with
           | Int v ->
             if VD.is_dynamically_safe_cast t1 (Cilfacade.typeOfLval x) (Int v) then
@@ -256,8 +256,8 @@ struct
               `NotUnderstood
           | _ -> `NotUnderstood
         end
-      | BinOp(op, rval, CastE (ti, Lval x), typ) when Cil.isIntegralType ti ->
-        derived_invariant (BinOp (switchedOp op, CastE(ti, Lval x), rval, typ)) tv
+      | BinOp(op, rval, CastE (k, ti, Lval x), typ) when Cil.isIntegralType ti ->
+        derived_invariant (BinOp (switchedOp op, CastE(k, ti, Lval x), rval, typ)) tv
       | BinOp(op, (Const _ | AddrOf _), rval, typ) ->
         (* This is last such that we never reach here with rval being Lval (it is swapped around). *)
         `NothingToRefine
@@ -647,15 +647,15 @@ struct
         | UnOp (Neg, e, _), Float c -> inv_exp (unop_FD Neg c) e st
         | UnOp ((BNot|Neg) as op, e, _), Int c -> inv_exp (Int (unop_ID op c)) e st
         (* no equivalent for Float, as VD.is_statically_safe_cast fails for all float types anyways *)
-        | BinOp((Eq | Ne) as op, CastE (t1, e1), CastE (t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) ->
+        | BinOp((Eq | Ne) as op, CastE (_, t1, e1), CastE (_, t2, e2), t), Int c when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) ->
           inv_exp (Int c) (BinOp (op, e1, e2, t)) st
         | BinOp (LOr, arg1, arg2, typ) as exp, Int c ->
           (* copied & modified from eval_rv_base... *)
           let (let*) = Option.bind in
           (* split nested LOr Eqs to equality pairs, if possible *)
           let rec split = function
             (* copied from above to support pointer equalities with implicit casts inserted *)
-            | BinOp (Eq, CastE (t1, e1), CastE (t2, e2), typ) when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) -> (* slightly different from eval_rv_base... *)
+            | BinOp (Eq, CastE (_, t1, e1), CastE (_, t2, e2), typ) when typeSig (Cilfacade.typeOf e1) = typeSig (Cilfacade.typeOf e2) && VD.is_statically_safe_cast t1 (Cilfacade.typeOf e1) && VD.is_statically_safe_cast t2 (Cilfacade.typeOf e2) -> (* slightly different from eval_rv_base... *)
               Some [(e1, e2)]
             | BinOp (Eq, arg1, arg2, _) ->
               Some [(arg1, arg2)]
@@ -833,7 +833,7 @@ struct
             | _ -> assert false
           end
         | Const _ , _ -> st (* nothing to do *)
-        | CastE (t, e), c_typed ->
+        | CastE (k, t, e), c_typed ->
           begin match Cil.unrollType t, c_typed with
             | TFloat (_, _), Float c ->
               (match unrollType (Cilfacade.typeOf e), FD.get_fkind c with
@@ -862,7 +862,7 @@ struct
                       fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st
                   | x -> fallback (fun () -> Pretty.dprintf "CastE: e did evaluate to Int, but the type did not match %a" CilType.Typ.pretty t) st)
                | v -> fallback (fun () -> Pretty.dprintf "CastE: e did not evaluate to Int, but %a" VD.pretty v) st)
-            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (t, e))) st
+            | _, _ -> fallback (fun () -> Pretty.dprintf "CastE: %a not implemented" d_plainexp (CastE (k, t, e))) st
           end
         | e, _ -> fallback (fun () -> Pretty.dprintf "%a not implemented" d_plainexp e) st
     in

src/analyses/condVars.ml

@@ -18,7 +18,7 @@ module Domain = struct
   and var_in_expr p = function
     | Const _ | SizeOf _ | SizeOfStr _ | AlignOf _ -> true
     | Lval l | AddrOf l | StartOf l -> var_in_lval p l
-    | SizeOfE e | AlignOfE e | UnOp (_,e,_) | CastE (_,e) | Imag e | Real e -> var_in_expr p e
+    | SizeOfE e | AlignOfE e | UnOp (_,e,_) | CastE (_,_,e) | Imag e | Real e -> var_in_expr p e
     | BinOp (_,e1,e2,_) -> var_in_expr p e1 && var_in_expr p e2
     | Question (c,t,e,_) -> var_in_expr p c && var_in_expr p t && var_in_expr p e
     | AddrOfLabel _ -> true

src/analyses/malloc_null.ml

@@ -70,7 +70,7 @@ struct
 
   let get_concrete_exp (exp:exp) gl (st:D.t) =
     match constFold true exp with
-    | CastE (_,Lval (Var v, offs))
+    | CastE (_,_,Lval (Var v, offs))
     | Lval (Var v, offs) -> Some (Var v,offs)
     | _ -> None
 

src/analyses/memOutOfBounds.ml

@@ -46,7 +46,7 @@ struct
     | SizeOfE e
     | AlignOfE e
     | UnOp (_, e, _)
-    | CastE (_, e) -> exp_contains_a_ptr e
+    | CastE (_, _, e) -> exp_contains_a_ptr e
     | BinOp (_, e1, e2, _) ->
       exp_contains_a_ptr e1 || exp_contains_a_ptr e2
     | Question (e1, e2, e3, _) ->
@@ -170,7 +170,7 @@ struct
       match ofs with
       | NoOffset -> `NoOffset
       | Field (fld, ofs) -> `Field (fld, convert_offset ofs)
-      | Index (exp, ofs) when CilType.Exp.equal exp (Lazy.force Offset.Index.Exp.any) -> (* special offset added by convertToQueryLval *)
+      | Index (exp, ofs) when Offset.Index.Exp.is_any exp -> (* special offset added by convertToQueryLval *)
         `Index (ID.top (), convert_offset ofs)
       | Index (exp, ofs) ->
         let i = match man.ask (Queries.EvalInt exp) with
@@ -352,7 +352,7 @@ struct
     | SizeOfE e
     | AlignOfE e
     | UnOp (_, e, _)
-    | CastE (_, e) -> check_exp_for_oob_access man ~is_implicitly_derefed e
+    | CastE (_, _, e) -> check_exp_for_oob_access man ~is_implicitly_derefed e
     | BinOp (bop, e1, e2, t) ->
       check_exp_for_oob_access man ~is_implicitly_derefed e1;
       check_exp_for_oob_access man ~is_implicitly_derefed e2

src/analyses/tutorials/taint.ml

@@ -45,7 +45,7 @@ struct
     | Imag e
     | SizeOfE e
     | AlignOfE e
-    | CastE (_,e)
+    | CastE (_,_,e)
     | UnOp (_,e,_) -> is_exp_tainted state e
     | SizeOf _ | SizeOfStr _ | Const _  | AlignOf _ | AddrOfLabel _ -> false
     | Question (b, t, f, _) -> is_exp_tainted state b || is_exp_tainted state t || is_exp_tainted state f

src/analyses/uninit.ml

@@ -65,7 +65,7 @@ struct
     | AddrOf lval -> access_lv_byval a lval
     | StartOf lval -> access_lv_byval a lval
     (* Most casts are currently just ignored, that's probably not a good idea! *)
-    | CastE  (t, exp) -> access_one_byval a rw exp
+    | CastE  (_, t, exp) -> access_one_byval a rw exp
     | Question (b, t, f, _) ->
       access_one_byval a rw b @ access_one_byval a rw t @ access_one_byval a rw f
   (* Accesses during the evaluation of an lval, not the lval itself! *)

src/analyses/varEq.ml

@@ -20,7 +20,7 @@ struct
     (* TODO: Should string constants not be added to D in the first place, rather than filtering them for witness invariants? *)
     let rec is_str_constant = function
       | Const (CStr _ | CWStr _) -> true
-      | CastE (_, e) -> is_str_constant e
+      | CastE (_, _, e) -> is_str_constant e
       | _ -> false
 
     let invariant ~scope ss =
@@ -97,7 +97,7 @@ struct
     | AddrOf  (Mem e,_)
     | StartOf (Mem e,_)
     | Lval    (Mem e,_)
-    | CastE (_,e)           -> interesting e
+    | CastE (_,_,e)           -> interesting e
 
   (* helper to decide equality *)
   let query_exp_equal ask e1 e2 g s =
@@ -138,7 +138,7 @@ struct
       | Lval (Mem e,o)
       | AddrOf (Mem e,o)
       | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t e bt
-      | CastE (t,e) -> type_may_change_t e bt
+      | CastE (_,t,e) -> type_may_change_t e bt
       | Question (b, t, f, _) -> type_may_change_t b bt || type_may_change_t t bt || type_may_change_t f bt
     in
     let bt =  unrollTypeDeep (Cilfacade.typeOf b) in
@@ -174,7 +174,7 @@ struct
       | Lval (Mem e,o)
       | AddrOf (Mem e,o)
       | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
-      | CastE (t,e) -> lval_may_change_pt e bl
+      | CastE (_,t,e) -> lval_may_change_pt e bl
       | Question (b, t, f, _) -> lval_may_change_pt t bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let bls = pt b in
@@ -235,7 +235,7 @@ struct
       | Lval (Mem e,o)    -> may_change_t_offset o || type_may_change_t true e
       | AddrOf (Mem e,o)  -> may_change_t_offset o || type_may_change_t false e
       | StartOf (Mem e,o) -> may_change_t_offset o || type_may_change_t false e
-      | CastE (t,e) -> type_may_change_t deref e
+      | CastE (_,t,e) -> type_may_change_t deref e
       | Question (b, t, f, _) -> type_may_change_t deref b || type_may_change_t deref t || type_may_change_t deref f
 
     and lval_may_change_pt a bl : bool =
@@ -253,7 +253,7 @@ struct
         | Lval    (Mem e,o) -> Some (AddrOf (Mem e, o))
         | AddrOf  (Mem e,o) -> (match addrOfExp e with Some e -> Some (AddrOf (Mem e, o)) | x -> x)
         | StartOf (Mem e,o) -> (match addrOfExp e with Some e -> Some (AddrOf (Mem e, o)) | x -> x)
-        | CastE   (t,e) -> addrOfExp e
+        | CastE   (_,t,e) -> addrOfExp e
         | _ -> None
       in
       let lval_is_not_disjoint (v,o) aad =
@@ -299,7 +299,7 @@ struct
            | Lval (Mem e,o)
            | AddrOf (Mem e,o)
            | StartOf (Mem e,o) -> may_change_pt_offset o || lval_may_change_pt e bl
-           | CastE (t,e) -> lval_may_change_pt e bl
+           | CastE (_,t,e) -> lval_may_change_pt e bl
            | Question (b, t, f, _) -> lval_may_change_pt b bl || lval_may_change_pt t bl || lval_may_change_pt f bl
     in
     let r =
@@ -361,7 +361,7 @@ struct
             ) ad)
         | _ -> Some true
       end
-    | CastE (t,e) -> is_global_var ask e
+    | CastE (_,t,e) -> is_global_var ask e
     | AddrOf (Var v,_) -> Some (ask.f (Queries.IsMultiple v)) (* Taking an address of a global is fine*)
     | AddrOf lv -> Some false (* TODO: sound?! *)
     | StartOf (Var v,_) ->  Some (ask.f (Queries.IsMultiple v)) (* Taking an address of a global is fine*)
@@ -545,7 +545,7 @@ struct
     | Some es ->
       let et = Cilfacade.typeOf e in
       let add x xs =
-        Queries.ES.add (CastE (et,x)) xs
+        Queries.ES.add (CastE (Unknown,et,x)) xs
       in
       D.B.fold add es (Queries.ES.empty ())
 
@@ -557,7 +557,7 @@ struct
         (* TODO: this applies eq_set_clos under the offset, unlike cases below; should generalize? *)
         Queries.ES.fold (fun e acc -> (* filter_map *)
             match e with
-            | CastE (_, StartOf a') -> (* eq_set adds casts *)
+            | CastE (_, _, StartOf a') -> (* eq_set adds casts *)
               let e' = AddrOf (Cil.addOffsetLval (Index (i, os)) a') in (* TODO: re-add cast? *)
               Queries.ES.add e' acc
             | _ -> acc
@@ -583,8 +583,8 @@ struct
         Queries.ES.map (fun e -> mkAddrOrStartOf (mkMem ~addr:e ~off:ofs)) (eq_set_clos e s)
       | Lval    (Mem e,ofs) ->
         Queries.ES.map (fun e -> Lval (mkMem ~addr:e ~off:ofs)) (eq_set_clos e s)
-      | CastE (t,e) ->
-        Queries.ES.map (fun e -> CastE (t,e)) (eq_set_clos e s)
+      | CastE (k,t,e) ->
+        Queries.ES.map (fun e -> CastE (k,t,e)) (eq_set_clos e s)
     in
     if M.tracing then M.traceu "var_eq" "eq_set_clos %a = %a" d_plainexp e Queries.ES.pretty r;
     r

src/autoTune.ml

@@ -342,7 +342,7 @@ let isComparison = function
 
 let rec extractVar = function
   | UnOp (Neg, e, _)
-  | CastE (_, e) -> extractVar e
+  | CastE (_, _, e) -> extractVar e
   | Lval ((Var info),_) when OctagonTracked.varinfo_tracked info -> Some info
   | _ -> None
 

src/cdomain/value/cdomains/arrayDomain.ml

@@ -140,7 +140,7 @@ struct
   let get ?(checkBounds=true) (ask: VDQ.t) a i = a
   let set (ask: VDQ.t) a (ie, i) v =
     match ie with
-    | Some ie when CilType.Exp.equal ie (Lazy.force Offset.Index.Exp.all) ->
+    | Some ie when Offset.Index.Exp.is_all ie ->
       v
     | _ ->
       join a v
@@ -243,7 +243,7 @@ struct
     else ((update_unrolled_values min_i (Z.of_int ((factor ())-1))), (Val.join xr v))
   let set ask (xl, xr) (ie, i) v =
     match ie with
-    | Some ie when CilType.Exp.equal ie (Lazy.force Offset.Index.Exp.all) ->
+    | Some ie when Offset.Index.Exp.is_all ie ->
       (* TODO: Doesn't seem to work for unassume because unrolled elements are top-initialized, not bot-initialized. *)
       (BatList.make (factor ()) v, v)
     | _ ->
@@ -440,7 +440,7 @@ struct
       |	AlignOfE _ -> false
       | Question(e1, e2, e3, _) ->
         contains_array_access e1 || contains_array_access e2 || contains_array_access e3
-      |	CastE(_, e)
+      |	CastE(_, _, e)
       |	UnOp(_, e , _)
       | Real e
       | Imag e -> contains_array_access e
@@ -525,10 +525,10 @@ struct
   let set_with_length length (ask:VDQ.t) x (i,_) a =
     if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
     match i with
-    | Some i when CilType.Exp.equal i (Lazy.force Offset.Index.Exp.all) ->
+    | Some i when Offset.Index.Exp.is_all i ->
       (* TODO: Doesn't seem to work for unassume. *)
       Joint a
-    | Some i when CilType.Exp.equal i (Lazy.force Offset.Index.Exp.any) ->
+    | Some i when Offset.Index.Exp.is_any i ->
       (assert !AnalysisState.global_initialization; (* just joining with xm here assumes that all values will be set, which is guaranteed during inits *)
        (* the join is needed here! see e.g 30/04 *)
        let o = match x with Partitioned (_, (_, xm, _)) -> xm | Joint v -> v in

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 ~e ~newt:(TInt (x.ikind, [])) in
+    let e' = Cilfacade.mkCast ~kind:Unknown ~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 ()) ^ "."