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_ex5B_true-termination.c.i, a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4e37f94 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T07:12:55Z | ||
03ac1ee | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2023-12-18T05:01:22+01:00 | ||
161940b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 6 | 2023-12-02T13:11:56Z | ||
d45ddc0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2023-11-29T20:20:14Z | ||
e263fd7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 6 | 2023-12-02T22:32:38Z | ||
be980a6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.4.0 kind | 4 | 2023-12-01T16:32:30Z | ||
c8c530a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-19T05:25:39+01:00 | cd6e50b | |
aa3bfae | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-05T14:38:41+01:00 | ffb7066 | |
8f4b117 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-04T16:44:34+01:00 | 4886b20 | |
0c0d370 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-04T12:13:35+01:00 | 161940b | |
af8e038 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-04T02:27:06+01:00 | f1f859d | |
2f9c6f6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:34:15+01:00 | d024419 | |
2c901dc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-03T10:01:34+01:00 | 4e37f94 | |
9ff2709 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-12-03T06:18:56+01:00 | e263fd7 | |
298d158 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-12-01T18:28:21+01:00 | be980a6 | |
bd73a03 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T13:43:50+01:00 | 30ea847 | |
30ea847 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 5 | 2023-11-30T05:12:55+01:00 | ||
3a54547 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-30T03:05:53+01:00 | d45ddc0 | |
74a3bc4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:33:24+01:00 | ac56be2 | |
f1f859d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T22:17:47+01:00 | ||
cd6e50b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-19T00:05:00+01:00 | ||
9886325 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 5 | 2023-12-17T20:02:02+01:00 | ||
ffb7066 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-05T12:38:27Z | ||
4886b20 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-04T09:44:58Z | ||
ac56be2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 6 | 2023-11-29T01:15:45Z | ||
d024419 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:53:02+01:00 | ||
2f47e56 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-18T06:11:22+01:00 | 03ac1ee | |
3df10c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-17T22:06:49+01:00 | 9886325 | |
c3aa1d6 | 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_157ea46c-471a-4383-be79-a551cf9a2ee9/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B.i line: 73 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_157ea46c-471a-4383-be79-a551cf9a2ee9/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B.i line: 74 type: function_return - segment: - waypoint: action: follow location: column: 2 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_157ea46c-471a-4383-be79-a551cf9a2ee9/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B.i line: 23 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T20:20:14Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_157ea46c-471a-4383-be79-a551cf9a2ee9/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B.i : a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_157ea46c-471a-4383-be79-a551cf9a2ee9/sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B.i language: C specification: CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.3 | 7 | 2023-11-30T03:00:47+01:00 |
Found 29 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i, a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
baeeaa4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | verifuzz | 3 | 2022-12-15T10:53:24+01:00 | ||
10dea46 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:32:24Z | ||
25e1bdb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2022-12-09T04:54:16+01:00 | ||
6f34960 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 6 | 2022-12-14T07:53:54Z | ||
0724e76 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2022-12-12T12:19:04Z | ||
a052189 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 6 | 2022-12-14T19:18:54Z | ||
9269a0c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.0.0 kind | 4 | 2022-12-19T01:24:04Z | ||
f667117 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 6.8.0 kind | 4 | 2022-12-25T09:57:01Z | ||
d0b18a5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T10:44:56+01:00 | 6f34960 | |
244b4b0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:53:44+01:00 | 3c7fdb0 | |
cb14488 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T06:37:23+01:00 | a052189 | |
8196587 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 6 | 2023-01-29T05:56:34+01:00 | 0724e76 | |
c013db5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-29T01:32:19+01:00 | 4c343aa | |
649a423 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:52:08+01:00 | ad65d02 | |
3d7eaa8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T21:04:28+01:00 | b7e7fe8 | |
4bd4a0f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T17:46:01+01:00 | 10dea46 | |
cc7e72b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:42:42+01:00 | 9269a0c | |
84221a8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:56:37+01:00 | e6ed69f | |
72ec741 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:22:39+01:00 | f667117 | |
e6ed69f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 5 | 2022-12-10T18:21:23+01:00 | ||
4c343aa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-11T21:18:12+01:00 | ||
b7e7fe8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-09T23:48:33+01:00 | ||
d0f98af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 5 | 2022-12-08T10:59:14+01:00 | ||
3f28bb4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2022-12-08T19:29:25Z | ||
3c7fdb0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 6 | 2022-12-13T18:45:51Z | ||
ad65d02 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:06:58+01:00 | ||
c6302d3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T08:32:54+01:00 | 25e1bdb | |
cbc0df7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T04:23:44+01:00 | d0f98af | |
e5fd00c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 8 | 2023-01-28T00:30:14+01:00 | 3f28bb4 |
Found 1 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i, a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
94301af | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T18:11:25 |
Found 2 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i, a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
ed14f0b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T18:38:11 | ||
ea4ec05 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-08T20:07:03 |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i, a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2.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_ex5B_true-termination.c.i, a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2.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_ex5B_true-termination.c.i, a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fbb756e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 28 | 2017-12-01T16:28 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-recursive-malloc/rec_malloc_ex5B_true-termination.c.i, a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/a2f1dacf23e701c88af5ee644fdcccaa723983d694e8bd4147c38940002aa7b2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |