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 27 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
98f4537 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:12:53+01:00 | ||
5cc9e88 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T20:18:33Z | ||
db1cf47 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T15:33:54+01:00 | b5ef6ed | |
bd9a99d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:27:14+01:00 | 272356a | |
c90f5f2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:02:06+01:00 | 98f4537 | |
2b512d8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:09:52+01:00 | c4243ca | |
71f60ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:10:48+01:00 | cf63783 | |
314d8de | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:37:41+01:00 | 58418ca | |
2dc698f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:43:07+01:00 | d2486f4 | |
f78a2ad | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:27:35+01:00 | 19e5689 | |
8fe20a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:53:33+01:00 | 90e2114 | |
54614fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:42:46+01:00 | 0c92acd | |
0c92acd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T09:10:18+01:00 | ||
cdf0c25 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:01:22+01:00 | 5cc9e88 | |
1767083 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:49:49+01:00 | 5d0c10e | |
19e5689 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-04T00:41:49+01:00 | ||
c4243ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2023-12-18T01:34:57+01:00 | ||
ff77329 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-01T18:27:16+01:00 | e19cdba | |
e19cdba | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T10:49:32Z | ||
b5ef6ed | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2023-12-19T12:30:12+01:00 | ||
cf63783 | 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-17T19:29:19+01:00 | ||
5d0c10e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T22:17:24Z | ||
272356a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T20:14:06+01:00 | ||
58418ca | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T11:40:32Z | ||
d2486f4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T09:53:12Z | ||
90e2114 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T19:38:58Z | ||
636a4eb | Inspect | - content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_97b054c5-7637-49b4-bb32-10ae097d106b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3-2.i line: 41 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:18:33Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_97b054c5-7637-49b4-bb32-10ae097d106b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3-2.i : 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_97b054c5-7637-49b4-bb32-10ae097d106b/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3-2.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:58:45+01:00 |
Found 22 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ee44764 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:10:41+01:00 | ||
118bb31 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T12:11:35Z | ||
d674ad2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:58:24+01:00 | 118bb31 | |
695598e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:30:17+01:00 | a6b7fba | |
2b0c4e6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T00:54:36+01:00 | da36b51 | |
0091ae7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:08:09+01:00 | 91cf44b | |
bcad851 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:20:24+01:00 | ee44764 | |
eca75a4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:54:05+01:00 | 6fec853 | |
f29520b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:01:06+01:00 | a7dee7d | |
11ebe20 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:23:12+01:00 | 5e514c2 | |
29b1aba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:29:30+01:00 | 641a1d0 | |
6fec853 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T20:43:58+01:00 | ||
a6b7fba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-12T00:48:53+01:00 | ||
91cf44b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-09T23:36:43+01:00 | ||
a7dee7d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2022-12-09T02:28:07+01:00 | ||
391b9b1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T15:45:11+01:00 | 4098bc0 | |
af88681 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T02:20:10+01:00 | 33d278b | |
4098bc0 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T15:54:13Z | ||
33d278b | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T08:50:23Z | ||
5e514c2 | 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-08T08:37:14+01:00 | ||
da36b51 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2022-12-11T02:09:55+01:00 | ||
641a1d0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T15:18:21Z |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
72f8fad | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:19:38+01:00 | ||
d4a81bd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T18:10:38 | ||
865aad9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T14:04:30Z | ||
bca652f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T16:00:36+01:00 | c75911e | |
2024650 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:06:49+01:00 | e1a6f0f | |
b9db0a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:11:48+01:00 | 865aad9 | |
1daee13 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:24:51+01:00 | 72f8fad | |
a79764d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:55:52+01:00 | 6bfba35 | |
ebaf831 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T12:47:29+01:00 | b30b980 | |
2cb8fa5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:46:24+01:00 | b1a320d | |
addeeb3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:39:05+01:00 | 2077092 | |
2077092 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T18:30:57+01:00 | ||
6bfba35 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2021-12-07T01:56:48+01:00 | ||
7929750 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-10T21:25:38+01:00 | 6e5f1a6 | |
630369b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 8 | 2021-12-08T13:49:35+01:00 | e4475fb | |
e4475fb | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T04:54:32Z | ||
e1a6f0f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T20:06:41+01:00 | ||
b1a320d | 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-06T07:39:17+01:00 | ||
b30b980 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 3 | 2021-12-06T11:28:06+01:00 | ||
c75911e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T13:02:54+01:00 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c9edf43 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:06:46+01:00 | ||
6c4c285 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T19:24:38 | ||
0f235af | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-09T00:30:12 | ||
3c05f91 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:20:21+01:00 | 6c4c285 | |
e0b14b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T03:59:01+01:00 | 0f235af | |
0027e40 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T06:48:22+01:00 | a8a4ccd | |
84afcaf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T19:40:30+01:00 | c9edf43 | |
5440c03 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:25:27+01:00 | af95878 | |
f70114a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:49:42+01:00 | af95878 | |
a8a4ccd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T03:07:58+01:00 | ||
616122c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 8 | 2020-12-07T16:34:56+01:00 | ebfd887 | |
c4208e9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:00:26+01:00 | c9caea0 | |
602d4ba | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T17:59:04+01:00 | c9caea0 | |
c9caea0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T17:11:55+01:00 |
Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ca63a28 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 14:24:25 | ||
55e71c5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:54:25+01:00 | 2eb4708 | |
3dbb775 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:38:02+01:00 | e319b8f | |
164d88f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:10:15+01:00 | e275e74 | |
e275e74 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-29T14:43:42+01:00 | ||
2eb4708 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T01:47:56+01:00 | ||
d2aff32 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:45+01:00 | ca63a28 | |
e978991 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:20:30+01:00 | 62e0cca | |
66d8c2d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:50+01:00 | 3f57a79 | |
c4cc3f7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 8 | 2019-12-11T20:54:59+01:00 | f9373e5 |
Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d260e76 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T03:18 CET (sv-comp) | ||
bd34c58 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T20:28:57+01:00 | ||
a5d58eb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:54+01:00 | 7ac8600 | |
d5878db | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T23:44:42+01:00 | d260e76 | |
cc3611b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T08:49:37+01:00 | bd34c58 | |
c6e3272 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:48:10+01:00 | a6acc9c | |
1517697 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:18:33+01:00 | a6bb557 | |
61c397b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:17:22+01:00 | 7535854 | |
a6acc9c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T02:11:31+01:00 | ||
44b71ff | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-06T10:20:09+01:00 | 64779a5 | |
376450c | 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-08T11:00:58 | ||
c90406f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:11:04+01:00 | 376450c | |
b511d68 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T04:12:57+01:00 | 7ac8600 | |
50aa4e0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-07T01:18:41+01:00 | 0968068 | |
9e6c929 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 8 | 2018-12-08T04:56:50+01:00 | 0debcee |
Found 6 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3cce530 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:25 CET (sv-comp) | ||
665ea4c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:23:34+01:00 | ||
6201f8c | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T12:01:25.111407 | ||
93855b1 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:31:42.336180 | ||
007f036 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 3.1 | 7 | 2017-12-01T09:24 CET (sv-comp) | ||
fd2f33f | 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 | 2017-12-01T08:22 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i, 377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/377aee86f3d25151744ba97c5be1cc51175a6c56601277d198adc5214d6e67f8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |