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/memsetNonZero_false-valid-deref-write.c, e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ac3a890 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T09:52:07+01:00 | ||
eb0dddd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-12-17T00:41:17Z | ||
bd8071c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T19:43:19Z | ||
837b3ec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T15:33:42+01:00 | 0c4fb5b | |
f53d88a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:28:06+01:00 | afd1d67 | |
b24e43c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:05:02+01:00 | ac3a890 | |
863d0a7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:08:59+01:00 | 9f574e5 | |
09ca2e2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:06:21+01:00 | 16b7c8c | |
d6f2a65 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T06:38:11+01:00 | eb0dddd | |
d6e3033 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:40:32+01:00 | 6c51270 | |
8f105fe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:39:25+01:00 | 102bbe8 | |
9cc9d05 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:27:13+01:00 | 941260b | |
40bac66 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:54:05+01:00 | d18da85 | |
f72f958 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:44:12+01:00 | bb5474d | |
74065ff | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T09:44:10+01:00 | fa41687 | |
bb5474d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T08:21:41+01:00 | ||
52463b7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:06:21+01:00 | bd8071c | |
90d777d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:49:45+01:00 | ebfde74 | |
941260b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T22:32:16+01:00 | ||
0c4fb5b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2023-12-19T13:09:08+01:00 | ||
9f574e5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T02:13:06+01:00 | ||
97822c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-04T12:12:28+01:00 | d07a403 | |
d8327df | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-03T06:18:19+01:00 | d1b7cd7 | |
4ac1cbc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-01T18:28:06+01:00 | d60ac4a | |
20bc3ee | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-29T08:34:55+01:00 | 1683b7b | |
d60ac4a | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T12:22:48Z | ||
d07a403 | 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:54:04Z | ||
d1b7cd7 | 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-03T02:44:33Z | ||
16b7c8c | 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:20:33+01:00 | ||
1683b7b | 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:27:04Z | ||
ebfde74 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T22:13:02Z | ||
fa41687 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:25:10Z | ||
afd1d67 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-19T00:51:05+01:00 | ||
6c51270 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T10:46:31Z | ||
102bbe8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T14:27:19Z | ||
d18da85 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T19:58:00Z | ||
a0f5534 | Inspect | - content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_417acdb7-e156-4182-bbf3-914e3c7a0296/sv-benchmarks/c/ldv-memsafety/memsetNonZero_-write.c line: 27 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T19:43:19Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_417acdb7-e156-4182-bbf3-914e3c7a0296/sv-benchmarks/c/ldv-memsafety/memsetNonZero_-write.c : e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_417acdb7-e156-4182-bbf3-914e3c7a0296/sv-benchmarks/c/ldv-memsafety/memsetNonZero_-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:59+01:00 |
Found 29 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_false-valid-deref-write.c, e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0d78025 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T07:12:31+01:00 | ||
99d45bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-25T11:52:26Z | ||
a76f53b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T15:17:58Z | ||
06cb28a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:56:11+01:00 | a76f53b | |
a159a0b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T04:19:11+01:00 | 476c694 | |
1b0610e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:32:17+01:00 | 56aeedd | |
30463b3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T00:54:01+01:00 | f9c208e | |
0440256 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:06:49+01:00 | 97f66d7 | |
f9806f6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:09:48+01:00 | 0d78025 | |
c98c5c4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:56:15+01:00 | cdd58de | |
082daba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:01:31+01:00 | 51b6793 | |
c429156 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:22:07+01:00 | 6aec860 | |
1adf276 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T02:23:57+01:00 | 99d45bf | |
2070360 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:27:59+01:00 | 7fad1ae | |
cdd58de | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T19:27:25+01:00 | ||
56aeedd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T23:10:39+01:00 | ||
97f66d7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T02:20:07+01:00 | ||
51b6793 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T02:47:39+01:00 | ||
80c1925 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T10:44:10+01:00 | 6312003 | |
7b74de2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:52:41+01:00 | 77f1dd6 | |
40ba8be | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:38:44+01:00 | a122dc3 | |
62afbc1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T15:45:13+01:00 | 3a95323 | |
3a95323 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T19:19:13Z | ||
6312003 | 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-14T05:51:47Z | ||
a122dc3 | 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:37:04Z | ||
6aec860 | 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-08T10:03:46+01:00 | ||
77f1dd6 | 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-13T16:09:19Z | ||
f9c208e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2022-12-11T02:10:44+01:00 | ||
7fad1ae | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T18:57:42Z |
Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_false-valid-deref-write.c, e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0566baf | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:15:03+01:00 | ||
1dfa180 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T19:09:09 | ||
e79eafe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T15:09:18Z | ||
9b037de | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-10T21:29:02+01:00 | 1dfa180 | |
f4d7d61 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T16:03:28+01:00 | 898fa28 | |
f3cb45b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T06:21:41+01:00 | 476c694 | |
f095f4f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:07:38+01:00 | 9ed6689 | |
2f5b0d5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:10:42+01:00 | e79eafe | |
6fcc147 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:27:51+01:00 | 0566baf | |
4db31bb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:55:20+01:00 | 15ab98e | |
100d8f8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:48:32+01:00 | 3c49b71 | |
0ef9ea3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:41:32+01:00 | 7920d35 | |
7920d35 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T16:35:41+01:00 | ||
898fa28 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T13:38:37+01:00 | ||
15ab98e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T01:57:41+01:00 | ||
f2fa505 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T17:27:05+01:00 | 33d4f38 | |
4b4f4fc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T08:33:20+01:00 | 6eaee37 | |
eed1c9d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-08T13:46:31+01:00 | 289dabf | |
7c16ac8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-07T02:34:54+01:00 | cc7beba | |
289dabf | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T06:38:26Z | ||
6eaee37 | 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:28:28Z | ||
33d4f38 | 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-10T15:28:13Z | ||
3c49b71 | 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-06T02:08:55+01:00 | ||
cc7beba | 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-07T00:03:39Z | ||
9ed6689 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T17:45:24+01:00 |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_false-valid-deref-write.c, e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
11308da | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T12:02:54+01:00 | ||
e1c1b21 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T19:32:51 | ||
9799315 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-09T01:10:52 | ||
ad6e715 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:38:40+01:00 | e1c1b21 | |
2c55628 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:49:42+01:00 | cdb7ea1 | |
8d94533 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:43:12+01:00 | 973bcc2 | |
f1e85a2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T04:11:50+01:00 | 9799315 | |
d736055 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T06:35:39+01:00 | 1868975 | |
b3f147d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:27:32+01:00 | 83dbb6b | |
e5e7902 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:01:38+01:00 | 849d7f1 | |
5a5733f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:40:42+01:00 | 83dbb6b | |
7b46dce | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T18:49:29+01:00 | 849d7f1 | |
849d7f1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T14:48:02+01:00 | ||
1868975 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-08T04:58:49+01:00 | ||
7159f29 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T02:08:28+01:00 | 8b45f78 | |
a0defcf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:59:43+01:00 | 11308da | |
75e6fec | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-07T16:23:40+01:00 | 0390139 |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_false-valid-deref-write.c, e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d370090 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 08:17:55 | ||
365c739 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:55:54+01:00 | 1836263 | |
ee04ca1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:45:05+01:00 | 3a0e509 | |
b7cd9bd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:05+01:00 | d370090 | |
b845bb7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:06:03+01:00 | 476c694 | |
3384d55 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:38:42+01:00 | e2e8c0c | |
0005c9a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:21:50+01:00 | 057aa5f | |
66ef6bb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:05+01:00 | 5a60021 | |
f6bd0fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-30T06:44:03+01:00 | ||
4560160 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:26:27+01:00 | 203c929 | |
4028af3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-07T21:16:43+01:00 | 2c799b5 | |
3a0e509 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-12-01T12:46:52+01:00 | ||
feafb48 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-11T20:54:46+01:00 | c3fbefe | |
88a995f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:07:37+01:00 | f6bd0fd |
Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_false-valid-deref-write.c, e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9b94744 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:02 CET (sv-comp) | ||
4527c4b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:22:27+01:00 | 3845d9a | |
9dc4a8e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T23:43:58+01:00 | 9b94744 | |
c0cecf1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T08:47:27+01:00 | f18749f | |
52664af | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:16:59+01:00 | 52d5fdf | |
1d77960 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T03:19:22+01:00 | ||
342215b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T10:18:03+01:00 | 463bb75 | |
f18749f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T23:27:56+01:00 | ||
22f411b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:48+01:00 | bb35bf0 | |
6005d96 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:53:07+01:00 | 5b955ed | |
23e90b7 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:07:24+01:00 | f5c8275 | |
057c469 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-07T09:27:03+01:00 | e64e6ee | |
e67a2f2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:48:00+01:00 | 1d77960 | |
f5c8275 | 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:26:25 | ||
acfb326 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:39:28+01:00 | 5387be7 | |
513fcf7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T03:38:43+01:00 | bb35bf0 | |
0c92b0b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:18:05+01:00 | 7ad9e0e | |
1371aa0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T05:02:11+01:00 | 576f7ba |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_false-valid-deref-write.c, e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0bc8828 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:43 CET (sv-comp) | ||
6adbcf2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:28:19+01:00 | ||
c03a9bc | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T11:21:49.779166 | ||
1864fd4 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:51:13.282858 | ||
db10baf | 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:55Z | ||
46fbbd6 | 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:42Z | ||
0afea7a | 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:49 CET (sv-comp) | ||
3b5b94f | 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:29 CET (sv-comp) | ||
a4d48ef | 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:43Z | ||
e64e6ee | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T21:56 CET (sv-comp) | ||
3e57dee | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:46 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero_false-valid-deref-write.c, e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e1bccb981acdddec34b38cf69d1550cfb048293e7126831a8b31b1b676fdcae7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |