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-properties/list_true-unreach-call_false-valid-memtrack.i |
programSHA | 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99 |
witnessName | results-verified/smack.2018-12-07_1913.logfiles/sv-comp19_prop-memsafety.list_true-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | c6fc2436af995266eb261c1c94f4d12ad7571aef280991a1459b801340149f88 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T02:57:38 |
error-specification-length | Key 'specification' longer than 100 characters. |
producer | SMACK 1.9.3 |
program-sha256 | 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_87352aac-4ed9-45f2-9ece-bf0d33f93a61/sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i |
programhash | 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99 |
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/c6fc2436af995266eb261c1c94f4d12ad7571aef280991a1459b801340149f88.graphml |
witness-sha256 | c6fc2436af995266eb261c1c94f4d12ad7571aef280991a1459b801340149f88 |
witness-size | 3357 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99).
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 20 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d135ecc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:30 CET (sv-comp) | ||
1779cdd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-10T10:48:58+01:00 | 49c1cd2 | |
a79d5b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:43:40+01:00 | d135ecc | |
bf91378 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 10 | 2018-12-07T21:44:35+01:00 | ||
d65d55e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T04:54:37+01:00 | 6d23772 | |
8233bb5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T09:26:13+01:00 | 596c526 | |
cea9620 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:41:46+01:00 | e369631 | |
8a87936 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-05T23:42:49+01:00 | ||
c6fc243 | 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-08T02:57:38 | ||
d1adac8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T03:52:32+01:00 | 49c1cd2 | |
597a3e1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T01:13:34+01:00 | a839745 | |
d1891d7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T22:10:05+01:00 | c6fc243 | |
602534d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T10:19:35+01:00 | 10f70b0 | |
d62a729 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | SMACK 1.9.3 | 3 | 2018-12-08T12:35:18 | ||
2cf8670 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 11 | 2018-12-07T05:33:23+01:00 | ||
c41a228 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T21:43:54+01:00 | d62a729 | |
66b488b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T07:15:13+01:00 | 2cf8670 | |
5a1f3a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T09:07:06+01:00 | a7bcba7 | |
d0a8c62 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:28:06+01:00 | 49bb96e | |
49bb96e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-05T09:39:33+01:00 |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/list-properties/list_true-unreach-call_false-valid-memtrack.i, 26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/26b5a7bbd16519673528c372a7f998be13aa98fc0f83138cc2984438ba904c99.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |