#define NULL ((void *)0)


/*@
    requires n >= 0;
    assigns \result \from \nothing;
    ensures \result == \null || \valid(((char*)\result)+(0..n-1));
@*/
void *malloc(int n);

/*@
    requires \valid(a);
    requires \valid(b);
    requires \separated(a, b);
    assigns \nothing;
    ensures \result == \null || \valid(\result);
    ensures \separated(a, b);
    ensures \result != \null ==> \separated(a, b, \result); // proved on assumption with HELPER
@*/
int* foo(int *a, int *b){
    int *c = (int*)malloc(sizeof(int));
    if(!c) return NULL;
    //@ assert \separated(a, b);
    //@ assert HELPER: \separated(a, b, c); // cant prove this.
    return c;
}