microsoft / Armada

Armada is a tool for writing, and proving correct, high-performance concurrent programs.
Other
137 stars 19 forks source link

Can't subtract pointers into the same array #11

Open jaylorch opened 3 years ago

jaylorch commented 3 years ago

In C, one can subtract pointers from each other. We don't want to allow this for arbitrary pointers in Armada, but it makes sense to allow it for pointers into the same array. After all, we already allow adding an integer to a pointer to an array element.

It would be useful to support subtracting pointers, with undefined-behavior semantics if they don't point into the same array.