diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 929dce6c25..0fb9bd32b5 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -531,6 +531,12 @@ let stmt_fundecs: fundec StmtH.t ResettableLazy.t = h ) + +let get_pseudo_return_id fd = + let start_id = 10_000_000_000 in (* TODO get max_sid? *) + let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *) + if sid < start_id then sid + start_id else sid + let pseudo_return_to_fun = StmtH.create 113 (** Find [fundec] which the [stmt] is in. *) diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index af887da432..1afdb69514 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -122,10 +122,6 @@ let rec pretty_edges () = function | [_,x] -> Edge.pretty_plain () x | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs -let get_pseudo_return_id fd = - let start_id = 10_000_000_000 in (* TODO get max_sid? *) - let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *) - if sid < start_id then sid + start_id else sid let node_scc_global = NH.create 113 @@ -260,7 +256,7 @@ let createCFG (file: file) = if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname; let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in let newst = mkStmt (Return (None, fd_end_loc)) in - newst.sid <- get_pseudo_return_id fd; + newst.sid <- Cilfacade.get_pseudo_return_id fd; Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd; Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst; let newst_node = Statement newst in diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index bdb4370b39..77d3a38186 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -1004,7 +1004,7 @@ struct let dummy_pseudo_return_node f = (* not the same as in CFG, but compares equal because of sid *) - Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f}) + Node.Statement ({Cil.dummyStmt with sid = Cilfacade.get_pseudo_return_id f}) in let add_nodes_of_fun (functions: fundec list) (withEntry: fundec -> bool) = let add_stmts (f: fundec) = diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml index 225cbb1c76..55b3fa8fc5 100644 --- a/src/incremental/compareCFG.ml +++ b/src/incremental/compareCFG.ml @@ -17,7 +17,7 @@ let (&&<>) (prev_result: bool * rename_mapping) f : bool * rename_mapping = let eq_node (x, fun1) (y, fun2) ~rename_mapping = let isPseudoReturn f sid = - let pid = CfgTools.get_pseudo_return_id f in + let pid = Cilfacade.get_pseudo_return_id f in sid == pid in match x,y with | Statement s1, Statement s2 ->