test/bufferTest.out

   1
   2 test4.c: (in function t)
   3 test4.c:6:3: Variable g used before definition
   4 test4.c:6:3: Possible out-of-bounds store.  Unable to resolve constraint:
   5     requires maxSet(g @ test4.c:6:3) >= 100
   6      needed to satisfy precondition:
   7     requires maxSet(g @ test4.c:6:3) >= 100
   8 test6.c:2:6: Function t defined more than once
   9    test4.c:15:1: Previous definition of t
  10 test6.c: (in function t)
  11 test6.c:5:4: Variable g used before definition
  12 test6.c:6:3: Possible out-of-bounds store.  Unable to resolve constraint:
  13     requires maxSet(g @ test6.c:5:4) >= 1
  14      needed to satisfy precondition:
  15     requires maxSet(g @ test6.c:6:3) >= 0
  16 test6.c:6:10: Possible out-of-bounds read.  Unable to resolve constraint:
  17     requires maxRead(g @ test6.c:5:4) >= 2
  18      needed to satisfy precondition:
  19     requires maxRead(g @ test6.c:6:10) >= 1
  20
  21 Finished LCLint checking --- 6 code errors found