fix get_ikind invalid argument error

goblint · Feb 1, 2024 · 34b2667 · 34b2667
1 parent 2e9284d
commit 34b2667
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 19 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -1019,7 +1019,7 @@ struct
     match ofs with
     | NoOffset -> `NoOffset
     | Field (fld, ofs) -> `Field (fld, convert_offset ~ctx st ofs)
-    | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *)
+    | Index (exp, ofs) when CilType.Exp.equal exp (Offset.Index.Exp.any ()) -> (* special offset added by convertToQueryLval *)
       `Index (IdxDom.top (), convert_offset ~ctx st ofs)
     | Index (exp, ofs) ->
       match eval_rv ~ctx st exp with
@@ -2343,7 +2343,7 @@ struct
                | CArrays.IsNotSubstr -> Address (AD.null_ptr)
                | CArrays.IsSubstrAtIndex0 -> Address (eval_lv ~ctx st (mkMem ~addr:(Cil.stripCasts haystack) ~off:NoOffset))
                | CArrays.IsMaybeSubstr -> Address (AD.join (eval_lv ~ctx st
-                                                              (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Offset.Index.Exp.any, NoOffset)))) (AD.null_ptr)))
+                                                              (mkMem ~addr:(Cil.stripCasts haystack) ~off:(Index (Offset.Index.Exp.any (), NoOffset)))) (AD.null_ptr)))
         | None -> st
       end
     | Strcmp { s1; s2; n }, _ ->

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
@@ -171,7 +171,7 @@ struct
       match ofs with
       | NoOffset -> `NoOffset
       | Field (fld, ofs) -> `Field (fld, convert_offset ofs)
-      | Index (exp, ofs) when CilType.Exp.equal exp Offset.Index.Exp.any -> (* special offset added by convertToQueryLval *)
+      | Index (exp, ofs) when CilType.Exp.equal exp (Offset.Index.Exp.any ()) -> (* special offset added by convertToQueryLval *)
         `Index (ID.top (), convert_offset ofs)
       | Index (exp, ofs) ->
         let i = match ctx.ask (Queries.EvalInt exp) with

diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/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 Offset.Index.Exp.all ->
+    | Some ie when CilType.Exp.equal ie (Offset.Index.Exp.all ()) ->
       v
     | _ ->
       join a v
@@ -164,7 +164,7 @@ struct
     match offset with
     (* invariants for all indices *)
     | NoOffset when get_bool "witness.invariant.goblint" ->
-      let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all, NoOffset)) lval in
+      let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all (), NoOffset)) lval in
       value_invariant ~offset ~lval:i_lval x
     | NoOffset ->
       Invariant.none
@@ -246,7 +246,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 Offset.Index.Exp.all ->
+    | Some ie when CilType.Exp.equal ie (Offset.Index.Exp.all ()) ->
       (* TODO: Doesn't seem to work for unassume because unrolled elements are top-initialized, not bot-initialized. *)
       (BatList.make (factor ()) v, v)
     | _ ->
@@ -279,7 +279,7 @@ struct
         if Val.is_bot xr then
           Invariant.top ()
         else if get_bool "witness.invariant.goblint" then (
-          let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all, NoOffset)) lval in
+          let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all (), NoOffset)) lval in
           value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
         )
         else
@@ -534,10 +534,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\n" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a;
     match i with
-    | Some ie when CilType.Exp.equal ie Offset.Index.Exp.all ->
+    | Some ie when CilType.Exp.equal ie (Offset.Index.Exp.all ()) ->
       (* TODO: Doesn't seem to work for unassume. *)
       Joint a
-    | Some i when CilType.Exp.equal i Offset.Index.Exp.any ->
+    | Some i when CilType.Exp.equal i (Offset.Index.Exp.any ()) ->
       (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
@@ -818,7 +818,7 @@ struct
     match offset with
     (* invariants for all indices *)
     | NoOffset when get_bool "witness.invariant.goblint" ->
-      let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all, NoOffset)) lval in
+      let i_lval = Cil.addOffsetLval (Index (Offset.Index.Exp.all (), NoOffset)) lval in
       value_invariant ~offset ~lval:i_lval (join_of_all_parts x)
     | NoOffset ->
       Invariant.none

diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml
@@ -23,11 +23,11 @@ struct
     let name () = "exp index"
 
     let any = Cilfacade.any_index_exp
-    let all = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index")
+    let all () = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index")
 
     (* Override output *)
     let pretty () x =
-      if equal x any then
+      if equal x (any ()) then
         Pretty.text "?"
       else
         dn_exp () x
@@ -41,7 +41,7 @@ struct
 
     let equal_to _ _ = `Top (* TODO: more precise for definite indices *)
     let to_int _ = None (* TODO: more precise for definite indices *)
-    let top () = any
+    let top = any
   end
 end
 
@@ -108,7 +108,7 @@ struct
     | `Index (i,o) ->
       let i_exp = match Idx.to_int i with
         | Some i -> Const (CInt (i, Cilfacade.ptrdiff_ikind (), Some (Z.to_string i)))
-        | None -> Index.Exp.any
+        | None -> Index.Exp.any ()
       in
       `Index (i_exp, to_exp o)
     | `Field (f,o) -> `Field (f, to_exp o)
@@ -118,7 +118,7 @@ struct
     | `Index (i,o) ->
       let i_exp = match Idx.to_int i with
         | Some i -> Const (CInt (i, Cilfacade.ptrdiff_ikind (), Some (Z.to_string i)))
-        | None -> Index.Exp.any
+        | None -> Index.Exp.any ()
       in
       Index (i_exp, to_cil o)
     | `Field (f,o) -> Field (f, to_cil o)

diff --git a/src/cdomain/value/cdomains/offset_intf.ml b/src/cdomain/value/cdomains/offset_intf.ml
@@ -129,12 +129,12 @@ sig
       (** Special index expression for some unknown index.
           Weakly updates array in assignment.
           Used for [exp.fast_global_inits]. *)
-      val any: GoblintCil.exp
+      val any: unit -> GoblintCil.exp
 
       (** Special index expression for all indices.
           Strongly updates array in assignment.
           Used for Goblint-specific witness invariants. *)
-      val all: GoblintCil.exp
+      val all: unit -> GoblintCil.exp
     end
   end
 

diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml
@@ -681,7 +681,7 @@ let getGlobalInits (file: file) : edges  =
       lval
     in
     let rec any_index_offset = function
-      | Index (e,o) -> Index (Cilfacade.any_index_exp, any_index_offset o)
+      | Index (e,o) -> Index (Cilfacade.any_index_exp (), any_index_offset o)
       | Field (f,o) -> Field (f, any_index_offset o)
       | NoOffset -> NoOffset
     in

diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
@@ -716,4 +716,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 = CastE (TInt (ptrdiff_ikind (), []), mkString "any_index") (* TODO: move back to Offset *)
+let any_index_exp () = CastE (TInt (ptrdiff_ikind (), []), mkString "any_index") (* TODO: move back to Offset *)