From 85ab1fdc9edddf65a8f1a6c8bae74c1a417859f0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 25 Jun 2024 12:09:46 +0300
Subject: [PATCH] Check YAML witness existence before analysis

---
 src/framework/control.ml   | 1 +
 src/witness/yamlWitness.ml | 9 +++++++++
 2 files changed, 10 insertions(+)

diff --git a/src/framework/control.ml b/src/framework/control.ml
index bb1d7bab58..5e92282210 100644
--- a/src/framework/control.ml
+++ b/src/framework/control.ml
@@ -357,6 +357,7 @@ struct
     (* real beginning of the [analyze] function *)
     if get_bool "ana.sv-comp.enabled" then
       Witness.init (module FileCfg); (* TODO: move this out of analyze_loop *)
+    YamlWitness.init ();
 
     AnalysisState.global_initialization := true;
     GobConfig.earlyglobs := get_bool "exp.earlyglobs";
diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml
index bb91e195ef..7134211d32 100644
--- a/src/witness/yamlWitness.ml
+++ b/src/witness/yamlWitness.ml
@@ -514,6 +514,15 @@ struct
     Timing.wrap "yaml witness" write ()
 end
 
+let init () =
+  match GobConfig.get_string "witness.yaml.validate" with
+  | "" -> ()
+  | path ->
+    (* Check witness existence before doing the analysis. *)
+    if not (Sys.file_exists path) then (
+      Logs.error "witness.yaml.validate: %s not found" path;
+      Svcomp.errorwith "witness missing"
+    )
 
 module ValidationResult =
 struct