SE547: CBMC: CBMC Algorithm [13/19] Previous pageContentsNext page

Do an example...

int factorial (int x) {
  int result;
  if (x < 2) { result = 1; } else { result = factorial (x-1) * x; }
  assert (result > 0);
}

file:factorial.c Is this program OK?

Previous pageContentsNext page