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/forester-heap/sll-01_false-unreach-call_false-valid-deref.i |
programSHA | 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-divine-explicit.2018-12-10_1048.logfiles/sv-comp19_prop-memsafety.sll-01_false-unreach-call_false-valid-deref.i.files/witness.graphml |
witnessSHA | 53c0adeee6cc13c62f8bb0f1caff2828f80805529f77494891d2e73827d18922 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-10T10:48:40+01:00 |
inputwitnesshash | a74a19a4d51d953355d96cfce9b5572c1efef7cd3494cbe01b8b938196ce8536 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024 |
programfile | ../../sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i |
programhash | 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/53c0adeee6cc13c62f8bb0f1caff2828f80805529f77494891d2e73827d18922.graphml |
witness-sha256 | 53c0adeee6cc13c62f8bb0f1caff2828f80805529f77494891d2e73827d18922 |
witness-size | 11540 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024).
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 25 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
01e887b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-02 00:43:28 | ||
eeccdf9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 17 | 2019-12-11T20:54:21+01:00 | 4aa5fad | |
97c9667 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 17 | 2019-12-08T00:26:25+01:00 | a4dbb93 | |
4257a5d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 17 | 2019-12-07T21:17:20+01:00 | 6de4aad | |
f52ca21 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 12 | 2019-12-06T02:39:40+01:00 | 4e3ed52 | |
bc242cc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 17 | 2019-12-05T19:34:37+01:00 | 8c93c68 | |
e15c3cb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 21 | 2019-12-03T08:09:58+01:00 | 722952a | |
722952a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 20 | 2019-11-29T21:56:36+01:00 | ||
da16034 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 17 | 2019-12-11T21:40:11+01:00 | d88ad1c | |
bd82b18 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-11T21:09:07+01:00 | 01e887b | |
23d6b72 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 21 | 2019-12-11T21:45:37+01:00 | f2681fc | |
77e4f63 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 21 | 2019-12-05T20:21:18+01:00 | 9366d8e | |
f2681fc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 20 | 2019-12-01T18:09:05+01:00 | ||
5393add | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 17 | 2019-12-08T00:07:32+01:00 | 690457f | |
0926da2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-11T21:56:54+01:00 | c7e724c | |
4c5f020 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-11T21:56:16+01:00 | ac7ec78 | |
da3c62f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 19 | 2019-12-11T20:54:51+01:00 | 2d0dd39 | |
7a1cc7d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-08T00:26:12+01:00 | f10b86a | |
f25cd18 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-07T21:17:26+01:00 | c82d0bd | |
ef0cd15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 15 | 2019-12-03T08:09:00+01:00 | 770c811 | |
770c811 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 15 | 2019-11-30T12:19:24+01:00 | ||
1485a0f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 4 | 2019-12-07T11:07:27+01:00 | ||
c7e724c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 15 | 2019-12-01T13:46:47+01:00 | ||
17b7c56 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 20 | 2019-12-08T01:51:36+01:00 | 1485a0f | |
52866dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-05T20:20:15+01:00 | fea95ec |
Found 30 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
862527a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T00:29 CET (sv-comp) | ||
53c0ade | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-10T10:48:40+01:00 | a74a19a | |
2b0f8a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-09T20:53:15+01:00 | c21c9dd | |
7ce2e12 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-09T20:39:55+01:00 | 591edc9 | |
d6415c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-09T20:26:08+01:00 | d0242be | |
10e1a9e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-06T09:42:07+01:00 | 2383255 | |
9f26790 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-07T09:14:01+01:00 | c2f66cc | |
69888e9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-06T10:17:50+01:00 | 995c8fd | |
3c8d090 | 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:11:03 | ||
5c44294 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T23:44:45+01:00 | 862527a | |
168eaaa | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T22:09:22+01:00 | 3c8d090 | |
030cdfb | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T05:03:45+01:00 | 04602b4 | |
3ea2a9a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-08T03:39:35+01:00 | a74a19a | |
997c18b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 12 | 2018-12-07T01:17:24+01:00 | 9954fd2 | |
be3a436 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:40 CET (sv-comp) | ||
85c81d3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T02:27:36 | ||
69870af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 4 | 2018-12-10T17:43:40+01:00 | ||
e54152e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 15 | 2018-12-07T10:59:32+01:00 | ||
472f1d1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:53:21+01:00 | 46bf54f | |
50c1f47 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:37:11+01:00 | bef2d15 | |
4799750 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:33:28+01:00 | 1523490 | |
8cbc583 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T08:55:02+01:00 | e54152e | |
d413381 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 24 | 2018-12-08T05:05:44+01:00 | 2c7b9e8 | |
5e7e0e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-06T10:12:10+01:00 | 9450a38 | |
4dd4aaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T09:48:38+01:00 | 2d9d68c | |
7f1bebd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 21 | 2018-12-06T09:18:44+01:00 | 6a6bbe0 | |
2d9d68c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T00:29:47+01:00 | ||
ab8562e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-10T20:35:16+01:00 | 69870af | |
8c848be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T23:43:30+01:00 | be3a436 | |
9a6150d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T22:10:59+01:00 | 85c81d3 |
Found 23 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
03185e9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:16 CET (sv-comp) | ||
0cba977 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 6 | 2017-12-02T10:45:07.430399 | ||
f89e2f5 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T23:38:13.368357 | ||
d80f432 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:24 CET (sv-comp) | ||
183fb99 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 11 | 2017-12-03T06:55Z | ||
907471f | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 11 | 2017-12-03T04:32Z | ||
12e341b | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Forester | 10 | 2017-12-01T19:12 CET (sv-comp) | ||
628bca3 | 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 | 19 | 2017-12-01T08:31 CET (sv-comp) | ||
8a608ba | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 10 | 2017-12-03T03:47Z | ||
c102a09 | 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 | 7 | 2017-12-01T08:19 CET (sv-comp) | ||
c2f66cc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 5 | 2017-12-01T21:51 CET (sv-comp) | ||
785d5a0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:24 CET (sv-comp) | ||
c994b44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 13 | 2017-12-03T02:54Z | ||
e0a0d50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 12 | 2017-12-02T21:19Z | ||
7689902 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Forester | 10 | 2017-12-01T17:47 CET (sv-comp) | ||
bc89453 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 6 | 2017-12-02T00:20:47.693713 | ||
45df104 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 6 | 2017-12-01T10:02:16.525423 | ||
fa8dc13 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T03:31 CET (sv-comp) | ||
30ed9c9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 18 | 2017-11-30T11:49:45+01:00 | ||
df6aaa9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 20 | 2017-12-01T03:11:04+01:00 | ||
f59d188 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 4 | 2017-11-30T15:17:06+01:00 | ||
f4d7e7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 14 | 2017-11-30T18:01 CET (sv-comp) | ||
8418218 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 12 | 2017-12-02T15:25Z |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/sll-01_false-unreach-call_false-valid-deref.i, 04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/04a668b517adc36b6ba64cb8bfea3a7d3c6080e86848215b01673710ab94b024.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |