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_test5_1_false-valid-memtrack_true-termination.i |
programSHA | e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9 |
witnessName | results-verified/2ls.2017-12-01_0819.logfiles/sv-comp18.memleaks_test5_1_false-valid-memtrack_true-termination.i.files/witness.graphml |
witnessSHA | b716fbadae4f631ff2d6711455e97490a07dd90078ce6b941d470276978f0830 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T08:25 CET (sv-comp) |
error-specification-length | Key 'specification' longer than 100 characters. |
producer | 2LS |
program-sha256 | e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9 |
programfile | ../../sv-benchmarks/c/ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i |
programhash | 0051a83bf62f20b9aeb9a1e703c5dcd0949649f1 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/b716fbadae4f631ff2d6711455e97490a07dd90078ce6b941d470276978f0830.graphml |
witness-sha256 | b716fbadae4f631ff2d6711455e97490a07dd90078ce6b941d470276978f0830 |
witness-size | 3934 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i, e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9.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_test5_1_false-valid-memtrack_true-termination.i, e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9.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_test5_1_false-valid-memtrack_true-termination.i, e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9.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_test5_1_false-valid-memtrack_true-termination.i, e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9.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_test5_1_false-valid-memtrack_true-termination.i, e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i, e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a63f902 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T12:14 CET (sv-comp) | ||
93d34cd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-07T07:23:21+01:00 | ||
40d42ea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:43:14+01:00 | a63f902 | |
a5e0af5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T08:51:59+01:00 | 93d34cd | |
b0d183b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:47:55+01:00 | 07f9d5c | |
900dfa9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T04:55:44+01:00 | d6f67bc | |
6ff2afe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T10:18:11+01:00 | 708b3ae | |
43ae25a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T09:15:12+01:00 | e160a64 | |
7444296 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:19:59+01:00 | 4a31999 | |
eb9f793 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:14:20+01:00 | 36cc73e | |
e6d7d9d | 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-08T08:52:51 | ||
55bb901 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T22:09:58+01:00 | e6d7d9d | |
8f0324b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T01:12:47+01:00 | db2628f | |
5bfa530 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:41:18+01:00 | d6c3cef | |
07f9d5c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-05T14:11:46+01:00 | ||
2abfd81 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T11:04 CET (sv-comp) | ||
2f5057f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Pinaka | 3 | 2018-12-07T02:48 CET (sv-comp) |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i, e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6404f1b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:19 CET (sv-comp) | ||
e160a64 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:13 CET (sv-comp) | ||
959c9d6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:31 CET (sv-comp) | ||
6791138 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:20:57.650697 | ||
a6b98f9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:50:01.912318 | ||
28abcef | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:09 CET (sv-comp) | ||
43ad1db | 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:19 CET (sv-comp) | ||
b716fba | 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:25 CET (sv-comp) | ||
91e3cde | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T08:25:48+01:00 | ||
4a9f329 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-03T00:38:01.154132 | ||
a962f44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 4.6.0 | 3 | 2017-12-02T09:53:22.755354 | ||
6b571b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 5 | 2017-12-01T18:37 CET (sv-comp) | ||
1b11c6b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 4 | 2017-12-01T13:11 CET (sv-comp) | ||
57ad2c7 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 16 | 2017-12-01T14:52 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i, e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e923dac0c9df2d32576a4d1efa28919091d142ab835d41b4436b3539055306b9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |