Pointers to locals can escape, allowing UB

[mb64]

The following compiles:

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;
}

Here is an example output on my machine:

a is 12
12 == 2147450884 guaranteed by ZZ's static analysis

I love the concept behind ZZ, so I'm sad to have found such a gaping hole.

[aep]

yes, there's no lifetime checking at all. see also #13 for a lower hanging fruit in that direction. Implementing that depends on a whole lot of infrastructure that ins't there yet, specifically i need to separate SSA form from the symbolic prover so we can add more static analysis tools.

so I'm sad to have found such a gaping hole.

Oh there are much worse bugs than this :-P