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.1_false-valid-deref.i, b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4fbbb0d | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:58:50+01:00 | ||
369eb99 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T19:01:04Z | ||
9e04605 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T15:32:30+01:00 | bff5042 | |
222e34b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:27:00+01:00 | 5bb0ddc | |
4e46153 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:05:12+01:00 | 4fbbb0d | |
3f56afb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:09:48+01:00 | 1e8bbf3 | |
5c8b337 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:07:35+01:00 | a782499 | |
d8671b3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:37:41+01:00 | 82b1d8d | |
502e806 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:39:23+01:00 | ff6d6e8 | |
965386a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:26:11+01:00 | 343fa00 | |
1588bc2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:53:45+01:00 | 2b143ce | |
aed2e6e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:44:18+01:00 | 5dfc125 | |
5dfc125 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T08:05:42+01:00 | ||
96713b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:04:55+01:00 | 369eb99 | |
dcd2be2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:49:41+01:00 | 1d127a7 | |
343fa00 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T22:10:43+01:00 | ||
bff5042 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2023-12-19T10:39:18+01:00 | ||
1e8bbf3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2023-12-18T01:33:29+01:00 | ||
97fc7e4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T18:27:31+01:00 | fd801f9 | |
fd801f9 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T13:17:26Z | ||
a782499 | 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-17T12:12:06+01:00 | ||
1d127a7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T21:52:06Z | ||
5bb0ddc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-19T00:56:43+01:00 | ||
82b1d8d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T09:25:47Z | ||
ff6d6e8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T05:21:53Z | ||
2b143ce | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:51:04Z | ||
1b69ebd | Inspect | - content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c7367ec9-4137-4685-90f1-5b72ee0d85c7/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1-2.i line: 42 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:01:04Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c7367ec9-4137-4685-90f1-5b72ee0d85c7/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1-2.i : b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_c7367ec9-4137-4685-90f1-5b72ee0d85c7/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1-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:56:43+01:00 |
Found 22 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i, b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
257f9df | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:52:26+01:00 | ||
f13de33 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T10:41:01Z | ||
1511c2b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:58:41+01:00 | f13de33 | |
7d51ad3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:31:08+01:00 | 9403797 | |
3ca9d67 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T00:55:02+01:00 | 4f09348 | |
caced13 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:08:36+01:00 | 3f481f2 | |
78f3090 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:13:06+01:00 | 257f9df | |
d42e9da | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:56:19+01:00 | 9e3b4ed | |
380463e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:01:18+01:00 | 9fb8409 | |
4357e47 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:23:14+01:00 | 174e5a2 | |
763fb80 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:28:02+01:00 | 32b52d5 | |
9e3b4ed | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T17:43:06+01:00 | ||
9403797 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T20:55:26+01:00 | ||
4f09348 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2022-12-11T05:59:16+01:00 | ||
3f481f2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T04:19:27+01:00 | ||
9fb8409 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2022-12-09T02:56:05+01:00 | ||
d346e8e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T15:45:25+01:00 | 083db42 | |
e16072b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T02:24:42+01:00 | b65ea28 | |
083db42 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T16:38:38Z | ||
b65ea28 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T11:51:23Z | ||
174e5a2 | 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-08T02:32:08+01:00 | ||
32b52d5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T15:39:58Z |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i, b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e28c850 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:18:52+01:00 | ||
c608f99 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T19:18:21 | ||
da77726 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T15:31:01Z | ||
2478edd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T16:02:56+01:00 | 88eeb26 | |
6547000 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:09:28+01:00 | f0e5580 | |
e03f66b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:14:04+01:00 | da77726 | |
198b934 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:24:31+01:00 | e28c850 | |
dc97940 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:55:34+01:00 | 95d90f8 | |
729e435 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T12:47:38+01:00 | 1961c85 | |
75e3b6f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:49:34+01:00 | 2f5d85a | |
7f010ab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:38:44+01:00 | 282f171 | |
282f171 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T14:52:36+01:00 | ||
88eeb26 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T13:43:42+01:00 | ||
95d90f8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2021-12-07T02:30:26+01:00 | ||
1647584 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-10T21:27:18+01:00 | e9b2060 | |
38b0b90 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 6 | 2021-12-08T13:49:44+01:00 | 2719b6d | |
2719b6d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T08:36:35Z | ||
2f5d85a | 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-06T02:44:08+01:00 | ||
1961c85 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 3 | 2021-12-06T11:40:00+01:00 | ||
f0e5580 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T18:46:03+01:00 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i, b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
76e7dff | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:42:02+01:00 | ||
90af137 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T14:40:47 | ||
3a72ac9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T15:03:25 | ||
e4a32e4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:42:19+01:00 | 90af137 | |
15fe4fb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T03:58:59+01:00 | 3a72ac9 | |
edcee6c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T07:32:36+01:00 | 28d9cbd | |
91cd143 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:26:29+01:00 | 56c93f4 | |
09e1759 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:01:48+01:00 | 76d88b0 | |
c5adce6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:54:42+01:00 | 56c93f4 | |
76d88b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T17:05:18+01:00 | ||
28d9cbd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T00:01:54+01:00 | ||
5c71ef5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 6 | 2020-12-07T16:43:39+01:00 | 2025d08 | |
5c739cf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T19:16:45+01:00 | 76e7dff | |
54bd7c5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T18:42:49+01:00 | 76d88b0 |
Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i, b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3670a5a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 04:48:00 | ||
baa3646 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:39:24+01:00 | e2594db | |
9986154 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:10:35+01:00 | f47287b | |
9dd95b3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T00:11:50+01:00 | ||
c5c24cb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 6 | 2019-12-11T20:54:19+01:00 | c318cad | |
f47287b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-29T14:50:00+01:00 | ||
dbb5994 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:41:53+01:00 | 9dd95b3 | |
0b06757 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:21+01:00 | 3670a5a | |
4abb338 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:20:12+01:00 | 61ebb63 | |
85fb616 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:48+01:00 | 4b72209 |
Found 15 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i, b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b32668f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:37 CET (sv-comp) | ||
6ff0ae1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:50+01:00 | ae5b12c | |
85962a7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T23:44:48+01:00 | b32668f | |
beeac0d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T08:24:17+01:00 | c551e1c | |
20c745a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:00:30+01:00 | fb00a18 | |
5c82bc6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T07:24:42+01:00 | ||
f6c584f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-06T10:09:40+01:00 | 6724cc8 | |
e880386 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:48:06+01:00 | 5c82bc6 | |
3c674f5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:19:31+01:00 | b8df7a6 | |
bed3fa4 | 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-08T06:45:51 | ||
c551e1c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T01:37:29+01:00 | ||
25a6b6b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:09:44+01:00 | bed3fa4 | |
f71cc6b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T03:45:29+01:00 | ae5b12c | |
158327b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-07T01:08:15+01:00 | 18e30eb | |
6450743 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-08T04:55:03+01:00 | 2d24f47 |
Found 5 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i, b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
abcf523 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:27 CET (sv-comp) | ||
50bb843 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:26:50+01:00 | ||
e9c9973 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T10:34:07.349692 | ||
16c7b8f | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:40:36.988615 | ||
02f8330 | 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.1_false-valid-deref.i, b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b1b021e6d9a2738a433255a5090e8bc6a16512946b766dfe0e7714e9e7b1f123.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |