aeneas
aeneas copied to clipboard
Add a way of providing information about borrows in external types
trafficstars
External types are opaque, but we need to know if some of their lifetimes are used in mutable borrows or not to properly generate the backward functions.
Example :
struct S<'a, T>;
impl<'a, T> S<'a, T> {
fn use(self);
}
If S doesn't use 'a for mutable borrows, then the pure model for use will have the following signature:
def use {T} (x : S T) -> Result () := ...
If it uses 'a for mutable borrows, it will have the following signature:
def use {T} (x : S T) -> Result (S T) := ...