Skip to content

Commit

Permalink
[pulse][specialization] do not die if the expected specialized summar…
Browse files Browse the repository at this point in the history
…y is no there

Summary:
this case was unexpected but it seems to appear in practice. For some
reason the specialized summary was not computed properly.

Reviewed By: dulmarod, geralt-encore

Differential Revision: D45811752

fbshipit-source-id: b22f7b2fb271f99f10770f9137d0499e20cdd068
  • Loading branch information
davidpichardie authored and facebook-github-bot committed May 12, 2023
1 parent 6d1cbed commit a063217
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion infer/src/pulse/PulseCallOperations.ml
Original file line number Diff line number Diff line change
Expand Up @@ -552,7 +552,9 @@ let call tenv path ~caller_proc_desc
in
match Specialization.Pulse.Map.find_opt specialization specialized_summary.specialized with
| None ->
L.die InternalError "ondemand engine did not return the expected specialized summary"
L.internal_error "ondemand engine did not return the expected specialized summary" ;
(* we use the non-specialized summary instead *)
specialized_summary.main
| Some pre_posts ->
pre_posts
in
Expand Down

0 comments on commit a063217

Please sign in to comment.