Unsoundness with recursive functions

[chkl]

Hi,
I was wondering whether crab-llvm handles recursive functions. Consider the following program:

extern int __VERIFIER_nondet_int();
extern void __VERIFIER_error();
void __VERIFIER_assert(int cond) {
  if (!cond) {
  ERROR: __VERIFIER_error();
  }
}

int fibo(int n) {
  // This does not hold
  __VERIFIER_assert(n != 0);
  if (n < 1) {
      return 0;
  } else if (n == 1) {
      return 1;
  } else {
      return fibo(n - 1) + fibo(n - 2);
  }
}

int main(void) {
  int x = 10;
  int result = fibo(x);
  return 0;
}

./crabllvm.py -m 32 --crab-inter --crab-check=assert --crab-dom=int /database/confrontation/crab/fibo.c yields

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

Another question, and only slightly related: Do crab-llvm and seahorn use the same frontend? Because as discussed in seahorn/seahorn#152, seahorn does not completely cover all potential program behavior if some part is implementation-specific (e.g. uninitialized variables). So, naturally I assumed that crab-llvm and seahorn would handle those cases similarly. Interestingly, sometimes there are still cases where crab-llvm and seahorn disagree because of undefined behavior, e.g.:

extern void __VERIFIER_error() __attribute__((__noreturn__));

void __VERIFIER_assert(int cond)
{
    if (!cond)
    {
    ERROR:
        __VERIFIER_error();
    }
    return;
}
extern int __VERIFIER_nondet_int();
int main()
{
    int i, n = __VERIFIER_nondet_int();
    if (!(n < 1000 && n >= -1000))
    {
        return 0;
    }
    __VERIFIER_assert(i <= n );
}

(seahorn: Sat, crab-llvm: Unsat)

[caballa]

There was a bug in the code. It has been fixed in crab commit 11fffc78ff7851fa950953a9fd31c980dece8a79.
You need to update the subdirectory crab with git pull origin master.
Regarding undefined behavior, the frontend of crab-llvm is different from the one from seahorn. They share a lot of stuff but there are differences. Thus, it's not surprising they behave differently in presence of undefined behavior.