]>
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, ...) | |
16c024b5 | 7 | mystrncat.c:10:3: Storage *b allocated |
7bf96067 | 8 | mystrncat.c:12:3: Possible out-of-bounds store: |
9276a168 | 9 | mystrncat(buffer, str, sizeof((buffer)) - 1) |
7bf96067 | 10 | Unable to resolve constraint: |
4109ede4 | 11 | requires maxRead(buffer @ mystrncat.c:12:13) <= 0 |
b9904f57 | 12 | needed to satisfy precondition: |
4109ede4 | 13 | requires maxSet(buffer @ mystrncat.c:12:13) >= maxRead(buffer @ |
14 | mystrncat.c:12:13) + 255 | |
15 | derived from mystrncat precondition: | |
16 | requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3> | |
7bf96067 | 17 | mystrncat.c:13:3: Possible out-of-bounds store: |
9276a168 | 18 | mystrncat(b, str, sizeof((buffer)) - 1) |
7bf96067 | 19 | Unable to resolve constraint: |
4109ede4 | 20 | requires maxRead(malloc(256) @ mystrncat.c:10:7) <= 0 |
02984642 | 21 | needed to satisfy precondition: |
4109ede4 | 22 | requires maxSet(b @ mystrncat.c:13:13) >= maxRead(b @ mystrncat.c:13:13) + |
23 | 255 | |
24 | derived from mystrncat precondition: | |
25 | requires maxSet(<parameter 1>) >= maxRead(<parameter 1>) + <parameter 3> | |
98ed3b22 | 26 | |
11db3170 | 27 | Finished checking --- 4 code warnings, as expected |