From 1816d77c30336bb14ad4f23e33f73456f0784868 Mon Sep 17 00:00:00 2001
From: Nicholas Coughlin <n.coughlin@uq.edu.au>
Date: Tue, 24 Dec 2024 08:54:31 +1000
Subject: [PATCH] Offline fixes for new reachable code

Calls without bodies are left in the partial eval result.
This is a little unexpected, leading to offline issues.

Also fix some sanity tests to handle failure consistently.
---
 libASL/symbolic.ml        | 4 ++++
 libASL/symbolic_lifter.ml | 6 +++---
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml
index a904fcfb..a999a19c 100644
--- a/libASL/symbolic.ml
+++ b/libASL/symbolic.ml
@@ -990,6 +990,10 @@ let prims_impure () =
     FIdent("AtomicEnd",0);
     FIdent("AArch64.MemTag.read",0);
     FIdent("AArch64.MemTag.set",0);
+    FIdent("SetTagCheckedInstruction",0);
+    FIdent("SpeculativeStoreBypassBarrierToPA",0);
+    FIdent("SpeculationBarrier",0);
+    FIdent("SpeculativeStoreBypassBarrierToVA",0);
   ]
 
 (** Test if an expression is only over constants, variables and pure operations. Does not
diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml
index 86dd03b4..4a37306c 100644
--- a/libASL/symbolic_lifter.ml
+++ b/libASL/symbolic_lifter.ml
@@ -135,9 +135,9 @@ module RemoveUnsupported = struct
       | Stmt_Dep_ImpDef (_, loc)
       | Stmt_See (_, loc)
       | Stmt_Throw (_, loc)
-      | Stmt_DecodeExecute (_, _, loc) -> ChangeTo (assert_false loc)
-
-      | _ -> failwith @@ "Unknown stmt: " ^ (pp_stmt e))
+      | Stmt_DecodeExecute (_, _, loc)
+      | Stmt_Try (_, _, _, _, loc)
+      | Stmt_Repeat (_, _, loc) -> ChangeTo (assert_false loc))
   end
 
   let run unsupported env body =