xr0-org / xr0

The Xr0 Verifier for C
https://xr0.dev
Apache License 2.0
173 stars 4 forks source link

Enforce pre-declaration #30

Closed claude-betz closed 5 months ago

claude-betz commented 6 months ago

Currently a block like this doesn't require pre-declaration of func(). It should

int
main()
{
    int *i;
    int *j;

    i = func();
    j = *i;     /* ERROR: unjusitified indirection */

    return 0;
}

int *
func()
{
    int *p;
    p = malloc(1);
    free(p);    /* p dangling */

    return p;   /* return dangling ptr */
}
claude-betz commented 5 months ago

implemented as part of #32