PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
425 stars 91 forks source link

Transparent Vptrofs #699

Open andrew-appel opened 11 months ago

andrew-appel commented 11 months ago

It appears that Vptrofs is transparent by default. Perhaps it would be better to have it Global Opaque. However, doing so causes "forward" to fail when doing an array subscript load x=a[i], especially when the index i is a Vlong.