test/simplebufferConstraintTests.expect

   1
   2 m.c: (in function t)
   3 m.c:9:1: Index of possibly null pointer f: f
   4    m.c:8:5: Storage f may become null
   5 sizeof.c: (in function f)
   6 sizeof.c:17:1: Likely out-of-bounds store:
   7     x[(sizeof(x))]
   8     Unable to resolve constraint:
   9     requires 2 >= 3
  10      needed to satisfy precondition:
  11     requires maxSet(x @ sizeof.c:17:1) >= 3
  12 test3.c:2:6: Function t defined more than once
  13    m.c:11:1: Previous definition of t
  14 test3.c: (in function t)
  15 test3.c:9:3: Likely out-of-bounds store:
  16     g[101]
  17     Unable to resolve constraint:
  18     requires 99 >= 101
  19      needed to satisfy precondition:
  20     requires maxSet(g @ test3.c:9:3) >= 101
  21 test7.c:2:6: Function t defined more than once
  22    m.c:11:1: Previous definition of t
  23 test7.c: (in function t)
  24 test7.c:6:3: Possible out-of-bounds store:
  25     g[2]
  26     Unable to resolve constraint:
  27     requires maxSet(g @ test7.c:4:3) >= 4
  28      needed to satisfy precondition:
  29     requires maxSet(g @ test7.c:6:3) >= 2
  30 test7.c:8:3: Possible out-of-bounds store:
  31     j[0]
  32     Unable to resolve constraint:
  33     requires maxSet(j @ test7.c:8:3) >= 0
  34      needed to satisfy precondition:
  35     requires maxSet(j @ test7.c:8:3) >= 0
  36
  37 Finished checking --- 7 code warnings, as expected