typedef enum { JAN, FEB, MAR, APR, MAY, JUN,                       /* months.c */
                          JUL, AUG, SEP, OCT, NOV, DEC } Month;
#include <stdio.h>
int main() {
  Month current = OCT;
  Month future = 100;  /*@{}@XPC{@B{no compile-time checks; no run-time checks!}}*/
  printf("This month: %d; next: %d; future: %d.\n", current, current + 1, future);
  return 0;
}