diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index b74cdcf348..72c646a6af 100644 --- 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 index a96a65e004..713ea62660 100644 --- 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