Out Parameters

C has no proper mechanism for out parameters, instead, out parameters need to be simulated by pass-by-pointer. This is an unnecessary burden for the prover. Thus, specification parameters can be passed as out parameters, which does not involve passing them by pointer and thus does not impose memory writes.

Syntactically, out parameters are declared by adding the out keyword. Inside the body of the function, the out parameters can then be assigned to as if they were local variables.

int foo(int a, int b spec(out int c)) {
  spec(c = 5;)
  return 0;
}

To call such a function with out parameters, the actual parameter will also have to be decorated with the out keyword:

void bar() {
  spec(int x;)
  foo(1, 2 spec(out x));
}