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_length_check_false-unreach-call_false-valid-memcleanup.i |
programSHA | 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-smack.2018-12-08_2205.logfiles/sv-comp19_prop-memsafety.sll_length_check_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml |
witnessSHA | 0787670603449ca650216cd174b6019e23df7d4fff97796c76d0ef164c100c51 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T22:08:01+01:00 |
inputwitnesshash | 38e8413a2f81892cae6e3c23a00be81fb59f8cf98352a83d857dcb4ac3e7e365 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940 |
programfile | ../../sv-benchmarks/c/list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i |
programhash | 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memcleanup) ) |
witness-file | witnessFileByHash/0787670603449ca650216cd174b6019e23df7d4fff97796c76d0ef164c100c51.graphml |
witness-sha256 | 0787670603449ca650216cd174b6019e23df7d4fff97796c76d0ef164c100c51 |
witness-size | 10944 |
witness-type | correctness_witness |
This witness was created for this program (cf. table above, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940).
Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940.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_length_check_false-unreach-call_false-valid-memcleanup.i, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940.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_length_check_false-unreach-call_false-valid-memcleanup.i, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940.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_length_check_false-unreach-call_false-valid-memcleanup.i, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 18 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d3aaf16 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2019-12-01 09:56:09 | ||
f6aa566 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-11T21:43:26+01:00 | 0d9df08 | |
1a3fa2d | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-11T21:41:07+01:00 | bd31db9 | |
5cc53bb | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-11T21:09:39+01:00 | d3aaf16 | |
720bce6 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-08T00:07:39+01:00 | 15cb38c | |
94874cf | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-07T21:14:15+01:00 | 132cfcf | |
ea374df | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 16 | 2019-12-03T08:10:33+01:00 | 64a00a1 | |
64a00a1 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-11-30T13:45:24+01:00 | ||
0d9df08 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 15 | 2019-12-01T02:25:45+01:00 | ||
c451cae | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.9 | 11 | 2019-12-05T20:20:19+01:00 | c362479 | |
b40ca5d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 18:12:48 | ||
2544dd6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-11T21:48:57+01:00 | c41a08c | |
e411854 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-11T21:43:14+01:00 | 073963d | |
9ddf42e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-08T00:26:18+01:00 | b8b19ee | |
64e209b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-07T21:18:33+01:00 | b7b8415 | |
5cce6d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 16 | 2019-12-03T08:09:33+01:00 | d25febd | |
d25febd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 16 | 2019-11-29T17:39:55+01:00 | ||
c41a08c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 16 | 2019-12-01T00:22:27+01:00 |
Found 19 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
da902f9 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2018-12-08T09:44 CET (sv-comp) | ||
38e8413 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | SMACK 1.9.3 | 5 | 2018-12-08T16:00:49 | ||
bcc4cb7 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T23:42:32+01:00 | da902f9 | |
03508c8 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-07T09:29:19+01:00 | 5fa0046 | |
8edf969 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T10:20:12+01:00 | c9395ea | |
22f4b0b | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T09:48:18+01:00 | bcb5daa | |
bcb5daa | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T02:58:28+01:00 | ||
0787670 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-08T22:08:01+01:00 | 38e8413 | |
add935c | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 11 | 2018-12-06T09:15:45+01:00 | 5714433 | |
05911cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T04:57 CET (sv-comp) | ||
17f2b9b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 5 | 2018-12-08T10:19:00 | ||
d4a3deb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 110 | 2018-12-07T14:30 CET (sv-comp) | ||
8f98fab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 16 | 2018-12-07T21:39:19+01:00 | ||
0908215 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:53:20+01:00 | 8fe6675 | |
1ec8362 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:39:37+01:00 | 716e323 | |
32f9d0d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-09T20:20:34+01:00 | 3e64c57 | |
d810d60 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-08T08:58:13+01:00 | 8f98fab | |
b8ec8d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T09:48:13+01:00 | c68edc1 | |
c68edc1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 16 | 2018-12-06T04:22:17+01:00 |
Found 0 witnesses for program sv-benchmarks/c/list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940.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_length_check_false-unreach-call_false-valid-memcleanup.i, 82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/82b6677755ab81188947c4bd6adf3ae4935685f86f4e03a395ac9fa5be49e940.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |