bad.c


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

/* This may look like nonsense, but really is -*- mode: C -*- */

/* The main thing that this program does. */
void main() {
  // Declarations
  int i;
  double A[5] = {
    9.0,
    2.9,
    3.E+25,
    .00007,
  };

  // Doing some work
  for (i = 0; i < 5; ++i) {
     printf("element %d is %g, \tits square is %g\n", /*@\label{printf-start-badly}*/
            i,
            A[i],
            A[i]*A[i]);                               /*@\label{printf-end-badly}*/
  }

  return 0;                                           /*@\label{main-return-badly}*/
}