https://gcc.gnu.org/bugzilla/show_bug.cgi?id=82898 --- Comment #1 from Marc Glisse <glisse at gcc dot gnu.org> --- At least in the gcc model, the type of a pointer is meaningless as long as you do not dereference it using that type, so I am not sure what can be done here.