sv-benchmarks
sv-benchmarks copied to clipboard
sosy-lab
Collection of Verification Tasks (MOVED, please follow the link)
It would be good to improve the compilation checks that are executed for all benchmarks: - [ ] Read architecture of files from official `Category.cfg` task-definition files instead of `Makefile`...
Please add other open points about the category structure for this year's SV-COMP to this issue once they surface. - Juliet Tasks: From last year (https://github.com/sosy-lab/sv-benchmarks/issues/819) we still have to...
*This is part 2 of two closely related issues, the first one (#1123) building the base for implementing this one.* We could try to allow for unpreprocessed program files to...
*This is part 1 of two closely related issues, the second one (#1124) building upon this one.* It has become more and more labor-intensive over the past years to maintain...
I've been investigating an issue that Clang has been warning about all over the place (-Wincompatible-library-redeclaration) and I'd like to draw attention to it because it implies that people who...
I read up a bit about the [Apache License 2.0](https://www.apache.org/licenses/LICENSE-2.0) and found out that it requires at point 4 b): > You must cause any modified files to carry prominent...
At least some of the tasks added in PR #808 contain overflows of signed integer variables, i.e. undefined behavior. Examples are [`divbin.c` in line 30](https://github.com/sosy-lab/sv-benchmarks/blob/ea7880ba32cb1c3c5a6276a29ded8efe29194a06/c/nla-digbench/divbin.c#L30)(multiplication of nondeterminisic signed integer with...
Creation of a StringBuilder with an input string of size `Integer.MAX_INT-15` will cause an `NegativeArraySizeException` during construction: https://github.com/sosy-lab/sv-benchmarks/blob/f86649d39588b62689bc63ae84f8ff53582b4d51/java/jbmc-regression/StringBuilderConstructors01/Main.java#L13-L19 Looking into the library the constructors are defined as follows: ```java public...
I would like to ask how unspecified method contracts should be handled. For example, the JDK I use explicitly throws ```java.lang.OutOfMemoryError``` inside the function ```java.lang.AbstractStringBuilder.hugeCapacity```. Now, I detect bugs, which...
Several benchmarks have calls to string functions that are not defined in the benchmark files. For instance, the following benchmarks have calls to `strcpy` without defining it: `c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i` `c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--platform--x86--topstar-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i` `c/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i`...
