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

Task ntdrivers/floppy2 is not memory safe #1263

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. The task should have the verdicts changed.