diff options
| author | Son HO | 2022-10-21 11:14:15 +0200 |
|---|---|---|
| committer | GitHub | 2022-10-21 11:14:15 +0200 |
| commit | b4be489e7a5753bcc7f8714273ae71260fac53ce (patch) | |
| tree | 45459740595bcdd70e5f4856b8499d1680d4ab91 /src/InterpreterPaths.ml | |
| parent | 53a2b8a2989485e8885d02c786206de84c9fd91d (diff) | |
| parent | d62563cf9b8ef29ce20e810a5b1da999122c7a2f (diff) | |
Merge pull request #4 from AeneasVerif/son_update_charon
Update the code to account for changes in Charon
Diffstat (limited to 'src/InterpreterPaths.ml')
| -rw-r--r-- | src/InterpreterPaths.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index edd27138..16ab9aad 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -771,6 +771,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) [end_borrows]: if false, we only end the outer loans we find. If true, we end all the loans and the borrows we find. + TODO: end_borrows is not necessary anymore. *) let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = |