| | 1 | |
| | 2 | Finished checking --- no warnings |
| | 3 | |
| | 4 | maxsetnoannotations.c: (in function noancopy) |
| | 5 | maxsetnoannotations.c:2:3: Possible out-of-bounds store: |
| | 6 | strcpy(a, b) |
| | 7 | Unable to resolve constraint: |
| | 8 | requires maxSet(a @ maxsetnoannotations.c:2:11) >= maxRead(b @ |
| | 9 | maxsetnoannotations.c:2:13) |
| | 10 | needed to satisfy precondition: |
| | 11 | requires maxSet(a @ maxsetnoannotations.c:2:11) >= maxRead(b @ |
| | 12 | maxsetnoannotations.c:2:13) |
| | 13 | derived from strcpy precondition: requires maxSet(<parameter 1>) >= |
| | 14 | maxRead(<parameter 2>) |
| | 15 | |
| | 16 | Finished checking --- 1 code warning, as expected |
andersk / splint.git / blame_incremental