diff options
| -rw-r--r-- | TODO.md | 7 | ||||
| -rw-r--r-- | src/Invariants.ml | 3 |
2 files changed, 6 insertions, 4 deletions
@@ -29,9 +29,6 @@ shared borrows?) necessary to know what to return. -* invariant: if a symbolic value is present multiple times in the concrete environment, - it means it is primitively copyable - * invariant: if there is a `proj_loans rset1 (s:rty)` where `s` contains mutable borrows, then: * either there is exactly one `s` in the current context @@ -90,3 +87,7 @@ function arguments or putting them in the return value, in order to deduplicate those values. Completion: we expand those values only upon copying them (that's enough). + +* invariant: if a symbolic value is present multiple times in the concrete environment, + it means it is primitively copyable + diff --git a/src/Invariants.ml b/src/Invariants.ml index ba069bc4..66a5e5ac 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -708,7 +708,8 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit = (* Check *) let check_info _id info = assert (info.env_count = 0 || info.aproj_borrows = []); - if ty_has_regions info.ty then assert (info.env_count <= 1) + if ty_has_regions info.ty then assert (info.env_count <= 1); + assert (info.env_count <= 1 || type_is_primitively_copyable info.ty) in M.iter check_info !infos |