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/dll-token_false-unreach-call_false-valid-memcleanup.i |
programSHA | b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc |
witnessName | results-verified/predatorhp.2017-12-01_2024.logfiles/sv-comp18.dll-token_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml |
witnessSHA | 5d6545d03fb1edd05377dcf8e072760e697268c9936d9ea6ffc5101500935fd9 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T20:30 CET (sv-comp) |
memorymodel | precise |
producer | PredatorHP |
program-sha256 | b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc |
programfile | ../../sv-benchmarks/c/forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i |
programhash | 35a5ccff58935eefedf723cd2243fac7c8b8e61b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/5d6545d03fb1edd05377dcf8e072760e697268c9936d9ea6ffc5101500935fd9.graphml |
witness-sha256 | 5d6545d03fb1edd05377dcf8e072760e697268c9936d9ea6ffc5101500935fd9 |
witness-size | 4282 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i, b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc.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/dll-token_false-unreach-call_false-valid-memcleanup.i, b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc.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/dll-token_false-unreach-call_false-valid-memcleanup.i, b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc.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/dll-token_false-unreach-call_false-valid-memcleanup.i, b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 29 witnesses for program sv-benchmarks/c/forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i, b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
76b9999 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2019-12-01 09:38:33 | ||
6878c79 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-11T21:44:18+01:00 | 5b2aade | |
1f6f916 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-11T21:42:19+01:00 | a5105e9 | |
0555fea | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-11T21:09:25+01:00 | 76b9999 | |
cc7c1a5 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-08T00:26:08+01:00 | 99cf16e | |
ac77eb8 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-08T00:06:22+01:00 | 17467ab | |
460b29b | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-07T21:17:28+01:00 | 36a7758 | |
1bc6e61 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-05T19:34:18+01:00 | 6a5c1f7 | |
0ff019f | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-03T08:09:49+01:00 | ae781c9 | |
ae781c9 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-11-30T06:22:15+01:00 | ||
5b2aade | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 7 | 2019-12-01T10:44:53+01:00 | ||
9468528 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 10:21:00 | ||
54cf2d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T22:00:26+01:00 | 6fc13c9 | |
fc90704 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T21:09:46+01:00 | 9468528 | |
c5b3bb9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T20:54:22+01:00 | acbae7f | |
efefadf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:26:03+01:00 | 5a1bc36 | |
82ce05f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-08T00:07:40+01:00 | e9c40ce | |
4d860a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-07T21:13:51+01:00 | 23d7944 | |
4eaddba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-06T02:40:17+01:00 | b0328db | |
367279c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-05T20:20:13+01:00 | 516c7ad | |
5596e97 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-05T19:34:05+01:00 | ec788f1 | |
8819f66 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-03T08:57:56+01:00 | 9abded9 | |
21a4f74 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 6 | 2019-11-29T16:28:44+01:00 | ||
a051d11 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 5 | 2019-12-07T16:43:13+01:00 | ||
9ce3488 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 6 | 2019-12-01T00:32:30+01:00 | ||
6e8af2a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 11 | 2019-12-11T21:52:11+01:00 | 9ce3488 | |
3790307 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 11 | 2019-12-11T20:45:49+01:00 | 851c4df | |
f5391f0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 11 | 2019-12-08T01:51:38+01:00 | a051d11 | |
f6f9606 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 11 | 2019-12-03T08:09:54+01:00 | 21a4f74 |
Found 33 witnesses for program sv-benchmarks/c/forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i, b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7ff958c | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:26 CET (sv-comp) | ||
360671a | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T07:17:18 | ||
e0e794e | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:41:59+01:00 | 7ff958c | |
1727be2 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T22:09:59+01:00 | 360671a | |
2bd4c43 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T09:27:31+01:00 | 7579894 | |
1b84072 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T10:14:04+01:00 | 7965514 | |
0197ff5 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:48:22+01:00 | b461608 | |
d07ea92 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:42:01+01:00 | 3b395dc | |
b461608 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T05:49:26+01:00 | ||
7d445ed | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:20:11+01:00 | 70c4c44 | |
d776190 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T02:26 CET (sv-comp) | ||
91ae8a7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T00:10:38 | ||
924a27a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 5 | 2018-12-10T17:28:01+01:00 | ||
7ddb2aa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-06T13:12:01+01:00 | ||
30c0c64 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-10T10:48:46+01:00 | 64a5183 | |
3df05a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:53:12+01:00 | 4930be7 | |
de8bbc0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:37:29+01:00 | d1edd40 | |
55c3456 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-09T20:18:59+01:00 | e273b4d | |
3b2c33e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T22:10:32+01:00 | 91ae8a7 | |
a175207 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T04:55:14+01:00 | 0be12f0 | |
e333a2c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T03:53:41+01:00 | 64a5183 | |
1005cc4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T09:20:12+01:00 | 5d6545d | |
b0d7e14 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T10:17:49+01:00 | 43f4453 | |
23f6b46 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:41:26+01:00 | 9dc4d78 | |
d651d4e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:19:09+01:00 | 71cfe45 | |
9706165 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-06T09:00:05+01:00 | 7e443b3 | |
fbaa5a1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T05:01:41+01:00 | ||
c205f32 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-10T20:37:16+01:00 | 924a27a | |
d9af33d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-09T18:21:26+01:00 | 210b581 | |
03e7df6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T23:41:58+01:00 | d776190 | |
94cb7be | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-08T08:12:09+01:00 | 7ddb2aa | |
83287d2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-07T01:15:39+01:00 | 30374b6 | |
a3d092f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:48:18+01:00 | fbaa5a1 |
Found 16 witnesses for program sv-benchmarks/c/forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i, b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c1a5687 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 9 | 2017-12-02T23:02Z | ||
8b98011 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T16:46 CET (sv-comp) | ||
5d6545d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | PredatorHP | 4 | 2017-12-01T20:30 CET (sv-comp) | ||
f299951 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 2 | 2017-12-01T21:19 CET (sv-comp) | ||
638168a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 9 | 2017-12-02T12:56Z | ||
9a0b93e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Forester | 6 | 2017-12-01T18:09 CET (sv-comp) | ||
20ecff2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-02T05:05:42.890408 | ||
bc16a06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T18:51:24.345554 | ||
0e849b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T04:44 CET (sv-comp) | ||
7ee180f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 8 | 2017-11-30T14:33:57+01:00 | ||
15a37cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 12 | 2017-12-01T01:16:11+01:00 | ||
61d0933 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 5 | 2017-11-30T14:01:37+01:00 | ||
0ed247e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 7 | 2017-12-02T10:36:39+01:00 | ||
bb2adc1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 8 | 2017-11-30T15:42 CET (sv-comp) | ||
52ac706 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 9 | 2017-12-02T04:29Z | ||
9cad96f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 5 | 2017-11-30T19:30 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i, b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b94bf54336d47003af5d313cc3960481df2073765cf9540ae3a07ec1e2314ddc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |