sosy-lab/sv-benchmarks

Question about usage of VERIFIER_assert

amordahl opened this issue · 5 comments

amordahl commented

Hello,

I am curious about the standard usage of VERIFIER_assert in the C benchmark. I have two main questions:

  1. By my count, the vast majority of usages of this macro are in reachability tasks, but there are a few usages in overflows valid memsafety and def behavior tasks. Is there any reasoning as to why some benchmarks use VERIFIER_assert and others do not?

  2. In tasks that have multiple calls to VERIFIER_assert (e.g., sv-benchmarks/c/seq-pthread/cs_queue-1.c), are all of these assertions checking the property (in this case, reachability)? Or are only some checking the property and others doing something else?

Thank you!

amordahl commented

Apologies, accidentally pressed enter before I was done writing. Please give me a few minutes to write the body of this question :)

PhilippWendler commented

__VERIFIER_assert is just an arbitrary utility function that happens to be exist in many tasks, but it has no special meaning at all. The only reason it exists is that some people find it useful to introduce such a utility function. The function may or may not have a similar implementation across the various tasks.

In particular, tools that analyze these tasks should not add any special handling for __VERIFIER_assert and specifically not assume that it somehow encodes the safety property. As property, tools should only use what is specified in the accompanying property file.

Does this answer your questions?

amordahl commented

Thanks for your reply. That does answer my questions, but I have a follow up. If we cannot make any assumptions about the usage of __VERIFIER_assert, then for tasks that are unsafe, is there any way to tell which specific part of the code is unsafe?

PhilippWendler commented

This information is not present in this repository. However, you can have a look at where these tasks are used, e.g., at SV-COMP, and check what other tools reported for a given task. All results from the last years of SV-COMP need to come with witnesses, which should give more information about a specification violation.

amordahl commented

Thank you for your responses, Philipp. This answers my questions. Closing the issue now.