f8caf38 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T06:43:17Z |
|
d75c12b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:37:08+01:00 |
|
56da5dc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
f1a75a3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
10 |
2023-12-02T17:55:32Z |
|
3529994 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Pinaka |
3 |
2023-12-19T20:43:36 |
|
430a000 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T15:50:31Z |
|
80e2b81 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
10 |
2023-12-02T23:52:31Z |
|
c7629f2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
27 |
2023-12-01T01:12:07Z |
|
8476074 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-20T03:41:14+01:00 |
56da5dc |
e95ee6f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-20T02:32:21+01:00 |
3529994 |
ea28781 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T15:01:47+01:00 |
85316f8 |
2353062 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T04:10:48+01:00 |
b5c0b44 |
f18e34d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-17T06:10:09+01:00 |
4750d89 |
7d2bc75 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T11:47:01+01:00 |
f1a75a3 |
ab678d3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-04T01:19:27+01:00 |
792508d |
6e8827a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T18:31:01+01:00 |
d75c12b |
22407eb |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T10:01:30+01:00 |
f8caf38 |
abd6207 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-03T05:50:35+01:00 |
80e2b81 |
3538c46 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-01T03:45:49+01:00 |
c7629f2 |
f4dc98e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-01T00:00:53+01:00 |
d1b6093 |
b118971 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T11:37:51+01:00 |
7886429 |
7886429 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T07:00:56+01:00 |
|
dd2ce57 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T18:29:44+01:00 |
430a000 |
7321d63 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-29T08:08:02+01:00 |
1e5736b |
792508d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-04T00:17:59+01:00 |
|
4750d89 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.1 |
7 |
2023-12-17T00:04:08+01:00 |
|
b5c0b44 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
7 |
2023-12-18T18:28:23+01:00 |
|
1e5736b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
10 |
2023-11-29T05:43:23Z |
|
d1b6093 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
2LS |
11 |
2023-11-30T22:39:34+01:00 |
|
a887239 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
VERIFUZZ |
32 |
2023-12-01T22:31:59Z |
|
005e49f |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.3 |
70 |
2023-11-30T04:38:07+01:00 |
|
088b352 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
80 |
2023-11-29T00:40:50Z |
|
160e35a |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
36 |
2023-11-30T22:55:57+01:00 |
|
ddb5ed1 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: db678696-3fbb-49c7-8387-3e5a82e5f419
creation_time: '2023-11-29T06:43:23+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_596d964c-7329-4ae2-ad9c-5bc0d0582037/sv-benchmarks/c/termination-restricted-15/Narrowing.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_596d964c-7329-4ae2-ad9c-5bc0d0582037/sv-benchmarks/c/termination-restricted-15/Narrowing.c
: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
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_596d964c-7329-4ae2-ad9c-5bc0d0582037/sv-benchmarks/c/termination-restricted-15/Narrowing.c
file_hash: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
line: 13
column: 0
function: main
value: (((((i <= 2147483647) && (0 <= (2147483646 + range))) && (range <= 20)) && (up == 0)) || (((((up == 1) && (0 <= (2147483646 + range))) && (range <= 20)) && (i <= 2147483646)) && (0 <= i)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T07:47:38+01:00 |
|
4a048f3 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 4ba297b8-b3f2-4989-be70-d6b00f30705d
creation_time: '2023-12-02T18:55:32+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b1441fd8-211b-4ae2-ab66-7e11cf4607a0/sv-benchmarks/c/termination-restricted-15/Narrowing.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_b1441fd8-211b-4ae2-ab66-7e11cf4607a0/sv-benchmarks/c/termination-restricted-15/Narrowing.c
: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
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_b1441fd8-211b-4ae2-ab66-7e11cf4607a0/sv-benchmarks/c/termination-restricted-15/Narrowing.c
file_hash: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
line: 13
column: 0
function: main
value: ((0 <= (2147483646 + range)) && (range <= 20))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T12:00:22+01:00 |
|
8ca1bb6 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 2021dc35-b9b0-49d0-bc19-d19f44d1ce55
creation_time: '2023-12-03T00:52:31+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cf3858ed-ce02-43da-b2fa-7364289c89b2/sv-benchmarks/c/termination-restricted-15/Narrowing.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_cf3858ed-ce02-43da-b2fa-7364289c89b2/sv-benchmarks/c/termination-restricted-15/Narrowing.c
: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
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_cf3858ed-ce02-43da-b2fa-7364289c89b2/sv-benchmarks/c/termination-restricted-15/Narrowing.c
file_hash: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
line: 13
column: 0
function: main
value: ((((i <= 2147483647) && (range <= 20)) || ((i + 2147483648) < 0)) || (range < 20))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T05:42:52+01:00 |
|
f63b020 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 5569be8c-b4c3-44fb-8bc5-067350518d87
creation_time: 2023-12-01T01:12:07Z
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-restricted-15/Narrowing.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-restricted-15/Narrowing.c
input_file_hashes:
../../sv-benchmarks/c/termination-restricted-15/Narrowing.c: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Narrowing.c
file_hash: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
line: 13
column: 11
function: main
value: (20LL - (long long )range) + (long long )up >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-restricted-15/Narrowing.c
file_hash: 65d96571ae692dc892a607d17412b050d92bd8365fc1d6c09a627f6750d6e1ac
line: 13
column: 11
function: main
value: ((((0 <= i && (long long )i + (long long )up >= 0LL) && (20LL + (long
long )i) - (long long )range >= 0LL) && (long long )i - (long long )up >=
0LL) && ((((((((((0 <= up && i <= 20) && range <= 20) && up <= 1) && (19LL
- (long long )i) + (long long )up >= 0LL) && (21LL - (long long )i) - (long
long )up >= 0LL) && (21LL - (long long )range) - (long long )up >= 0LL) &&
(40LL - (long long )i) - (long long )range >= 0LL) && (up == 0 || up == 1))
&& ((((1LL - (long long )i) + (long long )range >= 0LL && (((((((((1 <= range
&& (-1LL + (long long )i) + (long long )range >= 0LL) && (-1LL + (long long
)range) + (long long )up >= 0LL) && (long long )range - (long long )up >=
0LL) || (((16 <= range && (-17LL + (long long )i) + (long long )range >= 0LL)
&& (-16LL + (long long )range) + (long long )up >= 0LL) && (-15LL + (long
long )range) - (long long )up >= 0LL)) || (((16 <= range && (-17LL + (long
long )i) + (long long )range >= 0LL) && (-16LL + (long long )range) + (long
long )up >= 0LL) && (-15LL + (long long )range) - (long long )up >= 0LL))
|| (((((-32768 <= range && 17 <= range) && range <= 32767) && (-18LL + (long
long )i) + (long long )range >= 0LL) && (-17LL + (long long )range) + (long
long )up >= 0LL) && (-16LL + (long long )range) - (long long )up >= 0LL))
|| (((((-32768 <= range && 17 <= range) && range <= 32767) && (-18LL + (long
long )i) + (long long )range >= 0LL) && (-17LL + (long long )range) + (long
long )up >= 0LL) && (-16LL + (long long )range) - (long long )up >= 0LL))
|| (((((-128 <= range && 18 <= range) && range <= 255) && (-19LL + (long long
)i) + (long long )range >= 0LL) && (-18LL + (long long )range) + (long long
)up >= 0LL) && (-17LL + (long long )range) - (long long )up >= 0LL)) || (((((-128
<= range && 18 <= range) && range <= 255) && (-19LL + (long long )i) + (long
long )range >= 0LL) && (-18LL + (long long )range) + (long long )up >= 0LL)
&& (-17LL + (long long )range) - (long long )up >= 0LL))) || ((((((((0 <=
range && 19 <= range) && range <= 127) && (-20LL + (long long )i) + (long
long )range >= 0LL) && (-19LL + (long long )range) + (long long )up >= 0LL)
&& (0LL - (long long )i) + (long long )range >= 0LL) && (-18LL + (long long
)range) - (long long )up >= 0LL) && range != 0) && (range == 19 || range ==
20))) || ((((((((0 <= range && 19 <= range) && range <= 127) && (-20LL + (long
long )i) + (long long )range >= 0LL) && (-19LL + (long long )range) + (long
long )up >= 0LL) && (0LL - (long long )i) + (long long )range >= 0LL) && (-18LL
+ (long long )range) - (long long )up >= 0LL) && range != 0) && (range ==
19 || range == 20)))) || ((((((((-20LL + (long long )i) + (long long )range
>= 0LL && (-20LL + (long long )range) + (long long )up >= 0LL) && (-20LL +
(long long )range) - (long long )up >= 0LL) && (20LL - (long long )range)
- (long long )up >= 0LL) && 0 == up) && 20 == range) && range == 20) && up
== 0))) || (((((((-20LL + (long long )range) + (long long )up >= 0LL && (-20LL
+ (long long )range) - (long long )up >= 0LL) && (20LL - (long long )range)
- (long long )up >= 0LL) && 0 == up) && 20 == range) && range == 20) && up
== 0)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
12 |
2023-12-01T05:32:44+01:00 |
|