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 29 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i, b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
65a5754 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:34:25Z | ||
79799ad | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2023-12-18T04:47:10+01:00 | ||
eedd5ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 6 | 2023-12-02T17:43:11Z | ||
0102e55 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2023-11-29T23:02:12Z | ||
d5a284a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 6 | 2023-12-03T01:17:27Z | ||
254f229 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.4.0 kind | 4 | 2023-12-01T12:01:37Z | ||
74793c1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-19T05:26:01+01:00 | 709c0df | |
303ada6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-05T14:40:54+01:00 | 30a039b | |
b5c2ff1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-04T16:40:30+01:00 | 5dce0e5 | |
e6b2ac0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-04T12:12:41+01:00 | eedd5ab | |
a15fb79 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T02:26:59+01:00 | f75528f | |
5594d2a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:30:39+01:00 | 3cf4105 | |
9c6fbe5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-03T09:57:19+01:00 | 65a5754 | |
8fe7076 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-03T06:19:03+01:00 | d5a284a | |
39e0c94 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-01T18:28:32+01:00 | 254f229 | |
0f339ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T13:42:43+01:00 | b7e8f75 | |
b7e8f75 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:40:07+01:00 | ||
0bf3f4e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-30T03:03:03+01:00 | 0102e55 | |
6f57b65 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:34:29+01:00 | 1e9ab33 | |
f75528f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T23:47:27+01:00 | ||
709c0df | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T23:03:05+01:00 | ||
1681a92 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 5 | 2023-12-17T15:17:28+01:00 | ||
30a039b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-05T08:11:31Z | ||
5dce0e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-04T10:09:56Z | ||
1e9ab33 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 6 | 2023-11-29T03:45:03Z | ||
3cf4105 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:25:25+01:00 | ||
2818744 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-18T06:02:40+01:00 | 79799ad | |
74da423 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-12-17T22:08:29+01:00 | 1681a92 | |
a896b4f | Inspect | - content: - segment: - waypoint: action: follow constraint: format: C value: \result == 0 location: column: 30 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c742acf-df25-4bcb-95eb-996919a374d8/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5.i line: 60 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2147483647 location: column: 30 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c742acf-df25-4bcb-95eb-996919a374d8/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5.i line: 61 type: function_return - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c742acf-df25-4bcb-95eb-996919a374d8/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5.i line: 23 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T23:02:12Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c742acf-df25-4bcb-95eb-996919a374d8/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5.i : b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_6c742acf-df25-4bcb-95eb-996919a374d8/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5.i language: C specification: CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T03:00:21+01:00 |
Found 29 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i, b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7406481 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 3 | 2022-12-15T10:58:11+01:00 | ||
e577384 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T11:19:40Z | ||
e46f650 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2022-12-09T04:51:09+01:00 | ||
7229a54 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 6 | 2022-12-14T09:54:30Z | ||
13e6231 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2022-12-12T11:05:31Z | ||
37a4dd0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 6 | 2022-12-15T02:40:39Z | ||
d2ae22b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.0.0 kind | 4 | 2022-12-18T19:22:35Z | ||
3bcac25 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 6.8.0 kind | 4 | 2022-12-25T08:56:49Z | ||
dc48e42 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T10:44:39+01:00 | 7229a54 | |
df876af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:54:09+01:00 | d04f13f | |
22c3802 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:38:51+01:00 | 37a4dd0 | |
1221ec3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T05:58:00+01:00 | 13e6231 | |
1ebff72 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T01:30:48+01:00 | cb2e957 | |
41b9333 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:51:45+01:00 | d6027cc | |
5c0d969 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T21:07:02+01:00 | 0f921fe | |
7e9fddf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T17:44:33+01:00 | e577384 | |
f09f034 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:41:03+01:00 | d2ae22b | |
1447bfc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:54:18+01:00 | 1a41904 | |
de5cb59 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:22:55+01:00 | 3bcac25 | |
1a41904 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2022-12-10T17:58:19+01:00 | ||
cb2e957 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T02:55:32+01:00 | ||
0f921fe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-09T20:21:19+01:00 | ||
55221e2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 5 | 2022-12-08T09:08:08+01:00 | ||
e8b9e37 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2022-12-08T18:50:14Z | ||
d04f13f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 6 | 2022-12-13T17:20:32Z | ||
d6027cc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-11T01:51:14+01:00 | ||
189cf61 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T08:32:13+01:00 | e46f650 | |
2b0386f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T04:23:49+01:00 | 55221e2 | |
5535038 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 7 | 2023-01-28T00:29:30+01:00 | e8b9e37 |
Found 1 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i, b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
486b198 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T16:57:43 |
Found 2 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i, b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
96a3442 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T17:18:48 | ||
b92ae27 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T15:45:22 |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i, b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i, b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i, b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2f7f022 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 15 | 2017-12-01T18:29 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5_true-termination.c.i, b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/b834abf8dc1317d8271c7246f1223cb53b92d1ccf9f4021ff5d970b2c79106ab.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |