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_test21_false-valid-memtrack_true-termination.i |
programSHA | edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f |
witnessName | results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.memleaks_test21_false-valid-memtrack_true-termination.i.files/witness.graphml |
witnessSHA | 04a32ab6d25cfda0f30e97a8cdaa4d85b315e207602cf377fc5194e62fb0f0eb |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T23:47:03.923829 |
producer | ESBMC 4.6.0 incr |
program-sha256 | edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f |
programfile | ../../sv-benchmarks/c/ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i |
programhash | e4b7cfcfa6c3948b5dbd6b1b13ec55ada7526adf |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
witness-file | witnessFileByHash/04a32ab6d25cfda0f30e97a8cdaa4d85b315e207602cf377fc5194e62fb0f0eb.graphml |
witness-sha256 | 04a32ab6d25cfda0f30e97a8cdaa4d85b315e207602cf377fc5194e62fb0f0eb |
witness-size | 3634 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i, edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f.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_test21_false-valid-memtrack_true-termination.i, edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f.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_test21_false-valid-memtrack_true-termination.i, edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f.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_test21_false-valid-memtrack_true-termination.i, edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f.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_test21_false-valid-memtrack_true-termination.i, edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f.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_test21_false-valid-memtrack_true-termination.i, edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
112f74a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:18 CET (sv-comp) | ||
6b3ff42 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:42:27+01:00 | 112f74a | |
9b0116c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T08:05:02+01:00 | 45a52fd | |
4709720 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:19:30+01:00 | e66967f | |
a849a64 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-08T05:05:15+01:00 | c85abfd | |
9801a92 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-06T10:19:24+01:00 | 48811b1 | |
bcd8803 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T09:28:34+01:00 | b8f28cc | |
acb710d | 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-08T06:48:24 | ||
45a52fd | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 7 | 2018-12-07T10:44:10+01:00 | ||
2a7d28f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T22:09:08+01:00 | acb710d | |
e8ad26d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T01:04:59+01:00 | fc6f9f3 | |
3a5635e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:48:27+01:00 | d549341 | |
e53c4e5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:40:48+01:00 | f1e51ee | |
d549341 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T04:59:50+01:00 | ||
b0bfd72 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T03:12 CET (sv-comp) | ||
2b0937e | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-06T21:16 CET (sv-comp) |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i, edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e9f0275 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:00 CET (sv-comp) | ||
b8f28cc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 4 | 2017-12-01T21:57 CET (sv-comp) | ||
bad6c18 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:48 CET (sv-comp) | ||
320dfe0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T08:29:15+01:00 | ||
3809589 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:53:26.046933 | ||
04a32ab | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:47:03.923829 | ||
84ee0df | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:19 CET (sv-comp) | ||
024f66e | 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 | 5 | 2017-12-01T08:30 CET (sv-comp) | ||
fc28b88 | 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:19 CET (sv-comp) | ||
bfd4ebe | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T02:16:20.624509 | ||
98f509c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T12:14:01.773997 | ||
228f1ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T17:33 CET (sv-comp) | ||
6937a49 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 5 | 2017-12-01T17:58 CET (sv-comp) | ||
6d6ddac | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 19 | 2017-12-01T14:48 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i, edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/edcc1f2f3056fc6ebf245dac5b5eef7f93543161eb5e5f889366ba5b7c547d2f.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |