Added a new check to ensure that every call to another location points to an existing one

1 files changed, 13 insertions, 0 deletions

diff --git a/lib/syntax/check.ml b/lib/syntax/check.ml
index a5db091..9292a7a 100644
--- a/lib/syntax/check.ml
+++ b/lib/syntax/check.ml
@@ -123,6 +123,7 @@ end
 module Make (A : App) = struct
   let identifier = "main_checker"
   let description = "Internal module"
+  let is_global = false
   let active = ref false
 
   type context = result Array.t
@@ -136,6 +137,18 @@ module Make (A : App) = struct
         let value = S.initialize () in
         R { value; witness = context })
 
+  let finalize : result Array.t -> (string * Report.t) list =
+   fun context_array ->
+    let _, report =
+      Array.fold_left A.t ~init:(0, [])
+        ~f:(fun (i, acc) (E { module_ = (module S); context; _ }) ->
+          let result = Array.get context_array i in
+          let local_context = Option.get (get context result) in
+          let reports = S.finalize local_context in
+          (i + 1, List.rev_append reports acc))
+    in
+    report
+
   (* Global variable for the whole module *)
   let len = Array.length A.t