sosy-lab/sv-benchmarks

Issues

• Repository moved to GitLab

  #1308 opened 3 years ago by dbeyer
  1

• Info on SV-COMP 2022?

  #1305 opened 3 years ago by robdockins
  2

• Use of `__VERIFIER_nondet_*` functions that aren't specified in SV-COMP rules

  #1304 opened 3 years ago by RyanGlScott
  1

• geo1-ll.c can overflow

  #1289 opened 3 years ago by hernanponcedeleon
  3

• Implementation-defined behaviour

  #1290 opened 3 years ago by hernanponcedeleon
  3

• Reachable error in pthread-ext/41_FreeBSD_abd_kbd_sliced

  #1300 opened 3 years ago by schuessf
  0

• Benchmarks for weak memory models

  #1297 opened 3 years ago by hernanponcedeleon
  3

• __builtin_unreachable() in LDV benchmarks

  #1296 opened 3 years ago by sim642
  3

• why can echo-2.i overflow?

  #1295 opened 3 years ago by Cglasses
  2

• Incorrect Verification Task

  #1288 opened 4 years ago by sohah
  0

• "Repeated" benchmarks in pthread-wmm

  #1292 opened 3 years ago by hernanponcedeleon
  0

• SV-COMP concurrency benchmarks with data races

  #1291 opened 3 years ago by fatimahkj
  3

• MemSafety - unset subproperty for false verdict

  #1285 opened 4 years ago by versokova
  0

• Task ntdrivers/diskperf.i.cil-1.c is not memory safe

  #1266 opened 4 years ago by tautschnig
  2

• ntdrivers/parport.i.cil-2 is not memory safe

  #1269 opened 4 years ago by tautschnig
  0

• Undefined Behavior in c/loops/linear_search.c

  #1241 opened 4 years ago by michael-schwarz
  4

• cut-2 and od-1 from busy-box are not memory safe

  #1275 opened 4 years ago by mchalupa
  1

• Undefined behavior in two AWS benchmarks

  #1280 opened 4 years ago by mchalupa
  0

• Task ntdrivers/floppy2 is not memory safe

  #1263 opened 4 years ago by tautschnig
  0

• Tasks in seq-mthreaded wrongly marked as non-terminating

  #1259 opened 4 years ago by tautschnig
  2

• Double free in termination-recursive-malloc/chunk3.i

  #1257 opened 4 years ago by tautschnig
  1

• LDV tasks with undefined behaviour and/or wrong verdicts

  #1270 opened 4 years ago by tautschnig
  3

• Questionable verdict of ldv-validator-v0.8/linux-stable-5934df9-1-111_1a-drivers--scsi--gdth.ko-entry_point_ldv-val-v0.8.cil.out.i

  #1245 opened 4 years ago by zvonimir
  4

• Undefined behaviors in aws_array_list_pop_front_n_harness.i

  #1181 opened 4 years ago by zvonimir
  2

• Incorrectly labeled termination benchmarks in seq-mthreaded/

  #1240 opened 4 years ago by mchalupa
  0

• Uninitialized reads in date-1 in busybox

  #1250 opened 4 years ago by mchalupa
  0

• Incorrectly labeled benchmarks in nla-digibench-scaling

  #1238 opened 4 years ago by mchalupa
  4

• Invalid memsafety labelling of three busybox benchmarks

  #1246 opened 4 years ago by mchalupa
  0

• AWS benchmarks relaying on htonl and friends but spec is not provided - what is their spec?

  #1217 opened 4 years ago by zvonimir
  7

• Inconsistency in unreach-call verdicts for verifythis: tree_del_rec.yml, tree_del_iter.yml and tree_max.yml

  #1237 opened 4 years ago by holznerst
  1

• Duplicate Verification Tasks

  #1234 opened 4 years ago by dbeyer
  3

• missing function definition in goblint-regression benchmarks?

  #1225 opened 4 years ago by omainv
  4

• Question about usage of VERIFIER_assert

  #1224 opened 4 years ago by amordahl
  5

• Verdict for ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--mtd--sm_ftl.ko.cil.i

  #1233 opened 4 years ago by zvonimir
  1

• Broken generation script

  #1198 opened 4 years ago by hernanponcedeleon
  5

• Unreach-call verdict of ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--media--dvb-core--dvb-core.ko-entry_point.cil.out.yml

  #1207 opened 4 years ago by sim642
  4

• Reachability benchmarks with overflow

  #1166 opened 4 years ago by hernanponcedeleon
  4

• CI for coverage properties

  #1213 opened 4 years ago by lembergerth
  1

• Issue with zilu benchmark

  #1159 opened 4 years ago by hernanponcedeleon
  10

• Repeated benchmarks

  #1176 opened 4 years ago by hernanponcedeleon
  1

• Why is real-world busybox code rewritten into something artificial and weird?

  #1205 opened 4 years ago by zvonimir
  4

• Put scripts into the repository instead of into commit messages

  #1150 opened 4 years ago by MartinSpiessl
  10

• Competition organizers need to fix web site

  #1151 opened 4 years ago by dbeyer
  1

• Undefined behavior overlooked in a couple of array programs in PR #835

  #1173 opened 4 years ago by divyeshunadkat
  6

• Seeding bugs in AWS benchmarks

  #1183 opened 4 years ago by zvonimir
  4

• Linter for the Java tasks

  #1170 opened 4 years ago by mmuesly
  2

• Undefined behaviour of struct without members

  #1160 opened 4 years ago by KenjiroLotus
  1

• Document and improve PR merge policy

  #1149 opened 4 years ago by MartinSpiessl
  3

• How to proceed with the `.cfg` files?

  #1134 opened 4 years ago by MartinSpiessl
  4

• build fail after inserting assert(0) in body of reach error

  #1135 opened 4 years ago by skanav
  6