search

sosy-lab / sv-benchmarks

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

Task ntdrivers/diskperf.i.cil-1.c is not memory safe #1266

Closed tautschnig closed 3 years ago

tautschnig commented 3 years ago

The task sets devobj.DeviceExtension to NULL, but later on tries to access members of this struct. This is due to an error in (my commit) f885f716b5bd, which first invokes malloc, but then resets the points to NULL. (Before this commit, there were two calls to __VERIFIER_nondet_pointer().)

mchalupa commented 3 years ago

The task sets devobj.DeviceExtension to NULL

@tautschnig I cannot find this, I guess that should be devobj.DeviceObjectExtension according to your PR? But then I cannot find where DeviceObjectExtension is used in the code...

sim642 commented 3 years ago

This is due to an error in (my commit) f885f71, which first invokes malloc, but then resets the points to NULL.

These assignments are done to different fields though:

https://github.com/sosy-lab/sv-benchmarks/blob/efea7382584f8f664ee590f189a83485ff761e0b/c/ntdrivers/diskperf.i.cil-1.c#L3368

https://github.com/sosy-lab/sv-benchmarks/blob/efea7382584f8f664ee590f189a83485ff761e0b/c/ntdrivers/diskperf.i.cil-1.c#L3435