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 37 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0165793 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T08:59:30+01:00 | ||
40d27f7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-12-17T00:54:04Z | ||
fc792ba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-30T00:08:20Z | ||
9cc845c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T15:32:35+01:00 | 556460f | |
df0523d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:25:50+01:00 | 1e4e7e1 | |
e2c77cf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:01:20+01:00 | 0165793 | |
98358a4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:09:24+01:00 | eac2a19 | |
5930c31 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:10:13+01:00 | d4c1e49 | |
e93d281 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T06:37:59+01:00 | 40d27f7 | |
bf70006 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:36:48+01:00 | 485aaaa | |
f8cf720 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:45:27+01:00 | 5ca3552 | |
ebcf0a0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:26:17+01:00 | c484d2e | |
6403ce5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:53:57+01:00 | 462c7a8 | |
f0ac41c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:44:40+01:00 | e5c24ea | |
6a9ae0f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T09:44:24+01:00 | 3a5ce97 | |
e5c24ea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T09:11:49+01:00 | ||
33a65d6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:03:42+01:00 | fc792ba | |
56bebdb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:49:32+01:00 | 1038373 | |
c484d2e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T21:22:32+01:00 | ||
1e4e7e1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-19T00:28:11+01:00 | ||
eac2a19 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T02:15:51+01:00 | ||
18c5038 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-04T12:12:10+01:00 | 4c02b4b | |
b575348 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-03T06:19:04+01:00 | 6273e06 | |
91eb3ae | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-01T18:27:11+01:00 | 3133eca | |
b7b219d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-29T08:33:16+01:00 | c19431e | |
3133eca | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T14:47:34Z | ||
556460f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2023-12-19T10:55:25+01:00 | ||
4c02b4b | 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:12:53Z | ||
6273e06 | 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-02T23:31:52Z | ||
d4c1e49 | 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-17T08:53:56+01:00 | ||
c19431e | 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-28T23:16:14Z | ||
1038373 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T21:35:33Z | ||
3a5ce97 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:24:58Z | ||
485aaaa | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T10:04:27Z | ||
5ca3552 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T09:44:58Z | ||
462c7a8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T21:05:59Z | ||
03ae9e2 | Inspect | - content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb352223-50cb-425b-a1e9-0b3302338f96/sv-benchmarks/c/ldv-memsafety/memset_-write.c line: 27 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-30T00:08:20Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb352223-50cb-425b-a1e9-0b3302338f96/sv-benchmarks/c/ldv-memsafety/memset_-write.c : ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb352223-50cb-425b-a1e9-0b3302338f96/sv-benchmarks/c/ldv-memsafety/memset_-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-30T03:00:23+01:00 |
Found 29 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
e8d59a1 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:15:04+01:00 | ||
57cc314 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-25T10:03:30Z | ||
8df8251 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T11:53:03Z | ||
f455bd7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:58:13+01:00 | 8df8251 | |
4683749 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T04:19:23+01:00 | afea95f | |
992c265 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:31:07+01:00 | a01adb8 | |
8d390dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T00:53:41+01:00 | 9042a06 | |
d26590a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:07:44+01:00 | bbb4a94 | |
cbd769a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:12:00+01:00 | e8d59a1 | |
088e7f7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:54:58+01:00 | e54273e | |
24a8cf0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:01:23+01:00 | 84d511f | |
4b3422b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:21:50+01:00 | 1dedbfd | |
f50791b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T02:23:37+01:00 | 57cc314 | |
db4155a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:28:24+01:00 | 7c78617 | |
e54273e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T21:43:34+01:00 | ||
a01adb8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T22:08:32+01:00 | ||
9042a06 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2022-12-11T04:17:37+01:00 | ||
84d511f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T02:39:41+01:00 | ||
d64fb14 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T10:45:27+01:00 | c128622 | |
478881b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:53:12+01:00 | 4997e74 | |
52c07d3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:39:08+01:00 | 97b33bb | |
e07c982 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T15:45:00+01:00 | 630b291 | |
630b291 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T22:16:03Z | ||
c128622 | 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-14T11:32:51Z | ||
97b33bb | 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-15T02:51:12Z | ||
1dedbfd | 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-08T11:05:23+01:00 | ||
4997e74 | 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:44:50Z | ||
bbb4a94 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T04:06:37+01:00 | ||
7c78617 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T16:58:18Z |
Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9eae3b3 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T07:54:01+01:00 | ||
b536537 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:31:30 | ||
5fa6270 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T14:50:15Z | ||
cb7b91d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-10T21:29:22+01:00 | b536537 | |
ab61a9d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T16:02:26+01:00 | 2d76bb8 | |
f36813c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T06:21:29+01:00 | afea95f | |
0113b3c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:08:15+01:00 | 03e8e3a | |
d47151c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:10:16+01:00 | 5fa6270 | |
32090b7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:27:59+01:00 | 9eae3b3 | |
c2fe693 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:56:05+01:00 | 615b718 | |
9f100fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:49:36+01:00 | 7dfa5ce | |
f3a6ae0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:38:37+01:00 | bee1457 | |
bee1457 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T15:02:35+01:00 | ||
615b718 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T03:56:36+01:00 | ||
84df84b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T17:27:12+01:00 | 2111fe7 | |
3cea1ac | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T08:34:05+01:00 | a7f2562 | |
e6fde00 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-08T13:49:08+01:00 | ddfc50a | |
0bdeca8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-07T02:35:10+01:00 | f92a6b4 | |
ddfc50a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T04:22:48Z | ||
a7f2562 | 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:14:48Z | ||
2111fe7 | 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-10T07:09:09Z | ||
7dfa5ce | 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-05T14:26:29+01:00 | ||
f92a6b4 | 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-06T17:22:48Z | ||
03e8e3a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T19:53:34+01:00 | ||
2d76bb8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T13:52:41+01:00 |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0a5f011 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:45:17+01:00 | ||
6db179f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T19:03:30 | ||
aa7855a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-09T02:09:08 | ||
c631dc1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T04:12:27+01:00 | aa7855a | |
47ccb99 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T02:29:21+01:00 | d5c66a6 | |
f0a592f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:02:07+01:00 | 3e95adf | |
6b2da2a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:49:42+01:00 | b0a3926 | |
0388ac5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T18:04:18+01:00 | 3e95adf | |
3e95adf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T15:41:36+01:00 | ||
1951ab3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:52:49+01:00 | fe2c331 | |
fb97f24 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:25:50+01:00 | b0a3926 | |
ea83a00 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T05:35:07+01:00 | ||
0580224 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-07T16:38:57+01:00 | 5c15e3e | |
dea6fcf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:45:11+01:00 | 6db179f | |
b92ae26 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T22:12:39+01:00 | 28b1541 | |
536fa66 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T07:55:04+01:00 | ea83a00 | |
d36ef7b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T19:10:34+01:00 | 0a5f011 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ac90aa6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 03:20:20 | ||
f2a5dfe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T22:00:45+01:00 | b85b6a6 | |
a3e17b1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:43:43+01:00 | ba33c3e | |
8f9e321 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:42+01:00 | ac90aa6 | |
968dce1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:27:09+01:00 | b40073e | |
70d7078 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:38:42+01:00 | f7b2a25 | |
273a605 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:20:47+01:00 | f880d86 | |
58bb5e0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:52+01:00 | acd47f7 | |
45b92b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-11T20:54:26+01:00 | 6b462e5 | |
0c6f5c5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-07T21:16:06+01:00 | 3653244 | |
6637c16 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-30T00:18:46+01:00 | ||
b85b6a6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T10:49:17+01:00 | ||
17944f2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:06:01+01:00 | afea95f | |
a1c99b4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:09:32+01:00 | 6637c16 |
Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b0e3cf6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T10:05 CET (sv-comp) | ||
93438cb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T01:40:02+01:00 | ||
c67087d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:55+01:00 | 40154ac | |
7682c7f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:39:18+01:00 | 9eb8c59 | |
fc83a47 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T23:41:56+01:00 | b0e3cf6 | |
309aa65 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:07:24+01:00 | b18931b | |
f917db8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T08:00:30+01:00 | 93438cb | |
f52b0b9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T04:17:06+01:00 | 40154ac | |
58f79d4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:48:44+01:00 | d92985d | |
b59efbb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:09:43+01:00 | 4f97927 | |
d92985d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T05:15:27+01:00 | ||
4bbe5c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T10:18:14+01:00 | fa40e22 | |
c449ecd | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-07T09:30:15+01:00 | 1dd8a11 | |
b18931b | 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-08T02:00:33 | ||
6a176bd | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:53:17+01:00 | afb68eb | |
6c6a8a3 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:26:42+01:00 | 5f0b1e2 | |
54a1675 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:19:30+01:00 | f3f5b09 | |
ceab00f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T05:03:08+01:00 | d15d4ea |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
90c067c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-03T00:25 CET (sv-comp) | ||
6a7f6dd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:23:23+01:00 | ||
6dfb4c4 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T10:52:24.859348 | ||
1797bab | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:47:32.945975 | ||
0d6cfcd | 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 | ||
bd38d0f | 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-03T04:18Z | ||
db555a2 | 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:28 CET (sv-comp) | ||
42c735f | 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:24 CET (sv-comp) | ||
b90cfd9 | 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-03T03:50Z | ||
1dd8a11 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:02 CET (sv-comp) | ||
35459bd | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:42 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memset_false-valid-deref-write.c, ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ba21f683e7359b2183f84247787bae0200d2737e415ddf8263ed1dffc45ae166.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |