From ef78ba83cff979d5bb122a787333fed6e5ab229e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 14 Oct 2019 07:24:27 -0700
Subject: [PATCH] [sledge] Report the number of alarms

Summary:
For test scripting purposes, when the analysis finishes successfully,
report the number of alarms.

Reviewed By: ngorogiannis

Differential Revision: D17801947

fbshipit-source-id: 1660866df
---
 sledge/src/report.ml  | 4 ++++
 sledge/src/report.mli | 1 +
 sledge/src/sledge.ml  | 3 ++-
 3 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index ff91c5561..df0ea6a01 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -22,7 +22,11 @@ let unknown_call call =
         | _ -> () )
       call Llair.Term.pp call]
 
+let count = ref 0
+let invalid_access_count () = !count
+
 let invalid_access fmt_thunk pp access loc =
+  Int.incr count ;
   let rep fs =
     Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp
       (loc access) pp access
diff --git a/sledge/src/report.mli b/sledge/src/report.mli
index 04a8482e7..941b268c6 100644
--- a/sledge/src/report.mli
+++ b/sledge/src/report.mli
@@ -10,3 +10,4 @@
 val unknown_call : Llair.term -> unit
 val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit
 val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit
+val invalid_access_count : unit -> int
diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml
index d764bf85f..cd6d50e86 100644
--- a/sledge/src/sledge.ml
+++ b/sledge/src/sledge.ml
@@ -42,7 +42,8 @@ let command ~summary ?readme param =
     try
       main () |> ignore ;
       Trace.flush () ;
-      Format.printf "@\nRESULT: Success@."
+      Format.printf "@\nRESULT: Success: Invalid Accesses: %i@."
+        (Report.invalid_access_count ())
     with exn ->
       let bt = Caml.Printexc.get_raw_backtrace () in
       Trace.flush () ;