Add some sanity checks and comments

3 files changed, 19 insertions, 5 deletions

diff --git a/TODO.md b/TODO.md
index a70e4546..62871300 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,6 +1,6 @@
 # TODO
 
-0. add a meta-value in shared borrows to carry the shared value
+0. sanity checks in symbolic to pure!
 
 0. update the end borrows internal to abstractions to not introduce a Bottom
 
@@ -8,6 +8,11 @@
 
 0. remove ABottom from avalue
 
+0. micro-passes for pure:
+   - remove unused variables
+   - remove useless function calls *if* they are followed by associated
+     backward calls (because they may panic!)
+
 1. reorder the branches of matches
 
 1. stateful maps/sets modules (hashtbl?)
@@ -154,3 +159,5 @@
 
 * fix the static regions (with projectors)
   Before that, introduce a sanity check to make sure we don't use static regions.
+
+* add a meta-value in shared borrows to carry the shared value
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 *)