From 0dfe0b8f75448561a0f0d7e07483725b12489ff7 Mon Sep 17 00:00:00 2001 From: martinoluca Date: Tue, 8 Dec 2015 10:35:43 -0800 Subject: [PATCH] Let InferPrint count timeouts Reviewed By: jberdine Differential Revision: D2734464 fb-gh-sync-id: eae468d --- infer/src/backend/inferprint.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/infer/src/backend/inferprint.ml b/infer/src/backend/inferprint.ml index c2230b84f..1b32293d8 100644 --- a/infer/src/backend/inferprint.ml +++ b/infer/src/backend/inferprint.ml @@ -666,6 +666,7 @@ module Stats = struct mutable nLOC : int; mutable nprocs : int; mutable nspecs : int; + mutable ntimeouts : int; mutable nverified : int; mutable nwarnings : int; mutable saved_errors : string list; @@ -680,6 +681,7 @@ module Stats = struct nLOC = 0; nprocs = 0; nspecs = 0; + ntimeouts = 0; nverified = 0; nwarnings = 0; saved_errors = []; @@ -744,10 +746,12 @@ module Stats = struct let is_defective = found_errors in let is_verified = specs <> [] && not is_defective in let is_checked = not (is_defective || is_verified) in + let is_timeout = Specs.(summary.stats.stats_timeout) in stats.nprocs <- stats.nprocs + 1; stats.nspecs <- stats.nspecs + (IList.length specs); if is_verified then stats.nverified <- stats.nverified + 1; if is_checked then stats.nchecked <- stats.nchecked + 1; + if is_timeout then stats.ntimeouts <- stats.ntimeouts + 1; if is_defective then stats.ndefective <- stats.ndefective + 1; process_loc summary.Specs.attributes.ProcAttributes.loc stats @@ -758,6 +762,7 @@ module Stats = struct F.fprintf fmt "Files: %d@\n" (num_files stats); F.fprintf fmt "LOC: %d@\n" stats.nLOC; F.fprintf fmt "Specs: %d@\n" stats.nspecs; + F.fprintf fmt "Timeouts: %d@\n" stats.ntimeouts; F.fprintf fmt "Procedures: %d@\n" stats.nprocs; F.fprintf fmt " Verified: %d@\n" stats.nverified; F.fprintf fmt " Checked: %d@\n" stats.nchecked;