xr0-org / xr0

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

implement logic for advanced branching #49

Open claude-betz opened 4 months ago

claude-betz commented 4 months ago

We need to expand on the way we handle propositions to support the more advanced branching examples such as:

#include <stdlib.h> 

void 
foo(int a, int b) 
{ 
       int *p; 
       p = malloc(1); 
       if (!a) { 
                if (!b) { 
                        free(p); 
                } 
       } 
       if (a) { 
               free(p); 
       } 
       if (b) { 
               free(p); 
       } 
}

See feat/advanced-branching