69ce698 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T04:24:32Z |
|
c87ba8e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
7e0309d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
7 |
2023-12-02T14:47:35Z |
|
62fbc67 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T20:03:36 |
|
dcdc1dc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T11:28:19Z |
|
48cb4c6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
7 |
2023-12-02T20:08:16Z |
|
651bc7a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
22 |
2023-12-01T02:00:32Z |
|
7dbaa07 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-20T03:45:49+01:00 |
c87ba8e |
6df7725 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-20T02:37:03+01:00 |
62fbc67 |
c12c048 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-19T14:38:28+01:00 |
90d3478 |
4f5609e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-19T03:32:36+01:00 |
1f67f39 |
f45f0a9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-17T06:13:48+01:00 |
d447e34 |
2947d98 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T11:38:29+01:00 |
7e0309d |
088c792 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T02:14:21+01:00 |
52d3688 |
87740aa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T09:58:07+01:00 |
69ce698 |
db3e6dd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T06:07:46+01:00 |
48cb4c6 |
c2612c2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-01T03:50:02+01:00 |
651bc7a |
bd7379f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-01T00:22:44+01:00 |
5634e91 |
ba2ca45 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T11:59:54+01:00 |
7575df7 |
7575df7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T06:55:44+01:00 |
|
60b244b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T18:16:14+01:00 |
dcdc1dc |
d0b98cf |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T08:16:45+01:00 |
fddfb61 |
52d3688 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
5 |
2023-12-03T20:37:24+01:00 |
|
d447e34 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
5 |
2023-12-17T05:34:07+01:00 |
|
1f67f39 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2023-12-18T23:02:30+01:00 |
|
fddfb61 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
7 |
2023-11-29T01:50:28Z |
|
5634e91 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
1690 |
2023-11-30T22:19:24+01:00 |
|
e8ff682 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: e78b0436-0381-46a3-b584-8a6c77e38ed2
creation_time: '2023-11-29T02:50:28+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0d3f8d86-561b-441c-8326-066cf616968f/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0d3f8d86-561b-441c-8326-066cf616968f/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
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_0d3f8d86-561b-441c-8326-066cf616968f/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
file_hash: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
line: 17
column: 0
function: main
value: (x < 2147483648)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0d3f8d86-561b-441c-8326-066cf616968f/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
file_hash: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
line: 19
column: 0
function: main
value: (((x <= 1073741823) && (0 <= x)) && (1 <= y))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T07:49:16+01:00 |
|
7acdbf7 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: a4818fa9-5af5-4ff0-a914-fc11ed3f605d
creation_time: '2023-12-02T15:47:35+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_47fbd138-16a8-4c32-ba5a-bac801f3ba37/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_47fbd138-16a8-4c32-ba5a-bac801f3ba37/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
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_47fbd138-16a8-4c32-ba5a-bac801f3ba37/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
file_hash: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
line: 17
column: 0
function: main
value: (x < 2147483648)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_47fbd138-16a8-4c32-ba5a-bac801f3ba37/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
file_hash: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
line: 19
column: 0
function: main
value: (((x <= 1073741823) && (0 <= x)) && (1 <= y))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T12:08:16+01:00 |
|
0e6dd1e |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 3d33e291-ff62-4d2f-b177-5a5a00ee143a
creation_time: '2023-12-02T21:08:16+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0fae9819-1e3a-4fba-a0f4-f6e6d68e4e13/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0fae9819-1e3a-4fba-a0f4-f6e6d68e4e13/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
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_0fae9819-1e3a-4fba-a0f4-f6e6d68e4e13/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
file_hash: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
line: 17
column: 0
function: main
value: (x <= 2147483647)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0fae9819-1e3a-4fba-a0f4-f6e6d68e4e13/sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
file_hash: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
line: 19
column: 0
function: main
value: (((x <= 1073741823) && (0 <= x)) && (1 <= y))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T05:48:24+01:00 |
|
09c4301 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 2655a35b-61e6-4590-bde2-4866d11c81d9
creation_time: 2023-12-01T02:00:32Z
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-lit/PodelskiRybalchenko-LICS2004-Fig1.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
input_file_hashes:
../../sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
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-lit/PodelskiRybalchenko-LICS2004-Fig1.c
file_hash: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
line: 19
column: 9
function: main
value: x <= 1073741823
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted-lit/PodelskiRybalchenko-LICS2004-Fig1.c
file_hash: 4cf25ea48272ba4463d41281066a1cec5687f4083cfa8522d5a9622c6308689c
line: 19
column: 9
function: main
value: (((x != 0 && (((((((((((((((((((((((((((32769 <= x && (-98305LL + (long
long )x) + (long long )y >= 0LL) && (1073676287LL - (long long )x) + (long
long )y >= 0LL) && (32767LL + (long long )x) - (long long )y >= 0LL) && (1073807359LL
- (long long )x) - (long long )y >= 0LL) && y == 65536) || (((((16385 <= x
&& (-49153LL + (long long )x) + (long long )y >= 0LL) && (1073709055LL - (long
long )x) + (long long )y >= 0LL) && (16383LL + (long long )x) - (long long
)y >= 0LL) && (1073774591LL - (long long )x) - (long long )y >= 0LL) && y
== 32768)) || (((((8193 <= x && (-24577LL + (long long )x) + (long long )y
>= 0LL) && (1073725439LL - (long long )x) + (long long )y >= 0LL) && (8191LL
+ (long long )x) - (long long )y >= 0LL) && (1073758207LL - (long long )x)
- (long long )y >= 0LL) && y == 16384)) || (((((4097 <= x && (-12289LL + (long
long )x) + (long long )y >= 0LL) && (1073733631LL - (long long )x) + (long
long )y >= 0LL) && (4095LL + (long long )x) - (long long )y >= 0LL) && (1073750015LL
- (long long )x) - (long long )y >= 0LL) && y == 8192)) || (((((2049 <= x
&& (-6145LL + (long long )x) + (long long )y >= 0LL) && (1073737727LL - (long
long )x) + (long long )y >= 0LL) && (2047LL + (long long )x) - (long long
)y >= 0LL) && (1073745919LL - (long long )x) - (long long )y >= 0LL) && y
== 4096)) || (((((1025 <= x && (-3073LL + (long long )x) + (long long )y >=
0LL) && (1073739775LL - (long long )x) + (long long )y >= 0LL) && (1023LL
+ (long long )x) - (long long )y >= 0LL) && (1073743871LL - (long long )x)
- (long long )y >= 0LL) && y == 2048)) || (((((513 <= x && (-1537LL + (long
long )x) + (long long )y >= 0LL) && (1073740799LL - (long long )x) + (long
long )y >= 0LL) && (511LL + (long long )x) - (long long )y >= 0LL) && (1073742847LL
- (long long )x) - (long long )y >= 0LL) && y == 1024)) || (((((257 <= x &&
(-769LL + (long long )x) + (long long )y >= 0LL) && (1073741311LL - (long
long )x) + (long long )y >= 0LL) && (255LL + (long long )x) - (long long )y
>= 0LL) && (1073742335LL - (long long )x) - (long long )y >= 0LL) && y ==
512)) || (((((129 <= x && (-385LL + (long long )x) + (long long )y >= 0LL)
&& (1073741567LL - (long long )x) + (long long )y >= 0LL) && (127LL + (long
long )x) - (long long )y >= 0LL) && (1073742079LL - (long long )x) - (long
long )y >= 0LL) && y == 256)) || (((((65 <= x && (-193LL + (long long )x)
+ (long long )y >= 0LL) && (1073741695LL - (long long )x) + (long long )y
>= 0LL) && (63LL + (long long )x) - (long long )y >= 0LL) && (1073741951LL
- (long long )x) - (long long )y >= 0LL) && y == 128)) || (((((((16777217
<= x && 33554432 <= y) && y <= 2147483644) && (-50331649LL + (long long )x)
+ (long long )y >= 0LL) && (1040187391LL - (long long )x) + (long long )y
>= 0LL) && (1073741821LL + (long long )x) - (long long )y >= 0LL) && (3221225467LL
- (long long )x) - (long long )y >= 0LL) && y % 33554432 == 0)) || (((((33
<= x && (-97LL + (long long )x) + (long long )y >= 0LL) && (1073741759LL -
(long long )x) + (long long )y >= 0LL) && (31LL + (long long )x) - (long long
)y >= 0LL) && (1073741887LL - (long long )x) - (long long )y >= 0LL) && y
== 64)) || (((((8388609 <= x && (-25165825LL + (long long )x) + (long long
)y >= 0LL) && (1056964607LL - (long long )x) + (long long )y >= 0LL) && (8388607LL
+ (long long )x) - (long long )y >= 0LL) && (1090519039LL - (long long )x)
- (long long )y >= 0LL) && y == 16777216)) || (((((17 <= x && (-49LL + (long
long )x) + (long long )y >= 0LL) && (1073741791LL - (long long )x) + (long
long )y >= 0LL) && (15LL + (long long )x) - (long long )y >= 0LL) && (1073741855LL
- (long long )x) - (long long )y >= 0LL) && y == 32)) || (((((4194305 <= x
&& (-12582913LL + (long long )x) + (long long )y >= 0LL) && (1065353215LL
- (long long )x) + (long long )y >= 0LL) && (4194303LL + (long long )x) -
(long long )y >= 0LL) && (1082130431LL - (long long )x) - (long long )y >=
0LL) && y == 8388608)) || (((((9 <= x && (-25LL + (long long )x) + (long long
)y >= 0LL) && (1073741807LL - (long long )x) + (long long )y >= 0LL) && (7LL
+ (long long )x) - (long long )y >= 0LL) && (1073741839LL - (long long )x)
- (long long )y >= 0LL) && y == 16)) || (((((2097153 <= x && (-6291457LL +
(long long )x) + (long long )y >= 0LL) && (1069547519LL - (long long )x) +
(long long )y >= 0LL) && (2097151LL + (long long )x) - (long long )y >= 0LL)
&& (1077936127LL - (long long )x) - (long long )y >= 0LL) && y == 4194304))
|| (((((5 <= x && (-13LL + (long long )x) + (long long )y >= 0LL) && (1073741815LL
- (long long )x) + (long long )y >= 0LL) && (3LL + (long long )x) - (long
long )y >= 0LL) && (1073741831LL - (long long )x) - (long long )y >= 0LL)
&& y == 8)) || (((((1048577 <= x && (-3145729LL + (long long )x) + (long long
)y >= 0LL) && (1071644671LL - (long long )x) + (long long )y >= 0LL) && (1048575LL
+ (long long )x) - (long long )y >= 0LL) && (1075838975LL - (long long )x)
- (long long )y >= 0LL) && y == 2097152)) || (((((3 <= x && (-7LL + (long
long )x) + (long long )y >= 0LL) && (1073741819LL - (long long )x) + (long
long )y >= 0LL) && (1LL + (long long )x) - (long long )y >= 0LL) && (1073741827LL
- (long long )x) - (long long )y >= 0LL) && y == 4)) || (((((524289 <= x &&
(-1572865LL + (long long )x) + (long long )y >= 0LL) && (1072693247LL - (long
long )x) + (long long )y >= 0LL) && (524287LL + (long long )x) - (long long
)y >= 0LL) && (1074790399LL - (long long )x) - (long long )y >= 0LL) && y
== 1048576)) || (((((2 <= x && (-4LL + (long long )x) + (long long )y >= 0LL)
&& (1073741821LL - (long long )x) + (long long )y >= 0LL) && (1073741825LL
- (long long )x) - (long long )y >= 0LL) && (long long )x - (long long )y
>= 0LL) && y == 2)) || (((((262145 <= x && (-786433LL + (long long )x) + (long
long )y >= 0LL) && (1073217535LL - (long long )x) + (long long )y >= 0LL)
&& (262143LL + (long long )x) - (long long )y >= 0LL) && (1074266111LL - (long
long )x) - (long long )y >= 0LL) && y == 524288))) || ((((((0 <= x && (-1LL
+ (long long )x) + (long long )y >= 0LL) && (1073741822LL - (long long )x)
+ (long long )y >= 0LL) && (1LL + (long long )x) - (long long )y >= 0LL) &&
(1073741824LL - (long long )x) - (long long )y >= 0LL) && 1 == y) && y ==
1)) || ((((((131073 <= x && (-393217LL + (long long )x) + (long long )y >=
0LL) && (1073479679LL - (long long )x) + (long long )y >= 0LL) && (131071LL
+ (long long )x) - (long long )y >= 0LL) && (1074003967LL - (long long )x)
- (long long )y >= 0LL) && y == 262144) && x != 0)) || ((((((65537 <= x &&
(-196609LL + (long long )x) + (long long )y >= 0LL) && (1073610751LL - (long
long )x) + (long long )y >= 0LL) && (65535LL + (long long )x) - (long long
)y >= 0LL) && (1073872895LL - (long long )x) - (long long )y >= 0LL) && y
== 131072) && x != 0)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
16 |
2023-12-01T04:10:06+01:00 |
|