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 25 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b5e7e67 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:35:40+01:00 | ||
f057e52 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T20:14:48Z | ||
ade8075 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:26:09+01:00 | 634b1a1 | |
a6fd8e8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:05:35+01:00 | b5e7e67 | |
71c5831 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:09:33+01:00 | 32aa94c | |
224ea21 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:09:02+01:00 | fa1d731 | |
6069856 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:37:25+01:00 | c677a4e | |
da9fccb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:40:58+01:00 | ac39b85 | |
32a9e30 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:26:19+01:00 | c0a975f | |
adf3e98 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:55:05+01:00 | b2512f7 | |
89954e0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:44:52+01:00 | 8b82289 | |
8b82289 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-11-30T07:01:34+01:00 | ||
6799b63 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:01:09+01:00 | f057e52 | |
899a27f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:49:32+01:00 | 16804ad | |
c0a975f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T20:32:33+01:00 | ||
32aa94c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 5 | 2023-12-18T02:02:04+01:00 | ||
f6527b4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T18:27:38+01:00 | af7e10a | |
af7e10a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T15:57:11Z | ||
fa1d731 | 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-17T16:59:26+01:00 | ||
16804ad | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T21:05:24Z | ||
634b1a1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T21:53:59+01:00 | ||
c677a4e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T07:13:07Z | ||
ac39b85 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T08:34:59Z | ||
b2512f7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:21:40Z | ||
511dcb1 | Inspect | - content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37fc73e8-efb7-4901-9feb-513b0cc06b5b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2-1.i line: 31 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:14:48Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37fc73e8-efb7-4901-9feb-513b0cc06b5b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2-1.i : 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_37fc73e8-efb7-4901-9feb-513b0cc06b5b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2-1.i 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 | 4 | 2023-11-30T02:56:24+01:00 |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b0eb3ef | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:29:04+01:00 | ||
fa08476 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T13:19:53Z | ||
fca9ec3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:57:35+01:00 | fa08476 | |
56743ea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:30:33+01:00 | 2bb89a4 | |
3a7e784 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:05:51+01:00 | 1d5de4b | |
58a5532 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:16:56+01:00 | b0eb3ef | |
a0f1365 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:54:00+01:00 | 023bc9f | |
281e56b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:01:00+01:00 | 8a8476e | |
a931841 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:23:40+01:00 | 7e164ef | |
b379350 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:28:02+01:00 | 86c814a | |
023bc9f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T19:24:53+01:00 | ||
2bb89a4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T19:41:28+01:00 | ||
1d5de4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T02:55:56+01:00 | ||
8a8476e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 5 | 2022-12-09T03:01:56+01:00 | ||
79dcd4a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:44:20+01:00 | ff960c8 | |
8efb9bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:24:34+01:00 | 66a50b4 | |
ff960c8 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T23:51:20Z | ||
66a50b4 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T08:19:14Z | ||
7e164ef | 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-08T04:13:31+01:00 | ||
86c814a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T13:03:30Z |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
55c480f | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T07:49:52+01:00 | ||
420f649 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T16:05:08 | ||
bf4a3dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T14:23:40Z | ||
62b82e5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T16:03:11+01:00 | 46fcd0d | |
8562222 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:10:42+01:00 | e3a3ec0 | |
4ca4de1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:11:02+01:00 | bf4a3dc | |
9b5c020 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:28:02+01:00 | 55c480f | |
ff75c44 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:55:39+01:00 | 48af3f7 | |
06611cd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T12:47:38+01:00 | 7a116d5 | |
c48b654 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:46:14+01:00 | 481c1fc | |
5e34a16 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:41:16+01:00 | d1e65b5 | |
d1e65b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T18:02:00+01:00 | ||
46fcd0d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T14:36:06+01:00 | ||
48af3f7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 5 | 2021-12-07T02:11:45+01:00 | ||
46781a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2021-12-10T21:26:24+01:00 | 5b3be23 | |
db67bd2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2021-12-08T13:48:06+01:00 | f8ebd89 | |
f8ebd89 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T06:43:31Z | ||
e3a3ec0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T19:04:05+01:00 | ||
481c1fc | 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-06T07:05:24+01:00 | ||
7a116d5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 3 | 2021-12-06T11:57:09+01:00 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
543a486 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T12:44:41+01:00 | ||
28774e7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T21:57:54 | ||
92640de | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-09T00:46:00 | ||
da130ef | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:41:57+01:00 | 28774e7 | |
abd83c4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T04:12:29+01:00 | 92640de | |
a171930 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T06:32:50+01:00 | 143472a | |
81fb524 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T19:38:36+01:00 | 543a486 | |
1c1781f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:34:44+01:00 | ad1f8fe | |
3f587a3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T15:18:26+01:00 | ||
143472a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-07T23:18:56+01:00 | ||
4ccf5c5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:01:46+01:00 | 3f587a3 | |
2ebb649 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 5 | 2020-12-07T16:30:11+01:00 | acfd46c | |
c4fa6dd | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:28:30+01:00 | ad1f8fe | |
dacc82f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T18:27:27+01:00 | 3f587a3 |
Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
679575c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 10:09:48 | ||
f150a23 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:09+01:00 | 679575c | |
6d3e5c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:21:39+01:00 | f6e87a3 | |
d0cb374 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-30T09:53:16+01:00 | ||
0409a20 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:18+01:00 | c8bd57e | |
94b5106 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-11-30T21:27:21+01:00 | ||
c24a851 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T22:00:26+01:00 | 94b5106 | |
763eb5b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:39:51+01:00 | e8ed874 | |
b9fbed5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:09:02+01:00 | d0cb374 | |
23c7b2d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 5 | 2019-12-11T20:54:48+01:00 | 5b5ef41 |
Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0a1b8ea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T14:29 CET (sv-comp) | ||
105d40a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T22:10:08+01:00 | 0393e62 | |
28a2c4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T08:40:57+01:00 | b6ad5ce | |
ee28607 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:48:45+01:00 | 6821d97 | |
9e65db0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:19:58+01:00 | 0ac0373 | |
a388992 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:54:27+01:00 | 5c4227b | |
b6ad5ce | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 5 | 2018-12-07T19:18:13+01:00 | ||
a4fe933 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:48:48+01:00 | 01acbc7 | |
0393e62 | 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:37:15 | ||
909ee52 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:43:42+01:00 | 0a1b8ea | |
3f4394e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T03:25:14+01:00 | 01acbc7 | |
92d1cff | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T01:13:03+01:00 | 089977d | |
f305f62 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:00:14+01:00 | bee675f | |
6821d97 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T04:05:27+01:00 | ||
31a917b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T10:19:30+01:00 | 761a515 |
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5f036ad | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:24 CET (sv-comp) | ||
f1db14d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 5 | 2017-12-01T08:34:20+01:00 | ||
0d653a3 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:47:12.164402 | ||
c5056fb | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:30:31.914125 | ||
a7e8ecb | 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) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i, 71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/71977ff88a5661752c5d5a01d4769f04334116a88a2d9fa84ec77e61067c50d4.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |