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).
Found 31 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c, ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b99c6a5 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:13:20+01:00 | ||
bc63ff3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-19T05:26:14+01:00 | 0e8e528 | |
74ada1e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-18T12:01:10+01:00 | b99c6a5 | |
f501268 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-18T03:09:15+01:00 | 19f6171 | |
47c4f5e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-17T22:07:18+01:00 | 073a8e4 | |
d0a25a7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-05T14:39:26+01:00 | 9f0e8d7 | |
174d0d9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-04T16:44:52+01:00 | df5fa6d | |
f593a76 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-04T12:11:55+01:00 | e09d922 | |
b54b3a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-04T02:25:40+01:00 | adaab0f | |
a391719 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-03T06:18:30+01:00 | ddb73cd | |
85114ee | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-01T22:55:01+01:00 | 78b128b | |
f287198 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-01T18:29:33+01:00 | c513ec5 | |
61c8310 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-30T13:43:07+01:00 | 219cf0a | |
3388ba6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-30T09:44:18+01:00 | 0cfe110 | |
219cf0a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:54:47+01:00 | ||
ada3f8e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:32:59+01:00 | 34c31ec | |
5acf7da | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-28T23:49:34+01:00 | 04e0cd4 | |
adaab0f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T21:54:09+01:00 | ||
0e8e528 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T22:43:33+01:00 | ||
19f6171 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2023-12-18T02:23:53+01:00 | ||
1ec357d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T21:06:20Z | ||
c513ec5 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T10:47:21Z | ||
e09d922 | 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 | 5 | 2023-12-02T15:58:52Z | ||
ddb73cd | 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 | 5 | 2023-12-02T21:37:04Z | ||
073a8e4 | 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 | 3 | 2023-12-17T20:34:46+01:00 | ||
34c31ec | 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 | 5 | 2023-11-29T05:01:21Z | ||
04e0cd4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T19:51:06Z | ||
0cfe110 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:24:57Z | ||
9f0e8d7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T11:45:59Z | ||
df5fa6d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T13:01:50Z | ||
78b128b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:35:49Z |
Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c, ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ad5096e | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:15:09+01:00 | ||
954f250 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T12:59:12Z | ||
ebab2a9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T10:45:02+01:00 | 777e747 | |
d68a087 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:54:15+01:00 | 13870a3 | |
edc12e7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:38:30+01:00 | dde7cdd | |
86ab142 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T05:58:42+01:00 | 954f250 | |
977ead0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T04:19:12+01:00 | 7d8d8f4 | |
a66100c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T01:30:21+01:00 | 6bf640e | |
6dc68fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T21:06:20+01:00 | 3b2b0a3 | |
81245ac | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T15:43:56+01:00 | 7d3b913 | |
e37ddae | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T14:11:21+01:00 | ad5096e | |
a20cf2f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T08:55:42+01:00 | c4a1518 | |
8f2f8c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T06:01:36+01:00 | 1424ae6 | |
366ad5c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T04:21:53+01:00 | cfbc9ec | |
94eb2ce | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T02:20:48+01:00 | 1e16009 | |
fe6216c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-28T00:29:25+01:00 | 6a2458b | |
c4a1518 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2022-12-10T17:19:01+01:00 | ||
6bf640e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T21:39:58+01:00 | ||
1424ae6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2022-12-09T02:44:50+01:00 | ||
7d3b913 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T22:20:30Z | ||
1e16009 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T12:26:33Z | ||
3b2b0a3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-09T17:08:57+01:00 | ||
777e747 | 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 | 5 | 2022-12-14T06:15:00Z | ||
dde7cdd | 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 | 5 | 2022-12-15T00:38:13Z | ||
cfbc9ec | 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 | 3 | 2022-12-08T10:03:50+01:00 | ||
13870a3 | 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 | 5 | 2022-12-13T18:27:41Z | ||
6a2458b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T14:29:31Z |
Found 27 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c, ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6539740 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T07:56:32+01:00 | ||
bac5d60 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:44:28 | ||
17a235d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T16:20:52Z | ||
0384438 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-10T21:29:07+01:00 | e209b44 | |
f654f14 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-10T17:27:37+01:00 | 022c0f5 | |
8e4a1ec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-10T08:34:20+01:00 | 1e95ff0 | |
7f87998 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-09T16:03:24+01:00 | 87fa41e | |
9c3f927 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-09T06:21:39+01:00 | 7d8d8f4 | |
8726be7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-08T21:11:31+01:00 | 4bab1cd | |
db712c7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-08T13:48:03+01:00 | d90d440 | |
bb33201 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-07T19:12:17+01:00 | 17a235d | |
3828e6b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-07T11:26:02+01:00 | 6539740 | |
cdef524 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-07T04:56:30+01:00 | b2e8edd | |
be44763 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-07T02:37:04+01:00 | b456dba | |
72a67a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-06T12:47:38+01:00 | 627686b | |
4b1b2d6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-06T11:47:44+01:00 | 92474ca | |
72a5332 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-05T20:40:25+01:00 | 26d4ac3 | |
26d4ac3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-05T18:46:40+01:00 | ||
4bab1cd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 6 | 2021-12-08T17:57:05+01:00 | ||
87fa41e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2021-12-09T13:48:32+01:00 | ||
b2e8edd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2021-12-07T03:54:51+01:00 | ||
d90d440 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T09:07:44Z | ||
1e95ff0 | 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 | 5 | 2021-12-10T00:54:31Z | ||
022c0f5 | 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 | 5 | 2021-12-10T14:12:58Z | ||
92474ca | 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 | 2021-12-06T08:57:11+01:00 | ||
b456dba | 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 | 5 | 2021-12-07T00:30:43Z | ||
627686b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 3 | 2021-12-06T11:23:14+01:00 |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c, ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b6eaa89 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:46:53+01:00 | ||
f325427 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T19:52:56 | ||
e502c34 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T14:12:34 | ||
a95b000 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-09T02:08:59+01:00 | af3e69c | |
3717dda | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-08T07:48:59+01:00 | ac87075 | |
2c17f60 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-07T16:58:48+01:00 | 90dd2eb | |
38b5dc1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-06T18:28:42+01:00 | ee33034 | |
db2b86b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-05T18:22:42+01:00 | e0f0632 | |
ac87075 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2020-12-08T05:38:03+01:00 | ||
e0f0632 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-05T13:03:26+01:00 | ||
e3be454 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-12T01:41:53+01:00 | f325427 | |
eba4a3e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-09T22:13:31+01:00 | 0202b8e | |
aab24f8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-09T21:49:50+01:00 | b5cd904 | |
447cf20 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-09T04:11:48+01:00 | e502c34 | |
29305d7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-06T19:02:32+01:00 | b6eaa89 | |
707f1b4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-06T18:00:44+01:00 | e0f0632 | |
2f98313 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-06T07:39:20+01:00 | ee33034 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c, ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5caae42 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-02 00:42:49 | ||
c973d68 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-11T20:54:29+01:00 | 197bcc2 | |
9d10d59 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-08T00:27:07+01:00 | 25e03ab | |
d763f79 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-08T00:06:09+01:00 | 7d8d8f4 | |
1729a33 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-06T02:38:15+01:00 | 740cd2d | |
3316a96 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-03T08:08:12+01:00 | ada00aa | |
862a8c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6 | 2019-12-01T05:02:21+01:00 | ||
9c20558 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-11T21:46:52+01:00 | a6527d7 | |
3489bae | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-11T21:41:02+01:00 | 862a8c9 | |
6d6564f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-07T21:17:02+01:00 | 98aa060 | |
9a1f35b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-05T20:20:50+01:00 | 59ce1fc | |
633b00a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-03T08:56:48+01:00 | 6f00c92 | |
77f5d11 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-12-11T21:09:14+01:00 | 5caae42 | |
ada00aa | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-11-29T16:30:06+01:00 |
Found 19 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c, ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ac91c23 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T03:05 CET (sv-comp) | ||
a837811 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-07T15:43:18+01:00 | ||
5ad82ef | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T23:43:50+01:00 | ac91c23 | |
ed64212 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T22:10:53+01:00 | a57c22c | |
b4a2782 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T08:04:18+01:00 | a837811 | |
5ff812f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T03:10:45+01:00 | ||
12de5fa | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-10T10:48:40+01:00 | a7b81ea | |
21a00b0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T09:25:36+01:00 | a45f71e | |
a57c22c | 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-08T03:29:55 | ||
f7bd32c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:53:15+01:00 | bd70a2b | |
4550ab4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:38:42+01:00 | fc61a27 | |
f3b78cc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-09T20:17:45+01:00 | c15f18a | |
1673b72 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T04:58:06+01:00 | 40fdeaa | |
01076c5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T03:25:55+01:00 | a7b81ea | |
43d3f8a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-07T01:20:53+01:00 | 314737a | |
5e1656c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T10:18:04+01:00 | 5d18e15 | |
53e1fa1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:48:02+01:00 | 5ff812f | |
468bf6d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:08:47+01:00 | 635325e | |
9eda0c8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T09:00:20+01:00 | 490d661 |
Found 12 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c, ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7095787 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:39 CET (sv-comp) | ||
691103e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T08:30:08+01:00 | ||
ae2df6a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:33:37.227701 | ||
fee6789 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:50:38.195316 | ||
e873c6f | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 5 | 2017-12-01T09:30 CET (sv-comp) | ||
0a31e82 | 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 | 5 | 2017-12-03T06:53Z | ||
3e2886e | 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 | 5 | 2017-12-03T04:22Z | ||
0ac49bf | 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 | 2017-12-01T08:28 CET (sv-comp) | ||
e7ec4ff | 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 | 5 | 2017-12-03T04:06Z | ||
fa30890 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | 2LS | 4 | 2017-12-01T08:19 CET (sv-comp) | ||
a45f71e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:13 CET (sv-comp) | ||
3d870a6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:16 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c, ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ae57481434c4d2d83f3418f57c937e0ced919170ca4bdab03ab9b5db6056f353.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |