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-1_false-valid-deref.i, be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6ee88e4 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:19:06+01:00 | ||
c182a81 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T19:59:31Z | ||
09e57db | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-19T05:27:58+01:00 | 99409f4 | |
115fdb3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-18T12:07:22+01:00 | 6ee88e4 | |
8d6ac96 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-18T03:09:21+01:00 | 3dc5378 | |
8226e8a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-05T14:38:20+01:00 | 74f05ec | |
8244e46 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T16:45:17+01:00 | 507b45b | |
86c4687 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T02:25:10+01:00 | 1265c51 | |
53b067a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-01T22:53:41+01:00 | 4f38243 | |
a39a1a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T13:42:53+01:00 | 987625a | |
602fe10 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T03:03:08+01:00 | c182a81 | |
987625a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T02:21:40+01:00 | ||
80bd752 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-28T23:49:52+01:00 | c3e452a | |
1265c51 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T23:44:25+01:00 | ||
3dc5378 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2023-12-18T01:55:46+01:00 | ||
725b12f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T22:09:59+01:00 | d7d861c | |
e876eb8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T18:26:51+01:00 | 3d34b96 | |
3d34b96 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T13:52:54Z | ||
d7d861c | 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 | 2023-12-17T21:04:08+01:00 | ||
c3e452a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T19:45:36Z | ||
99409f4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T23:27:27+01:00 | ||
74f05ec | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T08:41:56Z | ||
507b45b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T12:52:45Z | ||
4f38243 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:39:05Z | ||
cc24d2e | Inspect | - content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0cebfbd6-1d8f-4f06-bef9-da577278f11f/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1-2.i line: 37 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:59:31Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0cebfbd6-1d8f-4f06-bef9-da577278f11f/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1-2.i : be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0cebfbd6-1d8f-4f06-bef9-da577278f11f/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-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 | 6 | 2023-11-30T02:57:09+01:00 |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i, be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
f815199 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:29:13+01:00 | ||
d376e2f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T14:45:29Z | ||
40cb777 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T05:55:27+01:00 | d376e2f | |
10ee36e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T01:30:25+01:00 | 9722f84 | |
a261137 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T21:04:46+01:00 | f730844 | |
26f10bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T14:19:19+01:00 | f815199 | |
da0a152 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:56:02+01:00 | 693bc12 | |
304b833 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T06:01:10+01:00 | b7ff7ca | |
07bd1fc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:22:01+01:00 | 7d5dab8 | |
9e1d295 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T00:27:55+01:00 | ab61c79 | |
693bc12 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2022-12-10T16:28:22+01:00 | ||
9722f84 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T00:15:05+01:00 | ||
f730844 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T02:27:07+01:00 | ||
b7ff7ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2022-12-09T03:00:25+01:00 | ||
4749a0d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:44:29+01:00 | 7e19505 | |
5add271 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T04:24:07+01:00 | 49ad1a3 | |
7e19505 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T19:40:06Z | ||
7d5dab8 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T08:36:15Z | ||
49ad1a3 | 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 | 2022-12-08T09:46:08+01:00 | ||
ab61c79 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T15:15:35Z |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i, be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5668868 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:27:07+01:00 | ||
8bfd40f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T18:10:35 | ||
af90ae2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T09:10:59Z | ||
28ccbc5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-09T15:59:51+01:00 | 5cf9fec | |
8714d7d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-08T21:06:54+01:00 | 8668345 | |
c3f4c58 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-08T13:49:45+01:00 | 8f667ea | |
fd757b8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T19:12:41+01:00 | af90ae2 | |
cfd1d60 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T11:27:35+01:00 | 5668868 | |
8e258c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T04:55:30+01:00 | 3284d8a | |
f87c129 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-05T20:41:24+01:00 | 2527ca4 | |
2527ca4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-05T15:16:06+01:00 | ||
8668345 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 5 | 2021-12-08T20:22:43+01:00 | ||
5cf9fec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 5 | 2021-12-09T14:42:35+01:00 | ||
3284d8a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2021-12-07T02:41:12+01:00 | ||
94b9e5b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2021-12-06T11:46:19+01:00 | 36c8e0f | |
8f667ea | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T11:30:53Z | ||
36c8e0f | 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 | 2021-12-06T09:00:03+01:00 |
Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i, be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3eb56ea | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:43:43+01:00 | ||
ae52017 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T18:35:53 | ||
d4938b1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T15:06:40 | ||
7a3bd4c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-12T01:29:48+01:00 | ae52017 | |
0b2e561 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-08T07:46:34+01:00 | eba2b9b | |
34c6dc6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-06T19:00:13+01:00 | 3eb56ea | |
9b7fa23 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-06T18:01:46+01:00 | 47516db | |
50846d8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-05T18:40:13+01:00 | 47516db | |
47516db | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-05T14:21:55+01:00 | ||
eba2b9b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 5 | 2020-12-08T05:14:27+01:00 | ||
52b389e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 5 | 2020-12-06T07:40:41+01:00 | bcffcd4 | |
9358fe9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 5 | 2020-12-06T18:29:03+01:00 | bcffcd4 | |
6c46a3b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-09T04:05:57+01:00 | d4938b1 |
Found 9 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i, be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5ff253a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 12:10:41 | ||
6480405 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T21:09:30+01:00 | 5ff253a | |
eb5f40a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-03T08:09:08+01:00 | 9ff1768 | |
3e464b1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 5 | 2019-12-03T08:57:33+01:00 | 0c7edd5 | |
7f11d58 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-06T02:38:09+01:00 | 35db913 | |
ff1fdc0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 5 | 2019-12-01T00:33:07+01:00 | ||
8386590 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T21:44:45+01:00 | ff1fdc0 | |
9ff1768 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-11-29T16:17:49+01:00 | ||
1786af9 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 5 | 2019-12-05T20:21:30+01:00 | abc5ddd |
Found 16 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i, be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8ea5f18 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T03:20 CET (sv-comp) | ||
051369d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T23:44:32+01:00 | 8ea5f18 | |
8be7721 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:48:03+01:00 | 533a1a2 | |
cb4681b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:41:43+01:00 | 273a6f8 | |
865604f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:16:42+01:00 | e3f3409 | |
afccff8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:10:17+01:00 | a6450c0 | |
25d99db | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 6 | 2018-12-08T02:24:45+01:00 | ||
10feff1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T22:07:35+01:00 | b1985c2 | |
62c37fb | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T08:54:48+01:00 | 25d99db | |
533a1a2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 6 | 2018-12-05T13:06:54+01:00 | ||
b1985c2 | 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:15:10 | ||
787f47d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-10T10:48:41+01:00 | 779c325 | |
8db5b03 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:57:40+01:00 | e4b2f53 | |
c594ae0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-08T04:36:27+01:00 | 779c325 | |
a7834c9 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-07T01:05:43+01:00 | 562c05e | |
f717e27 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T10:20:12+01:00 | 087cbc3 |
Found 6 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i, be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9e73c48 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:01 CET (sv-comp) | ||
224b115 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:25:50.921982 | ||
67a7618 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:35:00.014635 | ||
c1d3b49 | 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 | 8 | 2017-12-01T08:25 CET (sv-comp) | ||
c95a828 | 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) | ||
13222a2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 6 | 2017-12-01T08:34:04+01:00 |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i, be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/be1b201ec4bb736098743afd4181fcfc22c193becbd6f966d9c5be2ac7d72b7a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |