From 74aef0cc74487bbc1646f1761d573f572935a9c7 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 28 Jul 2016 13:37:15 +0100
Subject: Banish exit from the mips/cheri sail except at end of SignalException
 function. There is a plan to replace this syntax with something more
 understandable. Should make no functional difference using sequential
 interpretor but will need to do some work on exception functions when
 integrating with ppcmem so that it know register writes are exceptional etc.

---
 src/lem_interp/run_interp_model.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src')

diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 034fd991..87eafa56 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -245,6 +245,10 @@ let run
     | Error0 s -> 
       errorf "%s: %s: %s\n" (grey name) (red "error") s;
       (false, mode, !track_dependencies, env)
+    | Escape (None, _) ->
+      show "exiting current instruction" "" "" "";
+      interactf "%s: %s\n" (grey name) (blue "done");
+      (true, mode, !track_dependencies, env)
     | Fail0 (Some s) ->
       errorf "%s: %s: %s\n" (grey name) (red "assertion failed") s;
       (false, mode, !track_dependencies, env)
-- 
cgit v1.2.3