source: CIVL/examples/mem/writeset/ws_push_pop_memcpy-bad.cvl@ aaa9c8d

#include <mem.cvh>
#include <string.h>
$input int N, n;
$assume(N > n && n > 5);

int main() {
  double a[10], b[10][10];
  int x;

  $write_set_push();
  a[3] = 0;
  b[1][3] = 0;
  memcpy(&a[1], &a[2], sizeof(double) * 3);
  memcpy(&b[1][0], &a[0], sizeof(double) * 3);
 
  $mem m = $write_set_pop();

  $assert($mem_contains(m, &x));
  return 0;
}