From 036a016d3f1f219fc360fb5ba48e46bfc6f45364 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 6 Dec 2023 17:33:13 +0200 Subject: [PATCH] Remove CfgTools dependency on IntDomain via Offset --- src/cdomains/offset.ml | 2 +- src/common/util/cilfacade.ml | 8 +++++++- src/framework/cfgTools.ml | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/cdomains/offset.ml b/src/cdomains/offset.ml index eca85e08a4..52cfe9eb41 100644 --- 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 index 26a2f082a4..929dce6c25 100644 --- 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 \ No newline at end of file + 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 index 8f98a48e84..af887da432 100644 --- 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