New category for undefined behavior? about sv-benchmarks HOT 9 OPEN

Conclusion: For SV-COMP 2017, we leave the invalid derefs and invalid frees in MemSafety,
and the invalid overflows in Overflows.
Next time we reconsider adding a property for checking undefined variables and have another
category capturing this.

Compare with issue #270.

from sv-benchmarks.

We could generalise memory leaks to "resource leaks", which is a class of practically relevant problems. (And then, finally, the Infer team might want to join.)

from sv-benchmarks.

from sv-benchmarks.

Just to clarify, you are not suggesting that we add additional properties to check (such as undefined behaviors that are currently not specified/caught as SV-COMP properties), but rather only to restructure the benchmarks/categories. Is that right?

from sv-benchmarks.

That is right.
But we should have new properties in mind (for demo category or next year),
such as _no-undef-vars or so, in order to more thoroughly check for undefined behavior.
Even if we do not have a category of this in SV-COMP, it would be good for the
definedness checkers to provide a defined playground to them in the repository.

from sv-benchmarks.

Absolutely! That would be super valuable for a demo category and next year as well!

from sv-benchmarks.

Are we on a path to ending the never-ending category debate?

from sv-benchmarks.

I presume you changed the SVG in the current file, the main categories are Reachability, Memory Safety, Overflows, Concurrency, Termination, and Software Systems.

I think, we should not (neither now nor in the future) have a property "undefined behaviour". There are many kinds of undefined behaviour we might want to have a property for each of them and want to check them individually (wherever possible) because we want to attract also tools that check only some of these properties.

Regarding the other questions I do not have strong preferences. I fine with your current suggestions (SVG above).

from sv-benchmarks.

_false-def-behavior

is the label to mark programs that have undefined behavior different from

• invalid dereference (_false-valid-deref),
• invalid deallocation (_false-valid-free), and
• invalid overflows of signed integer variables (_false-no-overflow).

from sv-benchmarks.