f522f70 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T07:13:52Z |
|
eb89d7f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
crux-llvm-0.5.0.99 |
4 |
2023-12-18T05:22:50+01:00 |
|
a62d9d1 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
Taipan |
5 |
2023-12-02T13:51:43Z |
|
ababb4f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
Symbiotic |
3 |
2023-11-29T22:21:54Z |
|
e872c0c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
Kojak |
5 |
2023-12-03T02:34:10Z |
|
1d1bf62 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
ESBMC 7.4.0 kind |
4 |
2023-12-01T10:11:09Z |
|
442b3b2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
6 |
2023-12-18T06:07:42+01:00 |
eb89d7f |
f69e73f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-05T14:39:59+01:00 |
668df96 |
168124a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-04T16:40:34+01:00 |
ecc843a |
48d5395 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-04T12:12:16+01:00 |
a62d9d1 |
d812197 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-04T02:25:16+01:00 |
e2410b7 |
13275f6 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-03T18:33:17+01:00 |
7d68e3b |
8f09a99 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-03T09:58:50+01:00 |
f522f70 |
ecde7e4 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-03T06:18:53+01:00 |
e872c0c |
8fac61f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-12-01T18:28:10+01:00 |
1d1bf62 |
e7db78f |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-11-30T13:44:33+01:00 |
b5b332c |
ed4a19c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-11-30T03:01:17+01:00 |
ababb4f |
b5b332c |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-11-30T02:15:50+01:00 |
|
1616faa |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
5 |
2023-11-29T08:34:18+01:00 |
0c354d8 |
e2410b7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
5 |
2023-12-03T23:34:23+01:00 |
|
848b8a2 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
5 |
2023-12-18T19:40:23+01:00 |
|
b214f3a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CBMC |
5 |
2023-12-17T19:40:41+01:00 |
|
668df96 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
Bubaak |
3 |
2023-12-05T10:07:52Z |
|
ecc843a |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
Bubaak |
3 |
2023-12-04T12:42:55Z |
|
0c354d8 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
Automizer |
5 |
2023-11-29T03:44:52Z |
|
7d68e3b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
sv-comp-24 |
4 |
2023-12-03T17:35:42+01:00 |
|
a773728 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
8 |
2023-12-19T05:27:05+01:00 |
848b8a2 |
44d54ab |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
7 |
2023-12-17T22:07:40+01:00 |
b214f3a |
0f73bb7 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: ec021b70-0e78-4769-8fa6-d203648e5dd4
creation_time: 2023-12-01T01:35:54Z
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/mult_array-alloca-2.i'''
task:
input_files:
- ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
input_file_hashes:
../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
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/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 556
column: 6
function: main
value: 1 <= fac
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 556
column: 6
function: main
value: (2147483647LL + (long long )fac) + (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 556
column: 6
function: main
value: (2147483646LL + (long long )fac) - (long long )j >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 556
column: 6
function: main
value: length != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 556
column: 6
function: main
value: fac != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 556
column: 6
function: main
value: ((((((((((((((((((((8 <= i && (-9LL + (long long )fac) + (long long )i
>= 0LL) && (2147483640LL + (long long )i) + (long long )j >= 0LL) && (2147483639LL
+ (long long )i) - (long long )j >= 0LL) && ((((((((9 <= length && i <= 2147483646)
&& (-17LL + (long long )i) + (long long )length >= 0LL) && (-10LL + (long
long )fac) + (long long )length >= 0LL) && (2147483639LL + (long long )j)
+ (long long )length >= 0LL) && (-1LL - (long long )i) + (long long )length
>= 0LL) && (2147483638LL - (long long )j) + (long long )length >= 0LL) &&
i != 0) || (((((8 <= length && (-16LL + (long long )i) + (long long )length
>= 0LL) && (-9LL + (long long )fac) + (long long )length >= 0LL) && (2147483640LL
+ (long long )j) + (long long )length >= 0LL) && (0LL - (long long )i) + (long
long )length >= 0LL) && (2147483639LL - (long long )j) + (long long )length
>= 0LL))) || ((((((((((((8 <= length && (-15LL + (long long )i) + (long long
)length >= 0LL) && (-9LL + (long long )fac) + (long long )length >= 0LL) &&
(-8LL + (long long )fac) + (long long )i >= 0LL) && (2147483640LL + (long
long )j) + (long long )length >= 0LL) && (2147483641LL + (long long )i) +
(long long )j >= 0LL) && (-1LL - (long long )i) + (long long )length >= 0LL)
&& (2147483639LL - (long long )j) + (long long )length >= 0LL) && (2147483655LL
- (long long )i) + (long long )j >= 0LL) && (6LL + (long long )fac) - (long
long )i >= 0LL) && (2147483640LL + (long long )i) - (long long )j >= 0LL)
&& (2147483654LL - (long long )i) - (long long )j >= 0LL) && i == 7)) || ((((((((((((7
<= length && (-14LL + (long long )i) + (long long )length >= 0LL) && (-8LL
+ (long long )fac) + (long long )i >= 0LL) && (-8LL + (long long )fac) + (long
long )length >= 0LL) && (2147483641LL + (long long )i) + (long long )j >=
0LL) && (2147483641LL + (long long )j) + (long long )length >= 0LL) && (0LL
- (long long )i) + (long long )length >= 0LL) && (2147483640LL - (long long
)j) + (long long )length >= 0LL) && (2147483655LL - (long long )i) + (long
long )j >= 0LL) && (6LL + (long long )fac) - (long long )i >= 0LL) && (2147483640LL
+ (long long )i) - (long long )j >= 0LL) && (2147483654LL - (long long )i)
- (long long )j >= 0LL) && i == 7)) || ((((((((((((7 <= length && (-13LL +
(long long )i) + (long long )length >= 0LL) && (-8LL + (long long )fac) +
(long long )length >= 0LL) && (-7LL + (long long )fac) + (long long )i >=
0LL) && (2147483641LL + (long long )j) + (long long )length >= 0LL) && (2147483642LL
+ (long long )i) + (long long )j >= 0LL) && (-1LL - (long long )i) + (long
long )length >= 0LL) && (2147483640LL - (long long )j) + (long long )length
>= 0LL) && (2147483654LL - (long long )i) + (long long )j >= 0LL) && (5LL
+ (long long )fac) - (long long )i >= 0LL) && (2147483641LL + (long long )i)
- (long long )j >= 0LL) && (2147483653LL - (long long )i) - (long long )j
>= 0LL) && i == 6)) || ((((((((((((6 <= length && (-12LL + (long long )i)
+ (long long )length >= 0LL) && (-7LL + (long long )fac) + (long long )i >=
0LL) && (-7LL + (long long )fac) + (long long )length >= 0LL) && (2147483642LL
+ (long long )i) + (long long )j >= 0LL) && (2147483642LL + (long long )j)
+ (long long )length >= 0LL) && (0LL - (long long )i) + (long long )length
>= 0LL) && (2147483641LL - (long long )j) + (long long )length >= 0LL) &&
(2147483654LL - (long long )i) + (long long )j >= 0LL) && (5LL + (long long
)fac) - (long long )i >= 0LL) && (2147483641LL + (long long )i) - (long long
)j >= 0LL) && (2147483653LL - (long long )i) - (long long )j >= 0LL) && i
== 6)) || ((((((((((((6 <= length && (-11LL + (long long )i) + (long long
)length >= 0LL) && (-7LL + (long long )fac) + (long long )length >= 0LL) &&
(-6LL + (long long )fac) + (long long )i >= 0LL) && (2147483642LL + (long
long )j) + (long long )length >= 0LL) && (2147483643LL + (long long )i) +
(long long )j >= 0LL) && (-1LL - (long long )i) + (long long )length >= 0LL)
&& (2147483641LL - (long long )j) + (long long )length >= 0LL) && (2147483653LL
- (long long )i) + (long long )j >= 0LL) && (4LL + (long long )fac) - (long
long )i >= 0LL) && (2147483642LL + (long long )i) - (long long )j >= 0LL)
&& (2147483652LL - (long long )i) - (long long )j >= 0LL) && i == 5)) || ((((((((((((5
<= length && (-10LL + (long long )i) + (long long )length >= 0LL) && (-6LL
+ (long long )fac) + (long long )i >= 0LL) && (-6LL + (long long )fac) + (long
long )length >= 0LL) && (2147483643LL + (long long )i) + (long long )j >=
0LL) && (2147483643LL + (long long )j) + (long long )length >= 0LL) && (0LL
- (long long )i) + (long long )length >= 0LL) && (2147483642LL - (long long
)j) + (long long )length >= 0LL) && (2147483653LL - (long long )i) + (long
long )j >= 0LL) && (4LL + (long long )fac) - (long long )i >= 0LL) && (2147483642LL
+ (long long )i) - (long long )j >= 0LL) && (2147483652LL - (long long )i)
- (long long )j >= 0LL) && i == 5)) || ((((((((((((5 <= length && (-9LL +
(long long )i) + (long long )length >= 0LL) && (-6LL + (long long )fac) +
(long long )length >= 0LL) && (-5LL + (long long )fac) + (long long )i >=
0LL) && (2147483643LL + (long long )j) + (long long )length >= 0LL) && (2147483644LL
+ (long long )i) + (long long )j >= 0LL) && (-1LL - (long long )i) + (long
long )length >= 0LL) && (2147483642LL - (long long )j) + (long long )length
>= 0LL) && (2147483652LL - (long long )i) + (long long )j >= 0LL) && (3LL
+ (long long )fac) - (long long )i >= 0LL) && (2147483643LL + (long long )i)
- (long long )j >= 0LL) && (2147483651LL - (long long )i) - (long long )j
>= 0LL) && i == 4)) || ((((((((((((4 <= length && (-8LL + (long long )i) +
(long long )length >= 0LL) && (-5LL + (long long )fac) + (long long )i >=
0LL) && (-5LL + (long long )fac) + (long long )length >= 0LL) && (2147483644LL
+ (long long )i) + (long long )j >= 0LL) && (2147483644LL + (long long )j)
+ (long long )length >= 0LL) && (0LL - (long long )i) + (long long )length
>= 0LL) && (2147483643LL - (long long )j) + (long long )length >= 0LL) &&
(2147483652LL - (long long )i) + (long long )j >= 0LL) && (3LL + (long long
)fac) - (long long )i >= 0LL) && (2147483643LL + (long long )i) - (long long
)j >= 0LL) && (2147483651LL - (long long )i) - (long long )j >= 0LL) && i
== 4)) || ((((((((((((4 <= length && (-7LL + (long long )i) + (long long )length
>= 0LL) && (-5LL + (long long )fac) + (long long )length >= 0LL) && (-4LL
+ (long long )fac) + (long long )i >= 0LL) && (2147483644LL + (long long )j)
+ (long long )length >= 0LL) && (2147483645LL + (long long )i) + (long long
)j >= 0LL) && (-1LL - (long long )i) + (long long )length >= 0LL) && (2147483643LL
- (long long )j) + (long long )length >= 0LL) && (2147483651LL - (long long
)i) + (long long )j >= 0LL) && (2LL + (long long )fac) - (long long )i >=
0LL) && (2147483644LL + (long long )i) - (long long )j >= 0LL) && (2147483650LL
- (long long )i) - (long long )j >= 0LL) && i == 3)) || ((((((((((((3 <= length
&& (-6LL + (long long )i) + (long long )length >= 0LL) && (-4LL + (long long
)fac) + (long long )i >= 0LL) && (-4LL + (long long )fac) + (long long )length
>= 0LL) && (2147483645LL + (long long )i) + (long long )j >= 0LL) && (2147483645LL
+ (long long )j) + (long long )length >= 0LL) && (0LL - (long long )i) + (long
long )length >= 0LL) && (2147483644LL - (long long )j) + (long long )length
>= 0LL) && (2147483651LL - (long long )i) + (long long )j >= 0LL) && (2LL
+ (long long )fac) - (long long )i >= 0LL) && (2147483644LL + (long long )i)
- (long long )j >= 0LL) && (2147483650LL - (long long )i) - (long long )j
>= 0LL) && i == 3)) || ((((((((((((3 <= length && (-5LL + (long long )i) +
(long long )length >= 0LL) && (-4LL + (long long )fac) + (long long )length
>= 0LL) && (-3LL + (long long )fac) + (long long )i >= 0LL) && (2147483645LL
+ (long long )j) + (long long )length >= 0LL) && (2147483646LL + (long long
)i) + (long long )j >= 0LL) && (-1LL - (long long )i) + (long long )length
>= 0LL) && (2147483644LL - (long long )j) + (long long )length >= 0LL) &&
(2147483650LL - (long long )i) + (long long )j >= 0LL) && (1LL + (long long
)fac) - (long long )i >= 0LL) && (2147483645LL + (long long )i) - (long long
)j >= 0LL) && (2147483649LL - (long long )i) - (long long )j >= 0LL) && i
== 2)) || ((((((((((((2 <= length && (-4LL + (long long )i) + (long long )length
>= 0LL) && (-3LL + (long long )fac) + (long long )i >= 0LL) && (-3LL + (long
long )fac) + (long long )length >= 0LL) && (2147483646LL + (long long )i)
+ (long long )j >= 0LL) && (2147483646LL + (long long )j) + (long long )length
>= 0LL) && (0LL - (long long )i) + (long long )length >= 0LL) && (2147483645LL
- (long long )j) + (long long )length >= 0LL) && (2147483650LL - (long long
)i) + (long long )j >= 0LL) && (1LL + (long long )fac) - (long long )i >=
0LL) && (2147483645LL + (long long )i) - (long long )j >= 0LL) && (2147483649LL
- (long long )i) - (long long )j >= 0LL) && i == 2)) || ((((((((((((2 <= length
&& (-3LL + (long long )i) + (long long )length >= 0LL) && (-3LL + (long long
)fac) + (long long )length >= 0LL) && (-2LL + (long long )fac) + (long long
)i >= 0LL) && (2147483646LL + (long long )j) + (long long )length >= 0LL)
&& (2147483647LL + (long long )i) + (long long )j >= 0LL) && (-1LL - (long
long )i) + (long long )length >= 0LL) && (2147483645LL - (long long )j) +
(long long )length >= 0LL) && (2147483649LL - (long long )i) + (long long
)j >= 0LL) && (2147483646LL + (long long )i) - (long long )j >= 0LL) && (2147483648LL
- (long long )i) - (long long )j >= 0LL) && (long long )fac - (long long )i
>= 0LL) && i == 1)) || ((((((((((((1 <= length && (-2LL + (long long )i) +
(long long )length >= 0LL) && (-2LL + (long long )fac) + (long long )i >=
0LL) && (-2LL + (long long )fac) + (long long )length >= 0LL) && (2147483647LL
+ (long long )i) + (long long )j >= 0LL) && (2147483647LL + (long long )j)
+ (long long )length >= 0LL) && (0LL - (long long )i) + (long long )length
>= 0LL) && (2147483646LL - (long long )j) + (long long )length >= 0LL) &&
(2147483649LL - (long long )i) + (long long )j >= 0LL) && (2147483646LL +
(long long )i) - (long long )j >= 0LL) && (2147483648LL - (long long )i) -
(long long )j >= 0LL) && (long long )fac - (long long )i >= 0LL) && i == 1))
|| (((((((((((((1 <= length && (-2LL + (long long )fac) + (long long )length
>= 0LL) && (-1LL + (long long )i) + (long long )length >= 0LL) && (-1LL +
(long long )fac) + (long long )i >= 0LL) && (2147483647LL + (long long )j)
+ (long long )length >= 0LL) && (2147483648LL + (long long )i) + (long long
)j >= 0LL) && (-1LL - (long long )i) + (long long )length >= 0LL) && (2147483646LL
- (long long )j) + (long long )length >= 0LL) && (2147483648LL - (long long
)i) + (long long )j >= 0LL) && (-1LL + (long long )fac) - (long long )i >=
0LL) && (2147483647LL + (long long )i) - (long long )j >= 0LL) && (2147483647LL
- (long long )i) - (long long )j >= 0LL) && 0 == i) && i == 0)) || (((((((((((((1
<= length && (-2LL + (long long )fac) + (long long )length >= 0LL) && (-1LL
+ (long long )i) + (long long )length >= 0LL) && (-1LL + (long long )fac)
+ (long long )i >= 0LL) && (2147483647LL + (long long )j) + (long long )length
>= 0LL) && (2147483648LL + (long long )i) + (long long )j >= 0LL) && (-1LL
- (long long )i) + (long long )length >= 0LL) && (2147483646LL - (long long
)j) + (long long )length >= 0LL) && (2147483648LL - (long long )i) + (long
long )j >= 0LL) && (-1LL + (long long )fac) - (long long )i >= 0LL) && (2147483647LL
+ (long long )i) - (long long )j >= 0LL) && (2147483647LL - (long long )i)
- (long long )j >= 0LL) && 0 == i) && i == 0)) || (((((((((((1 <= length &&
(-2LL + (long long )fac) + (long long )length >= 0LL) && (2147483647LL + (long
long )i) + (long long )length >= 0LL) && (2147483647LL + (long long )j) +
(long long )length >= 0LL) && (2147483647LL + (long long )fac) + (long long
)i >= 0LL) && (4294967296LL + (long long )i) + (long long )j >= 0LL) && (2147483646LL
- (long long )i) + (long long )length >= 0LL) && (2147483646LL - (long long
)j) + (long long )length >= 0LL) && (4294967295LL - (long long )i) + (long
long )j >= 0LL) && (2147483646LL + (long long )fac) - (long long )i >= 0LL)
&& (4294967295LL + (long long )i) - (long long )j >= 0LL) && (4294967294LL
- (long long )i) - (long long )j >= 0LL)
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: 1 <= i
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: 1 <= length
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: 1 <= fac
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: (-2LL + (long long )i) + (long long )length >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: (-2LL + (long long )fac) + (long long )i >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: (-2LL + (long long )fac) + (long long )length >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: (0LL - (long long )i) + (long long )length >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: (long long )i - (long long )length >= 0LL
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: i != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: length != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: fac != 0
format: c_expression
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
file_hash: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
line: 559
column: 6
function: main
value: ((((((((((((((((((((((((((((((((-3LL + (long long )i) + (long long )j
>= 0LL && (-3LL + (long long )j) + (long long )length >= 0LL) && (-3LL + (long
long )fac) + (long long )j >= 0LL) && (1LL - (long long )j) + (long long )length
>= 0LL) && (1LL + (long long )i) - (long long )j >= 0LL) && (1LL + (long long
)fac) - (long long )j >= 0LL) && j == 2) || (((((((-2LL + (long long )i) +
(long long )j >= 0LL && (-2LL + (long long )j) + (long long )length >= 0LL)
&& (-2LL + (long long )fac) + (long long )j >= 0LL) && (0LL - (long long )j)
+ (long long )length >= 0LL) && (long long )i - (long long )j >= 0LL) && (long
long )fac - (long long )j >= 0LL) && j == 1)) || (((((((-2LL + (long long
)i) + (long long )j >= 0LL && (-2LL + (long long )j) + (long long )length
>= 0LL) && (-2LL + (long long )fac) + (long long )j >= 0LL) && (0LL - (long
long )j) + (long long )length >= 0LL) && (long long )i - (long long )j >=
0LL) && (long long )fac - (long long )j >= 0LL) && j == 1)) || ((((((((-1LL
+ (long long )i) + (long long )j >= 0LL && (-1LL + (long long )j) + (long
long )length >= 0LL) && (-1LL + (long long )fac) + (long long )j >= 0LL) &&
(-1LL - (long long )j) + (long long )length >= 0LL) && (-1LL + (long long
)i) - (long long )j >= 0LL) && (-1LL + (long long )fac) - (long long )j >=
0LL) && 0 == j) && j == 0)) || ((((((((-1LL + (long long )i) + (long long
)j >= 0LL && (-1LL + (long long )j) + (long long )length >= 0LL) && (-1LL
+ (long long )fac) + (long long )j >= 0LL) && (-1LL - (long long )j) + (long
long )length >= 0LL) && (-1LL + (long long )i) - (long long )j >= 0LL) &&
(-1LL + (long long )fac) - (long long )j >= 0LL) && 0 == j) && j == 0)) ||
((((((2147483647LL + (long long )i) + (long long )j >= 0LL && (2147483647LL
+ (long long )j) + (long long )length >= 0LL) && (2147483647LL + (long long
)fac) + (long long )j >= 0LL) && (2147483646LL - (long long )j) + (long long
)length >= 0LL) && (2147483646LL + (long long )i) - (long long )j >= 0LL)
&& (2147483646LL + (long long )fac) - (long long )j >= 0LL)) || (((((12 <=
j && j <= 2147483646) && (-13LL + (long long )i) + (long long )j >= 0LL) &&
(-13LL + (long long )j) + (long long )length >= 0LL) && (-13LL + (long long
)fac) + (long long )j >= 0LL) && j != 0)) || (((12 <= j && (-13LL + (long
long )i) + (long long )j >= 0LL) && (-13LL + (long long )j) + (long long )length
>= 0LL) && (-13LL + (long long )fac) + (long long )j >= 0LL)) || (((((((-12LL
+ (long long )i) + (long long )j >= 0LL && (-12LL + (long long )j) + (long
long )length >= 0LL) && (-12LL + (long long )fac) + (long long )j >= 0LL)
&& (10LL - (long long )j) + (long long )length >= 0LL) && (10LL + (long long
)i) - (long long )j >= 0LL) && (10LL + (long long )fac) - (long long )j >=
0LL) && j == 11)) || (((((((-12LL + (long long )i) + (long long )j >= 0LL
&& (-12LL + (long long )j) + (long long )length >= 0LL) && (-12LL + (long
long )fac) + (long long )j >= 0LL) && (10LL - (long long )j) + (long long
)length >= 0LL) && (10LL + (long long )i) - (long long )j >= 0LL) && (10LL
+ (long long )fac) - (long long )j >= 0LL) && j == 11)) || (((((((-11LL +
(long long )i) + (long long )j >= 0LL && (-11LL + (long long )j) + (long long
)length >= 0LL) && (-11LL + (long long )fac) + (long long )j >= 0LL) && (9LL
- (long long )j) + (long long )length >= 0LL) && (9LL + (long long )i) - (long
long )j >= 0LL) && (9LL + (long long )fac) - (long long )j >= 0LL) && j ==
10)) || (((((((-11LL + (long long )i) + (long long )j >= 0LL && (-11LL + (long
long )j) + (long long )length >= 0LL) && (-11LL + (long long )fac) + (long
long )j >= 0LL) && (9LL - (long long )j) + (long long )length >= 0LL) && (9LL
+ (long long )i) - (long long )j >= 0LL) && (9LL + (long long )fac) - (long
long )j >= 0LL) && j == 10)) || (((((((-10LL + (long long )i) + (long long
)j >= 0LL && (-10LL + (long long )j) + (long long )length >= 0LL) && (-10LL
+ (long long )fac) + (long long )j >= 0LL) && (8LL - (long long )j) + (long
long )length >= 0LL) && (8LL + (long long )i) - (long long )j >= 0LL) && (8LL
+ (long long )fac) - (long long )j >= 0LL) && j == 9)) || (((((((-10LL + (long
long )i) + (long long )j >= 0LL && (-10LL + (long long )j) + (long long )length
>= 0LL) && (-10LL + (long long )fac) + (long long )j >= 0LL) && (8LL - (long
long )j) + (long long )length >= 0LL) && (8LL + (long long )i) - (long long
)j >= 0LL) && (8LL + (long long )fac) - (long long )j >= 0LL) && j == 9))
|| (((((((-9LL + (long long )i) + (long long )j >= 0LL && (-9LL + (long long
)j) + (long long )length >= 0LL) && (-9LL + (long long )fac) + (long long
)j >= 0LL) && (7LL - (long long )j) + (long long )length >= 0LL) && (7LL +
(long long )i) - (long long )j >= 0LL) && (7LL + (long long )fac) - (long
long )j >= 0LL) && j == 8)) || (((((((-9LL + (long long )i) + (long long )j
>= 0LL && (-9LL + (long long )j) + (long long )length >= 0LL) && (-9LL + (long
long )fac) + (long long )j >= 0LL) && (7LL - (long long )j) + (long long )length
>= 0LL) && (7LL + (long long )i) - (long long )j >= 0LL) && (7LL + (long long
)fac) - (long long )j >= 0LL) && j == 8)) || (((((((-8LL + (long long )i)
+ (long long )j >= 0LL && (-8LL + (long long )j) + (long long )length >= 0LL)
&& (-8LL + (long long )fac) + (long long )j >= 0LL) && (6LL - (long long )j)
+ (long long )length >= 0LL) && (6LL + (long long )i) - (long long )j >= 0LL)
&& (6LL + (long long )fac) - (long long )j >= 0LL) && j == 7)) || (((((((-8LL
+ (long long )i) + (long long )j >= 0LL && (-8LL + (long long )j) + (long
long )length >= 0LL) && (-8LL + (long long )fac) + (long long )j >= 0LL) &&
(6LL - (long long )j) + (long long )length >= 0LL) && (6LL + (long long )i)
- (long long )j >= 0LL) && (6LL + (long long )fac) - (long long )j >= 0LL)
&& j == 7)) || (((((((-7LL + (long long )i) + (long long )j >= 0LL && (-7LL
+ (long long )j) + (long long )length >= 0LL) && (-7LL + (long long )fac)
+ (long long )j >= 0LL) && (5LL - (long long )j) + (long long )length >= 0LL)
&& (5LL + (long long )i) - (long long )j >= 0LL) && (5LL + (long long )fac)
- (long long )j >= 0LL) && j == 6)) || (((((((-7LL + (long long )i) + (long
long )j >= 0LL && (-7LL + (long long )j) + (long long )length >= 0LL) && (-7LL
+ (long long )fac) + (long long )j >= 0LL) && (5LL - (long long )j) + (long
long )length >= 0LL) && (5LL + (long long )i) - (long long )j >= 0LL) && (5LL
+ (long long )fac) - (long long )j >= 0LL) && j == 6)) || (((((((-6LL + (long
long )i) + (long long )j >= 0LL && (-6LL + (long long )j) + (long long )length
>= 0LL) && (-6LL + (long long )fac) + (long long )j >= 0LL) && (4LL - (long
long )j) + (long long )length >= 0LL) && (4LL + (long long )i) - (long long
)j >= 0LL) && (4LL + (long long )fac) - (long long )j >= 0LL) && j == 5))
|| (((((((-6LL + (long long )i) + (long long )j >= 0LL && (-6LL + (long long
)j) + (long long )length >= 0LL) && (-6LL + (long long )fac) + (long long
)j >= 0LL) && (4LL - (long long )j) + (long long )length >= 0LL) && (4LL +
(long long )i) - (long long )j >= 0LL) && (4LL + (long long )fac) - (long
long )j >= 0LL) && j == 5)) || (((((((-5LL + (long long )i) + (long long )j
>= 0LL && (-5LL + (long long )j) + (long long )length >= 0LL) && (-5LL + (long
long )fac) + (long long )j >= 0LL) && (3LL - (long long )j) + (long long )length
>= 0LL) && (3LL + (long long )i) - (long long )j >= 0LL) && (3LL + (long long
)fac) - (long long )j >= 0LL) && j == 4)) || (((((((-5LL + (long long )i)
+ (long long )j >= 0LL && (-5LL + (long long )j) + (long long )length >= 0LL)
&& (-5LL + (long long )fac) + (long long )j >= 0LL) && (3LL - (long long )j)
+ (long long )length >= 0LL) && (3LL + (long long )i) - (long long )j >= 0LL)
&& (3LL + (long long )fac) - (long long )j >= 0LL) && j == 4)) || (((((((-4LL
+ (long long )i) + (long long )j >= 0LL && (-4LL + (long long )j) + (long
long )length >= 0LL) && (-4LL + (long long )fac) + (long long )j >= 0LL) &&
(2LL - (long long )j) + (long long )length >= 0LL) && (2LL + (long long )i)
- (long long )j >= 0LL) && (2LL + (long long )fac) - (long long )j >= 0LL)
&& j == 3)) || (((((((-4LL + (long long )i) + (long long )j >= 0LL && (-4LL
+ (long long )j) + (long long )length >= 0LL) && (-4LL + (long long )fac)
+ (long long )j >= 0LL) && (2LL - (long long )j) + (long long )length >= 0LL)
&& (2LL + (long long )i) - (long long )j >= 0LL) && (2LL + (long long )fac)
- (long long )j >= 0LL) && j == 3)) || (((((((-3LL + (long long )i) + (long
long )j >= 0LL && (-3LL + (long long )j) + (long long )length >= 0LL) && (-3LL
+ (long long )fac) + (long long )j >= 0LL) && (1LL - (long long )j) + (long
long )length >= 0LL) && (1LL + (long long )i) - (long long )j >= 0LL) && (1LL
+ (long long )fac) - (long long )j >= 0LL) && j == 2)
format: c_expression |
violation_witness |
CPAchecker 2.3 |
40 |
2023-12-01T05:18:23+01:00 |
|
103bb37 |
Inspect |
|
- content:
- segment:
- waypoint:
action: follow
constraint:
format: C
value: \result == 2
location:
column: 38
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_af6a415c-c063-4e52-ad46-ba5771169d1a/sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
line: 549
type: function_return
- segment:
- waypoint:
action: follow
constraint:
format: C
value: \result == 1073741824
location:
column: 35
file_name: /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_af6a415c-c063-4e52-ad46-ba5771169d1a/sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
line: 551
type: function_return
- segment:
- waypoint:
action: follow
location:
column: 3
file_name: vcloud_worker_vcloud-master_on_vcloud-master/run_dir_af6a415c-c063-4e52-ad46-ba5771169d1a/sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
line: 554
type: target
entry_type: violation_sequence
metadata:
creation_time: '2023-11-29T22:21:54Z'
format_version: '0.1'
producer:
name: symbiotic
task:
data_model: LP64
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_af6a415c-c063-4e52-ad46-ba5771169d1a/sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
: 5744db56abf24224cf1693e3e46d5bede5dd8c74199d1ade21d96d1156922237
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_af6a415c-c063-4e52-ad46-ba5771169d1a/sv-benchmarks/c/termination-memory-alloca/mult_array-alloca-2.i
language: C
specification: CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
CPAchecker 2.3 |
7 |
2023-11-30T02:59:07+01:00 |
|