sv-benchmarks
sv-benchmarks copied to clipboard
sosy-lab
Collection of Verification Tasks (MOVED, please follow the link)
There were at least two cases (#979, #1036) where a freed pointer was accessed (read) afterwards. According to ISO-C99 6.2.4(2), the value of a pointer becomes indeterminate when the object...
test27-2.c isn't memory safe (neither was memory safe before nor is now), and test27-1.c is memory safe irrespective of the value used here as that value is never read. I've...
... other than those explicitly listed in the SV-COMP rules. As initially many benchmarks will violate this check, a blacklist needs to be maintained. I will push for this as...
For example: https://github.com/sosy-lab/sv-benchmarks/blob/b61ec96df19679bf5a65ec48ec1651ad2c8a0374/c/aws-c-common/aws_byte_buf_cat_harness.i#L9113 leading to undefined behavior in the test harness.
The problem was the following: The collection clauses/BOOL/slam.zip was checked in as a zip archive in the SVN repository (the previous version of this repo), while the repository directory clauses/...
Link to the current version of the program: [c/loops/eureka_01-1.c@d44f38aa](https://github.com/sosy-lab/sv-benchmarks/blob/d44f38aa398b1d4beef189a068756aa5949c9025/c/loops/eureka_01-1.c) The tasks accesses uninitialized parts of the array `int distance[5]`, which is in the scope of the function `main` (if it...
The AWS-C-Common task `memcpy_using_uint64_harness` contains the following code: https://github.com/sosy-lab/sv-benchmarks/blob/b61ec96df19679bf5a65ec48ec1651ad2c8a0374/c/aws-c-common/memcpy_using_uint64_harness.i#L5936-L5943 As indicated by its name, `memcpy_using_uint64_impl` copies from the array `s` to the array `d2` using an `uint64_t` pointer. According to...
Various device driver benchmarks either completely lack initialisation of pointers passed around or do not suitably initialise members of allocated storage. See #1049 for a (likely incomplete) list of benchmarks,...
In program https://github.com/sosy-lab/sv-benchmarks/blob/36898a735c5fb9bc0c43d3556dd09cd05969f1ef/c/loops/insertion_sort-1.c, `int v[SIZE];` creates a local array on the stack without initialization. Possible solution: Move array declaration outside of function `main`?
WORK IN PROGRESS. This issue discusses the problem with the slow CI and possible solutions. ## Use CCache for GCC and Clang I tried to add `ccache` for the `gcc`...