sosy-lab/sv-benchmarks

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

tautschnig opened this issue · 2 comments

tautschnig commented

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) f885f71, which first invokes malloc, but then resets the points to NULL. (Before this commit, there were two calls to __VERIFIER_nondet_pointer().)

mchalupa commented

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

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:

sv-benchmarks/c/ntdrivers/diskperf.i.cil-1.c

Line 3368 in efea738

devobj.DeviceExtension = malloc(sizeof(struct _DEVICE_EXTENSION));

sv-benchmarks/c/ntdrivers/diskperf.i.cil-1.c

Line 3435 in efea738

devobj.DeviceObjectExtension = (struct _DEVOBJ_EXTENSION *)0;