[backend] utility function for checking if a procdesc has an empty body

Reviewed By: jeremydubreil

Differential Revision: D4210501

fbshipit-source-id: d0cdb14

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));

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;
 

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) = []
+              if not (Procdesc.is_body_empty pdesc)
-              then ()
+              then failwith "Couldn't compute post"
-              else failwith "Couldn't compute post"
         end in
     let callbacks =
       {