From 7703c4ca86a390303d0a120f8811c8fd704c5168 Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Tue, 21 Jun 2022 11:41:09 +0200
Subject: concrete & symbolic evaluation work with new LLBC format

---
 src/InterpreterUtils.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'src/InterpreterUtils.ml')

diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 7a2e22f7..47323cc2 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -33,8 +33,6 @@ let typed_value_to_string = PA.typed_value_to_string
 
 let typed_avalue_to_string = PA.typed_avalue_to_string
 
-let operand_constant_value_to_string = PA.operand_constant_value_to_string
-
 let place_to_string = PA.place_to_string
 
 let operand_to_string = PA.operand_to_string
-- 
cgit v1.2.3


From cd754eabe3af025ca3465c5fc6d8cb48da66a1ae Mon Sep 17 00:00:00 2001
From: Sidney Congard
Date: Wed, 10 Aug 2022 18:56:25 +0200
Subject: Corrected translation without using functions, remaining bug in
 hashmap translation

---
 src/InterpreterUtils.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/InterpreterUtils.ml')

diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 47323cc2..6ef66f1d 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -238,8 +238,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
               raise Found
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack ->
-            ()
+        | V.SynthRetGivenBack -> ()
+        | V.Global -> ()
     end
   in
   (* We use exceptions *)
-- 
cgit v1.2.3


From 4a8b4b1be044ffaa8de72cf847c00184b6b8ab40 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 22 Sep 2022 18:45:25 +0200
Subject: Reformat the project with dune

---
 src/InterpreterUtils.ml | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

(limited to 'src/InterpreterUtils.ml')

diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 6ef66f1d..fed5ff9b 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -12,33 +12,19 @@ module PA = Print.EvalCtxLlbcAst
 (** Some utilities *)
 
 let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string
-
 let ety_to_string = PA.ety_to_string
-
 let rty_to_string = PA.rty_to_string
-
 let symbolic_value_to_string = PA.symbolic_value_to_string
-
 let borrow_content_to_string = PA.borrow_content_to_string
-
 let loan_content_to_string = PA.loan_content_to_string
-
 let aborrow_content_to_string = PA.aborrow_content_to_string
-
 let aloan_content_to_string = PA.aloan_content_to_string
-
 let aproj_to_string = PA.aproj_to_string
-
 let typed_value_to_string = PA.typed_value_to_string
-
 let typed_avalue_to_string = PA.typed_avalue_to_string
-
 let place_to_string = PA.place_to_string
-
 let operand_to_string = PA.operand_to_string
-
 let statement_to_string ctx = PA.statement_to_string ctx "" "  "
-
 let statement_to_string_with_tab ctx = PA.statement_to_string ctx "  " "  "
 
 let same_symbolic_id (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) : bool =
@@ -211,7 +197,6 @@ let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) :
   let obj =
     object
       inherit [_] V.iter_typed_value
-
       method! visit_Bottom _ = raise Found
 
       method! visit_symbolic_value _ s =
@@ -238,7 +223,8 @@ let value_has_ret_symbolic_value_with_borrow_under_mut (ctx : C.eval_ctx)
               raise Found
             else ()
         | V.SynthInput | V.SynthInputGivenBack | V.FunCallGivenBack
-        | V.SynthRetGivenBack -> ()
+        | V.SynthRetGivenBack ->
+            ()
         | V.Global -> ()
     end
   in
-- 
cgit v1.2.3