method assign<T>(&T x, &T y, T v1, T v2)
ensures *x == v1
ensures *y == v2:
// Broken if x == y
*x = v1
*y = v2
This doesn't allow the dereference. I think to make this work, we need some information about T --- namely that it is statically sized. This is evident from the fact that it is passed as a parameter.
Test
001137is as follows:This doesn't allow the dereference. I think to make this work, we need some information about
T--- namely that it is statically sized. This is evident from the fact that it is passed as a parameter.