sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

Uninitialized reads in date-1 in busybox #1250

Closed mchalupa closed 3 years ago

mchalupa commented 3 years ago

The date-1 benchmark in busybox contains an uninitialized read on several paths. One path is again because the bb_show_usage function does not abort the program. The other path arises probably due to the approximation of modeling the posix environment. Here is a test harness that you can use to reproduce the issues (compile the harness with date-1.i and -fsanitize=memory). harness.zip