Remove CfgTools dependency on IntDomain via Offset

goblint · Dec 6, 2023 · 036a016 · 036a016
1 parent b5f6272
commit 036a016
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 3 deletions.
diff --git a/src/cdomains/offset.ml b/src/cdomains/offset.ml
@@ -22,7 +22,7 @@ struct
     include CilType.Exp
     let name () = "exp index"
 
-    let any = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "any_index")
+    let any = Cilfacade.any_index_exp
     let all = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index")
 
     (* Override output *)

diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
@@ -706,4 +706,10 @@ let add_function_declarations (file: Cil.file): unit =
   in
   let fun_decls = List.filter_map declaration_from_GFun functions in
   let globals = upto_last_type @ fun_decls @ non_types @ functions in
-  file.globals <- globals
+  file.globals <- globals
+
+
+(** 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")
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
@@ -685,7 +685,7 @@ let getGlobalInits (file: file) : edges  =
       lval
     in
     let rec any_index_offset = function
-      | Index (e,o) -> Index (Offset.Index.Exp.any, 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