2 buffertest1.c: (in function t1)
3 buffertest1.c:5:3: Variable g used before definition
4 buffertest1.c:5:3: Possible out-of-bounds store:
5 Unable to resolve constraint:
6 requires maxSet(g @ buffertest1.c:5:3) >= 100
7 needed to satisfy precondition:
8 requires maxSet(g @ buffertest1.c:5:3) >= 100
9 buffertest1.c: (in function t2)
10 buffertest1.c:20:3: Variable g used before definition
11 buffertest1.c:21:3: Possible out-of-bounds store:
12 Unable to resolve constraint:
13 requires maxSet(g @ buffertest1.c:20:3) >= 1
14 needed to satisfy precondition:
15 requires maxSet(g @ buffertest1.c:21:3) >= 0
16 buffertest1.c:21:10: Possible out-of-bounds read:
17 Unable to resolve constraint:
18 requires maxRead(g @ buffertest1.c:20:3) >= 2
19 needed to satisfy precondition:
20 requires maxRead(g @ buffertest1.c:21:10) >= 1
22 Finished checking --- 5 code warnings, as expected