summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--TODO.md4
-rw-r--r--src/InterpreterStatements.ml2
2 files changed, 4 insertions, 2 deletions
diff --git a/TODO.md b/TODO.md
index c56c91a9..471d230f 100644
--- a/TODO.md
+++ b/TODO.md
@@ -11,9 +11,13 @@
borrow parameters *if* they come from the "input abstractions".
In order to do this, add a symbolic value kind (would make things easier than
adding ad-hoc lookups...): `FunRet`, `FunGivenBack`, `SynthInput`, `SynthGivenBack`
+ Rk.: pay attention: we can't give borrows of borrows to functions, but borrows
+ are ok.
5. add `mvalue` (meta values) stored in abstractions when ending loans
+6. update the printing of mut_borrows and mut_loans ([s@0 <: ...]) and (s@0)
+
* write an interesting example to study with Jonathan
* add option for: `allow_borrow_overwrites_on_input_values`
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index e6fadbdd..8768461c 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -891,8 +891,6 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
in
(* Evaluate the input operands *)
let ctx, args = eval_operands config ctx args in
- (* TODO: expand the primitively copyable symbolic values *)
- raise Errors.Unimplemented;
let args_with_rtypes = List.combine args inst_sg.A.inputs in
(* Check the type of the input arguments *)
assert (