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.

{6} All Tickets By Milestone (Including closed) (123 matches)

A more complex example to show how to make advanced reports.

Results (1 - 100 of 123)

1 2 →

4.2 (8 matches)

Ticket Summary Comp Type Status
#1 Fix memory leaks in DiOS DiOS defect closed
#21 Implement clock_gettime DiOS feature closed
#2 Lazy loading / linking of DiOS bitcode. MC feature closed
#7 Problems with --symbolic in SV-COMP benchmarks DiOS defect closed
#9 Problem with cast form abstract int to abstract pointer. LART defect closed
#15 Implement strcmp for mstring domain. DiOS feature closed
#11 Implement string abstraction with 'strlen' function. LART task closed
#12 Have both versions of strerror_r DiOS defect closed

4.3 (38 matches)

Ticket Summary Comp Type Status
#59 Make it possible for `step --over` to stop on thread switch sim defect new
#87 Struct self-assignment results in assertion failure in memcpy DiOS defect accepted
#62 Generate concrete counterexample from smt. MC feature assigned
#4 Implement exec --symbolic. MC feature assigned
#60 missing __sym_sitofp other defect assigned
#90 VFS: Divine segfaults while loading when capturing a diffutils directory DiOS defect new
#53 divcc: Investigate and fix coreutils' ls divcc defect assigned
#49 Build system should check for minimal version of Z3 other defect assigned
#92 divine info is outdated DiOS defect accepted
#22 Use lifetime markers to move allocas LART task closed
#48 Destroy symbolic formula directly when 0 reference count is reached DiOS feature closed
#73 make install failure - Divine 4.3.2 other defect closed
#81 dioscc and divine cc explicitly undefine the __x86_64__ macro divcc defect closed
#91 Make (install) enhancements other feature closed
#65 Error message in symbolic mode other defect closed
#54 Split global variables by compilation unit. VM task closed
#74 make static failures - Divine 4.3.2 other defect closed
#93 Memory leak in stdio tracing code. DiOS defect closed
#84 FindZ3.cmake fails on Fedora other defect closed
#71 Divine 4.3.2 Build failures other defect closed
#82 Help commands segmentation faults UI defect closed
#46 Simplify stashing mechanism DiOS feature closed
#86 Dioscc produces a broken gzip binary divcc defect closed
#89 VFS: Divine crashes while capturing files created by truncate DiOS defect closed
#88 VFS: Divine crashes while capturing current directory DiOS defect closed
#80 dioscc without any arguments fails with ld error divcc defect closed
#79 Divine help commands crash UI defect closed
#50 Comparison of pointers in usermeta is incorrect. VM defect closed
#76 Divcc produces a broken gzip divcc defect closed
#77 divcc -v segfault divcc defect closed
#78 Sigaction in enquiry mode causes unexpected error while checking DiOS defect closed
#37 Update libc++ and libc++abi. DiOS task closed
#24 divcc needs native libc++ and libc++abi to build C++ programs DiOS defect closed
#61 Problems in SV-COMP other defect closed
#56 Showing globals does not work sim defect closed
#52 unable to reproduce divcc/gzip hello world with divine-4.2.1+2019.02.06 VM defect closed
#41 Faults that are suppressed should not appear in the trace DiOS defect closed
#36 Assign 'types' (weak, marked) to objects, not to pointers. VM task closed

4.4 (32 matches)

Ticket Summary Comp Type Status
#64 Integrate Ballista into DiOS' testsuite. DiOS task new
#95 sim: Integers < -5 appearing in dbg.value are discarded. sim defect accepted
#66 Re-write addSection in terms of llvm code. divcc task new
#69 Fix linking with lld divcc defect new
#68 sysconf macros should be inferred via hostabi DiOS task new
#122 Verify properties described using LTL formulas other feature new
#55 Store snapshots in 2 layers. VM task new
#105 make: Move any compilation out of make install other feature accepted
#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
#94 sim: Signed integer value is shown as unsigned. sim defect accepted
#25 Make metadata exception map lock-free VM feature assigned
#107 unreachable executed: unknown binary operation fp.leq DiOS defect assigned
#121 Where can I get the extract-llvm from? other feature new
#114 divine check fails with "cannot enter kernel mode here" other defect closed
#111 libc: zero size allocations are handled improperly DiOS defect closed
#110 DiOS: -o {stdout|stderr}:notrace results in a null pointer dereference DiOS defect closed
#97 DiOS: Passing the debug:mainargs option results in config error in kernel DiOS defect closed
#96 DiOS: Passing the debug:faultcfg option results in null pointer dereference in kernel DiOS defect closed
#115 make says "missing separator" on CentOS 7 other defect closed
#112 libc: perror behaves incorrectly when its input is an empty string DiOS defect closed
#109 libc: calloc forgets to set errno whenever it fails DiOS defect closed
#108 symbolic: __VERIFIER_nondet_(u)int() causes a memory leak DiOS defect closed
#75 cmake: Build of 4.4.2 fails due to missing target dependencies other defect closed
#98 testsuite: Testsuite does not use clang from Divine's toolchain other defect closed
#100 libc: getline implementation incorrectly checks the failure of realloc DiOS defect closed
#99 The '+' character in nightly tars breaks some tests other defect closed
#103 libc: strcpy and strncpy do not check if the strings overlap DiOS defect closed
#102 VFS: DiOS fails to boot when capturing an absolute path other defect closed
#85 testsuite: Some simulator tests fail consistently on Fedora sim defect closed
#70 libpng tests in divine hit op != OpCode::Call in setjmp divcc defect closed

4.5 (6 matches)

Ticket Summary Comp Type Status
#118 libc: isatty(3) is POSIX-nonconformant DiOS defect 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
#119 libc: make return value of isatty(3) user configurable DiOS feature new
#83 Divince check: false negative when using NULL as the first argument of the pthread_create() other defect closed

5.0 (16 matches)

Ticket Summary Comp Type Status
#32 Allow usermeta layers to be weak (debug). VM feature new
#26 The weakmem runtime leaks memory DiOS defect assigned
#123 How to use the command line to check whether a C program satisfies the LTL nature other defect new
#47 Benchmark abstraction cleanup influence DiOS task assigned
#45 Add support for __atomic_* libcalls DiOS defect new
#6 Improve support for debugging inlined functions sim defect new
#72 Termination testing our data structures other defect assigned
#31 Capture 'mount points' are confusing. UI task new
#33 Return the list of leaked objects back to userspace. VM feature new
#10 Memory leak from symbolic values. DiOS defect new
#34 Add _VM_T_StackTrace to __vm_trace. VM feature new
#35 Track origins of memory objects. DiOS feature new
#51 Write a style guide. other 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
#39 Hunt down libc functions that should be defined weak DiOS task assigned
1 2 →
Note: See TracReports for help on using and creating reports.
Show open issues