#4 |
Implement exec --symbolic.
|
assigned
|
adamatousek
|
feature
|
major
|
4.3
|
#6 |
Improve support for debugging inlined functions
|
new
|
mornfall
|
defect
|
major
|
5.0
|
#10 |
Memory leak from symbolic values.
|
new
|
|
defect
|
major
|
5.0
|
#19 |
SYM: Spurious errors due to infeasible explicit values
|
assigned
|
Henrich Lauko
|
defect
|
major
|
5.0
|
#25 |
Make metadata exception map lock-free
|
assigned
|
adamatousek
|
feature
|
major
|
4.4
|
#26 |
The weakmem runtime leaks memory
|
assigned
|
Vladimír Štill
|
defect
|
major
|
5.0
|
#31 |
Capture 'mount points' are confusing.
|
new
|
mornfall
|
task
|
major
|
5.0
|
#32 |
Allow usermeta layers to be weak (debug).
|
new
|
mornfall
|
feature
|
major
|
5.0
|
#33 |
Return the list of leaked objects back to userspace.
|
new
|
mornfall
|
feature
|
major
|
5.0
|
#34 |
Add _VM_T_StackTrace to __vm_trace.
|
new
|
mornfall
|
feature
|
major
|
5.0
|
#35 |
Track origins of memory objects.
|
new
|
|
feature
|
major
|
5.0
|
#40 |
Error with _SYM and array indexing (worked in 4.1.6)
|
new
|
Henrich Lauko
|
feature
|
major
|
5.0
|
#43 |
Fix thread_local
|
accepted
|
mornfall
|
defect
|
major
|
4.5
|
#45 |
Add support for __atomic_* libcalls
|
new
|
|
defect
|
major
|
5.0
|
#47 |
Benchmark abstraction cleanup influence
|
assigned
|
Henrich Lauko
|
task
|
major
|
5.0
|
#51 |
Write a style guide.
|
new
|
mornfall
|
task
|
major
|
5.0
|
#53 |
divcc: Investigate and fix coreutils' ls
|
assigned
|
blurry
|
defect
|
major
|
4.3
|
#55 |
Store snapshots in 2 layers.
|
new
|
mornfall
|
task
|
major
|
4.4
|
#59 |
Make it possible for `step --over` to stop on thread switch
|
new
|
mornfall
|
defect
|
major
|
4.3
|
#60 |
missing __sym_sitofp
|
assigned
|
Henrich Lauko
|
defect
|
major
|
4.3
|
#62 |
Generate concrete counterexample from smt.
|
assigned
|
Henrich Lauko
|
feature
|
major
|
4.3
|
#64 |
Integrate Ballista into DiOS' testsuite.
|
new
|
|
task
|
major
|
4.4
|
#66 |
Re-write addSection in terms of llvm code.
|
new
|
blurrymoi
|
task
|
major
|
4.4
|
#68 |
sysconf macros should be inferred via hostabi
|
new
|
|
task
|
major
|
4.4
|
#69 |
Fix linking with lld
|
new
|
blurrymoi
|
defect
|
major
|
4.4
|
#72 |
Termination testing our data structures
|
assigned
|
xstill
|
defect
|
major
|
5.0
|
#87 |
Struct self-assignment results in assertion failure in memcpy
|
accepted
|
mornfall
|
defect
|
major
|
4.3
|
#90 |
VFS: Divine segfaults while loading when capturing a diffutils directory
|
new
|
|
defect
|
major
|
4.3
|
#94 |
sim: Signed integer value is shown as unsigned.
|
accepted
|
Vladimír Štill
|
defect
|
major
|
4.4
|
#95 |
sim: Integers < -5 appearing in dbg.value are discarded.
|
accepted
|
mornfall
|
defect
|
major
|
4.4
|
#105 |
make: Move any compilation out of make install
|
accepted
|
mornfall
|
feature
|
major
|
4.4
|
#106 |
make: CMake does not set PYTHON_INTERP during libcxx configuration
|
accepted
|
Vladimír Štill
|
defect
|
major
|
4.4
|
#113 |
make install fails for DIVINE 4.4.2 on Debian 10
|
new
|
mornfall
|
defect
|
major
|
4.4
|
#116 |
Divine fails to build on distributions with recent glibc and GNU toolchain
|
new
|
mornfall
|
defect
|
major
|
4.5
|
#117 |
Possibility of symbolic argc + argv
|
new
|
mornfall
|
feature
|
major
|
4.5
|
#118 |
libc: isatty(3) is POSIX-nonconformant
|
new
|
|
defect
|
major
|
4.5
|
#119 |
libc: make return value of isatty(3) user configurable
|
new
|
|
feature
|
major
|
4.5
|
#120 |
Divine-4.4.2 was built failed in ubuntu 20.04
|
new
|
mornfall
|
defect
|
major
|
4.4
|
#122 |
Verify properties described using LTL formulas
|
new
|
mornfall
|
feature
|
major
|
4.4
|
#123 |
How to use the command line to check whether a C program satisfies the LTL nature
|
new
|
mornfall
|
defect
|
major
|
5.0
|
#30 |
Possibly move divine's version() out of UI.
|
new
|
mornfall
|
feature
|
minor
|
5.0
|
#39 |
Hunt down libc functions that should be defined weak
|
assigned
|
blurry
|
task
|
minor
|
5.0
|
#44 |
Multi-Threaded Performance Doesn't Scale
|
accepted
|
mornfall
|
defect
|
minor
|
5.0
|
#49 |
Build system should check for minimal version of Z3
|
assigned
|
Henrich Lauko
|
defect
|
minor
|
4.3
|
#63 |
Use refcount_ptr in DiOS.
|
new
|
|
task
|
minor
|
5.0
|
#92 |
divine info is outdated
|
accepted
|
Vladimír Štill
|
defect
|
minor
|
4.3
|
#104 |
build Divine against system LLVM 13
|
new
|
mornfall
|
feature
|
minor
|
5.0
|
#107 |
unreachable executed: unknown binary operation fp.leq
|
assigned
|
Henrich Lauko
|
defect
|
minor
|
4.4
|
#121 |
Where can I get the extract-llvm from?
|
new
|
mornfall
|
feature
|
trivial
|
4.4
|