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/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i |
programSHA | 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35 |
witnessName | results-verified/divine-smt.2018-12-06_1106.logfiles/sv-comp19_prop-memsafety.sll_circular_traversal_true-unreach-call_true-valid-memsafety.i.files/witness.graphml |
witnessSHA | 81aa1f0d665fcab0dc2cd95018d8c7192a895d1fd3e7d4aa539d91dd0c5b535d |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T23:02 CET (sv-comp) |
memorymodel | precise |
producer | DIVINE 4 |
programfile | ../../sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i |
programhash | 15c2a0dbf98e8d278e41c47d311b6d4dc752a8f7 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/81aa1f0d665fcab0dc2cd95018d8c7192a895d1fd3e7d4aa539d91dd0c5b535d.graphml |
witness-sha256 | 81aa1f0d665fcab0dc2cd95018d8c7192a895d1fd3e7d4aa539d91dd0c5b535d |
witness-size | 3235 |
witness-type | correctness_witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i, 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i, 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i, 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i, 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 13 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i, 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
96fb29e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 22 | 2019-11-30T00:34:42+01:00 | ||
c6e6401 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 22 | 2019-11-30T22:47:48+01:00 | ||
d3c5477 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2019-12-03T22:17 CET (comp) | ||
692ffdf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:51:02+01:00 | 7558074 | |
5c7ebc3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:02:42+01:00 | 7859013 | |
b2a1c3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-06T02:10:47+01:00 | b011523 | |
896115a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T20:15:34+01:00 | 3ec268d | |
50c1bdf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-04T02:22:28+01:00 | d3c5477 | |
5de5ead | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T19:55:24+01:00 | 699c05f | |
17b1b6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-11-30T17:32:21+01:00 | e64a3be | |
e64a3be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / svcomp20 | 14 | 2019-11-30T14:50:02+01:00 | ||
7558074 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8 | 10 | 2019-12-07T12:42:39+01:00 | ||
5323d5f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 9 | 2019-12-01T02:53:28+01:00 |
Found 22 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i, 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8aa86b8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T03:45 CET (sv-comp) | ||
2caba7c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 9 | 2018-12-07T03:03:38+01:00 | ||
11b1245 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-05T19:00:51+01:00 | ||
c744a8b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Symbiotic | 1 | 2018-12-08T07:36 CET (sv-comp) | ||
d15ce9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T01:23:54 | ||
4ba1519 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | Pinaka | 3 | 2018-12-07T08:08 CET (sv-comp) | ||
e12f070 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7 | 11 | 2018-12-10T19:02:53+01:00 | ||
c9301f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 12 | 2018-12-07T16:45:32+01:00 | ||
4353022 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-10T20:05:13+01:00 | e12f070 | |
3ac1146 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T10:31:34+01:00 | bf073bb | |
f7e5074 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T23:07:20+01:00 | c744a8b | |
cd89b62 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T21:43:23+01:00 | d15ce9b | |
108c872 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T06:34:35+01:00 | c9301f0 | |
5fe5b20 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T02:49:17+01:00 | efddd03 | |
94c1499 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T02:03:25+01:00 | bf073bb | |
d39827a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T16:38:58+01:00 | 4ba1519 | |
fa136e1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T08:52:39+01:00 | 9029704 | |
045f93f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:29:13+01:00 | 618748b | |
af60288 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:07:03+01:00 | 4fe822e | |
d7c5eb7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T08:28:49+01:00 | 9a0d376 | |
9d71471 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T08:25:30+01:00 | 4c58f57 | |
4fe822e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-05T17:37:58+01:00 |
Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i, 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i, 73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/73c4302b7339a9d755d18122b343a21b5cce1ebf088316deb9677b9b076e4b35.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |