diff --git a/infer/src/IR/Procdesc.re b/infer/src/IR/Procdesc.re
index 64edb1749..94f6910ce 100644
--- a/infer/src/IR/Procdesc.re
+++ b/infer/src/IR/Procdesc.re
@@ -419,6 +419,8 @@ let get_slope pdesc => Node.get_generated_slope (get_start_node pdesc) Node.get_
 /** Return [true] iff the procedure is defined, and not just declared */
 let is_defined pdesc => pdesc.attributes.is_defined;
 
+let is_body_empty pdesc => Node.get_succs (get_start_node pdesc) == [];
+
 let is_java_synchronized pdesc => pdesc.attributes.is_java_synchronized_method;
 
 let iter_nodes f pdesc => IList.iter f (IList.rev (get_nodes pdesc));
diff --git a/infer/src/IR/Procdesc.rei b/infer/src/IR/Procdesc.rei
index 7fd72425b..f7b04ccb6 100644
--- a/infer/src/IR/Procdesc.rei
+++ b/infer/src/IR/Procdesc.rei
@@ -235,6 +235,10 @@ let get_start_node: t => Node.t;
 let is_defined: t => bool;
 
 
+/** Return [true] if the body of the procdesc is empty (no instructions) */
+let is_body_empty: t => bool;
+
+
 /** Return [true] if the procedure signature has the Java synchronized keyword */
 let is_java_synchronized: t => bool;
 
diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml
index 47f96394f..0cceec7f6 100644
--- a/infer/src/quandary/TaintAnalysis.ml
+++ b/infer/src/quandary/TaintAnalysis.ml
@@ -540,9 +540,8 @@ module Make (TaintSpec : TaintSpec.S) = struct
               let summary = make_summary formals access_tree in
               Summary.write_summary (Procdesc.get_proc_name pdesc) summary;
           | None ->
-              if Procdesc.Node.get_succs (Procdesc.get_start_node pdesc) = []
-              then ()
-              else failwith "Couldn't compute post"
+              if not (Procdesc.is_body_empty pdesc)
+              then failwith "Couldn't compute post"
         end in
     let callbacks =
       {