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).
Key | Value |
programName | sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c |
programSHA | f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7 |
witnessName | results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.memsetNonZero3_false-valid-deref-write.c.files/witness.graphml |
witnessSHA | e240167c87ff91ac0ded57c784479e841b1424c3cb996e0ac6d89075faed065a |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-03T00:25 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_5b231b70-2cda-4c1b-a304-c5da8dfc986f/sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c |
programhash | 2400e27d5b2639ed1593fd2baea66159e12a4386 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/e240167c87ff91ac0ded57c784479e841b1424c3cb996e0ac6d89075faed065a.graphml |
witness-sha256 | e240167c87ff91ac0ded57c784479e841b1424c3cb996e0ac6d89075faed065a |
witness-size | 937 |
witness-type | violation_witness |
Found 37 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c, f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2b09132 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:41:49+01:00 | ||
375ec18 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-12-17T04:34:24Z | ||
aef3724 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T18:53:52Z | ||
0e97b55 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T15:34:17+01:00 | d40652f | |
9c31ac5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:26:53+01:00 | b7ec33a | |
69448ae | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:01:41+01:00 | 2b09132 | |
a54d9ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:09:40+01:00 | 8dd3217 | |
25c9846 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:06:54+01:00 | 5475db1 | |
0f8b7d4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T06:39:15+01:00 | 375ec18 | |
2ad582e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:40:24+01:00 | c498fc2 | |
1b07e6a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:39:23+01:00 | c562717 | |
737235d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:27:21+01:00 | a0166eb | |
7410644 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:56:27+01:00 | de7cef9 | |
040ea29 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:43:05+01:00 | 5f89981 | |
81d606b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T09:44:13+01:00 | d10b9d5 | |
000fe8c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:05:30+01:00 | aef3724 | |
5f89981 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T02:09:53+01:00 | ||
1f39e26 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:50:01+01:00 | 546bc2b | |
a0166eb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T23:34:06+01:00 | ||
8dd3217 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2023-12-18T01:36:11+01:00 | ||
e88e438 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-04T12:12:12+01:00 | 32c437d | |
0b54f46 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-03T06:19:15+01:00 | a9dd65d | |
986ece0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-01T18:29:54+01:00 | a839416 | |
21985b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-29T08:33:38+01:00 | defe1be | |
a839416 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T15:05:01Z | ||
d40652f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2023-12-19T11:43:25+01:00 | ||
32c437d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 4 | 2023-12-02T17:28:46Z | ||
a9dd65d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 4 | 2023-12-03T00:23:13Z | ||
5475db1 | 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-17T05:53:59+01:00 | ||
defe1be | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 4 | 2023-11-29T02:07:14Z | ||
546bc2b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T22:18:21Z | ||
d10b9d5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:23:47Z | ||
b7ec33a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T20:15:33+01:00 | ||
c498fc2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T12:54:41Z | ||
c562717 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T08:51:28Z | ||
de7cef9 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T20:30:10Z | ||
db85ef5 | Inspect | - content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_82768315-0a4e-4798-95c3-ae37d9c7b66e/sv-benchmarks/c/ldv-memsafety/memsetNonZero3_-write.c line: 29 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T18:53: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_82768315-0a4e-4798-95c3-ae37d9c7b66e/sv-benchmarks/c/ldv-memsafety/memsetNonZero3_-write.c : f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_82768315-0a4e-4798-95c3-ae37d9c7b66e/sv-benchmarks/c/ldv-memsafety/memsetNonZero3_-write.c 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:59:45+01:00 |
Found 29 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c, f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7a427d3 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:56:02+01:00 | ||
e7a3243 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-25T11:59:24Z | ||
de49dfd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T11:42:19Z | ||
174e7fa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:58:18+01:00 | de49dfd | |
2ea73cd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T04:19:13+01:00 | c054602 | |
a6f6e2e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:30:42+01:00 | f908cf0 | |
88a6eb8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T00:54:14+01:00 | ab50d61 | |
3237782 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:08:40+01:00 | 8790126 | |
4015550 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:19:19+01:00 | 7a427d3 | |
018a2dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:55:45+01:00 | 2f358e4 | |
7f9755e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:01:06+01:00 | 65aaa38 | |
2165e3e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:21:41+01:00 | bcc8e02 | |
9026789 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T02:23:37+01:00 | e7a3243 | |
4f5cf11 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:28:17+01:00 | fe7aa15 | |
2f358e4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T16:12:40+01:00 | ||
f908cf0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T20:23:55+01:00 | ||
ab50d61 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2022-12-11T06:01:59+01:00 | ||
8790126 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T00:10:20+01:00 | ||
65aaa38 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2022-12-09T03:06:20+01:00 | ||
901f4dd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T10:43:55+01:00 | fa575b9 | |
fe6f59c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:53:08+01:00 | e8ff809 | |
00299c1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:38:39+01:00 | f99523b | |
183f8a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T15:45:36+01:00 | 74b1527 | |
74b1527 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-19T00:58:38Z | ||
fa575b9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 4 | 2022-12-14T12:42:41Z | ||
f99523b | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 4 | 2022-12-14T20:33:08Z | ||
bcc8e02 | 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-08T12:34:03+01:00 | ||
e8ff809 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 4 | 2022-12-13T11:50:19Z | ||
fe7aa15 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T14:42:28Z |
Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c, f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
338012a | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:27:53+01:00 | ||
de3e03c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:02:22 | ||
e7416e8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T15:19:14Z | ||
3a1adca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-10T21:27:22+01:00 | de3e03c | |
1057ca0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T16:00:36+01:00 | 21ea646 | |
fae2957 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T06:22:08+01:00 | c054602 | |
ae480f4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:11:10+01:00 | 55957e1 | |
31da26c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:10:53+01:00 | e7416e8 | |
7dce3e6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:28:03+01:00 | 338012a | |
6eeb783 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:56:28+01:00 | 6549ffa | |
f1e6aa8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:47:32+01:00 | e61656a | |
39c7d64 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:38:29+01:00 | 7831419 | |
7831419 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T17:07:29+01:00 | ||
21ea646 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T14:35:35+01:00 | ||
6549ffa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2021-12-07T02:11:58+01:00 | ||
5dcc32e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T17:27:45+01:00 | c96ad26 | |
07571a0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T08:34:07+01:00 | 49e95aa | |
a308e02 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-08T13:50:21+01:00 | 8061e9b | |
c0a34b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-07T02:35:09+01:00 | 4033092 | |
8061e9b | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T10:32:20Z | ||
49e95aa | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 4 | 2021-12-10T02:58:19Z | ||
c96ad26 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 4 | 2021-12-10T13:18:28Z | ||
e61656a | 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-06T04:13:50+01:00 | ||
4033092 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 4 | 2021-12-06T16:35:36Z | ||
55957e1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T19:37:48+01:00 |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c, f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
66a9411 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:46:22+01:00 | ||
22be08c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T22:19:01 | ||
9b2f9aa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-09T01:12:02 | ||
6551674 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:30:23+01:00 | 22be08c | |
f744a8e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T06:46:11+01:00 | fcecbf9 | |
6411dd1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:01:19+01:00 | 7f4c537 | |
66326fa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T18:36:59+01:00 | 7f4c537 | |
7f4c537 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T15:23:32+01:00 | ||
93836b6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T04:11:29+01:00 | 9b2f9aa | |
7809b7a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T02:37:56+01:00 | fb61bc0 | |
cf080bc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:26:42+01:00 | d028d76 | |
07726a5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-07T16:12:35+01:00 | 90f42f9 | |
78aef1d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:56:09+01:00 | 871826c | |
b847167 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:15:17+01:00 | cbf8d32 | |
b805905 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T19:05:38+01:00 | 66a9411 | |
672c1c3 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:41:58+01:00 | d028d76 | |
fcecbf9 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T00:05:02+01:00 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c, f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9772ba7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 06:14:22 | ||
cde9c1a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:27+01:00 | 9772ba7 | |
3b5026c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:26:19+01:00 | b014204 | |
7d60072 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:40:29+01:00 | 1956ecf | |
4b818fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:20:23+01:00 | 4ba71d0 | |
6d2e55d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:09:50+01:00 | a5bfabc | |
5988bb9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T11:49:44+01:00 | ||
d5026c7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-11T20:54:52+01:00 | faaf945 | |
ba8d240 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:40:21+01:00 | 0f2d847 | |
d20d76f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:06:01+01:00 | c054602 | |
72fbe77 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-07T21:17:59+01:00 | 4c132ac | |
bd5f812 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:39:48+01:00 | 5988bb9 | |
6f3a00d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:28+01:00 | 7c37a5b | |
a5bfabc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-29T23:33:17+01:00 |
Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c, f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0192518 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T19:17 CET (sv-comp) | ||
8b59fc6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T17:57:15+01:00 | ||
894e9eb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:43+01:00 | 001761f | |
9151aed | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:53:08+01:00 | a5f95aa | |
dd74d0f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T23:44:00+01:00 | 0192518 | |
8e2eaed | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:10:05+01:00 | 517c06e | |
c5c0528 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:01:14+01:00 | a8b2a4f | |
2fe8b1a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-05T09:33:22+01:00 | ||
25ef98b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:34:10+01:00 | 6b52329 | |
486e61d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T08:33:35+01:00 | 8b59fc6 | |
dc10f54 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-07T09:26:48+01:00 | 34592e2 | |
c8781ae | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:07:22+01:00 | 519bffe | |
517c06e | 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-08T12:18:05 | ||
93d7fef | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:38:03+01:00 | 24c20d4 | |
8a24673 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T04:25:09+01:00 | 001761f | |
f23b301 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:49:09+01:00 | 2fe8b1a | |
86103e7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T05:06:29+01:00 | f1188dc | |
6e864d9 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T10:18:29+01:00 | ad826b5 |
Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c, f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e240167 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:25 CET (sv-comp) | ||
7de639d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:30:35+01:00 | ||
15c8694 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T10:34:06.584146 | ||
f83cf46 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:52:25.095591 | ||
d607cf7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Taipan | 4 | 2017-12-03T06:53Z | ||
c558e6d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Kojak | 4 | 2017-12-03T03:58Z | ||
bec4fe4 | 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:19 CET (sv-comp) | ||
17a1954 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Automizer | 4 | 2017-12-03T04:27Z | ||
34592e2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:01 CET (sv-comp) | ||
298359f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:16 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero3_false-valid-deref-write.c, f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f8ef618a7358dc412b70902583de953a04e571e0ed67df570396dd01a1cd7ca7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |