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 33 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers2_false-valid-deref.c, cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
74ea12e | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T11:02:36+01:00 | ||
24171b3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T21:14:37Z | ||
1412e56 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-12-18T12:04:49+01:00 | 74ea12e | |
e48f371 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-12-17T22:08:37+01:00 | a116548 | |
36a732a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-12-05T14:39:37+01:00 | 95d2e16 | |
6066ab6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-12-04T16:44:57+01:00 | b4e6bfd | |
ca9402b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-12-04T12:13:26+01:00 | 8838223 | |
7239dae | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-12-03T06:19:02+01:00 | 8c302fb | |
bc8b908 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-12-01T22:54:28+01:00 | 3b2e36b | |
48fc5fe | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-12-01T18:28:03+01:00 | c370532 | |
f8a0257 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-11-30T13:45:41+01:00 | d4cb6b7 | |
4a2179c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-11-30T09:44:07+01:00 | 6421710 | |
d4cb6b7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 20 | 2023-11-30T05:02:25+01:00 | ||
c89ef40 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-11-30T03:01:51+01:00 | 24171b3 | |
eb57621 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-11-29T08:31:57+01:00 | be894d3 | |
ac5f1d0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 28 | 2023-11-28T23:49:40+01:00 | 7fc8695 | |
b74ed02 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 26 | 2023-12-03T21:36:34+01:00 | ||
183749f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 35 | 2023-12-18T01:33:25+01:00 | ||
0cc15f6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-19T05:25:58+01:00 | 4d1b6b7 | |
9ff3b77 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-18T03:09:22+01:00 | 183749f | |
8eba12a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-04T02:27:11+01:00 | b74ed02 | |
c370532 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T15:02:57Z | ||
8838223 | 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 | 21 | 2023-12-02T17:58:29Z | ||
8c302fb | 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 | 21 | 2023-12-03T02:59:31Z | ||
a116548 | 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 | 2023-12-17T08:39:18+01:00 | ||
be894d3 | 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 | 21 | 2023-11-29T05:52:15Z | ||
7fc8695 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T21:16:42Z | ||
6421710 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:25:42Z | ||
4d1b6b7 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 26 | 2023-12-18T16:20:11+01:00 | ||
95d2e16 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T08:20:41Z | ||
b4e6bfd | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T05:30:43Z | ||
3b2e36b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-01T19:57:25Z | ||
97e4279 | Inspect | - content: - segment: - waypoint: action: follow location: column: 4 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ab30c78d-4f72-492b-afda-5eceb0505a7f/sv-benchmarks/c/memsafety-ext3/getNumbers2.c line: 26 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T21:14:37Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ab30c78d-4f72-492b-afda-5eceb0505a7f/sv-benchmarks/c/memsafety-ext3/getNumbers2.c : cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_ab30c78d-4f72-492b-afda-5eceb0505a7f/sv-benchmarks/c/memsafety-ext3/getNumbers2.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 | 29 | 2023-11-30T03:00:30+01:00 |
Found 27 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers2_false-valid-deref.c, cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
15f17eb | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T05:13:28+01:00 | ||
6028eab | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T15:02:54Z | ||
efd8210 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-29T10:44:09+01:00 | 99333f8 | |
cfb4e9b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-29T06:53:12+01:00 | c9cdd6e | |
5652187 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-29T06:38:24+01:00 | 4b6dcb5 | |
ca7c107 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-29T05:55:50+01:00 | 6028eab | |
4041847 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-29T04:19:21+01:00 | e4000a0 | |
75dd771 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-28T15:45:44+01:00 | 2936932 | |
707fba8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-28T14:18:51+01:00 | 15f17eb | |
82906c5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-28T04:22:21+01:00 | 1b357cc | |
8f77a5a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-28T02:24:42+01:00 | 4a53104 | |
050b288 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 28 | 2023-01-28T00:29:23+01:00 | b863289 | |
dde91b7 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 26 | 2022-12-10T19:31:42+01:00 | ||
b150fd8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 26 | 2022-12-12T02:42:16+01:00 | ||
23f1678 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 26 | 2022-12-10T01:45:52+01:00 | ||
2708771 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 35 | 2022-12-09T03:19:05+01:00 | ||
b5824ff | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-29T01:30:51+01:00 | b150fd8 | |
6a5b5f1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T21:07:31+01:00 | 23f1678 | |
075302b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T08:54:22+01:00 | dde91b7 | |
c84a345 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T06:01:36+01:00 | 2708771 | |
2936932 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T16:38:47Z | ||
4a53104 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T12:37:55Z | ||
99333f8 | 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 | 21 | 2022-12-14T11:20:03Z | ||
4b6dcb5 | 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 | 21 | 2022-12-14T21:20:01Z | ||
1b357cc | 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 | 2022-12-08T04:30:51+01:00 | ||
c9cdd6e | 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 | 22 | 2022-12-13T12:45:41Z | ||
b863289 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T20:08:09Z |
Found 25 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers2_false-valid-deref.c, cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
397741a | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T08:12:27+01:00 | ||
5565f6b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:23:01 | ||
df2855d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T11:24:04Z | ||
ee09800 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 28 | 2021-12-10T21:27:49+01:00 | 6f0999d | |
463c4d3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 28 | 2021-12-10T17:27:28+01:00 | ae0a77e | |
3efffb0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 28 | 2021-12-10T08:33:00+01:00 | 0dea970 | |
a8887c6 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 28 | 2021-12-09T06:21:30+01:00 | e4000a0 | |
aa63a3d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 28 | 2021-12-08T13:46:12+01:00 | 55a6f20 | |
d6cd918 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 28 | 2021-12-07T19:10:20+01:00 | df2855d | |
94ea0d9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 28 | 2021-12-07T11:25:14+01:00 | 397741a | |
3c08179 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 28 | 2021-12-07T02:34:44+01:00 | 1f1bfb5 | |
3a4dcae | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 31 | 2021-12-06T11:48:39+01:00 | f2b687c | |
d248512 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 26 | 2021-12-05T15:35:15+01:00 | ||
86c5f6b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 35 | 2021-12-07T02:19:47+01:00 | ||
2a6a6a3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-09T16:01:51+01:00 | e91dfcd | |
eb14428 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-08T21:09:23+01:00 | 70b3918 | |
bd59fa0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-07T04:55:19+01:00 | 86c5f6b | |
92a7185 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 7 | 2021-12-05T20:38:52+01:00 | d248512 | |
55a6f20 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T05:51:02Z | ||
e91dfcd | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 26 | 2021-12-09T12:20:09+01:00 | ||
0dea970 | 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 | 21 | 2021-12-10T01:18:06Z | ||
ae0a77e | 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 | 21 | 2021-12-10T09:55:57Z | ||
f2b687c | 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 | 19 | 2021-12-06T08:42:04+01:00 | ||
1f1bfb5 | 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 | 22 | 2021-12-07T00:25:23Z | ||
70b3918 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 26 | 2021-12-08T18:46:39+01:00 |
Found 17 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers2_false-valid-deref.c, cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5a017a0 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:59:23+01:00 | ||
b12ec68 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T22:56:57 | ||
e562d42 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-08T17:36:41 | ||
aaf4daf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 28 | 2020-12-12T01:33:54+01:00 | b12ec68 | |
1213b4a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 31 | 2020-12-06T07:43:21+01:00 | 0b5e6ff | |
94e06cb | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 26 | 2020-12-07T23:47:37+01:00 | ||
a41bc21 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-08T06:39:44+01:00 | 94e06cb | |
8b2d440 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-06T18:02:21+01:00 | 3df6b53 | |
0c5f129 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 7 | 2020-12-05T18:39:28+01:00 | 3df6b53 | |
99e49ce | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 28 | 2020-12-09T21:35:32+01:00 | 03d07ed | |
48e360e | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 28 | 2020-12-09T03:58:03+01:00 | e562d42 | |
9ffcd44 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 28 | 2020-12-07T16:28:17+01:00 | 90f241a | |
cecbacf | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 28 | 2020-12-06T19:25:44+01:00 | 5a017a0 | |
3df6b53 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 26 | 2020-12-05T12:58:53+01:00 | ||
868e2bb | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 28 | 2020-12-09T21:50:04+01:00 | 590ff00 | |
0b996f1 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 28 | 2020-12-09T02:12:39+01:00 | 20dc293 | |
34eda08 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 31 | 2020-12-06T18:26:55+01:00 | 0b5e6ff |
Found 13 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers2_false-valid-deref.c, cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7fc7b09 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 21:48:28 | ||
ba8989e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 28 | 2019-12-11T21:45:51+01:00 | 35be8d8 | |
bf34ba5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 28 | 2019-12-11T21:09:09+01:00 | 7fc7b09 | |
a5afb28 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 28 | 2019-12-08T00:26:03+01:00 | feecbde | |
83793d1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 28 | 2019-12-03T08:57:07+01:00 | 7560755 | |
813668b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 26 | 2019-11-30T08:29:44+01:00 | ||
5a9fa6d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 26 | 2019-12-01T00:13:16+01:00 | ||
3f25e33 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 7 | 2019-12-11T21:46:08+01:00 | 5a9fa6d | |
a4474a1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 7 | 2019-12-05T20:20:50+01:00 | 5d3b946 | |
6427c41 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 7 | 2019-12-03T08:09:38+01:00 | 813668b | |
70585dc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 28 | 2019-12-11T20:55:08+01:00 | efeb156 | |
e5a3c4a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 28 | 2019-12-08T00:06:05+01:00 | e4000a0 | |
d7bea2b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 28 | 2019-12-07T21:15:35+01:00 | 68e6056 |
Found 14 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers2_false-valid-deref.c, cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9981853 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T00:27 CET (sv-comp) | ||
8ef093c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 31 | 2018-12-07T13:16:41+01:00 | ||
e83305a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-09T20:53:13+01:00 | 836b878 | |
5fea9ef | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 31 | 2018-12-06T09:48:15+01:00 | 32a50a8 | |
32a50a8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 31 | 2018-12-05T16:07:01+01:00 | ||
7b53ec3 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-10T10:48:42+01:00 | 08997cb | |
08c723a | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 31 | 2018-12-08T08:17:30+01:00 | 8ef093c | |
1aa7369 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-07T09:21:50+01:00 | b3b565d | |
48fb689 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-09T20:39:04+01:00 | 4264319 | |
092e2b3 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-09T20:21:01+01:00 | 65ccbb6 | |
2ed421d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-08T23:42:48+01:00 | 9981853 | |
4644c36 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-08T04:01:23+01:00 | 08997cb | |
865f1a0 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 28 | 2018-12-06T09:19:31+01:00 | db0f5ba | |
80431d8 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 7 | 2018-12-06T09:00:06+01:00 | 5d932d6 |
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/getNumbers2_false-valid-deref.c, cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd.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/getNumbers2_false-valid-deref.c, cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/cf0bb070a6f67963fcaf42c16427fd9b591ad6ca597a21a650e9cf23fa51a6dd.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |