aeneas icon indicating copy to clipboard operation
aeneas copied to clipboard

Add a way of providing information about borrows in external types

Open sonmarcho opened this issue 11 months ago • 0 comments
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) := ...

sonmarcho avatar Nov 28 '24 14:11 sonmarcho