xr0-org / xr0

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

logical bang not working #43

Open akiarie opened 5 months ago

akiarie commented 5 months ago

As pointed out here bang isn't working in some simple code examples:

#include <stdlib.h>

void
x(int f)
{
        int *p;
        p = malloc(1);
        if(f) {
                free(p);
        }
        f = !f;
        if(f) {
                free(p);
        }
}

We're putting in a simple fix for this, but it's worth noting that Xr0 doesn't yet have a substantial logical/arithmetic engine, so a lot of these won't work.