Make minor modifications

2 files changed, 34 insertions, 4 deletions

diff --git a/src/Contexts.ml b/src/Contexts.ml
index cd433890..407f01bb 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -16,6 +16,33 @@ module M = Modules
  *   different contexts
  * - also, it is a lot more convenient to not store those counters in contexts
  *   objects
+ *
+ * =============
+ * **WARNNING**:
+ * =============
+ * Pay attention when playing with the function type abbreviations,
+ * as they may make you not always generate fresh identifiers. For
+ * instance, consider the following:
+ * ```
+ * type fun_type = unit -> ...
+ * fn f x : fun_type =
+ *   let id = fresh_id () in
+ *   ...
+ *
+ * let g = f x in   // <-- the fresh identifier gets generated here
+ * let x1 = g () in // <-- no fresh generation here
+ * let x2 = g () in
+ * ...
+ * ```
+ *
+ * This is one, in such cases, we often introduce all the inputs, even
+ * when they are not used (which happens!).
+ * ```
+ * fn f x : fun_type =
+ *  fun .. ->
+ *   let id = fresh_id () in
+ *   ...
+ * ```
  *)
 
 let symbolic_value_id_counter, fresh_symbolic_value_id =
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 80b06143..d3153110 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -271,6 +271,7 @@ let eval_unary_op_concrete (config : C.config) (unop : E.unop) (op : E.operand)
 
 let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
     (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+ fun ctx ->
   (* Evaluate the operand *)
   let eval_op = eval_operand config op in
   (* Generate a fresh symbolic value to store the result *)
@@ -291,7 +292,7 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
     cf (Ok (mk_typed_value_from_symbolic_value res_sv))
   in
   (* Compose and apply *)
-  comp eval_op apply cf
+  comp eval_op apply cf ctx
 
 let eval_unary_op (config : C.config) (unop : E.unop) (op : E.operand)
     (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
@@ -387,6 +388,7 @@ let eval_binary_op_concrete (config : C.config) (binop : E.binop)
 let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
     (op1 : E.operand) (op2 : E.operand)
     (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun =
+ fun ctx ->
   (* Evaluate the operands *)
   let eval_ops = eval_two_operands config op1 op2 in
   (* Compute the result of applying the binop *)
@@ -426,7 +428,7 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
     cf (Ok v)
   in
   (* Compose and apply *)
-  comp eval_ops compute cf
+  comp eval_ops compute cf ctx
 
 let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand)
     (op2 : E.operand) (cf : (V.typed_value, eval_error) result -> m_fun) : m_fun
@@ -491,6 +493,7 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
 
 let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
     (cf : V.typed_value -> m_fun) : m_fun =
+ fun ctx ->
   match bkind with
   | E.Shared | E.TwoPhaseMut ->
       (* Access the value *)
@@ -531,7 +534,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         cf rv ctx
       in
       (* Compose and apply *)
-      comp prepare eval cf
+      comp prepare eval cf ctx
   | E.Mut ->
       (* Access the value *)
       let access = Write in
@@ -554,7 +557,7 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind)
         cf rv ctx
       in
       (* Compose and apply *)
-      comp prepare eval cf
+      comp prepare eval cf ctx
 
 let eval_rvalue_aggregate (config : C.config)
     (aggregate_kind : E.aggregate_kind) (ops : E.operand list)