Blame tests/upstream-test-suite/035_invariant.c

Than Ngo b7bcaa
// objective: test \invariant, \pre and \post commands
Than Ngo b7bcaa
// check: 035__invariant_8c.xml
Than Ngo b7bcaa
Than Ngo b7bcaa
/** \file */
Than Ngo b7bcaa
Than Ngo b7bcaa
/** \invariant i+j=p
Than Ngo b7bcaa
 *  \pre       p\>=0
Than Ngo b7bcaa
 *  \post      *q=2^(p+1)
Than Ngo b7bcaa
 */
Than Ngo b7bcaa
void func(int p,int *q)
Than Ngo b7bcaa
{
Than Ngo b7bcaa
  int j = p, k=1, i;
Than Ngo b7bcaa
  for (i=0; i<=p; i++) j--,k=k*2;
Than Ngo b7bcaa
  *q = k;
Than Ngo b7bcaa
}