| | 1 | |
| | 2 | constannot.c: (in function foo2) |
| | 3 | constannot.c:11:3: Possible out-of-bounds store: |
| | 4 | str[20] |
| | 5 | Unable to resolve constraint: |
| | 6 | requires maxSet(str @ constannot.c:11:3) >= 20 |
| | 7 | needed to satisfy precondition: |
| | 8 | requires maxSet(str @ constannot.c:11:3) >= 20 |
| | 9 | constannot.c: (in function foo3) |
| | 10 | constannot.c:20:3: Possible out-of-bounds store: |
| | 11 | foo(buf) |
| | 12 | Unable to resolve constraint: |
| | 13 | requires <const int=20> <= 19 |
| | 14 | needed to satisfy precondition: |
| | 15 | requires maxSet(buf @ constannot.c:20:8) >= <const int=20> |
| | 16 | derived from foo precondition: requires maxSet(<parameter 1>) >= <const |
| | 17 | int=20> |
| | 18 | |
| | 19 | Finished checking --- 2 code warnings, as expected |
andersk / splint.git / blame_incremental