Skip to content

Commit

Permalink
[absint] do not fail when not finding a pre
Browse files Browse the repository at this point in the history
Summary: This code sometimes fails when there are unreachable nodes in the CFG. This diff should stop the failures while we investigate why this happens.

Reviewed By: davidpichardie

Differential Revision: D63024067

fbshipit-source-id: 58ba81d2f4c9f67956b4382771a641b66509859c
  • Loading branch information
ngorogiannis authored and facebook-github-bot committed Sep 19, 2024
1 parent a33e1f1 commit 2613563
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion infer/src/absint/AbstractInterpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -815,7 +815,9 @@ module MakeWTONode (TransferFunctions : NodeTransferFunctions) = struct
| Some astate_pre ->
exec_node ~pp_instr proc_data node ~is_loop_head ~is_narrowing astate_pre inv_map
| None ->
L.(die InternalError) "Could not compute the pre of a node"
L.internal_error "Could not compute the pre of a node in %a\@n" Procname.pp
(Procdesc.Node.get_proc_name (Node.underlying_node node)) ;
(inv_map, DidNotReachFixPoint)


(* [WidenThenNarrow] mode is to narrow the outermost loops eagerly, so that over-approximated
Expand Down

0 comments on commit 2613563

Please sign in to comment.