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..af56c66c 100644 --- a/libASL/symbolic_lifter.ml +++ b/libASL/symbolic_lifter.ml @@ -135,9 +135,12 @@ module RemoveUnsupported = struct | Stmt_Dep_ImpDef (_, loc) | Stmt_See (_, loc) | Stmt_Throw (_, loc) + | Stmt_Repeat(_, _, loc) + | Stmt_Try(_, _, _, _, loc) | Stmt_DecodeExecute (_, _, loc) -> ChangeTo (assert_false loc) - | _ -> failwith @@ "Unknown stmt: " ^ (pp_stmt e)) + ) + end let run unsupported env body = diff --git a/offlineASL/offline_utils.ml b/offlineASL/offline_utils.ml index 74e84992..f156f41f 100644 --- a/offlineASL/offline_utils.ml +++ b/offlineASL/offline_utils.ml @@ -191,6 +191,8 @@ let f_AtomicEnd () = push_stmt (Stmt_TCall (FIdent ("AtomicEnd", 0), [], [], Unknown)) let f_gen_AArch64_MemTag_set x y z: unit = failwith "MemTag_set unsupported" +let f_gen_AArch64_MemTag_read et x = + failwith "MemTag_read unsupported" (* Prim bool ops *) let f_gen_and_bool e1 e2 =