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 35 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
14025b5 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:52:52+01:00 | ||
8345726 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T23:55:00Z | ||
2c3b2d8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T15:33:31+01:00 | 08e3b30 | |
3a2cd7f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-19T05:27:59+01:00 | 4961e36 | |
5734ffb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T12:06:57+01:00 | 14025b5 | |
f16857a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-18T03:09:24+01:00 | edf2515 | |
45fe890 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:10:02+01:00 | 5ba7675 | |
8add923 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-05T14:36:57+01:00 | 15ad61a | |
b43c49e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T16:46:15+01:00 | 709be9f | |
a76278d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-04T02:26:49+01:00 | 4ed7a83 | |
d225cd2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-12-01T22:53:32+01:00 | 5f61fd5 | |
7d8cfbd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T13:44:07+01:00 | 185818d | |
7305c7e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T09:44:11+01:00 | 2a27592 | |
185818d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T06:52:03+01:00 | ||
e6d6a2b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T03:02:06+01:00 | 8345726 | |
1cbe852 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-28T23:49:34+01:00 | 8e33992 | |
4ed7a83 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 3 | 2023-12-03T23:10:33+01:00 | ||
edf2515 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2023-12-18T02:16:26+01:00 | ||
3f29225 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-04T12:13:58+01:00 | 46bfa01 | |
c6c018e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-03T06:18:55+01:00 | a94ef9d | |
5992a8f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-01T18:29:32+01:00 | 57bd539 | |
f0b614c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-29T08:33:57+01:00 | 44093e4 | |
57bd539 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T12:01:45Z | ||
4961e36 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2023-12-18T18:38:06+01:00 | ||
46bfa01 | 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-02T18:18:08Z | ||
a94ef9d | 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-03T01:50:25Z | ||
5ba7675 | 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-17T11:32:06+01:00 | ||
44093e4 | 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-29T01:53:05Z | ||
8e33992 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T19:49:40Z | ||
2a27592 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:23:42Z | ||
08e3b30 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2023-12-19T11:31:45+01:00 | ||
15ad61a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T08:44:27Z | ||
709be9f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T13:27:10Z | ||
5f61fd5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T19:58:26Z | ||
54b16a2 | Inspect | - content: - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb3e2dfe-2793-4a18-8172-8df2ef60bd8a/sv-benchmarks/c/ldv-memsafety/memsetNonZero2_-write.c line: 22 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:55:00Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb3e2dfe-2793-4a18-8172-8df2ef60bd8a/sv-benchmarks/c/ldv-memsafety/memsetNonZero2_-write.c : 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cb3e2dfe-2793-4a18-8172-8df2ef60bd8a/sv-benchmarks/c/ldv-memsafety/memsetNonZero2_-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:09+01:00 |
Found 29 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
cf99d25 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:12:05+01:00 | ||
c6a6fc4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T12:41:27Z | ||
7e42ffc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T05:56:13+01:00 | c6a6fc4 | |
5e55c01 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T04:19:23+01:00 | cb646d4 | |
c66e2be | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T01:30:25+01:00 | 6400df1 | |
3608aab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-29T00:51:58+01:00 | c584973 | |
b490f78 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T21:05:04+01:00 | e331f06 | |
2094fc1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T14:15:54+01:00 | cf99d25 | |
bcd5d5a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T08:56:53+01:00 | ed0b941 | |
98241ff | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T06:01:21+01:00 | 53f6088 | |
0fcae52 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:22:09+01:00 | f56c3c1 | |
9dfa2b3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2023-01-28T00:29:01+01:00 | 6fe1118 | |
ed0b941 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 3 | 2022-12-10T19:18:59+01:00 | ||
6400df1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 3 | 2022-12-11T20:56:12+01:00 | ||
c584973 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2022-12-11T05:38:42+01:00 | ||
53f6088 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2022-12-09T02:17:22+01:00 | ||
680a95a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T10:43:37+01:00 | 8ea4e2a | |
1e9cb24 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:54:32+01:00 | ae6ca79 | |
bdb85c1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:38:24+01:00 | 481e654 | |
3f2b9ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T15:43:46+01:00 | c71f9ef | |
de3f02a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T02:24:40+01:00 | af4a154 | |
c71f9ef | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T19:16:23Z | ||
af4a154 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T10:29:54Z | ||
e331f06 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 3 | 2022-12-10T02:31:32+01:00 | ||
8ea4e2a | 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-14T04:50:58Z | ||
481e654 | 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-14T21:15:03Z | ||
f56c3c1 | 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-08T06:25:47+01:00 | ||
ae6ca79 | 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-13T19:02:18Z | ||
6fe1118 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T19:00:45Z |
Found 25 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
96e74c5 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T08:11:09+01:00 | ||
f0d5caf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:48:24 | ||
da19b08 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T09:17:52Z | ||
531c4b7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-10T21:28:55+01:00 | f0d5caf | |
c5fbb89 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T15:59:02+01:00 | 70646a5 | |
0a1ac97 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-09T06:22:01+01:00 | cb646d4 | |
70abd32 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-08T21:06:56+01:00 | 875229f | |
2ca0344 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T19:10:06+01:00 | da19b08 | |
6676e1a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T11:28:02+01:00 | 96e74c5 | |
7ebe82b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-07T04:55:16+01:00 | d6e78b2 | |
e1f8d51 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:49:30+01:00 | ffa921c | |
cbfcc69 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T20:41:34+01:00 | 637ac4d | |
637ac4d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 3 | 2021-12-05T15:21:05+01:00 | ||
875229f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 3 | 2021-12-08T19:31:07+01:00 | ||
d6e78b2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 3 | 2021-12-07T02:10:31+01:00 | ||
617fbde | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T17:27:26+01:00 | 5bf484e | |
f0c0123 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T08:33:04+01:00 | 55548ed | |
158f418 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-08T13:48:41+01:00 | b98910e | |
dee8c1d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-07T02:34:58+01:00 | 89f231e | |
b98910e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T04:35:42Z | ||
55548ed | 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-10T00:03:09Z | ||
5bf484e | 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-10T09:05:40Z | ||
ffa921c | 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-06T04:15:38+01:00 | ||
89f231e | 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-06T22:17:13Z | ||
70646a5 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2021-12-09T14:19:00+01:00 |
Found 17 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9989d9f | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T12:16:53+01:00 | ||
11f4c86 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T18:37:48 | ||
cedd224 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T16:30:52 | ||
60cdd61 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-12T01:25:37+01:00 | 11f4c86 | |
27dea81 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:25:18+01:00 | 8e85914 | |
93e9587 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T19:03:47+01:00 | 9989d9f | |
2e88647 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:00:38+01:00 | a2114c0 | |
bebd1af | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:39:06+01:00 | 5ff4e3e | |
9fa77c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T18:09:51+01:00 | a2114c0 | |
6f16361 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 3 | 2020-12-07T23:09:30+01:00 | ||
003815b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T22:05:32+01:00 | 9afec46 | |
8ebee87 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T04:12:43+01:00 | cedd224 | |
a2114c0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-05T16:56:09+01:00 | ||
c1ebd0b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-07T16:09:34+01:00 | aad1f3b | |
d00502d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-09T01:49:10+01:00 | 1c69ee9 | |
3fa71dc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-08T06:36:42+01:00 | 6f16361 | |
bf5ecfb | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:27:11+01:00 | 5ff4e3e |
Found 14 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
bdc4770 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 20:50:57 | ||
ed0ee70 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:33:58+01:00 | a794efc | |
51168b0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:09:38+01:00 | bdc4770 | |
3a3e9f5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:26:51+01:00 | 2ffc23e | |
ce3ab92 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:07:35+01:00 | cb646d4 | |
343a744 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:39:28+01:00 | 44f835f | |
9a4ec8e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:20:50+01:00 | f5560b9 | |
3cf6eee | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-11-29T15:27:54+01:00 | ||
24c741b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:57:50+01:00 | f2491f9 | |
fc5d25d | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-03T08:31:21+01:00 | 3cf6eee | |
a794efc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 3 | 2019-11-30T22:03:27+01:00 | ||
1c2716f | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:43:51+01:00 | 1c475e3 | |
07145b0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 3 | 2019-12-07T21:13:52+01:00 | d6a5916 | |
cd3ee52 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-11T20:54:30+01:00 | 0493508 |
Found 18 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7d33d13 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T07:36 CET (sv-comp) | ||
db297f5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-10T10:48:39+01:00 | 885fa78 | |
18f5ffd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:53:05+01:00 | c4a8c93 | |
ebc08d1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:24:29+01:00 | a73d04b | |
1c28942 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T08:56:43+01:00 | b0cd215 | |
1d25d48 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:18:18+01:00 | 8f70620 | |
b0cd215 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 3 | 2018-12-07T20:44:38+01:00 | ||
57d9e57 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T22:07:27+01:00 | 2e3bf58 | |
e03b27f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-07T09:15:41+01:00 | 156de7e | |
c012e29 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:15:13+01:00 | d2a3ae4 | |
959ad92 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-05T18:26:12+01:00 | ||
fbe88e5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T10:20:13+01:00 | 6a618d5 | |
2e3bf58 | 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:06:38 | ||
b376c50 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:37:43+01:00 | 8a53cd6 | |
c8c4a79 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T23:42:34+01:00 | 7d33d13 | |
b2977f8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T03:24:54+01:00 | 885fa78 | |
b5c2250 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:48:10+01:00 | 959ad92 | |
f5f51ca | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-08T05:06:19+01:00 | 434e02f |
Found 11 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
323a41e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2017-12-02T23:42 CET (sv-comp) | ||
ac08659 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 3 | 2017-12-01T08:29:16+01:00 | ||
b3e2912 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-02T10:34:39.094221 | ||
30f7702 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T23:36:24.177572 | ||
9f129de | 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 | ||
547f8f9 | 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:47Z | ||
2f64a07 | 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:14 CET (sv-comp) | ||
9d536e2 | 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) | ||
a4abc45 | 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:18Z | ||
156de7e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2017-12-01T21:49 CET (sv-comp) | ||
2a99505 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Map2Check | 2 | 2017-12-01T23:47 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/ldv-memsafety/memsetNonZero2_false-valid-deref-write.c, 6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6ee5bab22bb27b31bdc1e46b5ad945cfa92016e1139565f86ec528ca863209ee.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |