sv-benchmarks
sv-benchmarks copied to clipboard
sosy-lab
Collection of Verification Tasks (MOVED, please follow the link)
It would be nice to include a new function into the benchmark rules void *__VERIFIER_base_pointer(void *ptr); that denotes the base pointer of an object, similarly to [__CPROVER_POINTER_OBJECT](http://www.cprover.org/cprover-manual/api/) as supported by...
At the moment there are a lot of Juliet benchmark c programs which are not yet categorized and pre processed. Furthermore some of the benchmarks uses non c99 standard functions...
Integrate property definitions for standard exceptions. There are various examples in the code base of SV-COMP triggering standard exceptions. As these are standard exceptions, Java verification tools should be able...
Benchmark `c/ldv-regression/fo_test.i` has the following sequence of calls: `int file = l_open("unknown",00);` where `l_open` eventually returns `__VERIFIER_nondet_int()` ... `int a = l_read(file,cbuf,99);` where `l_read` calls `read(file, ...)` But `read` is...
I believe there can be signed integer underflow in [termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i](https://sv-comp.sosy-lab.org/2019/results/sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i). In `main` 0 is passed as `n` to `new_cll`, hence -1 is passed to `new_lseg` as `n` which is recursively...
There can be an invalid dereference in benchmark [loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i](https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i) on line [61](https://github.com/sosy-lab/sv-benchmarks/blob/15b5d973979ad445f45dde28dd9c46deb14542ef/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i#L61) which leads to undefined behavior. The benchmark is labeled as false-unreach-call, which means that the assertion `__VERIFIER_assert(j -...
The benchmark `ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--input--touchscreen--penmount.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c` contains multiple invalid dereferences. On this link you can find a witness for one of the errors (invalid dereference on line 2852, due to the fact that...
The `c/array-multidimensional/add-3-n-u_true-unreach-call` benchmark contains following variables: ```c int i,j,k; int m=1000,n=1500,p=1800; unsigned int A [m][n][p]; unsigned int B [m][n][p]; unsigned int C [m][n][p]; ``` This should allocate 30 GB of...
The following tasks in `float-newlib` contain deliberate floating-point division by zero: ``` double_req_bl_0910a_true-unreach-call.c double_req_bl_0910b_true-unreach-call.c double_req_bl_0920a_true-unreach-call.c double_req_bl_0920b_true-unreach-call.c double_req_bl_0921_true-unreach-call.c double_req_bl_0930_true-unreach-call.c double_req_bl_0931_true-unreach-call.c double_req_bl_0960b_true-unreach-call.c double_req_bl_0970a_true-unreach-call.c double_req_bl_0970b_true-unreach-call.c double_req_bl_0971_true-unreach-call.c double_req_bl_0981_true-unreach-call.c float_req_bl_0910a_true-unreach-call.c float_req_bl_0910b_true-unreach-call.c float_req_bl_0920a_true-unreach-call.c float_req_bl_0920b_true-unreach-call.c float_req_bl_0921_true-unreach-call.c float_req_bl_0930_true-unreach-call.c...
Hi, I am getting a counterexample for which __VERIFIER_error is reachable in the program loop-floats-scientific-comp/loop4_true-unreach-call.c. The violation witness is also validated by CPAchecker. Is anyone else facing the same issue...
