incompleteness: crab-llvm(pk)

[chkl]

As a result of exp08, I found that the PK domain is sometimes less precise than the int domain. A case that demonstrates this is the following:

extern void __VERIFIER_error() __attribute__((__noreturn__));
void __VERIFIER_assert(int cond)
{
    if (!cond)
    {   
    ERROR:
        __VERIFIER_error();
    }   
}
int main() {
    int i, j, k;
    i = 0;
    j = 0;
    while (i <= 100) {
        __VERIFIER_assert(i + 1 != 0); 
        i = i + 1;
        /* this part is relevant to the reachability of the assertion */
        while (j < 20) {
            j = i + j;
        }   
    }   
    return 0;
}

For this file the verdicts are as follows:

> vdiff run --verifiers="crab-llvm(--crab-dom=pk)#pk crab-llvm(--crab-dom=oct)#oct uautomizer" oct-vs-pk-2.c
pk:         Sat
oct:        Unsat
uautomizer: Unsat

The output of crab-llvm ends in (for pk) and

************** ANALYSIS RESULTS ****************
0  Number of total safe checks
0  Number of total error checks
1  Number of total warning checks

and (for int, or any other domain)

************** ANALYSIS RESULTS ****************
1  Number of total safe checks
0  Number of total error checks
0  Number of total warning checks

The general pattern is that there's an update to a different variable that only reads the variable whose domain is relevant for the assertion and If I remove that update (in the example above the inner while-loop) the assertion holds again.

All other inclusion relations hold or are violated as a consequence of this non-inclusion.

TODO: I'm currently augmenting the data of exp08 with runs of uautomizer so we get another chance at finding some unsoundness in crab-llvm.

[chkl]

https://github.com/seahorn/crab-llvm/issues/18