search

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

Busybox memsafety fixes #1277

Closed mchalupa closed 3 years ago

mchalupa commented 3 years ago

Fix labeling of two busybox benchmarks, see #1275 .

tautschnig commented 3 years ago

@mchalupa Could we fix the benchmarks instead of altering the verdict?

mchalupa commented 3 years ago

@tautschnig The fix would be to forbid the paths on which getop32 does not initialize the variables, but I was not sure how to do that properly. However, I could initialize the variables to null and check for null before their dereference. That should work and it will probably not change the intended behavior of the benchmark.

mchalupa commented 3 years ago

Actually, it seems that the fix could be as easy as initializing the variables to "".

mchalupa commented 3 years ago

I preserved the altered verdicts and I added the fixed benchmarks as new benchmarks (-3 suffix).