using <stdio.h>::{printf};

fn addr_of_local() int* 
    model safe(return)
{
    int x = 12;
    return &x;
}

fn deref(int *x) int
    model *x == return
{
    return *x;
}

export fn main() -> int {
    int *ptr = addr_of_local();

    int a = *ptr;
    printf("a is %d\n", a);

    int b = deref(ptr);

    static_assert(a == b);
    printf("%d == %d guaranteed by ZZ's static analysis\n", a, b);

    return 0;
}