From 2bdc6b892bcf36c1f90a2349380c4ddb59262083 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 21 Oct 2020 09:46:15 -0700 Subject: [PATCH] [pulse] apply Abort specs too Summary: Before this diff we would just propagate the callee abstract state, which doesn't make sense in the caller. We could just remove the state from AbortProgram altogether as Pulse itself doesn't use it, but for now let's at least make sure it's accurate. Also needed for upcoming hackathon that will start from Pulse error specs to try to produce tests :) Reviewed By: ezgicicek Differential Revision: D24448073 fbshipit-source-id: 9100b3f79 --- infer/src/pulse/PulseOperations.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index b1f64647a..147760c22 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -458,10 +458,12 @@ let apply_callee ~caller_proc_desc callee_pname call_loc callee_exec_state ~ret in let open ExecutionDomain in match callee_exec_state with - | AbortProgram _ -> - (* Callee has failed; propagate the fact that a failure happened. TODO: should only do so if - we can apply the precondition? *) - Ok (Some callee_exec_state) + | AbortProgram astate -> + apply + (astate :> AbductiveDomain.t) + ~f:(fun astate -> + let astate_summary = AbductiveDomain.summary_of_post caller_proc_desc astate in + Ok (Some (AbortProgram astate_summary)) ) | ContinueProgram astate -> apply astate ~f:(fun astate -> Ok (Some (ContinueProgram astate))) | ExitProgram astate ->