search

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 same array #23

Open jaylorch opened 3 years ago

jaylorch commented 3 years ago

Currently, it's not supported to subtract two pointers, even if it's well-defined because those pointers point into the same array. For instance, you can't do:

  var a: uint32[10];
  ghost var i: int;
  i := &a[5] - &a[3]; // Should give 2