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