From 314506ec1a42c377b322d4f172f79f88f4c0f87b Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 8 Oct 2016 14:16:50 -0700 Subject: [PATCH] [quandary] ok to have no post if start node has no succs Reviewed By: sblackshear Differential Revision: D3991275 fbshipit-source-id: 5f8c4be --- infer/src/quandary/TaintAnalysis.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index d296334f6..4d907df35 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -441,7 +441,9 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct let summary = make_summary formals access_tree in Summary.write_summary (Cfg.Procdesc.get_proc_name pdesc) summary; | None -> - failwith "Couldn't compute post" in + if Cfg.Node.get_succs (Cfg.Procdesc.get_start_node pdesc) = [] + then () + else failwith "Couldn't compute post" in let callbacks = { Ondemand.analyze_ondemand;