DIVINE issueshttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues2018-07-07T03:15:48+02:00https://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/24Visualization of heap of program/counterexample2018-07-07T03:15:48+02:00Vladimír ŠtillVisualization of heap of program/counterexampleDIVINE 4 already has graph memory, so turning it into visualization e.g. using DOT should be possible. However, the challenge is in presentation: it would be useful to have nodes labeled with types and pointers with member/variable names...DIVINE 4 already has graph memory, so turning it into visualization e.g. using DOT should be possible. However, the challenge is in presentation: it would be useful to have nodes labeled with types and pointers with member/variable names they represent. Also it would be useful to be able to show only parts of the heap, e.g. corresponding to one thread, omitting DiOS,…Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/21Utilities for symbolized states in DIVINE: emptyness, equality, Z3/Q3B integr...2016-06-19T13:06:26+02:00Vladimír ŠtillUtilities for symbolized states in DIVINE: emptyness, equality, Z3/Q3B integration (SymDIVINE merge)Add support to extract path condition and data definitions from the symbolized state and to perform emptiness, subsumption, and equality checks on symbolized states. See also #20, #22.Add support to extract path condition and data definitions from the symbolized state and to perform emptiness, subsumption, and equality checks on symbolized states. See also #20, #22.SymMergehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/19Probabilistic extension for data-symbolic verification2016-06-19T13:04:15+02:00Jiří BarnatProbabilistic extension for data-symbolic verificationWaiting for #20, #21, #22.Waiting for #20, #21, #22.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/17Syscall record and replay.2016-06-17T10:22:40+02:00Vladimír ŠtillSyscall record and replay.Allow divine run to call syscalls, record them and then allow to replay them.Allow divine run to call syscalls, record them and then allow to replay them.Futurehttps://gitlab.fi.muni.cz/paradise/DIVINE/-/issues/9LART: Register allocation.2016-06-17T10:24:30+02:00Vladimír ŠtillLART: Register allocation.FutureVladimír ŠtillVladimír Štill