e6cc1ec |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.1 |
4 |
2023-12-17T03:55:29+01:00 |
|
86a9aa0 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.0 |
4 |
2023-12-19T13:11:22+01:00 |
|
2c90745 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
4 |
2023-12-19T00:55:18+01:00 |
|
afecc71 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:43:25+01:00 |
|
edd819b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T08:07:35Z |
|
e6173a7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
14 |
2023-12-02T13:21:32Z |
|
1e24f10 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T14:37:52Z |
|
82cf9f7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
25 |
2023-12-01T01:41:52Z |
|
7c75e2e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T15:33:07+01:00 |
86a9aa0 |
04ce3bd |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-19T05:28:28+01:00 |
2c90745 |
51cdab5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-17T06:39:02+01:00 |
e6cc1ec |
bd57058 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T11:24:46+01:00 |
e6173a7 |
073f0b6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T01:35:15+01:00 |
31b9182 |
337cc48 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T18:29:42+01:00 |
afecc71 |
401ae63 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T09:54:54+01:00 |
edd819b |
173a6b4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-01T03:44:00+01:00 |
82cf9f7 |
3c01202 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T12:25:28+01:00 |
55452c9 |
55452c9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-30T06:55:30+01:00 |
|
e5c2c3b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-29T18:12:12+01:00 |
1e24f10 |
c202485 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-29T07:53:00+01:00 |
e6b4b43 |
31b9182 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
6 |
2023-12-03T23:47:52+01:00 |
|
e6b4b43 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
14 |
2023-11-29T02:46:36Z |
|
4451d97 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 6f7ea996-9f49-4d6f-ad44-bb93fb71b8d2
creation_time: '2023-12-02T14:21: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_d873cdd1-4f6d-410e-a991-438aaeee1669/sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d873cdd1-4f6d-410e-a991-438aaeee1669/sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
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_d873cdd1-4f6d-410e-a991-438aaeee1669/sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 550
column: 0
function: insertionSort
value: (((((1 <= i) && (array_size <= 2147483647)) && (j <= 2147483648)) && (i <= 2147483647)) || ((i == 1) && (array_size <= 2147483647)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_d873cdd1-4f6d-410e-a991-438aaeee1669/sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 553
column: 0
function: insertionSort
value: ((((1 <= i) && (i <= 2147483646)) && (j <= 2147483647)) && (array_size <= 2147483647))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T12:01:09+01:00 |
|
4f51add |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 5580360d-3c9a-4ed2-93ab-ca0736bb8e53
creation_time: '2023-11-29T03:46:36+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a3d2201-3bb4-4127-a507-b60e1b51ced2/sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a3d2201-3bb4-4127-a507-b60e1b51ced2/sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
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_0a3d2201-3bb4-4127-a507-b60e1b51ced2/sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 550
column: 0
function: insertionSort
value: ((((array_size <= 2147483647) && (i == 1)) && (array_size <= 2147483647)) || (((((1 <= i) && (array_size <= 2147483647)) && (array_size <= 2147483647)) && (j <= 2147483648)) && (i <= 2147483647)))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_0a3d2201-3bb4-4127-a507-b60e1b51ced2/sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 553
column: 0
function: insertionSort
value: (((((1 <= i) && (array_size <= 2147483647)) && (i <= 2147483646)) && (array_size <= 2147483647)) && (j <= 2147483648))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T07:43:32+01:00 |
|
c7fc589 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: a873eb4f-bf90-48cb-bd22-3afc9d69787b
creation_time: 2023-12-01T01:41:52Z
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/insertionsort-alloca-2.i'''
task:
input_files:
- ../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
input_file_hashes:
../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
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/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 550
column: 8
function: insertionSort
value: array_size != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 550
column: 8
function: insertionSort
value: (1 <= i && ((((((((((0 <= j && 2 <= array_size) && i <= 2147483646) &&
j <= 2147483646) && (-3LL + (long long )array_size) + (long long )i >= 0LL)
&& (-2LL + (long long )array_size) + (long long )j >= 0LL) && (-1LL + (long
long )i) + (long long )j >= 0LL) && (-1LL + (long long )array_size) - (long
long )i >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL)
&& (long long )i - (long long )j >= 0LL) || ((((((1 <= array_size && (-2LL
+ (long long )array_size) + (long long )i >= 0LL) && (2147483647LL + (long
long )array_size) + (long long )j >= 0LL) && (2147483647LL + (long long )i)
+ (long long )j >= 0LL) && (2147483646LL + (long long )array_size) - (long
long )j >= 0LL) && (2147483646LL + (long long )i) - (long long )j >= 0LL)
&& (long long )array_size - (long long )i >= 0LL))) || ((((((((((((((((((1
<= array_size && (2147483647LL + (long long )array_size) + (long long )i >=
0LL) && (2147483647LL + (long long )array_size) + (long long )j >= 0LL) &&
(2147483647LL + (long long )array_size) + (long long )index >= 0LL) && (4294967296LL
+ (long long )i) + (long long )j >= 0LL) && (4294967296LL + (long long )i)
+ (long long )index >= 0LL) && (4294967296LL + (long long )index) + (long
long )j >= 0LL) && (4294967295LL - (long long )i) + (long long )j >= 0LL)
&& (4294967295LL - (long long )i) + (long long )index >= 0LL) && (4294967295LL
- (long long )index) + (long long )j >= 0LL) && (2147483646LL + (long long
)array_size) - (long long )i >= 0LL) && (2147483646LL + (long long )array_size)
- (long long )j >= 0LL) && (2147483646LL + (long long )array_size) - (long
long )index >= 0LL) && (4294967295LL + (long long )i) - (long long )j >= 0LL)
&& (4294967295LL + (long long )i) - (long long )index >= 0LL) && (4294967295LL
+ (long long )index) - (long long )j >= 0LL) && (4294967294LL - (long long
)i) - (long long )j >= 0LL) && (4294967294LL - (long long )i) - (long long
)index >= 0LL) && (4294967294LL - (long long )index) - (long long )j >= 0LL)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 553
column: 12
function: insertionSort
value: 1 <= i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 553
column: 12
function: insertionSort
value: 2 <= array_size
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 553
column: 12
function: insertionSort
value: i <= 2147483646
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 553
column: 12
function: insertionSort
value: (-1LL + (long long )array_size) - (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 553
column: 12
function: insertionSort
value: array_size != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/insertionsort-alloca-2.i
file_hash: de7da20d4eaaa585438f85709f7fd309a77ec10ab7307dad72c7fb2392cc347c
line: 553
column: 12
function: insertionSort
value: (((((((i != 0 && (((index <= 2147483646 && ((j != -1 && ((((j != -2 &&
((((j != -3 && ((((j != -4 && ((((j != -5 && ((((j != -6 && ((((j != -7 &&
((((j != -8 && ((((j != -9 && ((((((((j <= 2147483636 && (10LL - (long long
)i) + (long long )j >= 0LL) && (-11LL + (long long )array_size) - (long long
)j >= 0LL) && (-10LL + (long long )i) - (long long )j >= 0LL) && j != -10)
&& (((((1 <= j && (-23LL + (long long )array_size) + (long long )i >= 0LL)
&& (-13LL + (long long )array_size) + (long long )j >= 0LL) && (-12LL + (long
long )i) + (long long )j >= 0LL) && j != 0) || (((0 <= j && (-21LL + (long
long )array_size) + (long long )i >= 0LL) && (-11LL + (long long )array_size)
+ (long long )j >= 0LL) && (-10LL + (long long )i) + (long long )j >= 0LL)))
|| ((((((((1 <= j && j <= 2147483637) && (-21LL + (long long )array_size)
+ (long long )i >= 0LL) && (-12LL + (long long )array_size) + (long long )j
>= 0LL) && (-11LL + (long long )i) + (long long )j >= 0LL) && (9LL - (long
long )i) + (long long )j >= 0LL) && (-10LL + (long long )array_size) - (long
long )j >= 0LL) && (-9LL + (long long )i) - (long long )j >= 0LL) && j !=
0)) || ((((((((1 <= j && j <= 2147483637) && (-21LL + (long long )array_size)
+ (long long )i >= 0LL) && (-12LL + (long long )array_size) + (long long )j
>= 0LL) && (-11LL + (long long )i) + (long long )j >= 0LL) && (9LL - (long
long )i) + (long long )j >= 0LL) && (-10LL + (long long )array_size) - (long
long )j >= 0LL) && (-9LL + (long long )i) - (long long )j >= 0LL) && j !=
0)) || (((((((0 <= j && j <= 2147483637) && (-19LL + (long long )array_size)
+ (long long )i >= 0LL) && (-10LL + (long long )array_size) + (long long )j
>= 0LL) && (-9LL + (long long )i) + (long long )j >= 0LL) && (9LL - (long
long )i) + (long long )j >= 0LL) && (-10LL + (long long )array_size) - (long
long )j >= 0LL) && (-9LL + (long long )i) - (long long )j >= 0LL))) || ((((((((1
<= j && j <= 2147483638) && (-19LL + (long long )array_size) + (long long
)i >= 0LL) && (-11LL + (long long )array_size) + (long long )j >= 0LL) &&
(-10LL + (long long )i) + (long long )j >= 0LL) && (8LL - (long long )i) +
(long long )j >= 0LL) && (-9LL + (long long )array_size) - (long long )j >=
0LL) && (-8LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((1
<= j && j <= 2147483638) && (-19LL + (long long )array_size) + (long long
)i >= 0LL) && (-11LL + (long long )array_size) + (long long )j >= 0LL) &&
(-10LL + (long long )i) + (long long )j >= 0LL) && (8LL - (long long )i) +
(long long )j >= 0LL) && (-9LL + (long long )array_size) - (long long )j >=
0LL) && (-8LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || (((((((0
<= j && j <= 2147483638) && (-17LL + (long long )array_size) + (long long
)i >= 0LL) && (-9LL + (long long )array_size) + (long long )j >= 0LL) && (-8LL
+ (long long )i) + (long long )j >= 0LL) && (8LL - (long long )i) + (long
long )j >= 0LL) && (-9LL + (long long )array_size) - (long long )j >= 0LL)
&& (-8LL + (long long )i) - (long long )j >= 0LL))) || ((((((((1 <= j && j
<= 2147483639) && (-17LL + (long long )array_size) + (long long )i >= 0LL)
&& (-10LL + (long long )array_size) + (long long )j >= 0LL) && (-9LL + (long
long )i) + (long long )j >= 0LL) && (7LL - (long long )i) + (long long )j
>= 0LL) && (-8LL + (long long )array_size) - (long long )j >= 0LL) && (-7LL
+ (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((1 <= j &&
j <= 2147483639) && (-17LL + (long long )array_size) + (long long )i >= 0LL)
&& (-10LL + (long long )array_size) + (long long )j >= 0LL) && (-9LL + (long
long )i) + (long long )j >= 0LL) && (7LL - (long long )i) + (long long )j
>= 0LL) && (-8LL + (long long )array_size) - (long long )j >= 0LL) && (-7LL
+ (long long )i) - (long long )j >= 0LL) && j != 0)) || (((((((0 <= j && j
<= 2147483639) && (-15LL + (long long )array_size) + (long long )i >= 0LL)
&& (-8LL + (long long )array_size) + (long long )j >= 0LL) && (-7LL + (long
long )i) + (long long )j >= 0LL) && (7LL - (long long )i) + (long long )j
>= 0LL) && (-8LL + (long long )array_size) - (long long )j >= 0LL) && (-7LL
+ (long long )i) - (long long )j >= 0LL))) || ((((((((1 <= j && j <= 2147483640)
&& (-15LL + (long long )array_size) + (long long )i >= 0LL) && (-9LL + (long
long )array_size) + (long long )j >= 0LL) && (-8LL + (long long )i) + (long
long )j >= 0LL) && (6LL - (long long )i) + (long long )j >= 0LL) && (-7LL
+ (long long )array_size) - (long long )j >= 0LL) && (-6LL + (long long )i)
- (long long )j >= 0LL) && j != 0)) || ((((((((1 <= j && j <= 2147483640)
&& (-15LL + (long long )array_size) + (long long )i >= 0LL) && (-9LL + (long
long )array_size) + (long long )j >= 0LL) && (-8LL + (long long )i) + (long
long )j >= 0LL) && (6LL - (long long )i) + (long long )j >= 0LL) && (-7LL
+ (long long )array_size) - (long long )j >= 0LL) && (-6LL + (long long )i)
- (long long )j >= 0LL) && j != 0)) || (((((((0 <= j && j <= 2147483640) &&
(-13LL + (long long )array_size) + (long long )i >= 0LL) && (-7LL + (long
long )array_size) + (long long )j >= 0LL) && (-6LL + (long long )i) + (long
long )j >= 0LL) && (6LL - (long long )i) + (long long )j >= 0LL) && (-7LL
+ (long long )array_size) - (long long )j >= 0LL) && (-6LL + (long long )i)
- (long long )j >= 0LL))) || ((((((((1 <= j && j <= 2147483641) && (-13LL
+ (long long )array_size) + (long long )i >= 0LL) && (-8LL + (long long )array_size)
+ (long long )j >= 0LL) && (-7LL + (long long )i) + (long long )j >= 0LL)
&& (5LL - (long long )i) + (long long )j >= 0LL) && (-6LL + (long long )array_size)
- (long long )j >= 0LL) && (-5LL + (long long )i) - (long long )j >= 0LL)
&& j != 0)) || ((((((((1 <= j && j <= 2147483641) && (-13LL + (long long )array_size)
+ (long long )i >= 0LL) && (-8LL + (long long )array_size) + (long long )j
>= 0LL) && (-7LL + (long long )i) + (long long )j >= 0LL) && (5LL - (long
long )i) + (long long )j >= 0LL) && (-6LL + (long long )array_size) - (long
long )j >= 0LL) && (-5LL + (long long )i) - (long long )j >= 0LL) && j !=
0)) || (((((((0 <= j && j <= 2147483641) && (-11LL + (long long )array_size)
+ (long long )i >= 0LL) && (-6LL + (long long )array_size) + (long long )j
>= 0LL) && (-5LL + (long long )i) + (long long )j >= 0LL) && (5LL - (long
long )i) + (long long )j >= 0LL) && (-6LL + (long long )array_size) - (long
long )j >= 0LL) && (-5LL + (long long )i) - (long long )j >= 0LL))) || ((((((((1
<= j && j <= 2147483642) && (-11LL + (long long )array_size) + (long long
)i >= 0LL) && (-7LL + (long long )array_size) + (long long )j >= 0LL) && (-6LL
+ (long long )i) + (long long )j >= 0LL) && (4LL - (long long )i) + (long
long )j >= 0LL) && (-5LL + (long long )array_size) - (long long )j >= 0LL)
&& (-4LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((1
<= j && j <= 2147483642) && (-11LL + (long long )array_size) + (long long
)i >= 0LL) && (-7LL + (long long )array_size) + (long long )j >= 0LL) && (-6LL
+ (long long )i) + (long long )j >= 0LL) && (4LL - (long long )i) + (long
long )j >= 0LL) && (-5LL + (long long )array_size) - (long long )j >= 0LL)
&& (-4LL + (long long )i) - (long long )j >= 0LL) && j != 0)) || (((((((0
<= j && j <= 2147483642) && (-9LL + (long long )array_size) + (long long )i
>= 0LL) && (-5LL + (long long )array_size) + (long long )j >= 0LL) && (-4LL
+ (long long )i) + (long long )j >= 0LL) && (4LL - (long long )i) + (long
long )j >= 0LL) && (-5LL + (long long )array_size) - (long long )j >= 0LL)
&& (-4LL + (long long )i) - (long long )j >= 0LL))) || ((((((((1 <= j && j
<= 2147483643) && (-9LL + (long long )array_size) + (long long )i >= 0LL)
&& (-6LL + (long long )array_size) + (long long )j >= 0LL) && (-5LL + (long
long )i) + (long long )j >= 0LL) && (3LL - (long long )i) + (long long )j
>= 0LL) && (-4LL + (long long )array_size) - (long long )j >= 0LL) && (-3LL
+ (long long )i) - (long long )j >= 0LL) && j != 0)) || ((((((((1 <= j &&
j <= 2147483643) && (-9LL + (long long )array_size) + (long long )i >= 0LL)
&& (-6LL + (long long )array_size) + (long long )j >= 0LL) && (-5LL + (long
long )i) + (long long )j >= 0LL) && (3LL - (long long )i) + (long long )j
>= 0LL) && (-4LL + (long long )array_size) - (long long )j >= 0LL) && (-3LL
+ (long long )i) - (long long )j >= 0LL) && j != 0)) || (((((((0 <= j && j
<= 2147483643) && (-7LL + (long long )array_size) + (long long )i >= 0LL)
&& (-4LL + (long long )array_size) + (long long )j >= 0LL) && (-3LL + (long
long )i) + (long long )j >= 0LL) && (3LL - (long long )i) + (long long )j
>= 0LL) && (-4LL + (long long )array_size) - (long long )j >= 0LL) && (-3LL
+ (long long )i) - (long long )j >= 0LL))) || ((((((((1 <= j && j <= 2147483644)
&& (-7LL + (long long )array_size) + (long long )i >= 0LL) && (-5LL + (long
long )array_size) + (long long )j >= 0LL) && (-4LL + (long long )i) + (long
long )j >= 0LL) && (2LL - (long long )i) + (long long )j >= 0LL) && (-3LL
+ (long long )array_size) - (long long )j >= 0LL) && (-2LL + (long long )i)
- (long long )j >= 0LL) && j != 0)) || ((((((((1 <= j && j <= 2147483644)
&& (-7LL + (long long )array_size) + (long long )i >= 0LL) && (-5LL + (long
long )array_size) + (long long )j >= 0LL) && (-4LL + (long long )i) + (long
long )j >= 0LL) && (2LL - (long long )i) + (long long )j >= 0LL) && (-3LL
+ (long long )array_size) - (long long )j >= 0LL) && (-2LL + (long long )i)
- (long long )j >= 0LL) && j != 0)) || (((((((0 <= j && j <= 2147483644) &&
(-5LL + (long long )array_size) + (long long )i >= 0LL) && (-3LL + (long long
)array_size) + (long long )j >= 0LL) && (-2LL + (long long )i) + (long long
)j >= 0LL) && (2LL - (long long )i) + (long long )j >= 0LL) && (-3LL + (long
long )array_size) - (long long )j >= 0LL) && (-2LL + (long long )i) - (long
long )j >= 0LL))) || ((((((((1 <= j && j <= 2147483645) && (-5LL + (long long
)array_size) + (long long )i >= 0LL) && (-4LL + (long long )array_size) +
(long long )j >= 0LL) && (-3LL + (long long )i) + (long long )j >= 0LL) &&
(1LL - (long long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size)
- (long long )j >= 0LL) && (-1LL + (long long )i) - (long long )j >= 0LL)
&& j != 0)) || ((((((((1 <= j && j <= 2147483645) && (-5LL + (long long )array_size)
+ (long long )i >= 0LL) && (-4LL + (long long )array_size) + (long long )j
>= 0LL) && (-3LL + (long long )i) + (long long )j >= 0LL) && (1LL - (long
long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size) - (long
long )j >= 0LL) && (-1LL + (long long )i) - (long long )j >= 0LL) && j !=
0)) || (((((((0 <= j && j <= 2147483645) && (-3LL + (long long )array_size)
+ (long long )i >= 0LL) && (-2LL + (long long )array_size) + (long long )j
>= 0LL) && (-1LL + (long long )i) + (long long )j >= 0LL) && (1LL - (long
long )i) + (long long )j >= 0LL) && (-2LL + (long long )array_size) - (long
long )j >= 0LL) && (-1LL + (long long )i) - (long long )j >= 0LL))) || (((((((((1
<= j && j <= 2147483646) && (-3LL + (long long )array_size) + (long long )i
>= 0LL) && (-3LL + (long long )array_size) + (long long )j >= 0LL) && (-2LL
+ (long long )i) + (long long )j >= 0LL) && (0LL - (long long )i) + (long
long )j >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL)
&& (long long )i - (long long )j >= 0LL) && i == j) && j != 0))) || (((((((((1
<= j && j <= 2147483646) && (-3LL + (long long )array_size) + (long long )i
>= 0LL) && (-3LL + (long long )array_size) + (long long )j >= 0LL) && (-2LL
+ (long long )i) + (long long )j >= 0LL) && (0LL - (long long )i) + (long
long )j >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL)
&& (long long )i - (long long )j >= 0LL) && i == j) && j != 0)) || (((((((((1
<= j && j <= 2147483646) && (-3LL + (long long )array_size) + (long long )i
>= 0LL) && (-3LL + (long long )array_size) + (long long )j >= 0LL) && (-2LL
+ (long long )i) + (long long )j >= 0LL) && (0LL - (long long )i) + (long
long )j >= 0LL) && (-1LL + (long long )array_size) - (long long )j >= 0LL)
&& (long long )i - (long long )j >= 0LL) && i == j) && j != 0))) || ((((((((((((((((((((1
<= j && j <= 2147483634) && index <= 2147483646) && (-27LL + (long long )array_size)
+ (long long )i >= 0LL) && (-15LL + (long long )array_size) + (long long )j
>= 0LL) && (-14LL + (long long )i) + (long long )j >= 0LL) && (-13LL + (long
long )array_size) - (long long )j >= 0LL) && (-12LL + (long long )i) - (long
long )j >= 0LL) && j != -12) && j != -11) && j != -10) && j != -9) && j !=
-8) && j != -7) && j != -6) && j != -5) && j != -4) && j != -3) && j != -2)
&& j != -1) && j != 0)) || ((((((-3LL + (long long )array_size) + (long long
)i >= 0LL && (2147483646LL + (long long )array_size) + (long long )j >= 0LL)
&& (2147483647LL + (long long )i) + (long long )j >= 0LL) && (2147483645LL
+ (long long )array_size) - (long long )j >= 0LL) && (2147483646LL + (long
long )i) - (long long )j >= 0LL) && i != 0)) || ((((((((((((((((((((1 <= j
&& j <= 2147483634) && index <= 2147483646) && (-27LL + (long long )array_size)
+ (long long )i >= 0LL) && (-15LL + (long long )array_size) + (long long )j
>= 0LL) && (-14LL + (long long )i) + (long long )j >= 0LL) && (-13LL + (long
long )array_size) - (long long )j >= 0LL) && (-12LL + (long long )i) - (long
long )j >= 0LL) && j != -12) && j != -11) && j != -10) && j != -9) && j !=
-8) && j != -7) && j != -6) && j != -5) && j != -4) && j != -3) && j != -2)
&& j != -1) && j != 0)) || (((((((((((((((((((0 <= j && j <= 2147483634) &&
index <= 2147483646) && (-25LL + (long long )array_size) + (long long )i >=
0LL) && (-13LL + (long long )array_size) + (long long )j >= 0LL) && (-12LL
+ (long long )i) + (long long )j >= 0LL) && (-13LL + (long long )array_size)
- (long long )j >= 0LL) && (-12LL + (long long )i) - (long long )j >= 0LL)
&& j != -12) && j != -11) && j != -10) && j != -9) && j != -8) && j != -7)
&& j != -6) && j != -5) && j != -4) && j != -3) && j != -2) && j != -1)) ||
(((((((((((((((((((((1 <= j && j <= 2147483635) && index <= 2147483646) &&
(-25LL + (long long )array_size) + (long long )i >= 0LL) && (-14LL + (long
long )array_size) + (long long )j >= 0LL) && (-13LL + (long long )i) + (long
long )j >= 0LL) && (11LL - (long long )i) + (long long )j >= 0LL) && (-12LL
+ (long long )array_size) - (long long )j >= 0LL) && (-11LL + (long long )i)
- (long long )j >= 0LL) && i != 0) && j != -11) && j != -10) && j != -9) &&
j != -8) && j != -7) && j != -6) && j != -5) && j != -4) && j != -3) && j
!= -2) && j != -1) && j != 0)) || (((((((((((((((((((((1 <= j && j <= 2147483635)
&& index <= 2147483646) && (-25LL + (long long )array_size) + (long long )i
>= 0LL) && (-14LL + (long long )array_size) + (long long )j >= 0LL) && (-13LL
+ (long long )i) + (long long )j >= 0LL) && (11LL - (long long )i) + (long
long )j >= 0LL) && (-12LL + (long long )array_size) - (long long )j >= 0LL)
&& (-11LL + (long long )i) - (long long )j >= 0LL) && i != 0) && j != -11)
&& j != -10) && j != -9) && j != -8) && j != -7) && j != -6) && j != -5) &&
j != -4) && j != -3) && j != -2) && j != -1) && j != 0)) || ((((((((((((((((((((0
<= j && j <= 2147483635) && index <= 2147483646) && (-23LL + (long long )array_size)
+ (long long )i >= 0LL) && (-12LL + (long long )array_size) + (long long )j
>= 0LL) && (-11LL + (long long )i) + (long long )j >= 0LL) && (11LL - (long
long )i) + (long long )j >= 0LL) && (-12LL + (long long )array_size) - (long
long )j >= 0LL) && (-11LL + (long long )i) - (long long )j >= 0LL) && i !=
0) && j != -11) && j != -10) && j != -9) && j != -8) && j != -7) && j != -6)
&& j != -5) && j != -4) && j != -3) && j != -2) && j != -1)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
34 |
2023-12-01T04:36:09+01:00 |
|