Fix stmt_fundecs for CFG comparison

goblint · Dec 1, 2022 · 7527ff5 · 7527ff5
1 parent 494db8e
commit 7527ff5
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 1 deletion.
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
@@ -607,7 +607,22 @@ let getCFG (file: file) : cfg * cfg =
       cfgs
   in
   if get_bool "justcfg" then fprint_hash_dot cfgs;
-  (fun n -> H.find_default (fst @@ FH.find cfgs (Node.find_fundec n)) n []), (fun n -> H.find_default (snd @@ FH.find cfgs (Node.find_fundec n)) n [])
+  (* Inlined here to get non-shared stmt_fundecs for CFG comparison,
+     where two CFGs exist simultaneously. *)
+  (* TODO: add fundec to Statement node *)
+  ResettableLazy.reset Cilfacade.stmt_fundecs;
+  let stmt_fundecs = ResettableLazy.force Cilfacade.stmt_fundecs in
+  let find_stmt_fundec stmt =
+    try Cilfacade.StmtH.find Cilfacade.pseudo_return_to_fun stmt
+    with Not_found -> Cilfacade.StmtH.find stmt_fundecs stmt (* stmt argument must be explicit, otherwise force happens immediately *)
+  in
+  let find_fundec node =
+    match node with
+    | Statement stmt -> find_stmt_fundec stmt
+    | Function fd -> fd
+    | FunctionEntry fd -> fd
+  in
+  (fun n -> H.find_default (fst @@ FH.find cfgs (find_fundec n)) n []), (fun n -> H.find_default (snd @@ FH.find cfgs (find_fundec n)) n [])
 
 
 let iter_fd_edges (module Cfg : CfgBackward) fd =

diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
@@ -130,6 +130,8 @@ let compareCilFiles ?(eq=eq_glob) (oldAST: file) (newAST: file) =
     then Some (CfgTools.getCFG oldAST |> fst, CfgTools.getCFG newAST)
     else None in
 
+  ResettableLazy.reset Cilfacade.stmt_fundecs; (* reset due to getCFG *)
+
   let addGlobal map global  =
     try
       let name, col = match global with