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

change labelling for some Juliet tasks. #1236

Closed kfriedberger closed 3 years ago

kfriedberger commented 3 years ago

Those tasks all contain the same behaviour: They allocate some memory and store a reference to it in a global static variable CWE401_Memory_Leak__TASKNAME_badData that is never freed and remains reachable beyond the exit of the main function.

Found by CPAchecker (SMG analysis).

PhilippWendler commented 3 years ago

Previously, these tasks were claimed to violate memsafety. Now you are saying that they don't, and only memcleanup is violated? (This is the actual effect of this PR, but your description explains only that they do violate memcleanup, but doesn't say anything about memsafety.)

kfriedberger commented 3 years ago

You are right. The tasks do not violate any memsafety property, but only memcleanup.

kfriedberger commented 3 years ago

The name CWE401_Memory_Leak is misleading, the "leak" does only appear on program exit. There is an internal function badsink() that is called before returning and exiting. Maybe there is some missing documentation or convention about that function.

dbeyer commented 3 years ago

It is a common misconception that some people call it memleak when it really is only not yet deallocated just before the exit.

dbeyer commented 3 years ago

In the community meeting, people were in favor of merging here, and excluding the new verification tasks in the benchmark-definition XML files.

lucasccordeiro commented 3 years ago

@dbeyer: May I ask you whether you will remove all Juliet verification tasks? Or will you remove just the ones mentioned in this PR?