testing/035_invariant.c

   1 // objective: test \invariant, \pre and \post commands
   2 // check: 035__invariant_8c.xml
   3
   4 /** \file */
   5
   6 /** \invariant i+j=p
   7  *  \pre       p\>=0
   8  *  \post      *q=2^(p+1)
   9  */
  10 void func(int p,int *q)
  11 {
  12   int j = p, k=1, i;
  13   for (i=0; i<=p; i++) j--,k=k*2;
  14   *q = k;
  15 }