If you have encountered a problem with DIVINE, please check below whether there is an active ticket for your issue. Otherwise, please login with GitHub and report your issue. Thank you.

{1} Active Tickets (49 matches)

4.3 (9 matches)

Ticket Summary Comp. Type Status
#87 Struct self-assignment results in assertion failure in memcpy DiOS defect accepted
#90 VFS: Divine segfaults while loading when capturing a diffutils directory DiOS defect new
#92 divine info is outdated DiOS defect accepted
#53 divcc: Investigate and fix coreutils' ls divcc defect assigned
#4 Implement exec --symbolic. MC feature assigned
#62 Generate concrete counterexample from smt. MC feature assigned
#49 Build system should check for minimal version of Z3 other defect assigned
#60 missing __sym_sitofp other defect assigned
#59 Make it possible for `step --over` to stop on thread switch sim defect new

4.4 (15 matches)

Ticket Summary Comp. Type Status
#107 unreachable executed: unknown binary operation fp.leq DiOS defect assigned
#64 Integrate Ballista into DiOS' testsuite. DiOS task new
#68 sysconf macros should be inferred via hostabi DiOS task new
#69 Fix linking with lld divcc defect new
#66 Re-write addSection in terms of llvm code. divcc task new
#106 make: CMake does not set PYTHON_INTERP during libcxx configuration other defect accepted
#113 make install fails for DIVINE 4.4.2 on Debian 10 other defect new
#120 Divine-4.4.2 was built failed in ubuntu 20.04 other defect new
#105 make: Move any compilation out of make install other feature accepted
#121 Where can I get the extract-llvm from? other feature new
#122 Verify properties described using LTL formulas other feature new
#94 sim: Signed integer value is shown as unsigned. sim defect accepted
#95 sim: Integers < -5 appearing in dbg.value are discarded. sim defect accepted
#25 Make metadata exception map lock-free VM feature assigned
#55 Store snapshots in 2 layers. VM task new

4.5 (5 matches)

Ticket Summary Comp. Type Status
#118 libc: isatty(3) is POSIX-nonconformant DiOS defect new
#119 libc: make return value of isatty(3) user configurable DiOS feature new
#116 Divine fails to build on distributions with recent glibc and GNU toolchain other defect new
#117 Possibility of symbolic argc + argv other feature new
#43 Fix thread_local VM defect accepted

5.0 (20 matches)

Ticket Summary Comp. Type Status
#10 Memory leak from symbolic values. DiOS defect new
#26 The weakmem runtime leaks memory DiOS defect assigned
#45 Add support for __atomic_* libcalls DiOS defect new
#35 Track origins of memory objects. DiOS feature new
#39 Hunt down libc functions that should be defined weak DiOS task assigned
#47 Benchmark abstraction cleanup influence DiOS task assigned
#63 Use refcount_ptr in DiOS. DiOS task new
#19 SYM: Spurious errors due to infeasible explicit values LART defect assigned
#40 Error with _SYM and array indexing (worked in 4.1.6) LART feature new
#44 Multi-Threaded Performance Doesn't Scale other defect accepted
#72 Termination testing our data structures other defect assigned
#123 How to use the command line to check whether a C program satisfies the LTL nature other defect new
#104 build Divine against system LLVM 13 other feature new
#51 Write a style guide. other task new
#6 Improve support for debugging inlined functions sim defect new
#30 Possibly move divine's version() out of UI. UI feature new
#31 Capture 'mount points' are confusing. UI task new
#32 Allow usermeta layers to be weak (debug). VM feature new
#33 Return the list of leaked objects back to userspace. VM feature new
#34 Add _VM_T_StackTrace to __vm_trace. VM feature new
Note: See TracReports for help on using and creating reports.
Show all issues