From 8b6f8e5fb85bcd1b3257550270c4c857d4ee7f55 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 9 Nov 2022 18:04:03 +0100
Subject: Implement the generation of stateful backward functions (controlled
 by an option)

---
 compiler/Interpreter.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'compiler/Interpreter.ml')

diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index d3b3c7e6..e752594e 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -253,8 +253,15 @@ let evaluate_function_symbolic (config : C.partial_config) (synthesize : bool)
               cf_pop cf_return ctx
           | Some back_id ->
               (* Backward translation *)
-              evaluate_function_symbolic_synthesize_backward_from_return config
-                fdef inst_sg back_id ctx
+              let e =
+                evaluate_function_symbolic_synthesize_backward_from_return
+                  config fdef inst_sg back_id ctx
+              in
+              (* We insert a delimiter to indicate the point where we switch
+               * from the part which is common to all the functions (forwards
+               * and backwards) and the part specific to this backward function.
+               *)
+              S.synthesize_forward_end e
         else None
     | Panic ->
         (* Note that as we explore all the execution branches, one of
-- 
cgit v1.2.3