Skip to content

Conversation

@ssyram
Copy link
Contributor

@ssyram ssyram commented Oct 30, 2025

As mentioned in #310 , here's a fix to the problem mentioned there. But instead of the more complex substitution as in #308 , we simply fix it by using the tagged type of the place.

Notably, in #308 , we will need to fetch the vtable instance pointer, and substitute the generics with the generics args from the reference to generate the correct type ourselves. But in PlaceGlobal, we have available type tagged by Charon.

Further, please note that the tagged type may not yield exactly the same result as the substitution -- because of the difference in lifetime parameters.

As mentioned in #310 , there might be more hidden bugs like this.

@ssyram ssyram changed the title simple fix of global type simple fix of types of globals Oct 30, 2025
@protz protz merged commit 94cdf3b into AeneasVerif:main Oct 30, 2025
3 checks passed
@protz
Copy link
Contributor

protz commented Oct 30, 2025

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants