From 29204bfa338453b20bbc12ec0c0d3f0b8ddb3fbd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Feb 2023 14:20:50 +0200 Subject: [PATCH] Fix Node.of_id not handling pseudo returns --- src/framework/cfgTools.ml | 1 + src/util/cilfacade.ml | 6 +++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index a403502830..c4e2b97765 100644 --- 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 index ba06f5890d..be478622cc 100644 --- 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 () =