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_ex1_true-termination.c.i, 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b0137dd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:00:36Z | ||
485d218 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 7 | 2023-12-18T04:49:58+01:00 | ||
73b7edc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 11 | 2023-12-02T13:44:55Z | ||
04e4da8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 4 | 2023-11-30T00:03:32Z | ||
4a91582 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 11 | 2023-12-03T02:52:31Z | ||
faf7ef4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.4.0 kind | 5 | 2023-12-01T11:58:46Z | ||
c0ca114 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2023-12-18T19:00:24+01:00 | ||
df01c6b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 11 | 2023-12-17T17:30:20+01:00 | ||
e088246 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 4 | 2023-12-05T10:51:28Z | ||
2f5056c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 4 | 2023-12-04T14:36:17Z | ||
9511a46 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 11 | 2023-11-29T04:47:01Z | ||
734773c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:56:55+01:00 | ||
527deba | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2023-12-19T19:16:05 | ||
c78ac2c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-20T02:31:46+01:00 | 527deba | |
860e3fd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T05:26:47+01:00 | c0ca114 | |
1593db7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-18T06:08:03+01:00 | 485d218 | |
12af454 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T22:11:01+01:00 | df01c6b | |
6cadd90 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T12:14:00+01:00 | 73b7edc | |
9c99b5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T01:52:08+01:00 | ef26b4b | |
0db3774 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T18:29:38+01:00 | 734773c | |
16a061c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T09:57:35+01:00 | b0137dd | |
8ff7f8d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T06:19:12+01:00 | 4a91582 | |
3afe860 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T11:27:30+01:00 | 453c1ea | |
df7de7f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T03:04:34+01:00 | 04e4da8 | |
453c1ea | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T02:03:56+01:00 | ||
5c8139e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:32:37+01:00 | 9511a46 | |
ef26b4b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-04T00:27:53+01:00 | ||
6cf75f4 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: b198f4f8-051e-4b7a-8ca6-a6b479ffb6c4 creation_time: 2023-12-01T02:02:58Z 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_ex1.i''' task: input_files: - ../../sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i input_file_hashes: ../../sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i: 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T04:20:49+01:00 | ||
76610f8 | 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_33277cb0-87e6-4066-855c-e0d3b2748663/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i line: 26 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2 location: column: 30 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_33277cb0-87e6-4066-855c-e0d3b2748663/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i line: 27 type: function_return - 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_33277cb0-87e6-4066-855c-e0d3b2748663/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i line: 14 type: function_return - 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_33277cb0-87e6-4066-855c-e0d3b2748663/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i line: 14 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2147483648 location: column: 30 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_33277cb0-87e6-4066-855c-e0d3b2748663/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i line: 14 type: function_return - segment: - waypoint: action: follow location: column: 3 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_33277cb0-87e6-4066-855c-e0d3b2748663/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i line: 10 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-30T00:03:32Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_33277cb0-87e6-4066-855c-e0d3b2748663/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i : 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_33277cb0-87e6-4066-855c-e0d3b2748663/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1.i language: C specification: CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-30T03:00:00+01:00 |
Found 27 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i, 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
12d8f2d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T12:58:46Z | ||
a5db95c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 7 | 2022-12-09T05:04:44+01:00 | ||
e51a64b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 11 | 2022-12-14T12:45:01Z | ||
dc42cee | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 4 | 2022-12-12T14:19:45Z | ||
0a582b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 11 | 2022-12-14T18:04:41Z | ||
499ea71 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.0.0 kind | 6 | 2022-12-18T16:37:36Z | ||
e57cf2e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 6.8.0 kind | 5 | 2022-12-25T09:45:52Z | ||
7f5f781 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 7 | 2022-12-10T04:29:06+01:00 | ||
16a4044 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 11 | 2022-12-08T13:10:24+01:00 | ||
a1f29c2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 4 | 2022-12-08T15:42:43Z | ||
81b571b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 11 | 2022-12-13T13:45:51Z | ||
e57e6ba | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:10:49+01:00 | ||
5292809 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Pinaka | 3 | 2022-12-11T14:31:42 | ||
4d59447 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T10:44:03+01:00 | e51a64b | |
f411239 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:53:32+01:00 | 81b571b | |
10192ec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:38:37+01:00 | 0a582b8 | |
c13ca30 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T05:58:20+01:00 | dc42cee | |
4d7e3b1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T04:47:57+01:00 | 5292809 | |
f4c6ef0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T02:35:39+01:00 | 09ca5c1 | |
814fb5a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:50:57+01:00 | e57e6ba | |
88d80e6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T21:08:38+01:00 | 7f5f781 | |
834fb9e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:45:29+01:00 | 12d8f2d | |
7a2a775 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T11:27:10+01:00 | 611b399 | |
44daf47 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:34:09+01:00 | a5db95c | |
acbf675 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T04:23:54+01:00 | 16a4044 | |
611b399 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T21:20:30+01:00 | ||
09ca5c1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T00:05:22+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i, 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8.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_ex1_true-termination.c.i, 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8.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_ex1_true-termination.c.i, 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8.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_ex1_true-termination.c.i, 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8.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_ex1_true-termination.c.i, 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
2f49b4b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 11 | 2017-12-01T20:10 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex1_true-termination.c.i, 97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/97c126101f069ab488324cfc4632ee48c30de136646e991b84ddea84d63344d8.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |