Checking a Contract Against a Recursive Function

Back to top Code Contracts Transformation Specification

If the function to be checked is potentially recursive, we generate the wrapper function body such that the first call triggers the contract checking logic described in Checking a Contract Against a Function, and any subsequent call triggers the contract replacement logic described in Replacing a Function by a Contract :

static bool foo_check_started = false;
static bool foo_check_completed = false;
 
ret_t foo(foo_params, write_set_t caller_write_set) {
  assert(!foo_check_completed, "foo can only be called once from the harness");
 
   // first call, check the contract
  if(!foo_check_started) {
    // non-recursive contract checking instructions go here
    // ...
   return retval;
  } else {
    // contract replacement instructions
    // ...
    return retval;
  }
}

---

Prev	Next
Checking a Contract Against a Recursive Function	Replacing a Function by a Contract