]>
Commit | Line | Data |
---|---|---|
98ed3b22 | 1 | |
2 | mystrncat.c: (in function func) | |
3 | mystrncat.c:12:13: Passed storage buffer not completely defined (*buffer is | |
4 | undefined): mystrncat (buffer, ...) | |
5 | mystrncat.c:13:13: Passed storage b not completely defined (*b is undefined): | |
6 | mystrncat (b, ...) | |
7bf96067 | 7 | mystrncat.c:12:3: Possible out-of-bounds store: |
8 | Unable to resolve constraint: | |
4109ede4 | 9 | requires maxRead(buffer @ mystrncat.c:12:13) <= 0 |
b9904f57 | 10 | needed to satisfy precondition: |
4109ede4 | 11 | requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @ |
12 | mystrncat.c:12:13) + 255 | |
13 | derived from mystrncat precondition: | |
14 | requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3> | |
7bf96067 | 15 | mystrncat.c:13:3: Possible out-of-bounds store: |
16 | Unable to resolve constraint: | |
4109ede4 | 17 | requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0 |
02984642 | 18 | needed to satisfy precondition: |
4109ede4 | 19 | requires maxSet(b @ mystrncat.c:13:13) >= maxRead(b @ mystrncat.c:13:13) + |
20 | 255 | |
21 | derived from mystrncat precondition: | |
22 | requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3> | |
98ed3b22 | 23 | |
11db3170 | 24 | Finished checking --- 4 code warnings, as expected |