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-optional_false-unreach-call_false-valid-memcleanup.i |
programSHA | e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc |
witnessName | results-verified/predatorhp.2018-12-07_0408.logfiles/sv-comp19_prop-memsafety.dll-optional_false-unreach-call_false-valid-memcleanup.i.files/witness.graphml |
witnessSHA | 01f5532a932b48007574aa1215fc34b765e82257fb805a0ffe8914f10a6f7fc9 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-07T07:04 CET (sv-comp) |
memorymodel | precise |
producer | PredatorHP |
programfile | ../../sv-benchmarks/c/forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i |
programhash | 8409443a6b8db5c0500e3e8aa54c33463c524ec9 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memcleanup) ) |
witness-file | witnessFileByHash/01f5532a932b48007574aa1215fc34b765e82257fb805a0ffe8914f10a6f7fc9.graphml |
witness-sha256 | 01f5532a932b48007574aa1215fc34b765e82257fb805a0ffe8914f10a6f7fc9 |
witness-size | 4176 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i, e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc.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-optional_false-unreach-call_false-valid-memcleanup.i, e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc.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-optional_false-unreach-call_false-valid-memcleanup.i, e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc.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-optional_false-unreach-call_false-valid-memcleanup.i, e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc.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-optional_false-unreach-call_false-valid-memcleanup.i, e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
52e0b6b | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2019-12-01 22:48:41 | ||
0b05455 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-11T21:44:26+01:00 | bd842c0 | |
d5c0076 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-11T21:42:37+01:00 | 2b9f835 | |
4c7164d | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 8 | 2019-12-11T21:09:17+01:00 | 52e0b6b | |
1426edb | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-08T00:26:49+01:00 | 5ff08ee | |
d0cad22 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-08T00:06:12+01:00 | e155c4a | |
bc63d8a | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-07T21:14:56+01:00 | 6d605fd | |
82cf292 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-05T19:34:00+01:00 | 2e3433d | |
395024a | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-03T08:08:24+01:00 | 3590537 | |
3590537 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-11-29T15:43:45+01:00 | ||
bd842c0 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6 | 2019-12-01T03:58:44+01:00 | ||
fbb5746 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-02 00:19:00 | ||
8639aa3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-11T21:58:01+01:00 | 401695a | |
c788a39 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-11T21:56:32+01:00 | 4483235 | |
f9db07e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 9 | 2019-12-11T21:09:05+01:00 | fbb5746 | |
c335925 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 7 | 2019-12-11T20:54:37+01:00 | 66cc0d3 | |
33f5cfb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-08T01:51:24+01:00 | dcacdf6 | |
7845199 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-08T00:26:20+01:00 | a7f3d20 | |
be1b289 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-08T00:06:02+01:00 | 0215818 | |
0d95922 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-07T21:17:02+01:00 | 665fd41 | |
847f92b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-05T19:34:39+01:00 | 35b460e | |
38e6e67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-03T08:56:58+01:00 | 3a55958 | |
6d8450e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 8 | 2019-12-03T08:09:40+01:00 | 4ab071a | |
4ab071a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 8 | 2019-11-30T07:11:14+01:00 | ||
dcacdf6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 8 | 2019-12-07T22:30:59+01:00 | ||
401695a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 8 | 2019-11-30T21:19:12+01:00 | ||
6ac1485 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-11T20:46:06+01:00 | 5116245 | |
bc8f1e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-06T02:40:23+01:00 | 5151ce8 | |
3dc0ebf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 10 | 2019-12-05T20:21:24+01:00 | 539afe1 |
Found 31 witnesses for program sv-benchmarks/c/forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i, e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
39bc2ed | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | Symbiotic | 1 | 2018-12-08T11:16 CET (sv-comp) | ||
c7ef1d9 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T03:02:09 | ||
b09967b | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:44:00+01:00 | 39bc2ed | |
ae15d55 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T22:08:34+01:00 | c7ef1d9 | |
93878a7 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T09:23:03+01:00 | 01f5532 | |
89218b0 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T10:09:29+01:00 | 130ceac | |
2a81019 | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:48:57+01:00 | e1943cc | |
cadc60f | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:42:13+01:00 | 366f954 | |
e1943cc | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-05T16:28:59+01:00 | ||
400e02c | Inspect | CHECK( init(main()), LTL(G valid-memcleanup) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:12:14+01:00 | 20d7694 | |
5ccc7c6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T12:51 CET (sv-comp) | ||
8cebb8c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T08:54:35 | ||
f4f4830 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 8 | 2018-12-10T17:01:20+01:00 | ||
7993a06 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-08T02:40:01+01:00 | ||
a3a178a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-10T20:37:47+01:00 | f4f4830 | |
4de967c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-10T10:48:55+01:00 | bb637dc | |
f36eea2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:53:11+01:00 | 46f0732 | |
ee419e6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:39:08+01:00 | e2ab6aa | |
d494e07 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-09T20:35:33+01:00 | 20ce9b6 | |
b2cda3d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T23:44:52+01:00 | 5ccc7c6 | |
8c3cae1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T22:08:54+01:00 | 8cebb8c | |
9bc3d8d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T07:48:18+01:00 | 7993a06 | |
cd7c552 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T04:53:45+01:00 | 52e0b7f | |
594b266 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T03:26:16+01:00 | bb637dc | |
63eecb3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T09:18:06+01:00 | e29dc57 | |
85a6e22 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-07T01:09:41+01:00 | e4ba27b | |
eb209f7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T10:15:36+01:00 | 685c55b | |
8c3bc4e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:49:10+01:00 | 8129900 | |
231e873 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:40:42+01:00 | be5a380 | |
e3c800d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T09:20:13+01:00 | 13546f1 | |
8129900 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T05:37:49+01:00 |
Found 16 witnesses for program sv-benchmarks/c/forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i, e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
55d96c4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Taipan | 6 | 2017-12-03T02:08Z | ||
f9efc15 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T08:25 CET (sv-comp) | ||
e29dc57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | PredatorHP | 4 | 2017-12-01T20:41 CET (sv-comp) | ||
117553a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T20:38 CET (sv-comp) | ||
8f6aff9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 6 | 2017-12-02T10:01Z | ||
9b98d4a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Forester | 6 | 2017-12-01T18:04 CET (sv-comp) | ||
37f7c35 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T02:00:53.163587 | ||
a7fd525 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T08:51:18.084369 | ||
cf2fff1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T04:10 CET (sv-comp) | ||
b5eaec4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-11-30T18:47:34+01:00 | ||
4e88976 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 13 | 2017-11-30T12:11:00+01:00 | ||
2c009a1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 6 | 2017-11-30T13:58:35+01:00 | ||
64aa232 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 8 | 2017-12-02T01:14:35+01:00 | ||
5dd0a83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 6 | 2017-11-30T13:26 CET (sv-comp) | ||
63f75e5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 6 | 2017-12-02T09:32Z | ||
37c59c1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 5 | 2017-11-30T21:16 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i, e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e4e1d9b452956401b33141866a3b5377ff40c9d9524ab967479c2a1da6213cdc.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |