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/memsafety-ext3/scopes1_false-valid-deref.c, 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
441807b | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2023-12-18T10:07:30+01:00 | ||
96174c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2023-11-29T21:01:02Z | ||
9766ce4 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-19T15:34:23+01:00 | a1c8241 | |
910f4fa | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-19T05:26:41+01:00 | ff60220 | |
f3631fd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-18T12:07:21+01:00 | 441807b | |
ce2d95a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-18T03:09:53+01:00 | 96c01c2 | |
422c40b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-05T14:40:19+01:00 | 5c2f92c | |
eefbe64 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-04T16:42:34+01:00 | c42df8e | |
58ddc22 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-04T02:26:49+01:00 | cea1cc0 | |
7e43b65 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-01T18:28:16+01:00 | 2726292 | |
f25368a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-12-01T00:28:32+01:00 | 72c1dd1 | |
90ca974 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-11-30T13:43:09+01:00 | 5c62f2a | |
a977802 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-11-30T09:44:09+01:00 | cc9087a | |
5c62f2a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 3 | 2023-11-30T08:42:17+01:00 | ||
8093411 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-11-30T03:01:01+01:00 | 96174c2 | |
68f43e9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.3 | 4 | 2023-11-28T23:49:41+01:00 | f85ebf3 | |
cea1cc0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 4 | 2023-12-03T18:18:08+01:00 | ||
96c01c2 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 5 | 2023-12-18T02:15:43+01:00 | ||
c52995a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-17T22:08:04+01:00 | 89128b6 | |
6a0ae02 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-04T12:12:34+01:00 | e2f7acb | |
13989e1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-12-03T06:19:32+01:00 | 772b88a | |
85ee28f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.3 | 3 | 2023-11-29T08:34:30+01:00 | 1e884a1 | |
633bc29 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | Bubaak | 3 | 2023-12-01T20:18:18Z | ||
2726292 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.4.0 incr | 4 | 2023-12-01T16:51:55Z | ||
ff60220 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2023-12-18T16:39:58+01:00 | ||
e2f7acb | 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 | 6 | 2023-12-02T15:31:27Z | ||
772b88a | 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 | 6 | 2023-12-03T00:49:19Z | ||
89128b6 | 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-17T16:25:03+01:00 | ||
1e884a1 | 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 | 6 | 2023-11-28T23:31:30Z | ||
72c1dd1 | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | 2LS | 4 | 2023-11-30T20:42:01+01:00 | ||
f85ebf3 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | sv-sanitizers 0.1.1 | 3 | 2023-11-28T19:51:46Z | ||
cc9087a | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | PredatorHP | 4 | 2023-11-30T08:23:43Z | ||
5c2f92c | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-05T11:51:02Z | ||
c42df8e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2023-12-04T13:12:49Z | ||
95ea57e | Inspect | - content: - segment: - waypoint: action: follow location: column: 5 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6208fbf2-7967-45b6-8a75-c2d1fac37e5c/sv-benchmarks/c/memsafety-ext3/scopes1.c line: 16 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T21:01:02Z' format_version: '0.1' producer: name: symbiotic task: data_model: ILP32 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6208fbf2-7967-45b6-8a75-c2d1fac37e5c/sv-benchmarks/c/memsafety-ext3/scopes1.c : 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6208fbf2-7967-45b6-8a75-c2d1fac37e5c/sv-benchmarks/c/memsafety-ext3/scopes1.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 | 5 | 2023-11-30T02:58:39+01:00 |
Found 30 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes1_false-valid-deref.c, 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
75dd084 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2022-12-09T06:38:57+01:00 | ||
9a4b6f5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2022-12-12T10:41:23Z | ||
755546f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-29T05:57:32+01:00 | 9a4b6f5 | |
4f47b62 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-29T04:19:21+01:00 | fc1ab45 | |
33a6175 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-29T01:32:21+01:00 | 6154a71 | |
aa05454 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-29T00:54:22+01:00 | 90cd35e | |
5bf09c1 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-28T21:05:39+01:00 | c405cbf | |
9d574ba | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-28T15:41:43+01:00 | 7f9174e | |
0f4ca99 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-28T14:19:43+01:00 | 75dd084 | |
bf4dd4e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-28T08:58:04+01:00 | 20deaa9 | |
8975e48 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-28T06:01:23+01:00 | a412d98 | |
4da21c9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-28T02:23:30+01:00 | 67f7435 | |
01eb26f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-28T00:30:03+01:00 | 19072ae | |
a115167 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2023-01-27T23:37:24+01:00 | 0da9b8a | |
20deaa9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2 | 4 | 2022-12-10T16:35:28+01:00 | ||
6154a71 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 4 | 2022-12-12T01:54:44+01:00 | ||
c405cbf | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 4 | 2022-12-10T00:38:41+01:00 | ||
a412d98 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 5 | 2022-12-09T03:15:42+01:00 | ||
79ddd7e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T10:45:39+01:00 | 70dba0b | |
d23c09e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:54:22+01:00 | 400b1dc | |
2c1bfe3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-29T06:38:49+01:00 | 70705ad | |
9a9ed49 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.2 | 3 | 2023-01-28T04:22:40+01:00 | 8342f94 | |
7f9174e | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 7.0.0 incr | 4 | 2022-12-18T22:09:24Z | ||
67f7435 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2022-12-25T12:07:50Z | ||
70dba0b | 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 | 6 | 2022-12-14T12:40:03Z | ||
70705ad | 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 | 6 | 2022-12-14T17:25:34Z | ||
8342f94 | 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-08T08:50:14+01:00 | ||
400b1dc | 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 | 6 | 2022-12-13T20:49:56Z | ||
0da9b8a | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | 2LS | 4 | 2022-12-08T00:04:09+01:00 | ||
19072ae | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | Bubaak | 3 | 2022-12-08T14:44:37Z |
Found 28 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes1_false-valid-deref.c, 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5817ca4 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2021-12-07T07:49:34+01:00 | ||
ab40103 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2021-12-10T17:03:40 | ||
3d7063d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 3 | 2021-12-07T15:05:41Z | ||
a8ef730 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-10T21:28:13+01:00 | 0cd7237 | |
3a33240 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-09T16:03:18+01:00 | 15691ca | |
ef8533e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-09T06:21:57+01:00 | fc1ab45 | |
5466f99 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-08T21:07:02+01:00 | e8e0884 | |
e30876b | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-08T13:47:36+01:00 | 71de802 | |
61551c0 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-07T19:10:28+01:00 | 3d7063d | |
10e4449 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-07T11:26:53+01:00 | 5817ca4 | |
d37e8bc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-07T04:55:50+01:00 | 1f16e50 | |
fa52b81 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-06T01:24:53+01:00 | d5bbcfe | |
7dc2c15 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-05T20:40:47+01:00 | d825df9 | |
d825df9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.1 | 4 | 2021-12-05T17:25:19+01:00 | ||
15691ca | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2021-12-09T11:29:26+01:00 | ||
1f16e50 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-38892M | 5 | 2021-12-07T02:22:24+01:00 | ||
ee11132 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T17:26:53+01:00 | f084d04 | |
7dec2cc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-10T08:32:59+01:00 | 6d1b650 | |
1d4c8e5 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-07T02:34:44+01:00 | e19ea42 | |
a852e09 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.1 | 3 | 2021-12-06T11:46:38+01:00 | ad027d6 | |
71de802 | Inspect | CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) | violation_witness | ESBMC 6.8.0 incr | 4 | 2021-12-08T05:09:46Z | ||
e8e0884 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0.1-svn-fe6f522dd3+ | 4 | 2021-12-08T20:08:59+01:00 | ||
6d1b650 | 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 | 6 | 2021-12-10T01:15:03Z | ||
f084d04 | 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 | 6 | 2021-12-10T10:21:12Z | ||
ad027d6 | 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 | 6 | 2021-12-06T10:17:05+01:00 | ||
e19ea42 | 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 | 6 | 2021-12-06T19:47:15Z | ||
d5bbcfe | Inspect | CHECK( init(main()), LTL(G valid-free) ) CHECK( init(main()), LTL(G valid-deref) ) CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | 2LS | 4 | 2021-12-05T22:39:57+01:00 | ||
e3a1d24 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | SESL | 2 | 2021-12-06T11:57:25+01:00 |
Found 19 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes1_false-valid-deref.c, 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6054f91 | Inspect | valid-memsafety | violation_witness | DIVINE 4 | 2 | 2020-12-06T17:48:53+01:00 | ||
53aa5b8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-11T19:57:48 | ||
3f5e704 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 2 | 2020-12-09T01:53:04 | ||
f93c76d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-07T16:29:39+01:00 | 6866e25 | |
83182e3 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-06T19:22:59+01:00 | 6054f91 | |
5caf88d | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-06T19:22:08+01:00 | bb54ff0 | |
583a08f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-06T18:01:51+01:00 | c014589 | |
cbbe56a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-06T10:32:02+01:00 | bb54ff0 | |
c014589 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-05T13:40:40+01:00 | ||
2fced5e | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 2.0.1-svn-eda176372c+ | 4 | 2020-12-08T02:34:25+01:00 | ||
195470c | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:37:30+01:00 | 21481c9 | |
b75a10a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-06T18:27:50+01:00 | d8b3499 | |
fc56385 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-06T07:30:04+01:00 | d8b3499 | |
21f4ae5 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-12T01:28:29+01:00 | 53aa5b8 | |
b2e99fe | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-05T18:36:58+01:00 | c014589 | |
e082fdc | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-09T21:59:44+01:00 | 75b32a7 | |
3a3144d | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-09T03:58:05+01:00 | 3f5e704 | |
e486662 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 2.0 | 4 | 2020-12-08T07:31:00+01:00 | 2fced5e | |
0e95b35 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 2.0 | 3 | 2020-12-09T02:36:32+01:00 | 915131c |
Found 15 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes1_false-valid-deref.c, 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ec15cdd | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2019-12-01 07:46:54 | ||
a1b44a9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-08T00:06:05+01:00 | fc1ab45 | |
991e68a | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 4 | 2019-12-01T01:57:25+01:00 | ||
b367cb9 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-11T21:56:11+01:00 | aae4a31 | |
aa78ce8 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-08T00:26:43+01:00 | 67e3610 | |
230953f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-07T21:16:01+01:00 | 365f664 | |
416fbc9 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-11T21:09:03+01:00 | ec15cdd | |
8213e45 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-05T19:34:25+01:00 | 8c7b5f4 | |
de3a0b0 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-03T08:57:58+01:00 | 0ed2699 | |
ce8ca76 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-03T08:09:27+01:00 | 6d35583 | |
ff7a4d2 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-11T21:55:02+01:00 | 991e68a | |
8834edc | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-12-11T20:54:23+01:00 | 1d5a01d | |
6d35583 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.9 | 4 | 2019-11-30T01:00:53+01:00 | ||
eb4de19 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-06T02:39:05+01:00 | 5e343fd | |
4bd952e | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.9 | 3 | 2019-12-05T20:21:49+01:00 | a51bb5e |
Found 15 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes1_false-valid-deref.c, 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
9347720 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | Symbiotic | 1 | 2018-12-08T17:56 CET (sv-comp) | ||
f37de45 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 4 | 2018-12-07T10:54:39+01:00 | ||
e13544f | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T08:56:34+01:00 | f37de45 | |
32d3d71 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:41:53+01:00 | c6274c1 | |
ef43781 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T01:08:34+01:00 | ||
ab69b65 | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:00:23+01:00 | be42693 | |
d57b49f | Inspect | CHECK( init(main()), LTL(G valid-free) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-07T09:26:48+01:00 | 83527ee | |
7dfd910 | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:53:08+01:00 | f41244d | |
3757099 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-10T10:48:48+01:00 | aa16dcf | |
dbb5882 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T23:42:21+01:00 | 9347720 | |
2d7387b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-08T03:38:24+01:00 | aa16dcf | |
5671a13 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | violation_witness | CPAchecker 1.7-svn 29852 | 4 | 2018-12-06T09:49:19+01:00 | ef43781 | |
f960a9b | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:35:12+01:00 | 3051da9 | |
4a67b90 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-09T20:19:03+01:00 | c23842c | |
9c13963 | Inspect | CHECK( init(main()), LTL(G valid-deref) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 3 | 2018-12-06T09:16:50+01:00 | 3ff0374 |
Found 0 witnesses for program sv-benchmarks/c/memsafety-ext3/scopes1_false-valid-deref.c, 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a.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/scopes1_false-valid-deref.c, 5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5006077e10b123684af5816f85c68609f620d4e536300995b347b7a57b1efc6a.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |