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-rb-sentinel_false-unreach-call_false-valid-memtrack.i |
programSHA | 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6 |
witnessName | results-verified/map2check.2017-12-01_2312.logfiles/sv-comp18.dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i.files/witness.graphml |
witnessSHA | b2dbc3c39ed28d3e9ae5153bbd95d25aff2d96661362e527201a2c41b294d41e |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T23:20 CET (sv-comp) |
producer | Map2Check |
program-sha256 | 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6 |
programfile | ../../sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i |
programhash | b9633ec6dc7e01a7231c1be5ed310faef61ba6b0 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/b2dbc3c39ed28d3e9ae5153bbd95d25aff2d96661362e527201a2c41b294d41e.graphml |
witness-sha256 | b2dbc3c39ed28d3e9ae5153bbd95d25aff2d96661362e527201a2c41b294d41e |
witness-size | 2392 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.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-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.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-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.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-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.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/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
90b018c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 22:04:24 | ||
2e2d86c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 10 | 2019-12-11T21:09:16+01:00 | 90b018c | |
d97ab2b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 9 | 2019-12-08T00:06:16+01:00 | 3a8430a | |
d7c1103 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 9 | 2019-12-06T02:38:43+01:00 | be2d70c | |
52303d5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-12-11T21:59:42+01:00 | c8100dc | |
2adf800 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-12-05T20:21:08+01:00 | 02f3248 | |
06c5040 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-12-03T08:10:32+01:00 | cf8d0eb | |
c8100dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 13 | 2019-12-01T09:51:38+01:00 | ||
cf8d0eb | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-11-30T11:22:15+01:00 | ||
139a4b8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 13 | 2019-12-11T20:56:02+01:00 | f9fdd9a | |
cabe433 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2019-12-01 15:31:15 | ||
02059e8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-11T21:43:24+01:00 | 37ff597 | |
a5361df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-11T21:41:05+01:00 | 73d7f94 | |
d83d7ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 29 | 2019-12-11T20:54:23+01:00 | b93996c | |
7b13d43 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-08T00:07:40+01:00 | d6e7f22 | |
6b12ce3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-07T21:17:31+01:00 | 5601f78 | |
1be42dc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 21 | 2019-12-03T08:09:04+01:00 | cf038ac | |
cf038ac | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 18 | 2019-11-30T13:53:56+01:00 | ||
2160057 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8 | 8 | 2019-12-07T10:31:31+01:00 | ||
73d7f94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 18 | 2019-11-30T22:54:49+01:00 | ||
9d4ba55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T21:09:30+01:00 | cabe433 | |
90546ba | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-11T20:45:49+01:00 | 7b4d187 | |
8155bbf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-08T01:51:18+01:00 | 2160057 | |
f58adb6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-05T20:21:44+01:00 | ed86d1d | |
f883f65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 13 | 2019-12-03T08:56:48+01:00 | cb1e80f |
Found 28 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
629c89a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T08:03 CET (sv-comp) | ||
82eb977 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-08T23:44:42+01:00 | 629c89a | |
97d28b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn b8d6131600+ | 13 | 2018-12-08T04:24:31+01:00 | ||
2f577f0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T05:04:39+01:00 | f2d3710 | |
0ded626 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:20:57+01:00 | 6eb00da | |
86a767f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 14 | 2018-12-07T09:18:23+01:00 | ae84a1b | |
1d96055 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 9 | 2018-12-07T01:23:20+01:00 | d897e66 | |
8bafc0f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T10:19:22+01:00 | ff91600 | |
efa487e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T13:35 CET (sv-comp) | ||
e5381a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 3 | 2018-12-08T02:06:59 | ||
e73a503 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7 | 8 | 2018-12-10T18:57:09+01:00 | ||
d0fdba2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 17 | 2018-12-07T13:48:58+01:00 | ||
cf27cd5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-09T20:39:26+01:00 | 7adfa9a | |
440787a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-09T20:21:18+01:00 | 6fc70f4 | |
8ed62ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T08:39:43+01:00 | d0fdba2 | |
37bc56e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-08T05:00:42+01:00 | 9aab333 | |
58d9995 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-07T09:15:22+01:00 | e495841 | |
4286ad4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T10:13:58+01:00 | 02f8b43 | |
7e78e0b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:48:00+01:00 | 3e16c87 | |
48f8e44 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 20 | 2018-12-06T09:20:29+01:00 | 6261554 | |
3e16c87 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 17 | 2018-12-06T07:03:48+01:00 | ||
f9e1a81 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T20:38:15+01:00 | e73a503 | |
5ba71ce | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T10:48:46+01:00 | 9b29995 | |
c54cb8e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T18:22:11+01:00 | f0b2711 | |
205784f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T23:42:47+01:00 | efa487e | |
79d5dd6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T22:10:14+01:00 | e5381a6 | |
594160b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T04:18:53+01:00 | 9b29995 | |
a03b48c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T01:15:18+01:00 | 89214ee |
Found 21 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
47f82d5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:58 CET (sv-comp) | ||
ae84a1b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | PredatorHP | 5 | 2017-12-01T22:01 CET (sv-comp) | ||
b2dbc3c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:20 CET (sv-comp) | ||
33c4eaf | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-02T10:34:29.192989 | ||
332b311 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T23:14:57.149614 | ||
909804e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 4 | 2017-12-01T09:09 CET (sv-comp) | ||
4c84ed8 | 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:33 CET (sv-comp) | ||
acd2cdd | 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 | 14 | 2017-12-01T08:28 CET (sv-comp) | ||
0e6dbd6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T10:16 CET (sv-comp) | ||
e495841 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | PredatorHP | 5 | 2017-12-01T20:26 CET (sv-comp) | ||
8476adc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Map2Check | 3 | 2017-12-01T21:30 CET (sv-comp) | ||
07072af | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Kojak | 17 | 2017-12-02T08:56Z | ||
6e99233 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Forester | 10 | 2017-12-01T18:13 CET (sv-comp) | ||
997de13 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 7 | 2017-12-01T12:13:58.295261 | ||
de5b0d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 7 | 2017-12-01T09:02:39.967676 | ||
a3aed1c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 4 | 2017-11-30T22:35 CET (sv-comp) | ||
b3e991d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 16 | 2017-11-30T20:15:09+01:00 | ||
402059e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 4 | 2017-11-30T17:38:01+01:00 | ||
aab3594 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26725 | 2 | 2017-12-01T02:32:23+01:00 | ||
9b3c35d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 14 | 2017-11-30T20:07 CET (sv-comp) | ||
a18cbf8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Automizer | 17 | 2017-12-02T03:59Z |
Found 0 witnesses for program sv-benchmarks/c/forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i, 85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/85bd663c92282d4dfdefb34d4d1bb2e7b23df33069d11197ed5810f4ac1a16c6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |