Busybox fixes #513
Busybox fixes #513
Conversation
There was a problem hiding this comment.
The commit b16e0cd "Busybox: Remove conflicting memory safety property" claims it is about #480, but in fact it targets a different problem. This problem is actually not necessarily a problem: Some files have _false-unreach-call and _true-valid-memsafety, but we have noticed in the past that most programs do not not do a proper memory cleanup before calling __VERIFIER_error, so it is highly probably that these programs have a leak and are not _true-valid-memsafety. This commit now simplify removes all claims about memsafety from these files. I am ok with that. @dbeyer?
The busybox part of #480 is fixed by the other commits of this PR, and #444 and #511 are addressed as well.
Thus, I would approve if the above question is resolved.
|
I'm obviously happy to drop b16e0cd from this PR if this is not the way to go. |
|
Calling __VERIFIER_error does not cause a __false-valid-memtrack, but a __false-valid-memcleanup. |
So |
|
Ok, I think the check is older than the distinction between |
The version without undefined behaviour, where additional properties can be checked, already exists in the repository.
This is a follow-up to d115b6f, where the null-pointer dereference has been discussed.
tautschnig
force-pushed
the
busybox-fixes
branch
from
1c4c2b4 to
2035c67
Compare
|
Thanks @PhilippWendler - patch dropped and series rebased. |
| @@ -107,7 +107,7 @@ static void bb_error_msg_and_die(const char *s, ...) | |||
| // file ./libbb-dump.i line 1 | |||
| static void bb_show_usage(void) | |||
| { | |||
| ; | |||
| abort(); | |||
There was a problem hiding this comment.
Related to the discussions in some other PRs: should this be __VERIFIER_assume(false)?
There was a problem hiding this comment.
It would work for the moment, but would cause havoc when someone steps up to add termination analysis/labels to the benchmark?!
There was a problem hiding this comment.
I think 'abort' is best: (a) does not have a loop and (b) is a proper C call.
Addresses issues about the busybox benchmarks raised in #444 and #480 and #511.