source: CIVL/examples/mem/mem_tests/mem_convertion-bad.cvl

#include<mem.cvh>
#include<pointer.cvh>

struct T {
  int x;
};

int main() {
  $mem m;
  int a;
  struct T b;
  
  // invalid memory location reference:
  m = &(&b + 1)->x;
  $assert($equals(&m, &m));
}