a263dd6 |
Inspect |
|
valid-memsafety |
correctness_witness |
DIVINE 4 |
2 |
2023-12-18T10:33:18+01:00 |
|
cc72a4b |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T01:29:20Z |
|
941fd1e |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-29T20:47:42Z |
|
d906e7e |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-11-30T05:16:07+01:00 |
|
5d86603 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
7 |
2023-12-03T20:18:09+01:00 |
|
bea2dd5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 2.0.1-svn-38892M |
9 |
2023-12-18T01:51:50+01:00 |
|
d48122a |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T09:50:57Z |
|
4420263 |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T08:41:58Z |
|
24edb3c |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:40:29Z |
|
ec13c5a |
Inspect |
|
CHECK( init(main()), LTL(G valid-free|valid-deref|valid-memtrack) ) |
correctness_witness |
ESBMC 7.4.0 incr |
3 |
2023-12-01T10:42:57Z |
|
1246b90 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Taipan |
12 |
2023-12-02T11:22:28Z |
|
7605899 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
PredatorHP |
4 |
2023-11-30T08:29:11Z |
|
fd576f7 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T08:50:30Z |
|
fa2ad5a |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CBMC |
3415 |
2023-12-17T17:52:43+01:00 |
|
8df6726 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) )
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
Automizer |
12 |
2023-11-29T02:01:25Z |
|
d51154f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
sv-comp-24 |
4 |
2023-12-03T17:39:11+01:00 |
|
622f7e3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T06:24:20Z |
|
36177d6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
b6b768d |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
12 |
2023-12-02T16:51:07Z |
|
f6c37d7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-12-17T02:51:46Z |
|
f8eb7ad |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Symbiotic |
3 |
2023-11-30T00:59:50Z |
|
ae6b2f3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Mopsa (v1.0~pre2) |
3 |
2023-11-29T12:40:14Z |
|
3bf2c05 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Goblint (tags/svcomp24-0-gc2e9465a7) |
72 |
2023-12-01T01:51:10Z |
|
a40e177 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
ESBMC 7.4.0 kind |
3 |
2023-12-01T03:31:51Z |
|
bf18413 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
1294 |
2023-12-19T05:22:30+01:00 |
d3a3df3 |
d4367e7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-17T06:15:37+01:00 |
f6c37d7 |
ff7fa6e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-05T14:21:22+01:00 |
4e46049 |
b40417f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T16:28:09+01:00 |
4427bd1 |
ed23867 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-04T11:43:17+01:00 |
b6b768d |
7f8f7be |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T18:55:57+01:00 |
d51154f |
c0eb8d5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-03T09:54:06+01:00 |
622f7e3 |
44b80ae |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T22:46:46+01:00 |
3629efc |
e83c5ba |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T18:07:33+01:00 |
a40e177 |
8849c86 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-01T03:46:18+01:00 |
3bf2c05 |
079f6d8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T06:57:46+01:00 |
|
04ae217 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-30T02:27:48+01:00 |
f8eb7ad |
ba35f82 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T18:28:25+01:00 |
ae6b2f3 |
11a0e33 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-11-29T08:10:09+01:00 |
ccffa3e |
783abee |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
8 |
2023-12-03T23:01:53+01:00 |
|
d3a3df3 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
8 |
2023-12-18T17:40:33+01:00 |
|
3fdb8b4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CBMC |
3375 |
2023-12-17T15:54:52+01:00 |
|
4e46049 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-05T10:10:42Z |
|
4427bd1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-04T08:35:32Z |
|
3629efc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Bubaak |
3 |
2023-12-01T19:36:00Z |
|
ccffa3e |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
13 |
2023-11-29T04:52:42Z |
|
6798c52 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 492349fd-0584-4332-b3db-ebde8dcf2fa3
creation_time: '2023-12-02T17:51:07+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_056cb57c-1537-4645-8f99-59b8e56d683f/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_056cb57c-1537-4645-8f99-59b8e56d683f/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 32bit
language: C
content: [
] |
correctness_witness |
CPAchecker 2.3 |
9 |
2023-12-04T11:54:53+01:00 |
|
70de404 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 2252b35d-91d9-4749-abea-221eb32783e9
creation_time: '2023-11-29T05:52:42+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a0c7eb3d-12e3-4136-a022-f1eee3367cc7/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a0c7eb3d-12e3-4136-a022-f1eee3367cc7/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
specification: |+
CHECK( init(main()), LTL(G ! overflow) )
data_model: 32bit
language: C
content:
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a0c7eb3d-12e3-4136-a022-f1eee3367cc7/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 22
column: 0
function: main
value: ((((2 < i) || (i == 0)) || (i == 1)) || (2 == i))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a0c7eb3d-12e3-4136-a022-f1eee3367cc7/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 25
column: 0
function: main
value: (0 < (2147483649 + i))
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_a0c7eb3d-12e3-4136-a022-f1eee3367cc7/sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 14
column: 0
function: foo
value: (((((((((i == 0) && (size == 0)) && (i == 0)) || ((((i <= 99) && (i == 0)) && (3 <= i)) && (i == size))) || (((2 == i) && (1 <= i)) && (i == size))) || (((2 == size) && (2 == i)) && (i == 0))) || (((i == 1) && (i == 1)) && (size == 1))) || (((i == 1) && (i == 0)) && (size == 1))) || ((((size <= 99) && (3 <= i)) && (1 <= i)) && (i == size)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
10 |
2023-11-29T07:50:17+01:00 |
|
d7fd7cf |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: d135fab6-596f-412c-8f74-536a0ae8ab90
creation_time: 2023-12-01T01:51:10Z
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''
''32bit'' ''../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c'''
task:
input_files:
- ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
input_file_hashes:
../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
data_model: ILP32
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 14
column: 8
function: foo
value: n <= 99
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 14
column: 8
function: foo
value: size <= 99
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 14
column: 8
function: foo
value: (0LL - (long long )n) + (long long )size >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 14
column: 8
function: foo
value: (198LL - (long long )n) - (long long )size >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 14
column: 8
function: foo
value: (long long )n - (long long )size >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 14
column: 8
function: foo
value: (((n == size && size != 0) && (((((((((((((((8 <= n && ((((((((((((12
<= i && (87LL + (long long )i) - (long long )n >= 0LL) && (87LL + (long long
)i) - (long long )size >= 0LL) && (((((((((13 <= size && i <= 98) && (-26LL
+ (long long )n) + (long long )size >= 0LL) && (-25LL + (long long )i) + (long
long )n >= 0LL) && (-25LL + (long long )i) + (long long )size >= 0LL) && (-1LL
- (long long )i) + (long long )n >= 0LL) && (-1LL - (long long )i) + (long
long )size >= 0LL) && (197LL - (long long )i) - (long long )n >= 0LL) && (197LL
- (long long )i) - (long long )size >= 0LL) || ((((((((12 <= size && i <=
100) && (-24LL + (long long )n) + (long long )size >= 0LL) && (-24LL + (long
long )i) + (long long )n >= 0LL) && (-24LL + (long long )i) + (long long )size
>= 0LL) && (0LL - (long long )i) + (long long )n >= 0LL) && (0LL - (long long
)i) + (long long )size >= 0LL) && (198LL - (long long )i) - (long long )n
>= 0LL) && (198LL - (long long )i) - (long long )size >= 0LL))) || ((((((((((12
<= size && (-24LL + (long long )n) + (long long )size >= 0LL) && (-23LL +
(long long )i) + (long long )n >= 0LL) && (-23LL + (long long )i) + (long
long )size >= 0LL) && (-1LL - (long long )i) + (long long )n >= 0LL) && (-1LL
- (long long )i) + (long long )size >= 0LL) && (88LL + (long long )i) - (long
long )n >= 0LL) && (88LL + (long long )i) - (long long )size >= 0LL) && (110LL
- (long long )i) - (long long )n >= 0LL) && (110LL - (long long )i) - (long
long )size >= 0LL) && i == 11)) || ((((((((((11 <= size && (-22LL + (long
long )n) + (long long )size >= 0LL) && (-22LL + (long long )i) + (long long
)n >= 0LL) && (-22LL + (long long )i) + (long long )size >= 0LL) && (0LL -
(long long )i) + (long long )n >= 0LL) && (0LL - (long long )i) + (long long
)size >= 0LL) && (88LL + (long long )i) - (long long )n >= 0LL) && (88LL +
(long long )i) - (long long )size >= 0LL) && (110LL - (long long )i) - (long
long )n >= 0LL) && (110LL - (long long )i) - (long long )size >= 0LL) && i
== 11)) || ((((((((((11 <= size && (-22LL + (long long )n) + (long long )size
>= 0LL) && (-21LL + (long long )i) + (long long )n >= 0LL) && (-21LL + (long
long )i) + (long long )size >= 0LL) && (-1LL - (long long )i) + (long long
)n >= 0LL) && (-1LL - (long long )i) + (long long )size >= 0LL) && (89LL +
(long long )i) - (long long )n >= 0LL) && (89LL + (long long )i) - (long long
)size >= 0LL) && (109LL - (long long )i) - (long long )n >= 0LL) && (109LL
- (long long )i) - (long long )size >= 0LL) && i == 10)) || ((((((((((10 <=
size && (-20LL + (long long )n) + (long long )size >= 0LL) && (-20LL + (long
long )i) + (long long )n >= 0LL) && (-20LL + (long long )i) + (long long )size
>= 0LL) && (0LL - (long long )i) + (long long )n >= 0LL) && (0LL - (long long
)i) + (long long )size >= 0LL) && (89LL + (long long )i) - (long long )n >=
0LL) && (89LL + (long long )i) - (long long )size >= 0LL) && (109LL - (long
long )i) - (long long )n >= 0LL) && (109LL - (long long )i) - (long long )size
>= 0LL) && i == 10)) || ((((((((((10 <= size && (-20LL + (long long )n) +
(long long )size >= 0LL) && (-19LL + (long long )i) + (long long )n >= 0LL)
&& (-19LL + (long long )i) + (long long )size >= 0LL) && (-1LL - (long long
)i) + (long long )n >= 0LL) && (-1LL - (long long )i) + (long long )size >=
0LL) && (90LL + (long long )i) - (long long )n >= 0LL) && (90LL + (long long
)i) - (long long )size >= 0LL) && (108LL - (long long )i) - (long long )n
>= 0LL) && (108LL - (long long )i) - (long long )size >= 0LL) && i == 9))
|| ((((((((((9 <= size && (-18LL + (long long )n) + (long long )size >= 0LL)
&& (-18LL + (long long )i) + (long long )n >= 0LL) && (-18LL + (long long
)i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long long )n >=
0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && (90LL + (long
long )i) - (long long )n >= 0LL) && (90LL + (long long )i) - (long long )size
>= 0LL) && (108LL - (long long )i) - (long long )n >= 0LL) && (108LL - (long
long )i) - (long long )size >= 0LL) && i == 9)) || ((((((((((9 <= size &&
(-18LL + (long long )n) + (long long )size >= 0LL) && (-17LL + (long long
)i) + (long long )n >= 0LL) && (-17LL + (long long )i) + (long long )size
>= 0LL) && (-1LL - (long long )i) + (long long )n >= 0LL) && (-1LL - (long
long )i) + (long long )size >= 0LL) && (91LL + (long long )i) - (long long
)n >= 0LL) && (91LL + (long long )i) - (long long )size >= 0LL) && (107LL
- (long long )i) - (long long )n >= 0LL) && (107LL - (long long )i) - (long
long )size >= 0LL) && i == 8)) || ((((((((((8 <= size && (-16LL + (long long
)n) + (long long )size >= 0LL) && (-16LL + (long long )i) + (long long )n
>= 0LL) && (-16LL + (long long )i) + (long long )size >= 0LL) && (0LL - (long
long )i) + (long long )n >= 0LL) && (0LL - (long long )i) + (long long )size
>= 0LL) && (91LL + (long long )i) - (long long )n >= 0LL) && (91LL + (long
long )i) - (long long )size >= 0LL) && (107LL - (long long )i) - (long long
)n >= 0LL) && (107LL - (long long )i) - (long long )size >= 0LL) && i == 8))
|| ((((((((((8 <= size && (-16LL + (long long )n) + (long long )size >= 0LL)
&& (-15LL + (long long )i) + (long long )n >= 0LL) && (-15LL + (long long
)i) + (long long )size >= 0LL) && (-1LL - (long long )i) + (long long )n >=
0LL) && (-1LL - (long long )i) + (long long )size >= 0LL) && (92LL + (long
long )i) - (long long )n >= 0LL) && (92LL + (long long )i) - (long long )size
>= 0LL) && (106LL - (long long )i) - (long long )n >= 0LL) && (106LL - (long
long )i) - (long long )size >= 0LL) && i == 7))) || (((((((((((7 <= n && 7
<= size) && (-14LL + (long long )n) + (long long )size >= 0LL) && (-14LL +
(long long )i) + (long long )n >= 0LL) && (-14LL + (long long )i) + (long
long )size >= 0LL) && (0LL - (long long )i) + (long long )n >= 0LL) && (0LL
- (long long )i) + (long long )size >= 0LL) && (92LL + (long long )i) - (long
long )n >= 0LL) && (92LL + (long long )i) - (long long )size >= 0LL) && (106LL
- (long long )i) - (long long )n >= 0LL) && (106LL - (long long )i) - (long
long )size >= 0LL) && i == 7)) || (((((((((((7 <= n && 7 <= size) && (-14LL
+ (long long )n) + (long long )size >= 0LL) && (-13LL + (long long )i) + (long
long )n >= 0LL) && (-13LL + (long long )i) + (long long )size >= 0LL) && (-1LL
- (long long )i) + (long long )n >= 0LL) && (-1LL - (long long )i) + (long
long )size >= 0LL) && (93LL + (long long )i) - (long long )n >= 0LL) && (93LL
+ (long long )i) - (long long )size >= 0LL) && (105LL - (long long )i) - (long
long )n >= 0LL) && (105LL - (long long )i) - (long long )size >= 0LL) && i
== 6)) || (((((((((((6 <= n && 6 <= size) && (-12LL + (long long )n) + (long
long )size >= 0LL) && (-12LL + (long long )i) + (long long )n >= 0LL) && (-12LL
+ (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long
long )n >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && (93LL
+ (long long )i) - (long long )n >= 0LL) && (93LL + (long long )i) - (long
long )size >= 0LL) && (105LL - (long long )i) - (long long )n >= 0LL) && (105LL
- (long long )i) - (long long )size >= 0LL) && i == 6)) || (((((((((((6 <=
n && 6 <= size) && (-12LL + (long long )n) + (long long )size >= 0LL) && (-11LL
+ (long long )i) + (long long )n >= 0LL) && (-11LL + (long long )i) + (long
long )size >= 0LL) && (-1LL - (long long )i) + (long long )n >= 0LL) && (-1LL
- (long long )i) + (long long )size >= 0LL) && (94LL + (long long )i) - (long
long )n >= 0LL) && (94LL + (long long )i) - (long long )size >= 0LL) && (104LL
- (long long )i) - (long long )n >= 0LL) && (104LL - (long long )i) - (long
long )size >= 0LL) && i == 5)) || (((((((((((5 <= n && 5 <= size) && (-10LL
+ (long long )n) + (long long )size >= 0LL) && (-10LL + (long long )i) + (long
long )n >= 0LL) && (-10LL + (long long )i) + (long long )size >= 0LL) && (0LL
- (long long )i) + (long long )n >= 0LL) && (0LL - (long long )i) + (long
long )size >= 0LL) && (94LL + (long long )i) - (long long )n >= 0LL) && (94LL
+ (long long )i) - (long long )size >= 0LL) && (104LL - (long long )i) - (long
long )n >= 0LL) && (104LL - (long long )i) - (long long )size >= 0LL) && i
== 5)) || (((((((((((5 <= n && 5 <= size) && (-10LL + (long long )n) + (long
long )size >= 0LL) && (-9LL + (long long )i) + (long long )n >= 0LL) && (-9LL
+ (long long )i) + (long long )size >= 0LL) && (-1LL - (long long )i) + (long
long )n >= 0LL) && (-1LL - (long long )i) + (long long )size >= 0LL) && (95LL
+ (long long )i) - (long long )n >= 0LL) && (95LL + (long long )i) - (long
long )size >= 0LL) && (103LL - (long long )i) - (long long )n >= 0LL) && (103LL
- (long long )i) - (long long )size >= 0LL) && i == 4)) || (((((((((((4 <=
n && 4 <= size) && (-8LL + (long long )n) + (long long )size >= 0LL) && (-8LL
+ (long long )i) + (long long )n >= 0LL) && (-8LL + (long long )i) + (long
long )size >= 0LL) && (0LL - (long long )i) + (long long )n >= 0LL) && (0LL
- (long long )i) + (long long )size >= 0LL) && (95LL + (long long )i) - (long
long )n >= 0LL) && (95LL + (long long )i) - (long long )size >= 0LL) && (103LL
- (long long )i) - (long long )n >= 0LL) && (103LL - (long long )i) - (long
long )size >= 0LL) && i == 4)) || (((((((((((4 <= n && 4 <= size) && (-8LL
+ (long long )n) + (long long )size >= 0LL) && (-7LL + (long long )i) + (long
long )n >= 0LL) && (-7LL + (long long )i) + (long long )size >= 0LL) && (-1LL
- (long long )i) + (long long )n >= 0LL) && (-1LL - (long long )i) + (long
long )size >= 0LL) && (96LL + (long long )i) - (long long )n >= 0LL) && (96LL
+ (long long )i) - (long long )size >= 0LL) && (102LL - (long long )i) - (long
long )n >= 0LL) && (102LL - (long long )i) - (long long )size >= 0LL) && i
== 3)) || (((((((((((3 <= n && 3 <= size) && (-6LL + (long long )n) + (long
long )size >= 0LL) && (-6LL + (long long )i) + (long long )n >= 0LL) && (-6LL
+ (long long )i) + (long long )size >= 0LL) && (0LL - (long long )i) + (long
long )n >= 0LL) && (0LL - (long long )i) + (long long )size >= 0LL) && (96LL
+ (long long )i) - (long long )n >= 0LL) && (96LL + (long long )i) - (long
long )size >= 0LL) && (102LL - (long long )i) - (long long )n >= 0LL) && (102LL
- (long long )i) - (long long )size >= 0LL) && i == 3)) || (((((((((((3 <=
n && 3 <= size) && (-6LL + (long long )n) + (long long )size >= 0LL) && (-5LL
+ (long long )i) + (long long )n >= 0LL) && (-5LL + (long long )i) + (long
long )size >= 0LL) && (-1LL - (long long )i) + (long long )n >= 0LL) && (-1LL
- (long long )i) + (long long )size >= 0LL) && (97LL + (long long )i) - (long
long )n >= 0LL) && (97LL + (long long )i) - (long long )size >= 0LL) && (101LL
- (long long )i) - (long long )n >= 0LL) && (101LL - (long long )i) - (long
long )size >= 0LL) && i == 2)) || (((((((((((2 <= n && 2 <= size) && (-4LL
+ (long long )n) + (long long )size >= 0LL) && (-4LL + (long long )i) + (long
long )n >= 0LL) && (-4LL + (long long )i) + (long long )size >= 0LL) && (0LL
- (long long )i) + (long long )n >= 0LL) && (0LL - (long long )i) + (long
long )size >= 0LL) && (97LL + (long long )i) - (long long )n >= 0LL) && (97LL
+ (long long )i) - (long long )size >= 0LL) && (101LL - (long long )i) - (long
long )n >= 0LL) && (101LL - (long long )i) - (long long )size >= 0LL) && i
== 2)) || (((((((((((2 <= n && 2 <= size) && (-4LL + (long long )n) + (long
long )size >= 0LL) && (-3LL + (long long )i) + (long long )n >= 0LL) && (-3LL
+ (long long )i) + (long long )size >= 0LL) && (-1LL - (long long )i) + (long
long )n >= 0LL) && (-1LL - (long long )i) + (long long )size >= 0LL) && (98LL
+ (long long )i) - (long long )n >= 0LL) && (98LL + (long long )i) - (long
long )size >= 0LL) && (100LL - (long long )i) - (long long )n >= 0LL) && (100LL
- (long long )i) - (long long )size >= 0LL) && i == 1)) || (((((((((((1 <=
n && 1 <= size) && (-2LL + (long long )n) + (long long )size >= 0LL) && (-2LL
+ (long long )i) + (long long )n >= 0LL) && (-2LL + (long long )i) + (long
long )size >= 0LL) && (0LL - (long long )i) + (long long )n >= 0LL) && (0LL
- (long long )i) + (long long )size >= 0LL) && (98LL + (long long )i) - (long
long )n >= 0LL) && (98LL + (long long )i) - (long long )size >= 0LL) && (100LL
- (long long )i) - (long long )n >= 0LL) && (100LL - (long long )i) - (long
long )size >= 0LL) && i == 1)) || ((((((((((((1 <= n && 1 <= size) && (-2LL
+ (long long )n) + (long long )size >= 0LL) && (-1LL + (long long )i) + (long
long )n >= 0LL) && (-1LL + (long long )i) + (long long )size >= 0LL) && (-1LL
- (long long )i) + (long long )n >= 0LL) && (-1LL - (long long )i) + (long
long )size >= 0LL) && (99LL + (long long )i) - (long long )n >= 0LL) && (99LL
+ (long long )i) - (long long )size >= 0LL) && (99LL - (long long )i) - (long
long )n >= 0LL) && (99LL - (long long )i) - (long long )size >= 0LL) && 0
== i) && i == 0))) || (((((((((((0 <= n && 0 <= size) && (0LL - (long long
)i) + (long long )n >= 0LL) && (0LL - (long long )i) + (long long )size >=
0LL) && (long long )n + (long long )size >= 0LL) && (long long )i + (long
long )n >= 0LL) && (long long )i + (long long )size >= 0LL) && (99LL + (long
long )i) - (long long )n >= 0LL) && (99LL + (long long )i) - (long long )size
>= 0LL) && (99LL - (long long )i) - (long long )n >= 0LL) && (99LL - (long
long )i) - (long long )size >= 0LL) && i == 0)) || (((((((((((0 <= n && 0
<= size) && (2147483648LL + (long long )i) + (long long )n >= 0LL) && (2147483648LL
+ (long long )i) + (long long )size >= 0LL) && (2147483647LL - (long long
)i) + (long long )n >= 0LL) && (2147483647LL - (long long )i) + (long long
)size >= 0LL) && (long long )n + (long long )size >= 0LL) && (2147483747LL
+ (long long )i) - (long long )n >= 0LL) && (2147483747LL + (long long )i)
- (long long )size >= 0LL) && (2147483746LL - (long long )i) - (long long
)n >= 0LL) && (2147483746LL - (long long )i) - (long long )size >= 0LL) &&
n == size)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/ldv-memsafety/ArraysOfVariableLength.c
file_hash: eb589a592aff310a2662d7a22b89559cebd75929901bc5e2cc7816fe45d47c92
line: 25
column: 5
function: main
value: (((((((((((((((((((((((((((((((((((((((((((((((((((i == 21 || i == 6)
|| i == 20) || i == 6) || i == 20) || i == 5) || i == 19) || i == 5) || i
== 19) || i == 4) || i == 18) || i == 4) || i == 18) || i == 3) || i == 17)
|| i == 3) || i == 17) || i == 2) || i == 16) || i == 2) || i == 16) || i
== 1) || i == 15) || i == 1) || i == 15) || (0 == i && i == 0)) || i == 14)
|| (0 == i && i == 0)) || i == 14) || i == 100) || i == 13) || i == 13) ||
i == 12) || i == 12) || i == 11) || (25 <= i && i <= 100)) || i == 11) ||
(25 <= i && i <= 101)) || i == 10) || i == 24) || i == 10) || i == 24) ||
i == 9) || i == 23) || i == 9) || i == 23) || i == 8) || i == 22) || i ==
8) || i == 22) || i == 7) || i == 21) || i == 7
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
30 |
2023-12-01T04:54:17+01:00 |
|