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/memset2_false-valid-deref-write.c |
programSHA | d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a |
witnessName | results-verified/cpa-seq.2018-12-05_0546.logfiles/sv-comp19_prop-memsafety.memset2_false-valid-deref-write.c.files/witness.graphml |
witnessSHA | 89c78e84ce8a7e58086d36f6ebc5ac405098b6945b997ed3c6bd4a9f6f1cc996 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T22:30:32+01:00 |
producer | CPAchecker 1.7-svn 29852 |
program-sha256 | d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a |
programfile | ../../sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c |
programhash | d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-deref) ) |
witness-file | witnessFileByHash/89c78e84ce8a7e58086d36f6ebc5ac405098b6945b997ed3c6bd4a9f6f1cc996.graphml |
witness-sha256 | 89c78e84ce8a7e58086d36f6ebc5ac405098b6945b997ed3c6bd4a9f6f1cc996 |
witness-size | 2947 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a).
Found 35 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2adad80 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:05:22+01:00 | ||
32a0543 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T23:51:36Z | ||
518d8bc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T15:33:45+01:00 | 3b1c05c | |
f0d618d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:28:09+01:00 | 2a3ced6 | |
926bb1c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:07:24+01:00 | 2adad80 | |
0a981e7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:09:33+01:00 | 9791efd | |
12aba3f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:10:15+01:00 | fc6ba23 | |
8ed26a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:39:22+01:00 | 6cec610 | |
cf004af | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:44:08+01:00 | 10da975 | |
ef552a6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:25:21+01:00 | 4eb3a2b | |
c8c0c9d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:53:41+01:00 | 91db460 | |
8153aa8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:43:16+01:00 | f0da481 | |
455f3e8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T09:44:07+01:00 | 9b29e71 | |
f0da481 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T06:22:29+01:00 | ||
97984df | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:04:54+01:00 | 32a0543 | |
94c9d9d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:50:05+01:00 | 18005a7 | |
4eb3a2b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-04T00:20:13+01:00 | ||
3b1c05c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2023-12-19T11:59:51+01:00 | ||
9791efd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T01:56:42+01:00 | ||
bbea0b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-04T12:13:23+01:00 | dd99a6d | |
da8f661 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-03T06:19:21+01:00 | e88b063 | |
9115c02 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-01T18:29:02+01:00 | 12977b1 | |
bb0e6f9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-29T08:33:44+01:00 | 551ee3d | |
12977b1 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T13:15:30Z | ||
dd99a6d | 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-02T19:09:33Z | ||
e88b063 | 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:57:11Z | ||
fc6ba23 | 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-17T09:42:45+01:00 | ||
551ee3d | 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-29T04:15:23Z | ||
18005a7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T20:03:54Z | ||
9b29e71 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:25:56Z | ||
2a3ced6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T17:06:20+01:00 | ||
6cec610 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T11:42:41Z | ||
10da975 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T14:51:17Z | ||
91db460 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T21:10:57Z | ||
6fb3945 | Inspect | - content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4bd30fa3-bf96-429c-ade8-97ab67d53617/sv-benchmarks/c/ldv-memsafety/memset2_-write.c line: 22 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:51:36Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4bd30fa3-bf96-429c-ade8-97ab67d53617/sv-benchmarks/c/ldv-memsafety/memset2_-write.c : d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_4bd30fa3-bf96-429c-ade8-97ab67d53617/sv-benchmarks/c/ldv-memsafety/memset2_-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:57:31+01:00 |
Found 29 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
db289b6 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:23:55+01:00 | ||
95390c7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T14:15:20Z | ||
ebd4a4e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:58:20+01:00 | 95390c7 | |
edfbe7b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T04:19:12+01:00 | cc883df | |
984f3e6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:30:55+01:00 | 2de03ab | |
8cc1f6c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T00:54:52+01:00 | 487a05a | |
45f64df | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:08:39+01:00 | 7af74c3 | |
d7f6e28 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:17:24+01:00 | db289b6 | |
a52e615 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:55:23+01:00 | 7a9ed6c | |
7d8d126 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:00:58+01:00 | c9aa084 | |
1e9dd6f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:23:36+01:00 | ead463b | |
691ba6e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:29:48+01:00 | c812453 | |
7a9ed6c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T19:50:40+01:00 | ||
2de03ab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-12T02:21:26+01:00 | ||
487a05a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2022-12-11T03:36:17+01:00 | ||
7af74c3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T03:12:52+01:00 | ||
c9aa084 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T03:04:36+01:00 | ||
9b6faed | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T10:43:27+01:00 | 1f02553 | |
0d06511 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:54:50+01:00 | 984a502 | |
15e86a7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:38:33+01:00 | d30cd71 | |
89eaf45 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T15:45:34+01:00 | ce2d7dd | |
24d1248 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T02:23:37+01:00 | c7bb2d8 | |
ce2d7dd | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T16:10:54Z | ||
c7bb2d8 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T08:21:26Z | ||
1f02553 | 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:57:49Z | ||
d30cd71 | 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-14T22:45:39Z | ||
ead463b | 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-08T07:47:12+01:00 | ||
984a502 | 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-13T18:17:40Z | ||
c812453 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T14:25:55Z |
Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ffc22cf | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:13:40+01:00 | ||
fcf084c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:48:09 | ||
76a34c8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T15:45:53Z | ||
2ca76d2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-10T21:28:40+01:00 | fcf084c | |
2dfda2c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T16:02:25+01:00 | 76fd1c9 | |
b55257d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T06:21:15+01:00 | cc883df | |
c7a8028 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:09:28+01:00 | a5cca86 | |
f379be4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:12:51+01:00 | 76a34c8 | |
b01a28c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:25:54+01:00 | ffc22cf | |
7a502f8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:56:02+01:00 | b728354 | |
553bba2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:48:37+01:00 | 52d9b18 | |
4ea3e4a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:39:59+01:00 | 204bec0 | |
204bec0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T18:06:13+01:00 | ||
76fd1c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T12:06:02+01:00 | ||
b728354 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T02:30:25+01:00 | ||
250c94d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T17:26:52+01:00 | 0ac3a12 | |
1e556a9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T08:34:32+01:00 | 1197af1 | |
ecf26fc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-08T13:49:45+01:00 | 0b34164 | |
556b835 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-07T02:35:19+01:00 | fe2aa22 | |
0b34164 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T07:48:38Z | ||
a5cca86 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T18:22:26+01:00 | ||
1197af1 | 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-10T04:25:07Z | ||
0ac3a12 | 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:48:03Z | ||
52d9b18 | 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 | 2021-12-06T07:17:34+01:00 | ||
fe2aa22 | 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:29:51Z |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
c842339 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:15:44+01:00 | ||
b1f7065 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T23:00:53 | ||
57c0bab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T13:59:58 | ||
e03e784 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:29:49+01:00 | b1f7065 | |
8898dc3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:53:42+01:00 | cb7efb4 | |
14e817e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:31:52+01:00 | b9f34db | |
7c48fa4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T02:25:21+01:00 | 28b84bc | |
b69a1a3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T07:47:31+01:00 | 1729b64 | |
7b97bd5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:26:39+01:00 | 6ce96e2 | |
1784e09 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T12:55:42+01:00 | ||
1729b64 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-07T23:51:33+01:00 | ||
d1bf9b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-07T16:31:09+01:00 | b9fb5a9 | |
7bce899 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T04:03:27+01:00 | 57c0bab | |
651a4a7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T19:41:05+01:00 | c842339 | |
211893c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T18:41:12+01:00 | 1784e09 | |
6f0d8a8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:02:15+01:00 | 1784e09 | |
7bc8e82 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:50:44+01:00 | 6ce96e2 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
07bb3d2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 15:36:05 | ||
f682d5b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:41:47+01:00 | f9e9ca4 | |
66a38f7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:20+01:00 | 07bb3d2 | |
880b787 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:26:44+01:00 | b7b57f2 | |
07fa934 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:07:38+01:00 | cc883df | |
201aea1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:40:21+01:00 | c1a3f5a | |
7da9acf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:20:13+01:00 | 9eba3d4 | |
13767c5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-29T23:50:29+01:00 | ||
3cd4bb5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-11T20:54:52+01:00 | 4a9e10f | |
095f426 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-07T21:16:52+01:00 | 80f9c1b | |
b494405 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:38+01:00 | ddf80e2 | |
220cf4e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:10:13+01:00 | 13767c5 | |
7a1c435 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:46:22+01:00 | f1355c5 | |
f9e9ca4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T00:25:40+01:00 |
Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6033ad6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T13:16 CET (sv-comp) | ||
47400f3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T02:49:26+01:00 | ||
b10bbf9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:53:26+01:00 | 0a34946 | |
bae3769 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:33:41+01:00 | 1e7c926 | |
b87550e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:10:02+01:00 | d627739 | |
9dba359 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T08:53:35+01:00 | 47400f3 | |
f6f770d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:48:12+01:00 | 89c78e8 | |
1dd3a9c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:17:20+01:00 | dafc93b | |
a583b46 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T10:19:22+01:00 | 4cc052d | |
6a281a2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T23:44:04+01:00 | 6033ad6 | |
a59116a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-07T09:16:57+01:00 | 63447bc | |
8026d5e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T05:05:13+01:00 | d15dfdb | |
d627739 | 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:02:57 | ||
5c6bcd7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:52+01:00 | cf1f8fd | |
af4ab0c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:18:11+01:00 | 4e1e927 | |
9006d91 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T03:33:10+01:00 | cf1f8fd | |
996b8a6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:13:36+01:00 | e6dbc0e | |
89c78e8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-05T22:30:32+01:00 |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e3c6765 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:30 CET (sv-comp) | ||
506ebc9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:34:13+01:00 | ||
506f5b3 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T12:00:16.837611 | ||
dad43fd | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:41:20.690035 | ||
9a70254 | 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 | 3 | 2017-12-03T06:53Z | ||
08d0097 | 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:57Z | ||
1f8fe1d | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Forester | 4 | 2017-12-01T19:33 CET (sv-comp) | ||
3f338c5 | 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:28 CET (sv-comp) | ||
17836dd | 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 | 3 | 2017-12-03T04:25Z | ||
63447bc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T21:54 CET (sv-comp) | ||
5164507 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:16 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memset2_false-valid-deref-write.c, d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d4fc71baff335ff14a7aa80c850361218ce54d94877a63cc32d89565d13dae1a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |