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.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
22a2322 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:43:22+01:00 | ||
c04c8ab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T21:48:52Z | ||
86ef50a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-18T12:03:59+01:00 | 22a2322 | |
d23f479 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-05T14:41:09+01:00 | e7de7c4 | |
62f83bc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T16:39:24+01:00 | bf4e2d2 | |
fd607c7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-01T22:56:15+01:00 | 49b472c | |
5d009be | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-01T18:28:33+01:00 | 8049b7d | |
1f01ac4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-30T08:00:15+01:00 | ||
26098d3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T03:03:48+01:00 | c04c8ab | |
19e7a6b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-28T23:49:39+01:00 | bde8864 | |
df6d688 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-03T22:01:53+01:00 | ||
c761497 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2023-12-18T01:44:20+01:00 | ||
b1172d5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T05:27:28+01:00 | 920ea36 | |
0be3503 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-18T03:09:42+01:00 | c761497 | |
78f0615 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T22:07:29+01:00 | 9286813 | |
e379a8f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T02:25:46+01:00 | df6d688 | |
7db9798 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T13:43:27+01:00 | 1f01ac4 | |
8049b7d | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T16:02:50Z | ||
bde8864 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T21:04:26Z | ||
e7de7c4 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | Bubaak | 3 | 2023-12-05T11:00:40Z | ||
bf4e2d2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | Bubaak | 3 | 2023-12-04T08:35:45Z | ||
49b472c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:40:26Z | ||
9286813 | 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 | 2023-12-17T10:27:02+01:00 | ||
920ea36 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-18T19:07:58+01:00 | ||
54452b1 | Inspect | - content: - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b0cb3a5a-14a7-4e71-bfe0-0c2c4bf1ae22/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1-2.i line: 46 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T21:48:52Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b0cb3a5a-14a7-4e71-bfe0-0c2c4bf1ae22/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1-2.i : 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b0cb3a5a-14a7-4e71-bfe0-0c2c4bf1ae22/sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.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-30T03:00:38+01:00 |
Found 20 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
73408ad | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:33:55+01:00 | ||
08f3cc3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T17:15:59Z | ||
3cb0478 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T05:56:29+01:00 | 08f3cc3 | |
f850772 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:45:13+01:00 | b215435 | |
59531fe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T14:16:48+01:00 | 73408ad | |
cc57a23 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:22:32+01:00 | 4e5552c | |
3f093b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T00:29:12+01:00 | 088941e | |
33291c5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 6 | 2022-12-10T16:47:51+01:00 | ||
416bfa6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T23:23:58+01:00 | ||
16dce0c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2022-12-09T03:12:10+01:00 | ||
d3e4fe2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T01:31:06+01:00 | 416bfa6 | |
010d609 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T21:06:37+01:00 | c062d92 | |
01946f7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:58:37+01:00 | 33291c5 | |
f7a87c5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T06:01:32+01:00 | 16dce0c | |
0b22948 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T04:21:48+01:00 | 8c822b6 | |
b215435 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T20:22:18Z | ||
4e5552c | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T09:43:10Z | ||
088941e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | Bubaak | 3 | 2022-12-08T20:04:06Z | ||
8c822b6 | 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 | 2022-12-08T12:01:46+01:00 | ||
c062d92 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T03:25:32+01:00 |
Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
93c6a7b | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:40:23+01:00 | ||
a287226 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:24:24 | ||
4c122fb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T10:12:39Z | ||
609b7dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-10T21:24:56+01:00 | b1d9137 | |
70c9234 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-08T13:48:54+01:00 | fb5a7db | |
4bf5a3b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T19:12:47+01:00 | 4c122fb | |
1296bc1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T11:27:19+01:00 | 93c6a7b | |
797825d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 6 | 2021-12-05T17:33:23+01:00 | ||
b02e0d8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 6 | 2021-12-08T19:20:47+01:00 | ||
0bac56e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 9 | 2021-12-07T02:20:11+01:00 | ||
5818ca8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2021-12-09T16:00:40+01:00 | 75fb4b3 | |
e1ba6fb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2021-12-08T21:09:34+01:00 | b02e0d8 | |
d185475 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2021-12-07T04:55:30+01:00 | 0bac56e | |
f368cda | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2021-12-06T11:48:23+01:00 | 9687e7a | |
8848018 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 5 | 2021-12-05T20:41:27+01:00 | 797825d | |
fb5a7db | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T11:17:23Z | ||
75fb4b3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2021-12-09T11:22:09+01:00 | ||
9687e7a | 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 | 9 | 2021-12-06T10:30:26+01:00 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c3fcb6e | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:50:23+01:00 | ||
b9fd0de | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T18:54:21 | ||
e9d3b1c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-09T00:25:09 | ||
2f84bcb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-06T19:29:11+01:00 | c3fcb6e | |
551b0f5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 6 | 2020-12-08T01:42:37+01:00 | ||
3e0081b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 5 | 2020-12-06T18:25:25+01:00 | 1d3f396 | |
293cc6f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 5 | 2020-12-06T18:01:43+01:00 | b2f8211 | |
af409a5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 5 | 2020-12-06T07:56:20+01:00 | 1d3f396 | |
c0f64eb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 5 | 2020-12-05T18:00:34+01:00 | b2f8211 | |
eb873de | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-07T16:23:13+01:00 | 2f4fd2e | |
f1ebb34 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 5 | 2020-12-08T07:50:11+01:00 | 551b0f5 | |
f6b87d6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-12T01:41:13+01:00 | b9fd0de | |
2566377 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-09T04:13:35+01:00 | e9d3b1c | |
b2f8211 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 6 | 2020-12-05T14:07:49+01:00 |
Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7e26069 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 23:02:27 | ||
07f2468 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 5 | 2019-12-11T21:26:09+01:00 | 21ed9b9 | |
7e2c8e8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 5 | 2019-12-05T20:21:15+01:00 | 540a6c4 | |
42c224d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 5 | 2019-12-03T08:56:49+01:00 | de790e1 | |
f35936c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T21:09:42+01:00 | 7e26069 | |
b7fa4cd | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T20:54:22+01:00 | e8cc4d4 | |
21ed9b9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6 | 2019-12-01T01:55:52+01:00 | ||
892b094 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 5 | 2019-12-03T08:00:37+01:00 | 3612857 | |
e20fc3e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-06T02:41:23+01:00 | 1848036 | |
3612857 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 6 | 2019-11-29T15:05:36+01:00 |
Found 13 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
51201d6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:05 CET (sv-comp) | ||
3ddb909 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T23:43:52+01:00 | 51201d6 | |
7fe57e1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T05:05:04+01:00 | 43532ea | |
e56f1d0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:48:15+01:00 | 06b55ca | |
06b55ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-05T09:49:55+01:00 | ||
7af0aee | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 7 | 2018-12-07T15:46:19+01:00 | ||
3dd0bf6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T22:10:56+01:00 | 7092b8d | |
37dddb8 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-08T08:00:15+01:00 | 7af0aee | |
54d8899 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T10:11:46+01:00 | 0a7d14f | |
7092b8d | 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-08T17:04:11 | ||
227d965 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-07T01:11:56+01:00 | e8df6aa | |
e7ac206 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:20:23+01:00 | 7978bf1 | |
9388533 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 5 | 2018-12-06T09:10:08+01:00 | 99d455c |
Found 6 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bff66d5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:10 CET (sv-comp) | ||
c365a8e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 7 | 2017-12-01T08:30:07+01:00 | ||
1518174 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:47:05.236802 | ||
0ce3eb8 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:15:35.771454 | ||
949ac9f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:56 CET (sv-comp) | ||
5aed543 | 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 | 10 | 2017-12-01T08:28 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i, 635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/635b18d6f80f7fb9900da8d675380fff657b914eae0cc24d65a61c9c5ee07c25.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |