Fix Node.of_id not handling pseudo returns

goblint · Feb 22, 2023 · 29204bf · 29204bf
1 parent 7f7b9f0
commit 29204bf
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
@@ -236,6 +236,7 @@ let createCFG (file: file) =
           let newst = mkStmt (Return (None, fd_loc)) in
           newst.sid <- 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
           addEdge newst_node (fd_loc, Ret (None, fd)) (Function fd);
           newst_node

diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
@@ -513,9 +513,13 @@ let stmt_sids: stmt IntH.t ResettableLazy.t =
       h
     )
 
+let pseudo_return_stmt_sids: stmt IntH.t = IntH.create 13
+
 (** Find [stmt] by its [sid].
     @raise Not_found *)
-let find_stmt_sid sid = IntH.find (ResettableLazy.force stmt_sids) sid
+let find_stmt_sid sid =
+  try IntH.find pseudo_return_stmt_sids sid
+  with Not_found -> IntH.find (ResettableLazy.force stmt_sids) sid
 
 
 let reset_lazy () =