A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).
Key | Value |
programName | sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i |
programSHA | 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-2ls.2018-12-06_0936.logfiles/sv-comp19_prop-memsafety.memleaks_test20_false-valid-memtrack_true-termination.i.files/witness.graphml |
witnessSHA | 0d1ff5ba716bc8d8485e198ece7701bfc8f2c08ccf86ca6fad83081a55485ffb |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-06T09:41:00+01:00 |
inputwitnesshash | ec13e21da8c724a49ecf29513a4536620a6a3592e0ca248d7de77b977c353cd0 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5 |
programfile | ../../sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i |
programhash | 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/0d1ff5ba716bc8d8485e198ece7701bfc8f2c08ccf86ca6fad83081a55485ffb.graphml |
witness-sha256 | 0d1ff5ba716bc8d8485e198ece7701bfc8f2c08ccf86ca6fad83081a55485ffb |
witness-size | 7175 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5).
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 16 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
eef87d1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T04:16 CET (sv-comp) | ||
c01e98b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 7 | 2018-12-07T11:17:40+01:00 | ||
f3b36fe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T08:24:22+01:00 | c01e98b | |
0d1ff5b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:41:00+01:00 | ec13e21 | |
b1ee66c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:20:28+01:00 | b964027 | |
b86c0e2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T05:51:19+01:00 | ||
a49b5c0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T10:17:58+01:00 | 5430239 | |
6177e34 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:41:56+01:00 | eef87d1 | |
851d53e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T22:07:44+01:00 | 75dae7e | |
5670655 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T09:30:04+01:00 | f90047c | |
6ed4c63 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:48:37+01:00 | b86c0e2 | |
a42b6f4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T04:58:43+01:00 | cd0f1ba | |
75dae7e | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T16:33:26 | ||
d369a52 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T01:09:37+01:00 | 2ba2d4d | |
4aa5c25 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T00:13 CET (sv-comp) | ||
9ae6023 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T15:41 CET (sv-comp) |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6358d39 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:27 CET (sv-comp) | ||
f90047c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 4 | 2017-12-01T21:55 CET (sv-comp) | ||
95be57e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:36 CET (sv-comp) | ||
202b0b9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T08:30:41+01:00 | ||
1132141 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:32:12.334053 | ||
8770ec9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:51:55.339253 | ||
1070128 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:20 CET (sv-comp) | ||
fbadade | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CBMC | 6 | 2017-12-01T08:23 CET (sv-comp) | ||
cb4d810 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | 2LS | 4 | 2017-12-01T08:24 CET (sv-comp) | ||
b73b784 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T19:48:32.490387 | ||
12753e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T10:56:12.374651 | ||
8eee9bd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T20:49 CET (sv-comp) | ||
d37cd9d | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 6 | 2017-12-01T18:52 CET (sv-comp) | ||
fad9fce | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 18 | 2017-12-01T16:11 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i, 0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0e3bc00e43b1ae9f0b68a4338a20f095d734b4e80391f3e43bf171821454c8b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |