sosy-lab/sv-benchmarks

Invalid memsafety labelling of three busybox benchmarks

mchalupa opened this issue · 0 comments

Benchmarks mkdir-2, seq-1, and touch-2 are labeled as true, but should be labeled false(valid-deref), as can be witnessed by the attached harness files: harness.zip (just compile the benchmark with the harness file and -fsanitize=address,undefined and execute the binary to check that).

The problem is (at least in two of them that I checked) that the function bb_show_usage() does not abort the code and invalid pointer is accessed (the original implementation of this function from BusyBox code does that).