diff options
| author | Son HO | 2023-08-07 10:42:15 +0200 |
|---|---|---|
| committer | GitHub | 2023-08-07 10:42:15 +0200 |
| commit | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (patch) | |
| tree | c15a16b591cf25df3ccff87ad4cd7c46ddecc489 /compiler/InterpreterProjectors.mli | |
| parent | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (diff) | |
| parent | 9e14cdeaf429e9faff2d1efdcf297c1ac7dc7f1f (diff) | |
Merge pull request #32 from AeneasVerif/son_arrays
Add support for arrays/slices and const generics
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterProjectors.mli | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli index 1afb9d53..bcc3dee2 100644 --- a/compiler/InterpreterProjectors.mli +++ b/compiler/InterpreterProjectors.mli @@ -55,7 +55,16 @@ val prepare_reborrows : bool -> (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx) -(** Apply (and reduce) a projector over borrows to a value. +(** Apply (and reduce) a projector over borrows to an avalue. + We use this for instance to spread the borrows present in the inputs + of a function into the regions introduced for this function. For instance: + {[ + fn f<'a, 'b, T>(x: &'a T, y: &'b T) + ]} + If we call `f` with `x -> shared_borrow l0` and `y -> shared_borrow l1`, then + for the region introduced for `'a` we need to project the value for `x` to + a shared aborrow, and we need to ignore the borrow in `y`, because it belongs + to the other region. Parameters: - [check_symbolic_no_ended]: controls whether we check or not whether |