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 30 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
8c2e4c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T04:16:36Z | ||
5c37bec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 4 | 2023-12-18T04:35:09+01:00 | ||
88b771a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 5 | 2023-12-02T18:10:58Z | ||
a74d7ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2023-11-30T00:07:43Z | ||
91b6a5b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 5 | 2023-12-03T01:59:13Z | ||
3e4a807 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.4.0 kind | 4 | 2023-12-01T10:28:36Z | ||
5404d5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-19T05:28:24+01:00 | c801ea3 | |
1c4e3f5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-05T14:39:54+01:00 | b359420 | |
cf35dda | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T16:44:52+01:00 | 6844d18 | |
6e6e695 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T12:13:34+01:00 | 88b771a | |
a5cb96a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T02:26:58+01:00 | 8b50725 | |
cc794ea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:33:29+01:00 | 67b1a00 | |
39296b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-03T09:56:51+01:00 | 8c2e4c3 | |
5eea19f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-03T06:18:48+01:00 | 91b6a5b | |
02855de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T13:45:43+01:00 | fce4c3f | |
fce4c3f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:08:32+01:00 | ||
821b77d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T03:03:55+01:00 | a74d7ab | |
c66223a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:34:40+01:00 | 994b7ac | |
8b50725 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T23:11:33+01:00 | ||
c801ea3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-19T01:09:47+01:00 | ||
e40f58e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 4 | 2023-12-17T08:39:17+01:00 | ||
b359420 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-05T10:45:53Z | ||
6844d18 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-04T14:41:44Z | ||
994b7ac | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 5 | 2023-11-28T19:44:17Z | ||
67b1a00 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:48:36+01:00 | ||
8e78dea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-18T06:02:43+01:00 | 5c37bec | |
4b699a6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T22:07:44+01:00 | e40f58e | |
a038c16 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T18:27:20+01:00 | 3e4a807 | |
db9d16e | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 1b3fab0c-9618-4a4e-bb72-1296f783c67e creation_time: 2023-12-01T01:05:01Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i''' task: input_files: - ../../sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i input_file_hashes: ../../sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i: e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | violation_witness | CPAchecker 2.3 | 6 | 2023-12-01T05:22:02+01:00 | ||
e45ed39 | Inspect | - content: - segment: - waypoint: action: follow constraint: format: C value: \result == 1 location: column: 30 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i line: 44 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_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i line: 45 type: function_return - segment: - waypoint: action: follow location: column: 5 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i line: 13 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-30T00:07:43Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i : e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0637d806-5cbc-4042-b7b8-a658cc28c370/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8.i language: C specification: CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T02:57:23+01:00 |
Found 29 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
5aafc45 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 3 | 2022-12-15T12:11:22+01:00 | ||
08d6c85 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T10:02:42Z | ||
6ba141b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 4 | 2022-12-09T03:42:49+01:00 | ||
283fb4f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 5 | 2022-12-14T12:07:40Z | ||
6c0e8c8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2022-12-12T16:07:05Z | ||
e45c95c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 5 | 2022-12-14T16:53:54Z | ||
cebdabd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.0.0 kind | 4 | 2022-12-19T02:41:50Z | ||
b14c7f9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 6.8.0 kind | 4 | 2022-12-25T10:59:13Z | ||
f88ddf8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T10:44:49+01:00 | 283fb4f | |
f71d13f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:53:46+01:00 | 0946bc9 | |
a25fc1f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:38:00+01:00 | e45c95c | |
2c4d533 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T05:56:11+01:00 | 6c0e8c8 | |
b9cae5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T01:31:35+01:00 | b56964c | |
b4207fe | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:50:52+01:00 | cc235fa | |
53c1148 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T21:04:32+01:00 | 74f77d4 | |
570d62c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T17:48:06+01:00 | 08d6c85 | |
6e6f7de | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:42:19+01:00 | cebdabd | |
2b15b26 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:55:30+01:00 | c82b5f0 | |
17a3fa8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:22:24+01:00 | b14c7f9 | |
c82b5f0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2022-12-10T21:46:01+01:00 | ||
b56964c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T00:36:10+01:00 | ||
74f77d4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-10T00:26:43+01:00 | ||
3227d7a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 4 | 2022-12-08T11:12:36+01:00 | ||
1b4f6d1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2022-12-08T18:19:31Z | ||
0946bc9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 5 | 2022-12-13T11:36:27Z | ||
cc235fa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:17:12+01:00 | ||
603e2f0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:30:08+01:00 | 6ba141b | |
2362201 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T04:21:48+01:00 | 3227d7a | |
1fa9d32 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T00:29:59+01:00 | 1b4f6d1 |
Found 1 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2dce79f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T17:55:06 |
Found 2 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0a839c9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T18:37:12 | ||
dd2f3be | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T01:52:08 |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.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_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.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_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1e8abca | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 8 | 2017-12-01T20:28 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex8_true-termination.c.i, e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e0b97717a770147a51187027f49ce4841280b7c6199e58b9d59e9dd8baf91869.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |