From d7a13b0e5d6e746993e67a291376bd79766e0ed1 Mon Sep 17 00:00:00 2001
From: Chimrod <>
Date: Sat, 3 Feb 2024 17:42:16 +0100
Subject: Added a new check to ensure that every call to another location
 points to an existing one

---
 lib/syntax/check.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'lib/syntax/check.ml')

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
 
-- 
cgit v1.2.3