Use function end location for pseudo return node

goblint · Feb 22, 2023 · 30a2cff · 30a2cff
1 parent 29204bf
commit 30a2cff
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
@@ -233,12 +233,13 @@ let createCFG (file: file) =
          * lazy, so it's only added when actually needed *)
         let pseudo_return = lazy (
           if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname;
-          let newst = mkStmt (Return (None, fd_loc)) in
+          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;
           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);
+          addEdge newst_node (fd_end_loc, Ret (None, fd)) (Function fd);
           newst_node
         )
         in