sv-benchmarks

sv-benchmarks copied to clipboard

Score schema for the SoftwareSystems category

8

Hi all, I'm running some tests now and just saw the distribution for the SoftwareSystems category: Systems_BusyBox_MemSafety: 52 benchmarks Systems_BusyBox_Overflows: 52 benchmarks Systems_DeviceDriversLinux64_ReachSafety: 2796 benchmarks Given our meta category score...

mikhailramalho

Benchmarks depending on undefined functions in DeviceDriversLinux64

27

Hi, in those benchmarks there are calls to functions (or dereference of an external variable in one case) that are not defined and then a decision is made based on...

mchalupa

ntdriver benchmarks are not memory safe

9

Hi, I was just going through this `ntdrivers/kbfiltr_false-unreach-call_true-valid-memsafety.i.cil.c` benchmark again (#290) and found out that it is still not memory safe at all. There is a bunch of places where...

mchalupa

Files with known overflows outside of Bitvector category

6

This year several tasks with unsigned overflows have been added to some categories, e.g., in #234. In previous years, such tasks have been moved to the BitVectorsReach category and other...

PhilippWendler

New category for undefined behavior?

9

Currently, we have this structure for SV-COMP 2017: https://sv-comp.sosy-lab.org/2017/categories.svg The main categories Arrays, BitVectors, and HeapDataStructures contain each a sub-category for memsafety or overflows, which in turn represent undefined behavior...

dbeyer

Ping original submitters to fix errors spotted by continuous integration checks

5

Hi, In #4, #5, #6 I have provided patches for those benchmarks that I have submitted or feel somewhat responsible for. check-blacklist nevertheless still lists 3560 broken benchmarks, which ought...

tautschnig

seq-pthread benchmarks have misleading indentation

2

``` cs_queue_true-unreach-call.i: In function ‘empty’: cs_queue_true-unreach-call.i:1048:2: warning: this ‘else’ clause does not guard... [-Wmisleading-indentation] else ^~~~ cs_queue_true-unreach-call.i:1049:14: note: ...this statement, but the latter is misleadingly indented as if it is...

delcypher

Increase Traceability and Reduce Maintenance Effort for Verification Tasks

3

- How to generate the .i files automatically from the .c files? - How to remember architecture dependencies? - How to better reflect what the intentions of a verification tasks...

dbeyer

seq-mthread/pals_STARTPALS_ActiveStandby* benchmarks have suspicious self comparision

1

Clang is emitting a lot of warnings of the same type for some very suspicious looking code in the `seq-mthread/pals_STARTPALS_ActiveStandby*.c` benchmarks. The warnings look similar to this: ``` pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c:320:22: warning:...

delcypher

veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i has tautological compare

1

``` clang building /loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i:29:24: warning: comparison of unsigned expression >= 0 is always true [-Wtautological-compare] __VERIFIER_assert (i >= 0); ~ ^ ~ 1 warning generated. ```

delcypher