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