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).
Key | Value |
programName | sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i |
programSHA | 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 |
witnessName | results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.ex1-alloca_true-termination.c.i.files/witness.graphml |
witnessSHA | 0d900a620a5753161e83a114448ed8472b1809ec935d2a043f22b28f9d7d7103 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-01T18:15 CET (sv-comp) |
memoryModel | precise |
producer | ESBMC 3.1 |
program-sha256 | 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_fa14a551-ffbd-49cb-981a-a5df1fda0dd9/sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i |
programhash | 4b45df13f81f06cb5935eadea1b8dc5cf75af29d |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/0d900a620a5753161e83a114448ed8472b1809ec935d2a043f22b28f9d7d7103.graphml |
witness-sha256 | 0d900a620a5753161e83a114448ed8472b1809ec935d2a043f22b28f9d7d7103 |
witness-size | 6074 |
witness-type | correctness_witness |
Found 27 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
67b10c0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2023-12-18T05:09:37+01:00 | ||
e3d1f14 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 8 | 2023-12-02T15:27:09Z | ||
bc6f79c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2023-11-29T17:06:33Z | ||
8b8f5af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.4.0 kind | 4 | 2023-12-01T16:45:31Z | ||
d41bb52 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 5 | 2023-12-17T18:05:16+01:00 | ||
07daada | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2023-12-05T12:27:15Z | ||
e1aaf5e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 8 | 2023-11-29T03:27:21Z | ||
518fa38 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:37:54+01:00 | ||
72bd4a2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:59:16Z | ||
d05dd8e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T15:34:49+01:00 | a3f8971 | |
ed28ab4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-19T04:03:35+01:00 | ca48a93 | |
7b6ac66 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-18T06:10:09+01:00 | 67b10c0 | |
3a33e31 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-17T22:09:43+01:00 | d41bb52 | |
62a7481 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-05T14:36:33+01:00 | 07daada | |
71faa5c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T12:15:23+01:00 | e3d1f14 | |
47ae616 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-04T02:02:41+01:00 | 0396172 | |
238436d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T18:32:19+01:00 | 518fa38 | |
7fee101 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-03T09:54:33+01:00 | 72bd4a2 | |
7caf10c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-12-01T18:28:40+01:00 | 8b8f5af | |
0b36ec1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T12:40:13+01:00 | 59a06b5 | |
59a06b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T07:44:08+01:00 | ||
14fe72d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-30T03:06:08+01:00 | bc6f79c | |
7d49bcb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 5 | 2023-11-29T08:36:14+01:00 | e1aaf5e | |
0396172 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 5 | 2023-12-03T22:15:25+01:00 | ||
ca48a93 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2023-12-18T22:05:39+01:00 | ||
7d289e3 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: 8524fe1b-10f5-4d76-b04a-aa6cb7173da6 creation_time: 2023-12-01T01:57:45Z 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-memory-alloca/ex1-alloca.i''' task: input_files: - ../../sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i input_file_hashes: ../../sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i: 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i file_hash: 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 line: 556 column: 11 function: test_fun value: 1 == r format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i file_hash: 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 line: 556 column: 11 function: test_fun value: r == 1 format: c_expression | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-01T05:20:32+01:00 | ||
58bc4e2 | Inspect | - content: - segment: - waypoint: action: follow constraint: format: C value: \result == 46341 location: column: 41 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i line: 563 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 2 location: column: 65 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i line: 563 type: function_return - segment: - waypoint: action: follow constraint: format: C value: \result == 0 location: column: 89 file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i line: 563 type: function_return - segment: - waypoint: action: follow location: column: 9 file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i line: 557 type: target entry_type: violation_sequence metadata: creation_time: '2023-11-29T17:06:33Z' format_version: '0.1' producer: name: symbiotic task: data_model: LP64 input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i : 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0 input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_425bc055-4efa-457e-b4f7-091fb1f18826/sv-benchmarks/c/termination-memory-alloca/ex1-alloca.i language: C specification: CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 7 | 2023-11-30T03:00:38+01:00 |
Found 29 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
76793c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2022-12-09T04:46:05+01:00 | ||
9edef66 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Taipan | 8 | 2022-12-14T06:54:52Z | ||
5d62c30 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Symbiotic | 3 | 2022-12-12T12:25:54Z | ||
54ce536 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Kojak | 8 | 2022-12-14T16:55:30Z | ||
d623941 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 7.0.0 kind | 4 | 2022-12-18T15:47:27Z | ||
ec3d456 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | ESBMC 6.8.0 kind | 4 | 2022-12-25T11:27:31Z | ||
792ad6e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 10 | 2023-01-29T10:44:35+01:00 | 9edef66 | |
d580937 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CPAchecker 2.2 | 10 | 2023-01-29T06:53:33+01:00 | ebc7772 | |
1d78ff6 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | CBMC | 5 | 2022-12-08T10:43:19+01:00 | ||
cd7f7cf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Bubaak | 3 | 2022-12-08T21:48:17Z | ||
ebc7772 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | Automizer | 8 | 2022-12-13T21:13:07Z | ||
609e93c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:01:37+01:00 | ||
9507f27 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:20:04Z | ||
16b5e0b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T06:38:43+01:00 | 54ce536 | |
93da184 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T05:58:29+01:00 | 5d62c30 | |
552b614 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T02:34:02+01:00 | 37d6913 | |
8bd2207 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-29T00:52:44+01:00 | baadefd | |
ee0a6f9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T22:53:21+01:00 | 609e93c | |
4e38f6f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T18:38:42+01:00 | 5903754 | |
fc1665e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T17:38:45+01:00 | 9507f27 | |
675618f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T15:42:12+01:00 | d623941 | |
273aa33 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T11:28:49+01:00 | 1127ed2 | |
70a0686 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T08:35:17+01:00 | 76793c3 | |
dddc438 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T04:23:28+01:00 | 1d78ff6 | |
a6df91f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T02:25:30+01:00 | ec3d456 | |
043eb64 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2023-01-28T00:29:13+01:00 | cd7f7cf | |
1127ed2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 5 | 2022-12-10T18:37:44+01:00 | ||
37d6913 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 5 | 2022-12-12T01:59:21+01:00 | ||
5903754 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 5 | 2022-12-09T23:36:50+01:00 |
Found 1 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
92e4f8b | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T16:21:19 |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
49dedd9 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T22:40:21 | ||
58eab5f | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T00:10:50 |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 2 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
0d900a6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T18:15 CET (sv-comp) | ||
b4c6d35 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | 2LS | 29 | 2017-12-01T16:40 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-memory-alloca/ex1-alloca_true-termination.c.i, 0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/0e07f3778a6dc1ed71b4b2b55b5e5328fab33e7845cdda9d6dd07262778bbfc0.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |