]>
Commit | Line | Data |
---|---|---|
754e4dbd | 1 | |
11db3170 | 2 | Finished checking --- no warnings |
754e4dbd | 3 | |
4 | maxsetnoannotations.c: (in function noancopy) | |
7bf96067 | 5 | maxsetnoannotations.c:2:3: Possible out-of-bounds store: |
9276a168 | 6 | strcpy(a, b) |
7bf96067 | 7 | Unable to resolve constraint: |
4109ede4 | 8 | requires maxSet(a @ maxsetnoannotations.c:2:11) >= maxRead(b @ |
9 | maxsetnoannotations.c:2:13) | |
03d670b6 | 10 | needed to satisfy precondition: |
4109ede4 | 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>) | |
754e4dbd | 15 | |
11db3170 | 16 | Finished checking --- 1 code warning, as expected |