Submission of some small bitvector benchmarks.


git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@235 770dfece-24ca-4306-9060-4abab334d2a5
Submission of benchmarks for regression verification
created from Linux device drivers.


git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@237 770dfece-24ca-4306-9060-4abab334d2a5
Make license explicit

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@239 770dfece-24ca-4306-9060-4abab334d2a5
Make license explicit (2)

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@240 770dfece-24ca-4306-9060-4abab334d2a5
Make license explicit (3)

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@241 770dfece-24ca-4306-9060-4abab334d2a5
Make license explicit (4)

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@242 770dfece-24ca-4306-9060-4abab334d2a5
Patch by Jonas Wagner that removes all occurrences of (deprecated) nondet_int in favor of __VERIFIER_nondet_int.

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@245 770dfece-24ca-4306-9060-4abab334d2a5
Patch by Jiri Slaby for intializing memory that is allocated and accessed without prior initialization.

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@246 770dfece-24ca-4306-9060-4abab334d2a5
Contributed by Alexander Schremmer.
Add new benchmarks that exercise heap semantics of the tools. The
list-properties/*.c files are similar to their safe counterparts - I
usually just swapped constants. The heap-manipulation/tree* files are
new benchmarks that build a simple tree and check certain data
properties about it.

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@247 770dfece-24ca-4306-9060-4abab334d2a5
Recursive C programs, contributed by Matthias Heizmann.

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@248 770dfece-24ca-4306-9060-4abab334d2a5
Contributed by Alexander Driemeyer and Stefan Löwe

benchmarks adapted from
- original benchmarks developed by the maintainers of the BLAST project
- original benchmarks developed by the maintainers of the PREDATOR project

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@249 770dfece-24ca-4306-9060-4abab334d2a5
Verification tasks from the RERS Grey Box Challenge 2012. Submitted by Stefan Loewe

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@250 770dfece-24ca-4306-9060-4abab334d2a5
Contributed by the LDV project

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@251 770dfece-24ca-4306-9060-4abab334d2a5
Renaming of LDV directories

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@252 770dfece-24ca-4306-9060-4abab334d2a5
Linux drivers from the LDV team. Submitted by Vadim Mutilin.

git-svn-id: https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c@253 770dfece-24ca-4306-9060-4abab334d2a5
avoid defining assert function

Call it __VERIFIER_assert instead. Like in the other benchmarks. This
allows tools to include assert.h properly.
loops: initialize uninitalized
bitvector: fix all uninitialized accesses

Now symbiotic gives no false answers on these benchmarks 8-).
ldv: initialize more uninitialized variables
ntdrivers/cdaudio_unsafe.i.cil.c: fix final symbiotic fallout

This is the last one where we give incorrect results. Fix that by
intializing memory that is allocated and accessed without prior
initialization.