marek-trtik cbmc issues

marek-trtik / cbmc

C Bounded Model Checker

http://www.cprover.org/cbmc

Other

0 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Incorrect TRUE for ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--misc--legousbtower.ko_false-unreach-call.cil.c

#39 lucasccordeiro opened 6 years ago
5
Incorrect TRUE for warning: ignoring bswap

#38 lucasccordeiro opened 6 years ago
4
Incorrect FALSE related to pointer outside dynamic object bounds

#37 lucasccordeiro opened 6 years ago
9
Incorrect FALSE detected in function strcpy (module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i)

#36 lucasccordeiro opened 6 years ago
6
Incorrect FALSE detected in function strncpy (43_1a_cilled_true-unreach-call_ok_nondet_linux-43_1a-drivers--power--test_power.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c)

#35 lucasccordeiro opened 6 years ago
3
No violation node for some benchmarks in the memory safety category

#34 lucasccordeiro opened 6 years ago
3
Type-checking failure: "numeric exception"/"identifier XYZ not found"

#33 marek-trtik opened 6 years ago
6
RED status - strcpy/memcpy

#32 marek-trtik closed 6 years ago
2
Fixing: cannot unpack struct with non-byte aligned components

#31 marek-trtik closed 6 years ago
1
Fixing: warning: ignoring array_of

#30 marek-trtik closed 6 years ago
3
Fixing: implicit conversion not permitted

#29 marek-trtik closed 6 years ago
2
Fixing: byte_update of unknown width: byte_update_little_endian

#28 marek-trtik closed 6 years ago
2
Fixing: pointer handling for concurrency is unsound

#27 marek-trtik closed 6 years ago
2
Fixing: too many addressed objects

#26 marek-trtik closed 6 years ago
4
Fixing: too many addressed objects: maximum number of objects is set to 2^n=256 (with n=8);

#25 lucasccordeiro closed 6 years ago
2
Fixing: equality without matching types

#24 marek-trtik closed 6 years ago
13
Fixing: byte_extract flatting with negative offset: byte_extract_little_endian

#23 marek-trtik closed 6 years ago
2
18 red memsafety benchmarks

#22 marek-trtik closed 6 years ago
4
Improve the witness generation for ProductLines, Floats, and Sequentialized

#21 lucasccordeiro opened 7 years ago
0
OBSOLETE

#20 marek-trtik closed 7 years ago
0
11 memsafety issues

#19 marek-trtik closed 6 years ago
13
ldv_assert failure

#18 marek-trtik closed 6 years ago
2
19+3 guard failures of memcpy and strcpy

#17 marek-trtik closed 6 years ago
2
[NOT URGENT] mem-cleanup property

#16 peterschrammel closed 6 years ago
6
Benchmark: `product-lines/email_spec27_productSimulator_false-unreach-call_true-termination.cil.c`

#15 marek-trtik closed 7 years ago
1
[NOT URGENT] Support for variable arrays.

#14 marek-trtik opened 7 years ago
0
CBMC shell script has different behaviour in different machines/OSs

#13 lucasccordeiro opened 7 years ago
3
CBMC incorrectly provides false(unreach-call) in memleaks_test3_false-valid-free.i

#12 lucasccordeiro closed 7 years ago
2
Write the witness file for concurrent programs

#11 lucasccordeiro opened 7 years ago
20
No outgoing edges from violation nodes

#10 peterschrammel closed 7 years ago
2
Benchmark: list-ext-properties/test-0214_1_true-valid-memsafety.i

#9 marek-trtik closed 7 years ago
4
Benchmark: loop-acceleration/array_false-unreach-call2_true-termination.i

#8 marek-trtik closed 6 years ago
3
Benchmark: float-benchs/inv_Newton_false-unreach-call.c

#7 marek-trtik closed 6 years ago
3
Benchmark: ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i

#6 marek-trtik closed 7 years ago
4
Benchmark: ntdrivers/diskperf_true-unreach-call.i.cil.c

#5 marek-trtik closed 6 years ago
11
SV-COMP 2018: diff "CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr: Fixing `ntdrivers/diskperf_true-unreach-call.i.cil.c`

#4 marek-trtik closed 7 years ago
1
Benchmark: ntdrivers/floppy2_true-unreach-call.i.cil.c

#3 marek-trtik closed 6 years ago
8
SV-COMP 2018: diff "CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr: Fixing `ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety.i`

#2 marek-trtik closed 7 years ago
11
SV-COMP 2018: diff "CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr: Fixing `bitvector/modulus_true-unreach-call_true-no-overflow.i`

#1 marek-trtik closed 7 years ago
4