[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

@@ -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 ->