A description of this web service can be found in the CAV paper "Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses" (more material).
Key | Value |
programName | sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c |
programSHA | ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6 |
witnessName | results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-memsafety.getNumbers1_false-valid-deref.c.files/witness.graphml |
witnessSHA | b50bedfc719bae3aed0f1a52d59be3f1c3982024004a3b1b28277ae63ce7fab5 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-05T23:28 CET (sv-comp) |
error-specification-length | Key 'specification' longer than 100 characters. |
producer | CBMC |
programfile | ../../sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c |
programhash | 1b1751fe95f9cf655681429038c1cde9e9c074e8 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) |
witness-file | witnessFileByHash/b50bedfc719bae3aed0f1a52d59be3f1c3982024004a3b1b28277ae63ce7fab5.graphml |
witness-sha256 | b50bedfc719bae3aed0f1a52d59be3f1c3982024004a3b1b28277ae63ce7fab5 |
witness-size | 20169 |
witness-type | correctness_witness |
Found 30 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0ed4aab | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:29:36+01:00 | ||
bd3c1b8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T23:32:05Z | ||
ea63cfb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-19T05:26:46+01:00 | e811df7 | |
b5f0c90 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-18T12:06:56+01:00 | 0ed4aab | |
b087cf7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-17T22:10:54+01:00 | e324efc | |
1b058a2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-05T14:40:57+01:00 | fb3f93d | |
4ef171f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-04T16:45:13+01:00 | 826e983 | |
7bbee8a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-04T12:11:57+01:00 | 5b5ce81 | |
1e27fce | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-04T02:25:34+01:00 | 036d545 | |
d6c1efe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-03T06:18:23+01:00 | bb936fa | |
c6ce26b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-12-01T22:53:47+01:00 | 48075f6 | |
7d0d449 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-11-30T13:44:23+01:00 | d6aedea | |
5d4327c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-11-30T09:44:20+01:00 | 361e8d9 | |
d6aedea | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 13 | 2023-11-30T09:03:42+01:00 | ||
09e49e2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-11-30T03:06:04+01:00 | bd3c1b8 | |
69dc626 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 15 | 2023-11-29T08:32:08+01:00 | 1f27a2f | |
036d545 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 15 | 2023-12-04T00:38:29+01:00 | ||
e811df7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 15 | 2023-12-18T21:40:09+01:00 | ||
d0000f7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T18:28:44+01:00 | f3600e0 | |
ce0ed9c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2023-12-18T01:45:44+01:00 | ||
f3600e0 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 12 | 2023-12-01T13:51:35Z | ||
5b5ce81 | 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 | 13 | 2023-12-02T15:55:16Z | ||
bb936fa | 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 | 13 | 2023-12-03T01:35:49Z | ||
e324efc | 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 | 5 | 2023-12-17T12:58:49+01:00 | ||
1f27a2f | 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 | 13 | 2023-11-29T03:12:55Z | ||
361e8d9 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:24:02Z | ||
fb3f93d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T10:25:09Z | ||
826e983 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T13:43:58Z | ||
48075f6 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T21:18:56Z | ||
e4fbe78 | Inspect | - content: - segment: - waypoint: action: follow location: column: 7 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f95cfd60-e0c4-460f-9cbe-e33685b89e0b/sv-benchmarks/c/memsafety-ext3/getNumbers1-1.c line: 11 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:32:05Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f95cfd60-e0c4-460f-9cbe-e33685b89e0b/sv-benchmarks/c/memsafety-ext3/getNumbers1-1.c : ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_f95cfd60-e0c4-460f-9cbe-e33685b89e0b/sv-benchmarks/c/memsafety-ext3/getNumbers1-1.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 | 16 | 2023-11-30T02:58:51+01:00 |
Found 26 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5490b7f | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:30:56+01:00 | ||
492b38e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T13:22:23Z | ||
2d232c6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-29T10:44:16+01:00 | 0f60f5a | |
ba7bad4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-29T06:53:27+01:00 | dc45fab | |
4cd71ee | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-29T06:38:01+01:00 | 0a903d2 | |
714b0b5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-29T05:58:47+01:00 | 492b38e | |
228dd09 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-29T04:19:25+01:00 | c3c2f34 | |
38332c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-29T01:30:53+01:00 | c4ea0b4 | |
2e8769f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-28T21:06:18+01:00 | 2bce36b | |
517ef0a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-28T14:09:21+01:00 | 5490b7f | |
6e8f5ec | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-28T08:56:02+01:00 | 6500b71 | |
4472fe1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-28T04:21:52+01:00 | e5425aa | |
93ebe4f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2023-01-28T00:28:18+01:00 | 15ed886 | |
6500b71 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 15 | 2022-12-10T21:28:07+01:00 | ||
c4ea0b4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 15 | 2022-12-12T00:44:20+01:00 | ||
2bce36b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 15 | 2022-12-10T02:07:50+01:00 | ||
868a182 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T15:43:36+01:00 | 0319f61 | |
644cb69 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T02:22:43+01:00 | 1ce8447 | |
211dc39 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2022-12-09T03:12:00+01:00 | ||
0319f61 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 12 | 2022-12-18T21:18:39Z | ||
1ce8447 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 12 | 2022-12-25T09:28:25Z | ||
0f60f5a | 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 | 13 | 2022-12-14T04:16:15Z | ||
0a903d2 | 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 | 13 | 2022-12-14T15:35:01Z | ||
e5425aa | 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 | 5 | 2022-12-08T07:02:14+01:00 | ||
dc45fab | 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 | 13 | 2022-12-13T13:08:35Z | ||
15ed886 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T15:48:19Z |
Found 24 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8379b74 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T09:39:59+01:00 | ||
c97a097 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T14:11:14Z | ||
36b8041 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-10T21:29:17+01:00 | 68e17bf | |
5a565a1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-10T17:27:33+01:00 | 3c87532 | |
3dad931 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-10T08:33:37+01:00 | 44e125c | |
41e874f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-09T16:02:04+01:00 | 8f3bfe5 | |
b2759ba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-09T06:21:07+01:00 | c3c2f34 | |
90a56c0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-08T21:10:47+01:00 | 27344f2 | |
8a445b1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 5 | 2021-12-07T19:09:54+01:00 | c97a097 | |
3aaaa82 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-07T11:26:37+01:00 | 8379b74 | |
a4fefb3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-07T02:36:15+01:00 | b67e373 | |
2a0e0cb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-06T11:46:36+01:00 | 1c0c863 | |
869f64f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-05T20:41:30+01:00 | 722bead | |
722bead | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 15 | 2021-12-05T16:16:08+01:00 | ||
68e17bf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 15 | 2021-12-10T18:32:09+01:00 | ||
27344f2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 15 | 2021-12-08T18:44:19+01:00 | ||
8f3bfe5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 15 | 2021-12-09T14:14:06+01:00 | ||
3244b65 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-08T13:45:36+01:00 | 85bd301 | |
12d23b4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0.1-svn-38892M | 7 | 2021-12-07T02:41:29+01:00 | ||
85bd301 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 12 | 2021-12-08T04:02:07Z | ||
44e125c | 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 | 13 | 2021-12-09T23:38:47Z | ||
3c87532 | 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 | 13 | 2021-12-10T13:05:33Z | ||
1c0c863 | 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 | 11 | 2021-12-06T04:28:17+01:00 | ||
b67e373 | 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 | 13 | 2021-12-06T17:26:23Z |
Found 15 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
864a96b | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T18:41:21+01:00 | ||
f795473 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T16:59:44 | ||
d479fe7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T23:22:34 | ||
d48bdef | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-12T01:45:48+01:00 | f795473 | |
5f84804 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 15 | 2020-12-09T22:08:37+01:00 | 1ee7f9e | |
de5caa2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 5 | 2020-12-09T03:57:36+01:00 | d479fe7 | |
d454df8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 15 | 2020-12-09T02:03:12+01:00 | d863f95 | |
fbc6889 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 15 | 2020-12-06T19:25:25+01:00 | 864a96b | |
1e1aa54 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-07T16:45:14+01:00 | 41e2f90 | |
22d2a24 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 15 | 2020-12-09T21:49:27+01:00 | 4b5d7fe | |
2b7a996 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 15 | 2020-12-08T06:36:34+01:00 | 31fc15b | |
5dc67c4 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 15 | 2020-12-06T18:01:20+01:00 | 080ea9d | |
fa6506c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 15 | 2020-12-05T18:05:11+01:00 | 080ea9d | |
080ea9d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 15 | 2020-12-05T16:02:22+01:00 | ||
31fc15b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 15 | 2020-12-07T22:41:51+01:00 |
Found 13 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
534a08e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 09:47:00 | ||
864b11d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-11T21:42:28+01:00 | 4c1b689 | |
130dc64 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-03T08:10:04+01:00 | cffda01 | |
cffda01 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-11-30T06:32:39+01:00 | ||
ffdbeba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 7 | 2019-12-05T20:20:32+01:00 | 95acd46 | |
cc3467b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-11T21:55:08+01:00 | c0b8a8f | |
e9b453e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 5 | 2019-12-11T21:09:05+01:00 | 534a08e | |
31efc5a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-08T00:27:24+01:00 | bde8c42 | |
0ff493e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-08T00:06:01+01:00 | c3c2f34 | |
cb79190 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-07T21:12:42+01:00 | 857c86b | |
d6305f6 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-03T08:57:01+01:00 | 594cc92 | |
73f1ccf | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 15 | 2019-12-11T20:55:11+01:00 | c5052bd | |
4c1b689 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 15 | 2019-12-01T17:41:38+01:00 |
Found 10 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
62dd25a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:53:10+01:00 | 5b2ec9b | |
3ea7f49 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:18:12+01:00 | 6611709 | |
c3834da | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T08:11:32+01:00 | b702de8 | |
c8883c5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T09:48:19+01:00 | 4c0ea7f | |
641ba23 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-10T10:48:54+01:00 | ab28e3b | |
dde12d2 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-09T20:38:23+01:00 | 271c821 | |
0bf476c | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-07T09:29:31+01:00 | 677dd6c | |
4c0ea7f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-06T02:41:22+01:00 | ||
b702de8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 15 | 2018-12-08T02:35:41+01:00 | ||
f4559fe | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 15 | 2018-12-08T04:33:32+01:00 | ab28e3b |
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers1_false-valid-deref.c, ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ae33a6a64877fc5c824e4d2dbc13817f946c171e566de8189cdbc86c749355b6.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |