From c341c1cfbaaad52ff1282b08661e85334f383f9e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 2 Oct 2024 11:24:53 +0300
Subject: [PATCH] Add errors when architecture machdep not available

---
 src/common/util/cilfacade.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index a71f2544e3..344d29d246 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -50,10 +50,16 @@ let init_options () =
   Cabs2cil.addNestedScopeAttr := get_bool "cil.addNestedScopeAttr";
 
   if get_bool "ana.sv-comp.enabled" then (
-    Cil.envMachine := match get_string "exp.architecture" with
+    let machine = match get_string "exp.architecture" with
       | "32bit" -> Machdep.gcc32
       | "64bit" -> Machdep.gcc64
       | _ -> assert false
+    in
+    match machine with
+    | Some _ -> Cil.envMachine := machine
+    | None ->
+      GobRef.wrap AnalysisState.should_warn true (fun () -> Messages.msg_final Error ~category:Unsound "Machine definition not available for selected architecture");
+      Logs.error "Machine definition not available for selected architecture, defaulting to host"
   )
 
 let init () =