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 33 witnesses for program sv-benchmarks/c/termination-libowfat/strdup_true-termination.c.i, f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
d9e2fe0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2023-12-18T04:49:37+01:00 | ||
4bc6933 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:41:03+01:00 | ||
0e403b0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T06:22:08Z | ||
813882f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 18 | 2023-12-02T12:13:24Z | ||
dd6171f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T03:07:18Z | ||
5bb09ff | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T23:33:34Z | ||
925f838 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 18 | 2023-12-03T02:20:03Z | ||
bde552a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 12 | 2023-12-01T01:55:51Z | ||
3d241f0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-19T14:44:06+01:00 | 4941479 | |
8f65392 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-19T02:57:54+01:00 | 03ad3c1 | |
5243551 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-18T06:07:43+01:00 | d9e2fe0 | |
214df1c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-17T06:09:30+01:00 | dd6171f | |
bb61c1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T11:39:39+01:00 | 813882f | |
ba235ab | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-04T01:17:55+01:00 | 6c6fc4d | |
28006b9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-03T18:31:05+01:00 | 4bc6933 | |
0df5292 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-03T09:54:00+01:00 | 0e403b0 | |
5a04303 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-03T05:48:29+01:00 | 925f838 | |
c18412a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-12-01T03:37:29+01:00 | bde552a | |
8a491c3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-30T11:55:25+01:00 | 11765ef | |
11765ef | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-30T07:57:53+01:00 | ||
43db8f0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-30T02:32:20+01:00 | 5bb09ff | |
c4b72b8 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 9 | 2023-11-29T08:21:29+01:00 | e7fd15f | |
6c6fc4d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 9 | 2023-12-04T00:39:04+01:00 | ||
4941479 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 9 | 2023-12-19T12:11:54+01:00 | ||
03ad3c1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 9 | 2023-12-18T20:07:27+01:00 | ||
e7fd15f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 18 | 2023-11-28T22:52:00Z | ||
2ee8278 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-12-17T01:21:10Z | ||
7514c75 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2023-11-29T20:48:43Z | ||
68e8970 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Goblint (tags/svcomp24-0-gc2e9465a7) | 3 | 2023-12-01T02:01:20Z | ||
841caa8 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: f91b160b-43b8-48ee-abd1-7c2cbb91fdd2 creation_time: '2023-12-03T03:20:03+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5097f3ad-4cf1-4031-9b14-392210a7d519/sv-benchmarks/c/termination-dietlibc/strdup.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_5097f3ad-4cf1-4031-9b14-392210a7d519/sv-benchmarks/c/termination-dietlibc/strdup.i : f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 10 | 2023-12-03T05:32:59+01:00 | ||
c3c860a | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: dba8c316-2a2e-48ba-9b23-56423483c081 creation_time: 2023-11-28T23:52+01:00 producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_60b2cce8-73f8-428f-9960-1db969ba6aef/sv-benchmarks/c/termination-dietlibc/strdup.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_60b2cce8-73f8-428f-9960-1db969ba6aef/sv-benchmarks/c/termination-dietlibc/strdup.i : f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 10 | 2023-11-29T07:46:33+01:00 | ||
fc2e387 | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 84c4b0bf-810f-4f7a-9168-16f4240ddaa4 creation_time: '2023-12-02T13:13:25+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b0cf6644-53e0-4c41-b89e-660c56cc649f/sv-benchmarks/c/termination-dietlibc/strdup.i input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b0cf6644-53e0-4c41-b89e-660c56cc649f/sv-benchmarks/c/termination-dietlibc/strdup.i : f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] | correctness_witness | CPAchecker 2.3 | 10 | 2023-12-04T11:55:28+01:00 | ||
c54c81b | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: d9c8500a-45f1-4759-9495-1dc1ab1211d5 creation_time: 2023-12-01T01:55:51Z 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-dietlibc/strdup.i''' task: input_files: - ../../sv-benchmarks/c/termination-dietlibc/strdup.i input_file_hashes: ../../sv-benchmarks/c/termination-dietlibc/strdup.i: f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-dietlibc/strdup.i file_hash: f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496 line: 511 column: 11 function: memcpy value: dst == res format: c_expression - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-dietlibc/strdup.i file_hash: f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496 line: 511 column: 11 function: memcpy value: ((((n == 18446744073709551615UL || n == 0UL) || n == 0UL) || (((dst == c1 && src == c2) && n == 0UL) && res == c1)) || (((dst == c1 && src == c2) && n == 1UL) && res == c1)) || (((dst == c1 && src == c2) && n == 1UL) && res == c1) format: c_expression | correctness_witness | CPAchecker 2.3 | 11 | 2023-12-01T04:56:54+01:00 |
Found 28 witnesses for program sv-benchmarks/c/termination-libowfat/strdup_true-termination.c.i, f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
4421164 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | crux-llvm-0.5.0.99 | 5 | 2022-12-09T04:48:45+01:00 | ||
489b6f1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:15:30+01:00 | ||
9addba1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T13:10:38Z | ||
29416b7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 17 | 2022-12-14T07:01:30Z | ||
2b96df3 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T11:58:10Z | ||
c697e52 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T11:41:07Z | ||
57570e0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Kojak | 16 | 2022-12-15T01:38:31Z | ||
d0a4928 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Goblint (tags/svcomp23-0-g4f5dcf38f) | 17 | 2022-12-10T03:44:22Z | ||
1ceacd9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T11:11:05+01:00 | 29416b7 | |
928fd2c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T07:16:11+01:00 | 660b292 | |
0c8af2f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T06:23:37+01:00 | 57570e0 | |
8c0b4d2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T05:19:59+01:00 | c697e52 | |
54fb799 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T03:04:26+01:00 | a1e13c1 | |
2db2433 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-29T00:07:41+01:00 | 17c1b17 | |
adce774 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T22:50:53+01:00 | 489b6f1 | |
8973a95 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T22:39:23+01:00 | d0a4928 | |
639870f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T18:23:04+01:00 | 1dec323 | |
0903bbc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T17:37:56+01:00 | 9addba1 | |
35b72bb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T11:56:28+01:00 | d162c1b | |
a063046 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T08:33:51+01:00 | 4421164 | |
c4f11c2 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2023-01-28T00:45:46+01:00 | 2b96df3 | |
d162c1b | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 9 | 2022-12-10T19:58:40+01:00 | ||
a1e13c1 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 9 | 2022-12-12T02:50:57+01:00 | ||
17c1b17 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 9 | 2022-12-11T03:59:30+01:00 | ||
1dec323 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 9 | 2022-12-09T17:43:20+01:00 | ||
660b292 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 17 | 2022-12-13T12:18:26Z | ||
d31e51a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-25T10:43:02Z | ||
99d9f95 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2022-12-12T10:35:18Z |
Found 2 witnesses for program sv-benchmarks/c/termination-libowfat/strdup_true-termination.c.i, f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6c960a2 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2021-12-10T18:24:51 | ||
0affff0 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 3 | 2021-12-07T16:56:42Z |
Found 2 witnesses for program sv-benchmarks/c/termination-libowfat/strdup_true-termination.c.i, f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b0bd6da | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-11T15:46:22 | ||
78ca487 | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Symbiotic | 2 | 2020-12-09T02:24:12 |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strdup_true-termination.c.i, f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strdup_true-termination.c.i, f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strdup_true-termination.c.i, f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-libowfat/strdup_true-termination.c.i, f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/f841d4506b3d54a4be8e374f288503808db05c122988e690b43155c57f381496.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |