From f10dff1e13c00eaa49d78f5d7ba79366fa028a73 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 10:23:14 +0100
Subject: Add some sanity checks and comments

---
 src/Interpreter.ml    |  4 ++--
 src/SymbolicToPure.ml | 11 +++++++++--
 2 files changed, 11 insertions(+), 4 deletions(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index fbb7ef9b..d3e30519 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -47,8 +47,8 @@ module Test = struct
       Introduces local variables initialized in the following manner:
       - input arguments are initialized as symbolic values
       - the remaining locals are initialized as ⊥
-      "Dummy" abstractions are introduced for the regions present in the
-      function signature.
+      Abstractions are introduced for the regions present in the function
+      signature.
    *)
   let initialize_symbolic_context_for_fun (m : M.cfim_module) (fdef : A.fun_def)
       : C.eval_ctx =
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index a575e835..afca9398 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -856,9 +856,11 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       let inputs =
         List.concat [ fwd_inputs; back_ancestors_inputs; back_inputs ]
       in
+      (* TODO: check that the inputs have the proper number and the proper type *)
       (* Retrieve the values given back by this function: those are the output
        * values *)
       let ctx, outputs = abs_to_given_back abs ctx in
+      (* TODO: check that the outputs have the proper number and the proper type *)
       (* Retrieve the function id, and register the function call in the context
        * if necessary *)
       let ctx, func = bs_ctx_register_backward_call abs ctx in
@@ -906,9 +908,14 @@ and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
       assert (consumed = []);
       (* Retrieve the values given back upon ending this abstraction *)
       let ctx, given_back = abs_to_given_back abs ctx in
-      (* Link the inputs to those given back values - note that we must
-       * have the same number of values *)
+      (* Link the inputs to those given back values - note that this also
+       * checks we have the same number of values, of course *)
       let given_back_inputs = List.combine given_back inputs in
+      (* Sanity check *)
+      List.iter
+        (fun ((given_back, input) : typed_lvalue * var) ->
+          assert (given_back.ty = input.ty))
+        given_back_inputs;
       (* Translate the next expression *)
       let e = translate_expression e ctx in
       (* Generate the assignments *)
-- 
cgit v1.2.3