diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml index a403502830..28ca8fab1b 100644 --- a/src/framework/cfgTools.ml +++ b/src/framework/cfgTools.ml @@ -233,11 +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 diff --git a/src/framework/control.ml b/src/framework/control.ml index 7f5b3040e6..e79c822377 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -98,19 +98,24 @@ struct let live_lines = ref StringMap.empty in let dead_lines = ref StringMap.empty in let add_one n v = - (* Not using Node.location here to have updated locations in incremental analysis. - See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) - let l = UpdateCil.getLoc n in - let f = Node.find_fundec n in - let add_fun = BatISet.add l.line in - let add_file = StringMap.modify_def BatISet.empty f.svar.vname add_fun in - let is_dead = LT.for_all (fun (_,x,f) -> Spec.D.is_bot x) v in - if is_dead then ( - dead_lines := StringMap.modify_def StringMap.empty l.file add_file !dead_lines - ) else ( - live_lines := StringMap.modify_def StringMap.empty l.file add_file !live_lines; - NH.add live_nodes n () - ); + match n with + | Statement s when Cilfacade.(StmtH.mem pseudo_return_to_fun s) -> + (* Exclude pseudo returns from dead lines counting. No user code at "}". *) + () + | _ -> + (* Not using Node.location here to have updated locations in incremental analysis. + See: https://github.com/goblint/analyzer/issues/290#issuecomment-881258091. *) + let l = UpdateCil.getLoc n in + let f = Node.find_fundec n in + let add_fun = BatISet.add l.line in + let add_file = StringMap.modify_def BatISet.empty f.svar.vname add_fun in + let is_dead = LT.for_all (fun (_,x,f) -> Spec.D.is_bot x) v in + if is_dead then ( + dead_lines := StringMap.modify_def StringMap.empty l.file add_file !dead_lines + ) else ( + live_lines := StringMap.modify_def StringMap.empty l.file add_file !live_lines; + NH.add live_nodes n () + ); in Result.iter add_one xs; let live_count = StringMap.fold (fun _ file_lines acc -> 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 () =