source: CIVL/examples/contract.cvl@ 73f1e27

double f(double x) 
  \requires x > 0;
  \ensures \true;
  ;

double g(double x)
  \requires x > 0;
  \ensures \result >= 0;
{
  return g(x)*g(x);
}

double main() {
  return g(2);
}