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/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
a657cd3 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:58:50+01:00 | ||
57d2eed | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-12-17T01:59:44Z | ||
73b1225 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T19:28:53Z | ||
94122bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T15:32:25+01:00 | f2d89c2 | |
87f6149 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:26:36+01:00 | 40e76a0 | |
c53644f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:04:45+01:00 | a657cd3 | |
a6cdfac | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:09:22+01:00 | 9ac92d9 | |
c320eb7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:09:07+01:00 | bd3593b | |
737e989 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T06:41:21+01:00 | 57d2eed | |
2e48b30 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:40:49+01:00 | 9898ae2 | |
145cdf4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:42:37+01:00 | 433911a | |
0c3adfd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:25:52+01:00 | 2896c39 | |
0512a5a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:56:19+01:00 | bfdf60e | |
6630a7a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:43:50+01:00 | f8e1da8 | |
4e2c503 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T09:44:00+01:00 | 9c2d420 | |
f8e1da8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T06:04:17+01:00 | ||
d1678f0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:03:37+01:00 | 73b1225 | |
969d589 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:50:04+01:00 | bbef4fc | |
2896c39 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-04T00:16:58+01:00 | ||
f2d89c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2023-12-19T13:08:50+01:00 | ||
40e76a0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T19:49:28+01:00 | ||
9ac92d9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2023-12-18T01:49:00+01:00 | ||
12f17f3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-04T12:12:26+01:00 | 8b37ebf | |
457c801 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-03T06:19:25+01:00 | 6d3c842 | |
73d1b90 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-01T18:26:49+01:00 | 7efbb4e | |
ef09ec5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-29T08:33:20+01:00 | 2741589 | |
7efbb4e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T15:38:32Z | ||
8b37ebf | 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-02T12:46:20Z | ||
6d3c842 | 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:34:10Z | ||
bd3593b | 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-17T15:05:13+01:00 | ||
2741589 | 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:51:27Z | ||
bbef4fc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T22:24:38Z | ||
9c2d420 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:25:30Z | ||
9898ae2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T11:04:57Z | ||
433911a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T09:05:30Z | ||
bfdf60e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T21:17:54Z | ||
e9f59f6 | Inspect | - content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a406f42a-2e1f-44c5-b528-1d62b6120bc3/sv-benchmarks/c/ldv-memsafety/memset3_-write.c line: 29 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:28:53Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a406f42a-2e1f-44c5-b528-1d62b6120bc3/sv-benchmarks/c/ldv-memsafety/memset3_-write.c : 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a406f42a-2e1f-44c5-b528-1d62b6120bc3/sv-benchmarks/c/ldv-memsafety/memset3_-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:56:44+01:00 |
Found 29 witnesses for program sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bedbfd0 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:10:53+01:00 | ||
f87b5e4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-25T10:19:59Z | ||
50b1de3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T17:41:47Z | ||
e898c8e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:57:46+01:00 | 50b1de3 | |
619b778 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T04:19:19+01:00 | 0cdd984 | |
fac2e29 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:32:20+01:00 | defcdda | |
cc174fb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T00:54:31+01:00 | 6137e22 | |
4fc0350 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:06:26+01:00 | 7863901 | |
dbd1dff | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:17:57+01:00 | bedbfd0 | |
7c0ebbd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:58:42+01:00 | 13ea19c | |
a7036d7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:01:29+01:00 | dd069b1 | |
efd5ecb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:21:37+01:00 | b142ff5 | |
5002f14 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T02:24:06+01:00 | f87b5e4 | |
4d8008b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:29:32+01:00 | c9c1cb5 | |
13ea19c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T20:21:55+01:00 | ||
defcdda | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T23:34:27+01:00 | ||
7863901 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T04:24:16+01:00 | ||
dd069b1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2022-12-09T03:03:25+01:00 | ||
546cd71 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T10:44:39+01:00 | f997bd6 | |
3777b29 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:52:56+01:00 | 2b2cf5e | |
57bd4f2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:38:28+01:00 | 2db4745 | |
567fc97 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T15:45:37+01:00 | 2b0d140 | |
2b0d140 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T23:07:50Z | ||
f997bd6 | 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:19Z | ||
2db4745 | 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-15T00:33:18Z | ||
b142ff5 | 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-08T13:05:35+01:00 | ||
2b2cf5e | 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-13T21:21:42Z | ||
6137e22 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2022-12-11T04:38:46+01:00 | ||
c9c1cb5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T14:53:52Z |
Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
63ba42c | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T08:01:58+01:00 | ||
a25a8f3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T18:10:07 | ||
c0bae54 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T15:13:54Z | ||
c861735 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-10T21:26:56+01:00 | a25a8f3 | |
e0617a3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T16:02:25+01:00 | 182454f | |
2732d06 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T06:21:52+01:00 | 0cdd984 | |
1b73b84 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:06:33+01:00 | 241d28a | |
f9ab0db | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:12:33+01:00 | c0bae54 | |
49d69f5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:27:45+01:00 | 63ba42c | |
1217646 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:56:30+01:00 | 9dd5bca | |
e098c5e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:48:08+01:00 | a878d1e | |
38a5190 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:39:05+01:00 | f149055 | |
f149055 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T18:13:41+01:00 | ||
182454f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T14:10:55+01:00 | ||
9dd5bca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 4 | 2021-12-07T02:03:11+01:00 | ||
0a05ee9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T17:27:08+01:00 | 6f2adbd | |
017dee8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T08:34:10+01:00 | a4093b5 | |
f26f4d3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-08T13:50:18+01:00 | d1ad56a | |
fb0067f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-07T02:35:39+01:00 | 7e5169c | |
d1ad56a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T04:07:51Z | ||
a4093b5 | 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-09T22:53:33Z | ||
6f2adbd | 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:38:55Z | ||
a878d1e | 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-06T05:15:12+01:00 | ||
7e5169c | 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-06T23:26:21Z | ||
241d28a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T20:15:04+01:00 |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
845017a | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:43:43+01:00 | ||
c6d48e6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T20:09:19 | ||
ecdef01 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T20:10:28 | ||
7bd6e34 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:30:51+01:00 | c6d48e6 | |
a4c92bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T22:03:30+01:00 | a9df05b | |
81cd192 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:37:00+01:00 | 9044daa | |
d36c2c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T04:11:10+01:00 | ecdef01 | |
a2c5c9d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T06:27:34+01:00 | 4c3ee5e | |
eca7266 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T19:25:36+01:00 | 845017a | |
2a569ef | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:27:03+01:00 | 12d20ea | |
16c2928 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T18:24:54+01:00 | 3deddbf | |
4c3ee5e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T01:23:43+01:00 | ||
f4fd4d6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-07T16:32:01+01:00 | 2e48f79 | |
5666beb | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T02:30:29+01:00 | 0262057 | |
bd686ff | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:01:15+01:00 | 3deddbf | |
61ee6b1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:55:06+01:00 | 12d20ea | |
3deddbf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T16:55:16+01:00 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4dc144d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 23:41:08 | ||
92f5574 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:45:31+01:00 | ec0b59f | |
a446cad | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:23+01:00 | 4dc144d | |
1486414 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:06:05+01:00 | 0cdd984 | |
4f83e04 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-07T21:15:37+01:00 | 710c9d5 | |
87c15cc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:40:16+01:00 | cfe73b3 | |
8aff569 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:20:13+01:00 | 1ee8e9d | |
94d7607 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:58+01:00 | 8142b2f | |
48d246b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:10:32+01:00 | 61e3971 | |
61e3971 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-29T15:56:58+01:00 | ||
ec0b59f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T00:13:21+01:00 | ||
17019cc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-11T20:54:48+01:00 | 0dffc50 | |
25dc692 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:58:38+01:00 | c89f35b | |
9d8444d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:27:07+01:00 | 45a13a0 |
Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ee91291 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T10:00 CET (sv-comp) | ||
0e2c7db | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:39:27+01:00 | cc6ffca | |
c7a7e84 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:08:43+01:00 | bcfafb0 | |
afbfad9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:17:48+01:00 | 95815db | |
1e641fc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:17:44+01:00 | 1da0ebd | |
054dfc9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T06:23:49+01:00 | ||
009ab57 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T05:01:32+01:00 | d2fa7ff | |
9766d7b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:33:56+01:00 | 8950dc1 | |
de9f732 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T07:48:34+01:00 | 42939bf | |
fa99517 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-07T09:27:39+01:00 | 5da882d | |
0aa778f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:47:54+01:00 | 054dfc9 | |
e43a751 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T10:18:25+01:00 | fc13e3b | |
bcfafb0 | 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-07T21:40:08 | ||
42939bf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T14:46:18+01:00 | ||
2d9282f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:55+01:00 | b173d6d | |
00dcd65 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:53:25+01:00 | 5b473e8 | |
8399110 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T23:44:51+01:00 | ee91291 | |
f737376 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T03:42:48+01:00 | b173d6d |
Found 10 witnesses for program sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7fc6c06 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:12 CET (sv-comp) | ||
5929339 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:32:50+01:00 | ||
3faf943 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:53:58.375315 | ||
17d568e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:43:33.397765 | ||
83cdf12 | 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:54Z | ||
4a859e4 | 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:14Z | ||
b1497e3 | 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:25 CET (sv-comp) | ||
7a13a96 | 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:16Z | ||
5da882d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T22:06 CET (sv-comp) | ||
a902e3c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 3 | 2017-12-01T23:29 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memset3_false-valid-deref-write.c, 4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/4f4c34e89258ad08f5ff0f3cdaddc883f4834617a4558e66914b1b5dcd1f7778.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |