Add some sanity checks and comments

2 files changed, 11 insertions, 4 deletions

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 *)