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/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c |
programSHA | 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740 |
witnessName | results-validated/cpa-seq-validate-violation-witnesses-esbmc-kind.2018-12-08_0449.logfiles/sv-comp19_prop-memsafety.ArraysOfVariableLength2_false-valid-deref-read.c.files/witness.graphml |
witnessSHA | 1229ee2f74d51af2a97f0f1dab3c2a81da23f03457458c8f2deec30c9813404e |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T05:04:22+01:00 |
inputwitnesshash | 48ea5a0e8e1e5c9139d29e7ef98b2b7c919a4c3ff981d1d54e408807f452197e |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740 |
programfile | ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c |
programhash | 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-deref) ) |
witness-file | witnessFileByHash/1229ee2f74d51af2a97f0f1dab3c2a81da23f03457458c8f2deec30c9813404e.graphml |
witness-sha256 | 1229ee2f74d51af2a97f0f1dab3c2a81da23f03457458c8f2deec30c9813404e |
witness-size | 7446 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740).
Found 33 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e4ee27b | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:47:22+01:00 | ||
7da2839 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T20:49:14Z | ||
74e0977 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-19T05:27:03+01:00 | aa0040a | |
4e538b9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-18T12:07:26+01:00 | e4ee27b | |
08cfc6c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-18T03:09:38+01:00 | a212266 | |
3eda256 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-17T22:11:13+01:00 | 870bb62 | |
07640ad | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-05T14:38:51+01:00 | 8410a12 | |
69c2af8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-04T16:44:21+01:00 | 73758f5 | |
5c51337 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-04T12:13:32+01:00 | b884404 | |
b446a2f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-04T02:27:19+01:00 | 57bcf15 | |
17f49b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-03T06:18:09+01:00 | 849a20b | |
2069006 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-01T22:55:20+01:00 | 5f9a881 | |
395e7a4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-12-01T18:29:22+01:00 | 55fc0dc | |
b5ba090 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T13:42:36+01:00 | 52f8297 | |
691820a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T09:44:00+01:00 | e9171ea | |
52f8297 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-30T06:36:53+01:00 | ||
53fc346 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T03:02:16+01:00 | 7da2839 | |
35aa49d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-29T08:33:03+01:00 | e8bd7c0 | |
b0301ae | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-28T23:49:35+01:00 | 15a17c3 | |
57bcf15 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 7 | 2023-12-03T18:10:55+01:00 | ||
a212266 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2023-12-18T01:45:53+01:00 | ||
55fc0dc | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T11:40:05Z | ||
b884404 | 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 | 6 | 2023-12-02T16:00:34Z | ||
849a20b | 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 | 6 | 2023-12-03T00:16:29Z | ||
870bb62 | 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-17T18:55:53+01:00 | ||
e8bd7c0 | 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 | 6 | 2023-11-28T19:21:46Z | ||
15a17c3 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T22:16:00Z | ||
e9171ea | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:24:59Z | ||
aa0040a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-18T20:34:05+01:00 | ||
8410a12 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T07:54:05Z | ||
73758f5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T13:43:18Z | ||
5f9a881 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:29:21Z | ||
ac9590a | Inspect | - content: - segment: - waypoint: action: follow location: column: 6 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3805094c-8c90-449b-b5b9-04856a8043a3/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-read.c line: 14 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:49:14Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3805094c-8c90-449b-b5b9-04856a8043a3/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-read.c : 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_3805094c-8c90-449b-b5b9-04856a8043a3/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_-read.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 | 8 | 2023-11-30T02:58:20+01:00 |
Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7c102d0 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:21:12+01:00 | ||
2080a64 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T14:27:30Z | ||
a721342 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T10:45:05+01:00 | a586923 | |
9b92e7b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T06:52:34+01:00 | d4109ff | |
47a236b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T06:38:37+01:00 | 62dce7e | |
bdb243b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T05:57:57+01:00 | 2080a64 | |
be763e5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T04:19:26+01:00 | ac1ea66 | |
e3c9b6f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-29T01:30:26+01:00 | dd80107 | |
1da958f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T21:05:52+01:00 | 1553d6b | |
0150b36 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T15:43:20+01:00 | a5bc219 | |
641eea8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T14:18:10+01:00 | 7c102d0 | |
63070c3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T08:54:41+01:00 | 038e428 | |
d7493d9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T06:01:11+01:00 | 55f6792 | |
d4551b3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T04:22:31+01:00 | 3419557 | |
6696efe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T02:21:10+01:00 | bf8d990 | |
42a85c0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2023-01-28T00:29:22+01:00 | a56ce22 | |
038e428 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 7 | 2022-12-10T15:18:24+01:00 | ||
dd80107 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 7 | 2022-12-11T21:41:05+01:00 | ||
55f6792 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2022-12-09T03:00:31+01:00 | ||
a5bc219 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T17:33:39Z | ||
bf8d990 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T09:54:33Z | ||
a586923 | 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 | 6 | 2022-12-14T12:39:42Z | ||
62dce7e | 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 | 6 | 2022-12-14T20:57:20Z | ||
3419557 | 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-08T04:23:21+01:00 | ||
d4109ff | 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 | 6 | 2022-12-13T18:15:17Z | ||
1553d6b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-10T01:52:21+01:00 | ||
a56ce22 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T20:56:07Z |
Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ee728da | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:28:25+01:00 | ||
993bcd9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T16:07:40 | ||
ede0f5f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T13:49:27Z | ||
f7190b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-10T21:28:31+01:00 | 7fce120 | |
99ec8d3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-10T17:27:06+01:00 | f42ec0a | |
932a090 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-10T08:33:04+01:00 | 990da96 | |
6c60cb8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-09T16:02:48+01:00 | a9f942f | |
829951c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-09T06:21:45+01:00 | ac1ea66 | |
50525d4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-08T21:06:55+01:00 | 5eeee43 | |
6ab65b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-08T13:50:11+01:00 | 7c133d8 | |
63ce947 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-07T19:13:43+01:00 | ede0f5f | |
a1c418f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-07T11:27:54+01:00 | ee728da | |
6c18144 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-07T04:55:56+01:00 | 0887c5c | |
51932b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-07T02:36:10+01:00 | 3ebd01e | |
bdfdc7b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-06T12:47:38+01:00 | 3e93b96 | |
cc310ab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-05T20:39:04+01:00 | 48f7d1c | |
48f7d1c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 7 | 2021-12-05T15:40:26+01:00 | ||
5eeee43 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 7 | 2021-12-08T18:06:51+01:00 | ||
a9f942f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2021-12-09T14:10:18+01:00 | ||
0887c5c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2021-12-07T02:12:05+01:00 | ||
5cd6662 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 11 | 2021-12-06T11:48:21+01:00 | aef452d | |
7c133d8 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T09:42:22Z | ||
990da96 | 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 | 6 | 2021-12-10T04:03:51Z | ||
f42ec0a | 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 | 6 | 2021-12-10T08:44:06Z | ||
aef452d | 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 | 5 | 2021-12-06T02:08:54+01:00 | ||
3ebd01e | 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 | 6 | 2021-12-06T17:19:39Z | ||
3e93b96 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 3 | 2021-12-06T11:17:09+01:00 |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8f19a21 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:54:50+01:00 | ||
12bfac8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T15:25:17 | ||
8657117 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T19:17:36 | ||
21fd983 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-09T21:55:52+01:00 | 6eb6a1f | |
3adfce3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-07T16:54:17+01:00 | 1391632 | |
9a44b95 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-06T19:38:46+01:00 | 8f19a21 | |
b2cb6cb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 7 | 2020-12-08T00:00:40+01:00 | ||
e708d5d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-09T21:31:15+01:00 | 3acb7f1 | |
536d45f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-09T02:02:43+01:00 | 0395eec | |
601f5cd | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-08T07:27:57+01:00 | b2cb6cb | |
8806887 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 11 | 2020-12-06T18:25:22+01:00 | 3c4dc01 | |
959cfa9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 11 | 2020-12-06T07:34:54+01:00 | 3c4dc01 | |
59c340e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-12T01:36:39+01:00 | 12bfac8 | |
72c3e55 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-09T03:58:36+01:00 | 8657117 | |
399131e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-06T18:00:54+01:00 | 33c2d11 | |
16ffb8e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-05T18:29:16+01:00 | 33c2d11 | |
33c2d11 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 7 | 2020-12-05T16:36:39+01:00 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
faf3bd8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 11:49:18 | ||
552514e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-11T21:43:16+01:00 | 03d3a92 | |
f95a16b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-11T20:54:47+01:00 | cb4c562 | |
d351417 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-06T02:40:49+01:00 | 159d902 | |
441f7a7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-03T08:10:10+01:00 | 2b2b699 | |
2b2b699 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-11-30T11:46:20+01:00 | ||
21a4fd7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 7 | 2019-12-01T09:20:16+01:00 | ||
46bb0e4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-11T21:09:44+01:00 | faf3bd8 | |
f09675e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-07T21:16:17+01:00 | 893da6b | |
ed485bb | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 10 | 2019-12-05T20:20:40+01:00 | 938662c | |
6e9826d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-11T21:53:32+01:00 | 21a4fd7 | |
ee54270 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-08T00:27:17+01:00 | a63a3c0 | |
351ebf0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-08T00:06:03+01:00 | ac1ea66 | |
b27fccc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 7 | 2019-12-03T08:56:49+01:00 | 0c50a71 |
Found 19 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9276cdd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T02:27 CET (sv-comp) | ||
765acf5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-10T10:48:43+01:00 | 46df281 | |
24acc24 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:42:36+01:00 | 9276cdd | |
511a348 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T08:56:13+01:00 | cae3cd2 | |
98526d2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:48:01+01:00 | 0c16d0a | |
0c16d0a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-05T10:18:17+01:00 | ||
cf0bb5a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:18:59+01:00 | 59e1a70 | |
d7b49c6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 10 | 2018-12-06T09:18:04+01:00 | 2bd5a0d | |
5bcf470 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T20:37:09+01:00 | e732d9b | |
1b69117 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T09:24:59+01:00 | 809f85b | |
2ac396b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T10:19:11+01:00 | 1cf155e | |
d59001c | 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-08T05:49:08 | ||
cae3cd2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 7 | 2018-12-06T20:02:40+01:00 | ||
3a34468 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T20:53:23+01:00 | ffb2edd | |
c3f493c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-09T20:21:38+01:00 | c236f59 | |
52df65c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T22:10:02+01:00 | d59001c | |
1229ee2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T05:04:22+01:00 | 48ea5a0 | |
c6812c7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T03:36:09+01:00 | 46df281 | |
405415a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T01:16:49+01:00 | a8ff427 |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
97c09aa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:20 CET (sv-comp) | ||
d1a8633 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T10:49:15.844043 | ||
cb112be | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:14:33.827777 | ||
5fdb2d6 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T09:38 CET (sv-comp) | ||
ab404a3 | 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 | 6 | 2017-12-03T06:58Z | ||
fc03110 | 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 | 6 | 2017-12-03T04:12Z | ||
ff34165 | 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 | 6 | 2017-12-01T08:31 CET (sv-comp) | ||
dd58e91 | 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 | 6 | 2017-12-03T04:06Z | ||
809f85b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:03 CET (sv-comp) | ||
cbea6ba | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 4 | 2017-12-01T23:39 CET (sv-comp) | ||
9497faf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T08:31:06+01:00 |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c, 07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/07a396ef153f1ca8e856eefcfa25d3d77eb73f779a009e48698bf5ce12969740.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |