/* q18_a.c */

#include "q18_a.h"

static int a = 0;

/*@ requires a <= 10;
    ensures a == \old(a) + 1;
    assigns a;
*/
void incr_a(void)
{
  a += 1;
}

/*@ assigns a;
 */
int f(int p)
{
  if (a <= 10) {
    incr_a();
  }

  return p + 1;
}

/* q18_a.h */

/*@ requires p <= 10;
    ensures \result == p + 1;
 */
int f(int p);

#include "q18_a.h"

/*@ requires p <= 10;
    ensures \result == p + 1;
    assigns \nothing; // unprovable, cannot put "a" neither
 */
int g(int p)
{
  int r;

  return f(p);
}