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 26 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_true-termination_true-valid-memsafety.c, e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6fac193 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2023-12-03T08:11:49Z | ||
8fc12aa | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-24 | 4 | 2023-12-03T17:44:20+01:00 | ||
b58e1bd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2023-12-20T03:37 CET (comp) | ||
a2c7f4f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2023-12-02T14:46:18Z | ||
2e2fe4a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2023-11-29T14:47:10Z | ||
7d1b95d | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-20T03:41:23+01:00 | b58e1bd | |
3c82922 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T14:43:15+01:00 | 3ff0792 | |
ec790bf | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-19T03:09:21+01:00 | cd95f41 | |
b3ec79f | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-17T06:04:15+01:00 | c714f74 | |
d1ac5af | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T11:41:48+01:00 | a2c7f4f | |
84ee703 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-04T02:10:36+01:00 | 10490a7 | |
3526ebb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T18:31:05+01:00 | 8fc12aa | |
9587914 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-12-03T10:01:23+01:00 | 6fac193 | |
f4b1b4a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T11:33:17+01:00 | 37f11cb | |
37f11cb | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-30T05:45:07+01:00 | ||
cbdcacd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T18:35:34+01:00 | 2e2fe4a | |
0f3a5b5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.3 | 6 | 2023-11-29T08:14:31+01:00 | 7c20bda | |
10490a7 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-e677b7cd46+ | 6 | 2023-12-04T00:42:13+01:00 | ||
c714f74 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2023-12-17T01:58:17+01:00 | ||
3ff0792 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2023-12-19T13:34:49+01:00 | ||
cd95f41 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2023-12-19T01:09:37+01:00 | ||
7c20bda | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2023-11-29T02:48:12Z | ||
ba952ea | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 336 | 2023-12-17T12:27:01+01:00 | ||
90a4fde | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 447b0f7a-81f6-4e82-9671-c1b767f44928 creation_time: '2023-11-29T03:48:12+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0fcba2c5-8bc2-4a7a-a86c-0711fda0aa98/sv-benchmarks/c/termination-crafted/Mysore-2.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0fcba2c5-8bc2-4a7a-a86c-0711fda0aa98/sv-benchmarks/c/termination-crafted/Mysore-2.c : e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0fcba2c5-8bc2-4a7a-a86c-0711fda0aa98/sv-benchmarks/c/termination-crafted/Mysore-2.c file_hash: e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7 line: 22 column: 0 function: main value: ((((((0 <= (2147483649 + x)) && ((c + x) <= 65531)) && (3 <= c)) && ((x + (c * 4)) <= 2147483656)) || ((((3 <= c) && (c <= 65536)) && (0 <= ((c + x) + 65535))) && ((c + x) <= 65536))) || ((((2 <= c) && (c <= 65535)) && (0 <= (x + 65535))) && (x <= 65535))) format: c_expression | correctness_witness | CPAchecker 2.3 | 8 | 2023-11-29T07:49:36+01:00 | ||
6d3b0fc | Inspect | - entry_type: invariant_set metadata: format_version: '2.0' uuid: 2313642d-2f2f-4b4d-b840-af284003f7cd creation_time: '2023-12-02T15:46:18+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b5fd6672-494e-4228-b28e-5f2a43490038/sv-benchmarks/c/termination-crafted/Mysore-2.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b5fd6672-494e-4228-b28e-5f2a43490038/sv-benchmarks/c/termination-crafted/Mysore-2.c : e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: - invariant: type: loop_invariant location: file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b5fd6672-494e-4228-b28e-5f2a43490038/sv-benchmarks/c/termination-crafted/Mysore-2.c file_hash: e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7 line: 22 column: 0 function: main value: (((((((3 <= c) && (c <= 65536)) && (0 <= ((c + x) + 65535))) && ((c + x) <= 65536)) || (((((2 * c) + x) <= 65536) && (c <= (x + 196615))) && (3 <= c))) || ((((3 <= c) && (0 <= ((c + x) + 65535))) && (((2 * c) + x) <= 65538)) && (c <= 65537))) || ((((2 <= c) && (c <= 65535)) && (0 <= (x + 65535))) && (x <= 65535))) format: c_expression | correctness_witness | CPAchecker 2.3 | 8 | 2023-12-04T12:04:01+01:00 | ||
02c2748 | Inspect | - entry_type: invariant_set metadata: format_version: "2.0" uuid: aa6e1890-b60b-4d63-be3a-090edcccbabe creation_time: 2023-12-01T02:04:39Z 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-crafted/Mysore-2.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/Mysore-2.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/Mysore-2.c: e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: - invariant: type: loop_invariant location: file_name: ../../sv-benchmarks/c/termination-crafted/Mysore-2.c file_hash: e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7 line: 22 column: 12 function: main value: ((((((((((((((14 <= c && x <= 65445) && (65431LL + (long long )c) - (long long )x >= 0LL) && (65459LL - (long long )c) - (long long )x >= 0LL) || ((((((((-131090 <= x && 13 <= c) && c <= 65546) && x <= 65458) && (65544LL + (long long )c) + (long long )x >= 0LL) && (196636LL - (long long )c) + (long long )x >= 0LL) && (65445LL + (long long )c) - (long long )x >= 0LL) && (65471LL - (long long )c) - (long long )x >= 0LL) && c != 11)) || ((((((((-131088 <= x && 12 <= c) && c <= 65545) && x <= 65470) && (65543LL + (long long )c) + (long long )x >= 0LL) && (196633LL - (long long )c) + (long long )x >= 0LL) && (65458LL + (long long )c) - (long long )x >= 0LL) && (65482LL - (long long )c) - (long long )x >= 0LL) && c != 10)) || ((((((((-131086 <= x && 11 <= c) && c <= 65544) && x <= 65481) && (65542LL + (long long )c) + (long long )x >= 0LL) && (196630LL - (long long )c) + (long long )x >= 0LL) && (65470LL + (long long )c) - (long long )x >= 0LL) && (65492LL - (long long )c) - (long long )x >= 0LL) && c != 9)) || ((((((((-131084 <= x && 10 <= c) && c <= 65543) && x <= 65491) && (65541LL + (long long )c) + (long long )x >= 0LL) && (196627LL - (long long )c) + (long long )x >= 0LL) && (65481LL + (long long )c) - (long long )x >= 0LL) && (65501LL - (long long )c) - (long long )x >= 0LL) && c != 8)) || ((((((((-131082 <= x && 9 <= c) && c <= 65542) && x <= 65500) && (65540LL + (long long )c) + (long long )x >= 0LL) && (196624LL - (long long )c) + (long long )x >= 0LL) && (65491LL + (long long )c) - (long long )x >= 0LL) && (65509LL - (long long )c) - (long long )x >= 0LL) && c != 7)) || ((((((((-131080 <= x && 8 <= c) && c <= 65541) && x <= 65508) && (65539LL + (long long )c) + (long long )x >= 0LL) && (196621LL - (long long )c) + (long long )x >= 0LL) && (65500LL + (long long )c) - (long long )x >= 0LL) && (65516LL - (long long )c) - (long long )x >= 0LL) && c != 6)) || ((((((((-131078 <= x && 7 <= c) && c <= 65540) && x <= 65515) && (65538LL + (long long )c) + (long long )x >= 0LL) && (196618LL - (long long )c) + (long long )x >= 0LL) && (65508LL + (long long )c) - (long long )x >= 0LL) && (65522LL - (long long )c) - (long long )x >= 0LL) && c != 5)) || ((((((((-131076 <= x && 6 <= c) && c <= 65539) && x <= 65521) && (65537LL + (long long )c) + (long long )x >= 0LL) && (196615LL - (long long )c) + (long long )x >= 0LL) && (65515LL + (long long )c) - (long long )x >= 0LL) && (65527LL - (long long )c) - (long long )x >= 0LL) && c != 4)) || ((((((((-131074 <= x && 5 <= c) && c <= 65538) && x <= 65526) && (65536LL + (long long )c) + (long long )x >= 0LL) && (196612LL - (long long )c) + (long long )x >= 0LL) && (65521LL + (long long )c) - (long long )x >= 0LL) && (65531LL - (long long )c) - (long long )x >= 0LL) && c != 3)) || ((((((((-131072 <= x && 4 <= c) && c <= 65537) && x <= 65530) && (65535LL + (long long )c) + (long long )x >= 0LL) && (196609LL - (long long )c) + (long long )x >= 0LL) && (65526LL + (long long )c) - (long long )x >= 0LL) && (65534LL - (long long )c) - (long long )x >= 0LL) && c != 2)) || ((((((((-131070 <= x && 3 <= c) && c <= 65536) && x <= 65533) && (65534LL + (long long )c) + (long long )x >= 0LL) && (196606LL - (long long )c) + (long long )x >= 0LL) && (65530LL + (long long )c) - (long long )x >= 0LL) && (65536LL - (long long )c) - (long long )x >= 0LL) && c != 1)) || ((((((((-65535 <= x && 2 <= c) && c <= 65535) && x <= 65535) && (65533LL + (long long )c) + (long long )x >= 0LL) && (131070LL - (long long )c) + (long long )x >= 0LL) && (65533LL + (long long )c) - (long long )x >= 0LL) && (131070LL - (long long )c) - (long long )x >= 0LL) && c != 0) format: c_expression | correctness_witness | CPAchecker 2.3 | 12 | 2023-12-01T05:13:55+01:00 |
Found 24 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_true-termination_true-valid-memsafety.c, e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
16725a5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | violation_witness | frama-c-sv version 0.4.0 | 3 | 2022-12-09T09:47:04Z | ||
ad7e1e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | sv-comp-22 | 4 | 2022-12-10T22:15:16+01:00 | ||
b58e1bd | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | VeriOover | 1 | 2022-12-12T11:00 CET (comp) | ||
bc464f4 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Taipan | 9 | 2022-12-14T13:20:27Z | ||
becc442 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Mopsa (v1.0~pre2) | 3 | 2022-12-11T10:05:39Z | ||
f154299 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T11:32:19+01:00 | b58e1bd | |
cb90aa0 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T11:02:07+01:00 | bc464f4 | |
cb0bce9 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T07:29:08+01:00 | 37abc6a | |
af339ed | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T03:46:01+01:00 | becc442 | |
9b51150 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T03:10:10+01:00 | 9ddd07a | |
af750e5 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-29T00:06:44+01:00 | 2ab2acc | |
e50d7ec | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T22:52:39+01:00 | ad7e1e5 | |
fffd343 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T18:11:11+01:00 | 7a03005 | |
ec21e8e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T17:45:01+01:00 | 16725a5 | |
0f1cc88 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T11:26:15+01:00 | 9d00b2c | |
3c55d6e | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2023-01-28T00:46:13+01:00 | eb7d169 | |
9d00b2c | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2 | 6 | 2022-12-10T19:22:21+01:00 | ||
9ddd07a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.2.1-svn-1715bd67dc+ | 6 | 2022-12-11T22:00:23+01:00 | ||
eb7d169 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.1 | 6 | 2022-12-25T13:34:07+01:00 | ||
2ab2acc | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0 | 6 | 2022-12-11T03:59:37+01:00 | ||
7a03005 | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | CPAchecker 2.0.1-svn-a45b42da2f+ | 6 | 2022-12-10T04:13:26+01:00 | ||
37abc6a | Inspect | CHECK( init(main()), LTL(G ! overflow) ) | correctness_witness | Automizer | 9 | 2022-12-13T10:06:46Z | ||
fd6ba0a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | CBMC | 336 | 2022-12-08T08:31:46+01:00 | ||
614d38a | Inspect | CHECK( init(main()), LTL(F end) ) | correctness_witness | Bubaak | 3 | 2022-12-08T14:59:24Z |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_true-termination_true-valid-memsafety.c, e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_true-termination_true-valid-memsafety.c, e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_true-termination_true-valid-memsafety.c, e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
7fe30dc | Inspect | CHECK( init(main()), LTL(G valid-memtrack) ) | correctness_witness | CPAchecker 1.9 | 6 | 2019-11-30T08:52:03+01:00 | ||
e73541b | Inspect | CHECK( init(main()), LTL(G valid-free) ) | correctness_witness | CPAchecker 1.8-svn-35b8bb3bb3+ | 6 | 2019-12-01T09:04:25+01:00 |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_true-termination_true-valid-memsafety.c, e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 1 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_true-termination_true-valid-memsafety.c, e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
77b9acb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | ESBMC 3.1 | 6 | 2017-12-01T16:51 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_true-termination_true-valid-memsafety.c, e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/e573de14d9788c77bce7065ed34a1586a64b72729dbf270f6aaf1ae9cdd54fd7.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |