source: CIVL/examples/mem/mem_tests/mem_contains_malloced-bad2.cvl@ afc300c

#include<mem.cvh>
#include<stdlib.h>

$input int N;
$assume(N > 10);
int *a;
int **b;

int main() {
  a = (int *)malloc(sizeof(int) * N);
  b = (int **)malloc(sizeof(int*) * 10);
  for (int i = 0; i < 5; i++)
    b[i] = (int *)malloc(sizeof(int) * 5);
  
  $assert($mem_contains(b[0] + (0 .. 4), a));
  free(a);
  for (int i = 0; i < 5; i++)
    free(b[i]);
  free(b);
}