b77e058 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
violation_witness |
frama-c-sv version 0.4.0 |
3 |
2023-12-03T06:22:34Z |
|
d5be043 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
VeriOover |
1 |
2023-12-20T03:37 CET (comp) |
|
704d750 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Taipan |
5 |
2023-12-02T15:25:11Z |
|
bdb1d83 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Kojak |
5 |
2023-12-02T20:50:57Z |
|
1513234 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-20T03:55:56+01:00 |
d5be043 |
4917103 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-19T04:06:50+01:00 |
dea60e7 |
c36b6d9 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T12:01:10+01:00 |
704d750 |
9d03c26 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-04T01:48:29+01:00 |
c14fe74 |
222ae2b |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T09:58:00+01:00 |
b77e058 |
67b7578 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-12-03T06:19:17+01:00 |
bdb1d83 |
9d17721 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-30T12:57:43+01:00 |
a7a97ca |
a7a97ca |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
4 |
2023-11-30T07:57:11+01:00 |
|
c1604d5 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.3 |
5 |
2023-11-29T08:33:30+01:00 |
6fa1f64 |
c14fe74 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
4 |
2023-12-03T22:19:21+01:00 |
|
dea60e7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
4 |
2023-12-19T00:03:40+01:00 |
|
6fa1f64 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
Automizer |
5 |
2023-11-29T03:16:57Z |
|
4a518be |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: c8c22e4f-19b3-41fe-9c63-f3e855e78903
creation_time: '2023-11-29T04:16:57+01:00'
producer:
name: Automizer
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e92a614-134f-46de-8033-950395deae14/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_7e92a614-134f-46de-8033-950395deae14/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
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_7e92a614-134f-46de-8033-950395deae14/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
file_hash: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
line: 16
column: 0
function: main
value: ((x <= 2147483647) && (0 <= (x + 1)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-11-29T08:02:13+01:00 |
|
e179f77 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: b8e604bb-4e4d-4166-b9a5-23cfd11f8856
creation_time: '2023-12-02T21:50:57+01:00'
producer:
name: Kojak
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_eba80934-5b49-4bed-b0f4-7b572de1099a/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_eba80934-5b49-4bed-b0f4-7b572de1099a/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
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_eba80934-5b49-4bed-b0f4-7b572de1099a/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
file_hash: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
line: 16
column: 0
function: main
value: (((x <= 2147483647) && (1 <= x)) || ((x < 1) && (0 <= (x + 1))))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-03T05:51:48+01:00 |
|
93d5583 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: '2.0'
uuid: 12fe02ef-df5c-444f-81d3-b69d2d4d3df2
creation_time: '2023-12-02T16:25:12+01:00'
producer:
name: Taipan
version: 0.2.4-dev-0e0057c
task:
input_files:
- /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_49473b37-5680-4224-8ad0-7c453e6324de/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
input_file_hashes:
? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_49473b37-5680-4224-8ad0-7c453e6324de/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
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_49473b37-5680-4224-8ad0-7c453e6324de/sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
file_hash: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
line: 16
column: 0
function: main
value: ((x <= 2147483647) && (0 <= (x + 1)))
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
6 |
2023-12-04T12:19:20+01:00 |
|
727e315 |
Inspect |
|
- entry_type: invariant_set
metadata:
format_version: "2.0"
uuid: 511e247f-f30f-4ca7-9b1a-f4c72b2ae22d
creation_time: 2023-12-01T01:12:45Z
producer:
name: Goblint
version: tags/svcomp24-0-gc2e9465a7
command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification''
''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture''
''64bit'' ''../../sv-benchmarks/c/termination-crafted/Cairo_step2-1.c'''
task:
input_files:
- ../../sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
input_file_hashes:
../../sv-benchmarks/c/termination-crafted/Cairo_step2-1.c: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
data_model: LP64
language: C
specification: CHECK( init(main()), LTL(G ! overflow) )
content:
- invariant:
type: loop_invariant
location:
file_name: ../../sv-benchmarks/c/termination-crafted/Cairo_step2-1.c
file_hash: 709a9fb1525fc89256c547fbe03fef24399be5d6458f17d55fb4fce36419b886
line: 16
column: 12
function: main
value: (((((x != -3 && x != -2) && ((((((x != -5 && x != -4) && ((((((x != -7
&& x != -6) && ((((((x != -9 && x != -8) && ((((((x != -11 && x != -10) &&
((((((x != -13 && x != -12) && ((((((x != -15 && x != -14) && ((((((x != -17
&& x != -16) && ((((((x != -19 && x != -18) && ((((((x != -21 && x != -20)
&& ((((((x != -23 && x != -22) && ((((((x != -25 && x != -24) && (((((-24
<= x && x <= 2147483621) && x != -27) && x != -26) || ((-22 <= x && x <= 2147483623)
&& x != 0)) || (-22 <= x && x <= 2147483623))) || ((-20 <= x && x <= 2147483625)
&& x != 0)) || (-20 <= x && x <= 2147483625)) || (((((((((((((((((((((((((((((x
<= 2147483597 && x != -51) && x != -50) && x != -49) && x != -48) && x !=
-47) && x != -46) && x != -45) && x != -44) && x != -43) && x != -42) && x
!= -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36) &&
x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30)
&& x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24)
&& x != 0)) || ((((((((((((((((((((((((((((x <= 2147483597 && x != -51) &&
x != -50) && x != -49) && x != -48) && x != -47) && x != -46) && x != -45)
&& x != -44) && x != -43) && x != -42) && x != -41) && x != -40) && x != -39)
&& x != -38) && x != -37) && x != -36) && x != -35) && x != -34) && x != -33)
&& x != -32) && x != -31) && x != -30) && x != -29) && x != -28) && x != -27)
&& x != -26) && x != -25) && x != -24))) || ((-18 <= x && x <= 2147483627)
&& x != 0)) || (-18 <= x && x <= 2147483627)) || ((((((((((((((((((((((((((((((-46
<= x && x <= 2147483599) && x != -49) && x != -48) && x != -47) && x != -46)
&& x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40)
&& x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34)
&& x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28)
&& x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22)
&& x != 0)) || (((((((((((((((((((((((((((((-46 <= x && x <= 2147483599) &&
x != -49) && x != -48) && x != -47) && x != -46) && x != -45) && x != -44)
&& x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38)
&& x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32)
&& x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26)
&& x != -25) && x != -24) && x != -23) && x != -22))) || ((-16 <= x && x <=
2147483629) && x != 0)) || (-16 <= x && x <= 2147483629)) || ((((((((((((((((((((((((((((((-44
<= x && x <= 2147483601) && x != -47) && x != -46) && x != -45) && x != -44)
&& x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38)
&& x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32)
&& x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26)
&& x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20)
&& x != 0)) || (((((((((((((((((((((((((((((-44 <= x && x <= 2147483601) &&
x != -47) && x != -46) && x != -45) && x != -44) && x != -43) && x != -42)
&& x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36)
&& x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30)
&& x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20))) || ((-14 <= x && x <=
2147483631) && x != 0)) || (-14 <= x && x <= 2147483631)) || ((((((((((((((((((((((((((((((-42
<= x && x <= 2147483603) && x != -45) && x != -44) && x != -43) && x != -42)
&& x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36)
&& x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30)
&& x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18)
&& x != 0)) || (((((((((((((((((((((((((((((-42 <= x && x <= 2147483603) &&
x != -45) && x != -44) && x != -43) && x != -42) && x != -41) && x != -40)
&& x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34)
&& x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28)
&& x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22)
&& x != -21) && x != -20) && x != -19) && x != -18))) || ((-12 <= x && x <=
2147483633) && x != 0)) || (-12 <= x && x <= 2147483633)) || ((((((((((((((((((((((((((((((-40
<= x && x <= 2147483605) && x != -43) && x != -42) && x != -41) && x != -40)
&& x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34)
&& x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28)
&& x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22)
&& x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16)
&& x != 0)) || (((((((((((((((((((((((((((((-40 <= x && x <= 2147483605) &&
x != -43) && x != -42) && x != -41) && x != -40) && x != -39) && x != -38)
&& x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32)
&& x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26)
&& x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20)
&& x != -19) && x != -18) && x != -17) && x != -16))) || ((-10 <= x && x <=
2147483635) && x != 0)) || (-10 <= x && x <= 2147483635)) || ((((((((((((((((((((((((((((((-38
<= x && x <= 2147483607) && x != -41) && x != -40) && x != -39) && x != -38)
&& x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32)
&& x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26)
&& x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20)
&& x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14)
&& x != 0)) || (((((((((((((((((((((((((((((-38 <= x && x <= 2147483607) &&
x != -41) && x != -40) && x != -39) && x != -38) && x != -37) && x != -36)
&& x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30)
&& x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18)
&& x != -17) && x != -16) && x != -15) && x != -14))) || ((-8 <= x && x <=
2147483637) && x != 0)) || (-8 <= x && x <= 2147483637)) || ((((((((((((((((((((((((((((((-36
<= x && x <= 2147483609) && x != -39) && x != -38) && x != -37) && x != -36)
&& x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30)
&& x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18)
&& x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12)
&& x != 0)) || (((((((((((((((((((((((((((((-36 <= x && x <= 2147483609) &&
x != -39) && x != -38) && x != -37) && x != -36) && x != -35) && x != -34)
&& x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28)
&& x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22)
&& x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16)
&& x != -15) && x != -14) && x != -13) && x != -12))) || ((-6 <= x && x <=
2147483639) && x != 0)) || (-6 <= x && x <= 2147483639)) || ((((((((((((((((((((((((((((((-34
<= x && x <= 2147483611) && x != -37) && x != -36) && x != -35) && x != -34)
&& x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28)
&& x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22)
&& x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16)
&& x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10)
&& x != 0)) || (((((((((((((((((((((((((((((-34 <= x && x <= 2147483611) &&
x != -37) && x != -36) && x != -35) && x != -34) && x != -33) && x != -32)
&& x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26)
&& x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20)
&& x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14)
&& x != -13) && x != -12) && x != -11) && x != -10))) || ((-4 <= x && x <=
2147483641) && x != 0)) || (-4 <= x && x <= 2147483641)) || ((((((((((((((((((((((((((((((-32
<= x && x <= 2147483613) && x != -35) && x != -34) && x != -33) && x != -32)
&& x != -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26)
&& x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20)
&& x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14)
&& x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8)
&& x != 0)) || (((((((((((((((((((((((((((((-32 <= x && x <= 2147483613) &&
x != -35) && x != -34) && x != -33) && x != -32) && x != -31) && x != -30)
&& x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18)
&& x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12)
&& x != -11) && x != -10) && x != -9) && x != -8))) || ((-2 <= x && x <= 2147483643)
&& x != 0)) || (-2 <= x && x <= 2147483643)) || ((((((((((((((((((((((((((((((-30
<= x && x <= 2147483615) && x != -33) && x != -32) && x != -31) && x != -30)
&& x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18)
&& x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12)
&& x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6)
&& x != 0)) || (((((((((((((((((((((((((((((-30 <= x && x <= 2147483615) &&
x != -33) && x != -32) && x != -31) && x != -30) && x != -29) && x != -28)
&& x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22)
&& x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16)
&& x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10)
&& x != -9) && x != -8) && x != -7) && x != -6))) || ((-1 <= x && x <= 2147483645)
&& x != 0)) || (-1 <= x && x <= 2147483645)) || ((((((((((((((((((((((((((((((-28
<= x && x <= 2147483617) && x != -31) && x != -30) && x != -29) && x != -28)
&& x != -27) && x != -26) && x != -25) && x != -24) && x != -23) && x != -22)
&& x != -21) && x != -20) && x != -19) && x != -18) && x != -17) && x != -16)
&& x != -15) && x != -14) && x != -13) && x != -12) && x != -11) && x != -10)
&& x != -9) && x != -8) && x != -7) && x != -6) && x != -5) && x != -4) &&
x != 0)) || (((((((((((((((((((((((((((((-28 <= x && x <= 2147483617) && x
!= -31) && x != -30) && x != -29) && x != -28) && x != -27) && x != -26) &&
x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20)
&& x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14)
&& x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8)
&& x != -7) && x != -6) && x != -5) && x != -4))) || (1 <= x && x != 0)) ||
(1 <= x && x != 0)) || ((((((((((((((((((((((((((((((-26 <= x && x <= 2147483619)
&& x != -29) && x != -28) && x != -27) && x != -26) && x != -25) && x != -24)
&& x != -23) && x != -22) && x != -21) && x != -20) && x != -19) && x != -18)
&& x != -17) && x != -16) && x != -15) && x != -14) && x != -13) && x != -12)
&& x != -11) && x != -10) && x != -9) && x != -8) && x != -7) && x != -6)
&& x != -5) && x != -4) && x != -3) && x != -2) && x != 0)) || (((((((((((((((((((((((((((((-26
<= x && x <= 2147483619) && x != -29) && x != -28) && x != -27) && x != -26)
&& x != -25) && x != -24) && x != -23) && x != -22) && x != -21) && x != -20)
&& x != -19) && x != -18) && x != -17) && x != -16) && x != -15) && x != -14)
&& x != -13) && x != -12) && x != -11) && x != -10) && x != -9) && x != -8)
&& x != -7) && x != -6) && x != -5) && x != -4) && x != -3) && x != -2)
format: c_expression |
correctness_witness |
CPAchecker 2.3 |
25 |
2023-12-01T05:18:21+01:00 |
|