#1 |
Fix memory leaks in DiOS
|
|
defect
|
major
|
4.2
|
DiOS
|
#5 |
Invalid YAML report for programs with options or stdin
|
mornfall
|
defect
|
major
|
5.0
|
UI
|
#7 |
Problems with --symbolic in SV-COMP benchmarks
|
|
defect
|
major
|
4.2
|
DiOS
|
#8 |
Missing or spurious ODBC dependency
|
mornfall
|
defect
|
major
|
5.0
|
bench
|
#9 |
Problem with cast form abstract int to abstract pointer.
|
Henrich Lauko
|
defect
|
major
|
4.2
|
LART
|
#12 |
Have both versions of strerror_r
|
|
defect
|
major
|
4.2
|
DiOS
|
#13 |
pass CMake pthreads check
|
blurrymoi
|
defect
|
major
|
5.0
|
divcc
|
#14 |
Allow programs to override libc symbols
|
mornfall
|
defect
|
major
|
5.0
|
DiOS
|
#20 |
Use error output for actual errors only
|
mornfall
|
defect
|
minor
|
5.0
|
UI
|
#23 |
divine cc -c -Ipath does not work
|
blurrymoi
|
defect
|
major
|
5.0
|
divcc
|
#24 |
divcc needs native libc++ and libc++abi to build C++ programs
|
|
defect
|
major
|
4.3
|
DiOS
|
#27 |
build filaure (fatal error: dios.h: No such file or directory)
|
mornfall
|
defect
|
major
|
5.0
|
other
|
#28 |
Capturing symbolically linked files seem to crash DiOS
|
mornfall
|
defect
|
minor
|
5.0
|
DiOS
|
#29 |
Add/fix divcc --version and --help
|
blurry
|
defect
|
major
|
5.0
|
divcc
|
#38 |
Report attempts to use symbolic data if symbolic is disable
|
mornfall
|
defect
|
major
|
5.0
|
other
|
#41 |
Faults that are suppressed should not appear in the trace
|
|
defect
|
minor
|
4.3
|
DiOS
|
#42 |
DIVINE sim crashes after only six states
|
mornfall
|
defect
|
major
|
5.0
|
sim
|
#50 |
Comparison of pointers in usermeta is incorrect.
|
mornfall
|
defect
|
major
|
4.3
|
VM
|
#52 |
unable to reproduce divcc/gzip hello world with divine-4.2.1+2019.02.06
|
mornfall
|
defect
|
major
|
4.3
|
VM
|
#56 |
Showing globals does not work
|
mornfall
|
defect
|
major
|
4.3
|
sim
|
#57 |
Build error in divine-smt
|
mornfall
|
defect
|
major
|
5.0
|
other
|
#58 |
Build fails: Directory nonexistent
|
mornfall
|
defect
|
minor
|
5.0
|
other
|
#61 |
Problems in SV-COMP
|
mornfall
|
defect
|
major
|
4.3
|
other
|
#65 |
Error message in symbolic mode
|
mornfall
|
defect
|
major
|
4.3
|
other
|
#67 |
DiOS: VFS Capture does not work
|
mornfall
|
defect
|
major
|
5.0
|
other
|
#70 |
libpng tests in divine hit op != OpCode::Call in setjmp
|
blurrymoi
|
defect
|
major
|
4.4
|
divcc
|
#71 |
Divine 4.3.2 Build failures
|
mornfall
|
defect
|
major
|
4.3
|
other
|
#73 |
make install failure - Divine 4.3.2
|
mornfall
|
defect
|
major
|
4.3
|
other
|
#74 |
make static failures - Divine 4.3.2
|
mornfall
|
defect
|
major
|
4.3
|
other
|
#75 |
cmake: Build of 4.4.2 fails due to missing target dependencies
|
mornfall
|
defect
|
major
|
4.4
|
other
|
#76 |
Divcc produces a broken gzip
|
blurrymoi
|
defect
|
major
|
4.3
|
divcc
|
#77 |
divcc -v segfault
|
blurrymoi
|
defect
|
major
|
4.3
|
divcc
|
#78 |
Sigaction in enquiry mode causes unexpected error while checking
|
|
defect
|
major
|
4.3
|
DiOS
|
#79 |
Divine help commands crash
|
mornfall
|
defect
|
major
|
4.3
|
UI
|
#80 |
dioscc without any arguments fails with ld error
|
blurrymoi
|
defect
|
major
|
4.3
|
divcc
|
#81 |
dioscc and divine cc explicitly undefine the __x86_64__ macro
|
blurrymoi
|
defect
|
major
|
4.3
|
divcc
|
#82 |
Help commands segmentation faults
|
mornfall
|
defect
|
major
|
4.3
|
UI
|
#83 |
Divince check: false negative when using NULL as the first argument of the pthread_create()
|
mornfall
|
defect
|
major
|
4.5
|
other
|
#84 |
FindZ3.cmake fails on Fedora
|
mornfall
|
defect
|
major
|
4.3
|
other
|
#85 |
testsuite: Some simulator tests fail consistently on Fedora
|
mornfall
|
defect
|
major
|
4.4
|
sim
|
#86 |
Dioscc produces a broken gzip binary
|
mornfall
|
defect
|
major
|
4.3
|
divcc
|
#88 |
VFS: Divine crashes while capturing current directory
|
|
defect
|
major
|
4.3
|
DiOS
|
#89 |
VFS: Divine crashes while capturing files created by truncate
|
|
defect
|
major
|
4.3
|
DiOS
|
#93 |
Memory leak in stdio tracing code.
|
mornfall
|
defect
|
major
|
4.3
|
DiOS
|
#96 |
DiOS: Passing the debug:faultcfg option results in null pointer dereference in kernel
|
Vladimír Štill
|
defect
|
major
|
4.4
|
DiOS
|
#97 |
DiOS: Passing the debug:mainargs option results in config error in kernel
|
Vladimír Štill
|
defect
|
major
|
4.4
|
DiOS
|
#98 |
testsuite: Testsuite does not use clang from Divine's toolchain
|
Vladimír Štill
|
defect
|
major
|
4.4
|
other
|
#99 |
The '+' character in nightly tars breaks some tests
|
mornfall
|
defect
|
major
|
4.4
|
other
|
#100 |
libc: getline implementation incorrectly checks the failure of realloc
|
|
defect
|
major
|
4.4
|
DiOS
|
#101 |
Divine produces unusable memory leak reports
|
mornfall
|
defect
|
major
|
5.0
|
other
|
#102 |
VFS: DiOS fails to boot when capturing an absolute path
|
mornfall
|
defect
|
major
|
4.4
|
other
|
#103 |
libc: strcpy and strncpy do not check if the strings overlap
|
mornfall
|
defect
|
major
|
4.4
|
DiOS
|
#108 |
symbolic: __VERIFIER_nondet_(u)int() causes a memory leak
|
|
defect
|
major
|
4.4
|
DiOS
|
#109 |
libc: calloc forgets to set errno whenever it fails
|
|
defect
|
major
|
4.4
|
DiOS
|
#110 |
DiOS: -o {stdout|stderr}:notrace results in a null pointer dereference
|
mornfall
|
defect
|
major
|
4.4
|
DiOS
|
#111 |
libc: zero size allocations are handled improperly
|
Henrich Lauko
|
defect
|
major
|
4.4
|
DiOS
|
#112 |
libc: perror behaves incorrectly when its input is an empty string
|
|
defect
|
minor
|
4.4
|
DiOS
|
#114 |
divine check fails with "cannot enter kernel mode here"
|
mornfall
|
defect
|
major
|
4.4
|
other
|
#115 |
make says "missing separator" on CentOS 7
|
mornfall
|
defect
|
major
|
4.4
|
other
|
#2 |
Lazy loading / linking of DiOS bitcode.
|
mornfall
|
feature
|
major
|
4.2
|
MC
|
#3 |
Aggregate and garbage-collect *_log tables.
|
mornfall
|
feature
|
major
|
5.0
|
bench
|
#15 |
Implement strcmp for mstring domain.
|
|
feature
|
major
|
4.2
|
DiOS
|
#16 |
Undetected double free
|
Henrich Lauko
|
feature
|
major
|
5.0
|
LART
|
#17 |
Generalize smt builder interface to be usable with different back-ends.
|
Henrich Lauko
|
feature
|
major
|
5.0
|
MC
|
#21 |
Implement clock_gettime
|
mornfall
|
feature
|
minor
|
4.2
|
DiOS
|
#46 |
Simplify stashing mechanism
|
Henrich Lauko
|
feature
|
major
|
4.3
|
DiOS
|
#48 |
Destroy symbolic formula directly when 0 reference count is reached
|
Henrich Lauko
|
feature
|
major
|
4.3
|
DiOS
|
#91 |
Make (install) enhancements
|
Vladimír Štill
|
feature
|
minor
|
4.3
|
other
|
#11 |
Implement string abstraction with 'strlen' function.
|
Henrich Lauko
|
task
|
major
|
4.2
|
LART
|
#18 |
Implement string modification abstraction.
|
Henrich Lauko
|
task
|
major
|
5.0
|
LART
|
#22 |
Use lifetime markers to move allocas
|
Henrich Lauko
|
task
|
major
|
4.3
|
LART
|
#36 |
Assign 'types' (weak, marked) to objects, not to pointers.
|
mornfall
|
task
|
major
|
4.3
|
VM
|
#37 |
Update libc++ and libc++abi.
|
|
task
|
major
|
4.3
|
DiOS
|
#54 |
Split global variables by compilation unit.
|
mornfall
|
task
|
major
|
4.3
|
VM
|