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

ntdrivers/floppy2 is not memory safe #1264

Closed tautschnig closed 3 years ago

tautschnig commented 3 years ago

Much like floppy.i.cil-1.c, floppy2.i.cil.c uses _SLAM_alloc_dummy to implement malloc, and thus memory safety cannot be ensured. Thus change the verdict, removing termination and unreach-call, adding valid-memsafety(false) instead.

Fixes: #1263

mchalupa commented 3 years ago

I can confirm the invalid dereference.

sim642 commented 3 years ago

Oh also, I think you meant floppy2.i.cil.c is like floppy.i.cil-2.c, not floppy.i.cil-1.c because the latter doesn't contain _SLAM_alloc_dummy. Just like that pair of tasks, it might make sense to hopefully fix the original one by removing the malloc definition and keeping the invalid deref version as a copy.