Xavier Denis
Xavier Denis
> I don't really see what you mean, but my point is that by doing what I propose, we can rely on Rust's visibility mechanism, which is simple yet quite...
> Perhaps something which could be complicated if we want to implement that in Creusot is whether there exists in rustc's API a function to tell whether a symbol is...
> This is required because we don't want to make visible a private symbol used in a public definition. Ok, sorry I understand what you mean now, I wasn't getting...
Quoting myself: > I would still like this change to happen in the future, but I will do it properly using actual function contracts instead.
Oh that is clever.
I think it might be sufficient. I quite like this as i can then put off implementing old/labels.
Hmm I've encountered two issues with this so far: 1. Rust type inference sucks and forgets the generic parameter of `PhantomData` :/ 2. We really want `record` to take `self`...
Exactly, unless it were truly ghost and thus not subject to borrow checking restrictions.
@jhjourdan I actually think that we will be able to fully benefit from why3's old mechanism and labels! it will take a bit of work on the MLCFG side but...