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/memsafety-ext3/derefAfterFree2_false-valid-deref.c |
programSHA | 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5 |
witnessName | results-verified/utaipan.2018-12-08_1419.logfiles/sv-comp19_prop-memsafety.derefAfterFree2_false-valid-deref.c.files/witness.graphml |
witnessSHA | 64851d5ff9a13304525ff9b0543f04a2f82d1e11f8c9f10e9462cb8e631cded2 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-09T08:50Z |
error-specification-length | Key 'specification' longer than 100 characters. |
producer | Taipan |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_a451272d-c373-41c5-8fe9-6d85195698c7/sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c |
programhash | 44834c55142a76240cb3980fc2bb6f5aeaa27c83 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/64851d5ff9a13304525ff9b0543f04a2f82d1e11f8c9f10e9462cb8e631cded2.graphml |
witness-sha256 | 64851d5ff9a13304525ff9b0543f04a2f82d1e11f8c9f10e9462cb8e631cded2 |
witness-size | 11373 |
witness-type | violation_witness |
Found 33 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
aa899dd | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:59:45+01:00 | ||
aaf7c5f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T19:06:40Z | ||
7d52494 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-19T05:25:42+01:00 | e3f9174 | |
b1f4d7b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-18T12:06:44+01:00 | aa899dd | |
776c85c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-18T03:09:07+01:00 | 58c427b | |
37d2cda | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-17T22:06:24+01:00 | 6c656ea | |
a337b13 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-05T14:37:03+01:00 | 455a3e6 | |
80b7047 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-04T16:43:07+01:00 | 52e2c23 | |
40996b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-04T12:11:44+01:00 | 8920c11 | |
2ee5b2b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-04T02:26:08+01:00 | 0402502 | |
4e52c83 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-03T06:18:34+01:00 | 727ff01 | |
589fc7b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-01T22:56:15+01:00 | 3f0e10e | |
2c768dd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-12-01T18:30:00+01:00 | b814eeb | |
a83a78f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-11-30T13:42:52+01:00 | 399e83c | |
eb668f4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-11-30T09:44:05+01:00 | 75fa13f | |
399e83c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 11 | 2023-11-30T08:43:50+01:00 | ||
a637669 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-11-30T03:04:28+01:00 | aaf7c5f | |
dc745cc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-11-29T08:33:45+01:00 | 5322957 | |
71e5891 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-11-28T23:49:34+01:00 | 95671bf | |
0402502 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 13 | 2023-12-03T20:32:52+01:00 | ||
e3f9174 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 13 | 2023-12-18T23:53:55+01:00 | ||
58c427b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 17 | 2023-12-18T01:34:01+01:00 | ||
b814eeb | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T14:11:39Z | ||
8920c11 | 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 | 2023-12-02T18:59:12Z | ||
727ff01 | 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 | 2023-12-02T23:50:59Z | ||
6c656ea | 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 | 4 | 2023-12-17T08:24:42+01:00 | ||
5322957 | 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 | 11 | 2023-11-29T01:44:22Z | ||
95671bf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T20:31:14Z | ||
75fa13f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 5 | 2023-11-30T08:25:40Z | ||
455a3e6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T12:54:48Z | ||
52e2c23 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T09:05:00Z | ||
3f0e10e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:53:44Z | ||
bb35a15 | Inspect | - content: - segment: - waypoint: action: follow location: column: 9 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ee0282f-f1f9-4818-a0c1-c36196447bfc/sv-benchmarks/c/memsafety-ext3/derefAfterFree2.c line: 9 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:06:40Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ee0282f-f1f9-4818-a0c1-c36196447bfc/sv-benchmarks/c/memsafety-ext3/derefAfterFree2.c : 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3ee0282f-f1f9-4818-a0c1-c36196447bfc/sv-benchmarks/c/memsafety-ext3/derefAfterFree2.c language: C specification: CHECK( init(main()), LTL(G valid-free) ),CHECK( init(main()), LTL(G valid-deref) ),CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 14 | 2023-11-30T02:56:34+01:00 |
Found 27 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3208831 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:33:59+01:00 | ||
091d853 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T12:48:08Z | ||
d4001a2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-29T10:43:54+01:00 | 7b52144 | |
3ee9fd0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-29T06:53:24+01:00 | f2bae41 | |
3691221 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-29T06:38:23+01:00 | 9f0b106 | |
e4c998a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-29T05:56:50+01:00 | 091d853 | |
5d3f698 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-29T04:19:22+01:00 | 7b0e2fb | |
42c765c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-29T01:32:19+01:00 | 4636906 | |
1ee8ab2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-28T21:06:33+01:00 | 49a45db | |
7a6032c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-28T15:42:10+01:00 | 3135367 | |
fa3646a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-28T14:11:29+01:00 | 3208831 | |
8e77ffe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-28T08:58:37+01:00 | c071e0d | |
2a3225d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-28T06:01:34+01:00 | 833947f | |
7ba74ad | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-28T04:21:33+01:00 | ab29dd1 | |
2e2c89a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-28T02:23:04+01:00 | 0f12b85 | |
8c9eb52 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2023-01-28T00:29:14+01:00 | 27abf50 | |
c071e0d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 13 | 2022-12-10T18:40:01+01:00 | ||
4636906 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 13 | 2022-12-11T22:06:36+01:00 | ||
49a45db | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 13 | 2022-12-10T04:04:42+01:00 | ||
833947f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 17 | 2022-12-09T03:22:22+01:00 | ||
3135367 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T22:35:58Z | ||
0f12b85 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T08:56:18Z | ||
7b52144 | 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 | 2022-12-14T07:42:13Z | ||
9f0b106 | 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 | 2022-12-14T19:27:46Z | ||
ab29dd1 | 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 | 4 | 2022-12-08T05:38:01+01:00 | ||
f2bae41 | 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 | 11 | 2022-12-13T18:07:08Z | ||
27abf50 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T17:34:00Z |
Found 25 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bbb4d3b | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T10:03:41+01:00 | ||
80b254c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T18:55:05 | ||
f7053a1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T15:23:07Z | ||
139b830 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-10T21:26:16+01:00 | 1ce47a4 | |
4252f15 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-10T17:27:10+01:00 | fd19d4a | |
b1b0b5a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-10T08:33:28+01:00 | a551d55 | |
43eb9a3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-09T16:01:15+01:00 | 1d7e16f | |
54c01e3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-09T06:21:17+01:00 | 7b0e2fb | |
71e4cd2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-08T21:06:45+01:00 | f9af772 | |
1b6898a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-08T13:47:26+01:00 | 000877f | |
ed69e40 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-07T19:12:22+01:00 | f7053a1 | |
a86ee0a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-07T11:28:08+01:00 | bbb4d3b | |
117af65 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-07T04:56:27+01:00 | 753fa68 | |
7bfe807 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-07T02:36:39+01:00 | 9395076 | |
9856b9f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-06T11:48:26+01:00 | 5c45e0f | |
010edfc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-05T20:40:34+01:00 | 7c29257 | |
7c29257 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 13 | 2021-12-05T17:45:41+01:00 | ||
f9af772 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 13 | 2021-12-08T17:43:38+01:00 | ||
1d7e16f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 13 | 2021-12-09T12:05:59+01:00 | ||
753fa68 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 17 | 2021-12-07T02:08:42+01:00 | ||
000877f | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T11:07:18Z | ||
a551d55 | 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 | 2021-12-10T05:05:58Z | ||
fd19d4a | 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 | 2021-12-10T09:03:26Z | ||
5c45e0f | 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 | 9 | 2021-12-06T03:16:08+01:00 | ||
9395076 | 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 | 11 | 2021-12-06T18:19:15Z |
Found 17 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e9ddee0 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:57:25+01:00 | ||
e92d0a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T18:30:34 | ||
deb5ca3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-09T02:23:50 | ||
0942250 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-12T01:34:54+01:00 | e92d0a5 | |
8fe86a6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-09T21:55:10+01:00 | 9ffae74 | |
386c95d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-09T21:35:26+01:00 | a738630 | |
ae2c86b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-09T04:11:49+01:00 | deb5ca3 | |
06560b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-09T01:44:40+01:00 | 73f7078 | |
95a72e7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-08T07:52:21+01:00 | 63382bf | |
2102eb0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-07T16:55:49+01:00 | fa0dadd | |
71baf7d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-06T18:28:10+01:00 | bda7fcb | |
93b6f87 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-06T18:00:53+01:00 | 1707387 | |
70c0e5e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-06T07:51:14+01:00 | bda7fcb | |
87a7b0e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-05T18:35:05+01:00 | 1707387 | |
1707387 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-05T17:03:21+01:00 | ||
63382bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 13 | 2020-12-07T22:53:21+01:00 | ||
bd8c043 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 13 | 2020-12-06T19:13:31+01:00 | e9ddee0 |
Found 13 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
480af7e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 06:29:40 | ||
1d7aeb0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-11T21:46:32+01:00 | 40d361c | |
569ccd5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-11T21:09:17+01:00 | 480af7e | |
da2ad4a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-08T00:27:19+01:00 | f6bcf87 | |
742a2e2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-03T08:09:29+01:00 | 8b4c232 | |
8b4c232 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-11-30T10:19:39+01:00 | ||
032f1f4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-07T21:12:57+01:00 | 2ecacd3 | |
2fab3a7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-03T08:57:52+01:00 | 6e20181 | |
d0c984a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 5 | 2019-12-05T20:21:27+01:00 | 8f686ff | |
5429867 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-11T22:00:46+01:00 | 49ec423 | |
8aa8690 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-11T20:55:14+01:00 | 0397d4b | |
e9b026d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 13 | 2019-12-08T00:07:31+01:00 | 7b0e2fb | |
40d361c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 13 | 2019-12-01T00:25:37+01:00 |
Found 19 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
828b3ae | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T02:18 CET (sv-comp) | ||
11542f4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-10T10:48:40+01:00 | c8d1c29 | |
d453ac8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:53:09+01:00 | 64851d5 | |
40a60dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T22:07:37+01:00 | ea8a462 | |
17df607 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T07:43:43+01:00 | e3f9ce6 | |
8160fbc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T03:41:17+01:00 | c8d1c29 | |
f961cc6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T09:17:17+01:00 | 26c2ab4 | |
e7b3a73 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:16:54+01:00 | 60f1df6 | |
ea8a462 | 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-08T10:24:27 | ||
e3f9ce6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 15 | 2018-12-08T00:50:45+01:00 | ||
11a0af1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:38:29+01:00 | fb074f6 | |
bfd27b3 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-09T20:22:12+01:00 | 787c806 | |
e29602f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T23:43:59+01:00 | 828b3ae | |
ff52a83 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-08T05:03:22+01:00 | c36a716 | |
5c2f9db | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-07T01:15:52+01:00 | 6736b60 | |
701c750 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T10:15:11+01:00 | 79133ce | |
8380bea | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 13 | 2018-12-06T09:48:52+01:00 | 4aaad98 | |
4aaad98 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-05T12:28:14+01:00 | ||
3e07b82 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:00:28+01:00 | f15ded6 |
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/derefAfterFree2_false-valid-deref.c, 6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6c5050f69dd0fe75249366946a38ba884fb5943ccf611397d2d01e0ccda347b5.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |