Skip to content

Commit c324573

Browse files
tautschnigtautschnig
committed
clang-format recently moved tests
1 parent 94138b5 commit c324573

File tree

20 files changed

+420
-323
lines changed

20 files changed

+420
-323
lines changed

‎regression/cbmc/Array_UF1/main.c‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,14 @@
11
int main()
22
{
33
int a[10], b[10];
4-
int x,y,z;
5-
__CPROVER_assume(2<=y && y<=4);
6-
__CPROVER_assume(6<=z && z<=8);
4+
int x, y, z;
5+
__CPROVER_assume(2 <= y && y <= 4);
6+
__CPROVER_assume(6 <= z && z <= 8);
77
b[y] = x;
88
b[z] = x;
9-
for(unsigned i = 0;i<10;i++) {
9+
for(unsigned i = 0; i < 10; i++)
10+
{
1011
a[i] = b[i];
1112
}
12-
__CPROVER_assert(a[y]==a[z], "a[y]==a[z]");
13+
__CPROVER_assert(a[y] == a[z], "a[y]==a[z]");
1314
}

‎regression/cbmc/Array_UF10/main.c‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,20 +2,25 @@ extern void __VERIFIER_error();
22

33
int __VERIFIER_nondet_int();
44

5-
char x[100], y[100];
6-
int i,j,k;
5+
char x[100], y[100];
6+
int i, j, k;
77

8-
void main() {
8+
void main()
9+
{
910
k = __VERIFIER_nondet_int();
1011

1112
i = 0;
12-
while(x[i] != 0){
13+
while(x[i] != 0)
14+
{
1315
y[i] = x[i];
1416
i++;
1517
}
1618
y[i] = 0;
1719

1820
if(k >= 0 && k < i)
1921
if(y[k] == 0)
20-
{ERROR: __VERIFIER_error();}
22+
{
23+
ERROR:
24+
__VERIFIER_error();
25+
}
2126
}

‎regression/cbmc/Array_UF11/main.c‎

Lines changed: 21 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,33 @@
11
extern void __VERIFIER_error();
22

3-
void __VERIFIER_assert(int cond) {
4-
if (!(cond)) {
5-
ERROR: __VERIFIER_error();
3+
void __VERIFIER_assert(int cond)
4+
{
5+
if(!(cond))
6+
{
7+
ERROR:
8+
__VERIFIER_error();
69
}
710
return;
811
}
912

1013
_Bool __VERIFIER_nondet_bool();
1114

12-
int main(){
13-
int a[5];
14-
int len=0;
15-
_Bool c=__VERIFIER_nondet_bool();
16-
int i;
15+
int main()
16+
{
17+
int a[5];
18+
int len = 0;
19+
_Bool c = __VERIFIER_nondet_bool();
20+
int i;
1721

22+
while(c)
23+
{
24+
if(len == 4)
25+
len = 0;
1826

19-
while(c){
20-
21-
if (len==4)
22-
len =0;
23-
24-
a[len]=0;
25-
26-
len++;
27-
}
28-
__VERIFIER_assert(len==5);
29-
return 1;
30-
27+
a[len] = 0;
3128

29+
len++;
30+
}
31+
__VERIFIER_assert(len == 5);
32+
return 1;
3233
}

‎regression/cbmc/Array_UF12/main.c‎

Lines changed: 34 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,40 +1,47 @@
11
extern void __VERIFIER_error();
22

3-
void __VERIFIER_assert(int cond) {
4-
if (!(cond)) {
5-
ERROR: __VERIFIER_error();
3+
void __VERIFIER_assert(int cond)
4+
{
5+
if(!(cond))
6+
{
7+
ERROR:
8+
__VERIFIER_error();
69
}
710
return;
811
}
912
int b;
1013
_Bool __VERIFIER_nondet_bool();
11-
int main(){
12-
_Bool k=__VERIFIER_nondet_bool();
13-
int i,n,j;
14-
int a[1025];
14+
int main()
15+
{
16+
_Bool k = __VERIFIER_nondet_bool();
17+
int i, n, j;
18+
int a[1025];
1519

16-
if (k){
17-
n=0;
18-
} else {
19-
n=1023;
20-
}
21-
22-
i=0;
20+
if(k)
21+
{
22+
n = 0;
23+
}
24+
else
25+
{
26+
n = 1023;
27+
}
2328

24-
while ( i <= n){
25-
i++;
26-
j= j +2;
27-
}
29+
i = 0;
2830

29-
a[i]=0;
30-
a[j]=0;
31-
__VERIFIER_assert(j<1025);
32-
a[b]=0;
33-
if (b >= 0 && b < 1023)
34-
a[b]=1;
35-
else
36-
a[b%1023] =1;
31+
while(i <= n)
32+
{
33+
i++;
34+
j = j + 2;
35+
}
3736

38-
return 1;
37+
a[i] = 0;
38+
a[j] = 0;
39+
__VERIFIER_assert(j < 1025);
40+
a[b] = 0;
41+
if(b >= 0 && b < 1023)
42+
a[b] = 1;
43+
else
44+
a[b % 1023] = 1;
3945

46+
return 1;
4047
}

‎regression/cbmc/Array_UF13/main.c‎

Lines changed: 15 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,34 @@
11
extern void __VERIFIER_error();
22

3-
void __VERIFIER_assert(int cond) {
4-
if (!(cond)) {
5-
ERROR: __VERIFIER_error();
3+
void __VERIFIER_assert(int cond)
4+
{
5+
if(!(cond))
6+
{
7+
ERROR:
8+
__VERIFIER_error();
69
}
710
return;
811
}
912
int __VERIFIER_nondet_int();
1013

11-
char x[100], y[100];
12-
int i,j,k;
14+
char x[100], y[100];
15+
int i, j, k;
1316

14-
void main() {
17+
void main()
18+
{
1519
k = __VERIFIER_nondet_int();
1620

1721
i = 0;
18-
while(x[i] != 0){
22+
while(x[i] != 0)
23+
{
1924
y[i] = x[i];
2025
i++;
2126
}
2227
y[i] = 0;
2328

2429
if(k >= 0 && k < i)
2530
if(y[k] != 0)
26-
{__VERIFIER_assert(0);}
31+
{
32+
__VERIFIER_assert(0);
33+
}
2734
}

‎regression/cbmc/Array_UF14/main.c‎

Lines changed: 22 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,59 +1,57 @@
11
extern void __VERIFIER_error();
22

33
extern void __VERIFIER_assume(int);
4-
void __VERIFIER_assert(int cond) {
5-
if (!(cond)) {
6-
ERROR: __VERIFIER_error();
4+
void __VERIFIER_assert(int cond)
5+
{
6+
if(!(cond))
7+
{
8+
ERROR:
9+
__VERIFIER_error();
710
}
811
return;
912
}
1013

11-
12-
1314
extern char __VERIFIER_nondet_char();
1415

1516
main()
1617
{
1718
char string_A[5], string_B[5];
18-
int i, j, nc_A, nc_B, found=0;
19+
int i, j, nc_A, nc_B, found = 0;
1920

21+
for(i = 0; i < 5; i++)
22+
string_A[i] = __VERIFIER_nondet_char();
23+
__VERIFIER_assume(string_A[5 - 1] == '\0');
2024

21-
for(i=0; i<5; i++)
22-
string_A[i]=__VERIFIER_nondet_char();
23-
__VERIFIER_assume(string_A[5 -1]=='\0');
24-
25-
for(i=0; i<5; i++)
26-
string_B[i]=__VERIFIER_nondet_char();
27-
__VERIFIER_assume(string_B[5 -1]=='\0');
25+
for(i = 0; i < 5; i++)
26+
string_B[i] = __VERIFIER_nondet_char();
27+
__VERIFIER_assume(string_B[5 - 1] == '\0');
2828

2929
nc_A = 0;
30-
while(string_A[nc_A]!='\0')
30+
while(string_A[nc_A] != '\0')
3131
nc_A++;
3232

3333
nc_B = 0;
34-
while(string_B[nc_B]!='\0')
34+
while(string_B[nc_B] != '\0')
3535
nc_B++;
3636

3737
__VERIFIER_assume(nc_B >= nc_A);
3838

39-
40-
i=j=0;
41-
while((i<nc_A) && (j<nc_B))
39+
i = j = 0;
40+
while((i < nc_A) && (j < nc_B))
4241
{
4342
if(string_A[i] == string_B[j])
4443
{
45-
i++;
46-
j++;
44+
i++;
45+
j++;
4746
}
4847
else
4948
{
50-
i = i-j+1;
51-
j = 0;
49+
i = i - j + 1;
50+
j = 0;
5251
}
5352
}
5453

55-
found = (j>nc_B-1)<<i;
54+
found = (j > nc_B - 1) << i;
5655

5756
__VERIFIER_assert(found == 0 || found == 1);
58-
5957
}

‎regression/cbmc/Array_UF15/main.c‎

Lines changed: 22 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,56 +1,57 @@
11
extern void __VERIFIER_error();
22

33
extern void __VERIFIER_assume(int);
4-
void __VERIFIER_assert(int cond) {
5-
if (!(cond)) {
6-
ERROR: __VERIFIER_error();
4+
void __VERIFIER_assert(int cond)
5+
{
6+
if(!(cond))
7+
{
8+
ERROR:
9+
__VERIFIER_error();
710
}
811
return;
912
}
1013

11-
1214
extern char __VERIFIER_nondet_char();
1315

1416
main()
1517
{
1618
char string_A[5], string_B[5];
17-
int i, j, nc_A, nc_B, found=0;
19+
int i, j, nc_A, nc_B, found = 0;
1820

19-
for(i=0; i<5; i++)
20-
string_A[i]=__VERIFIER_nondet_char();
21-
__VERIFIER_assume(string_A[5 -1]=='\0');
21+
for(i = 0; i < 5; i++)
22+
string_A[i] = __VERIFIER_nondet_char();
23+
__VERIFIER_assume(string_A[5 - 1] == '\0');
2224

23-
for(i=0; i<5; i++)
24-
string_B[i]=__VERIFIER_nondet_char();
25-
__VERIFIER_assume(string_B[5 -1]=='\0');
25+
for(i = 0; i < 5; i++)
26+
string_B[i] = __VERIFIER_nondet_char();
27+
__VERIFIER_assume(string_B[5 - 1] == '\0');
2628

2729
nc_A = 0;
28-
while(string_A[nc_A]!='\0')
30+
while(string_A[nc_A] != '\0')
2931
nc_A++;
3032

3133
nc_B = 0;
32-
while(string_B[nc_B]!='\0')
34+
while(string_B[nc_B] != '\0')
3335
nc_B++;
3436

3537
__VERIFIER_assume(nc_B >= nc_A);
3638

37-
38-
i=j=0;
39-
while((i<nc_A) && (j<nc_B))
39+
i = j = 0;
40+
while((i < nc_A) && (j < nc_B))
4041
{
4142
if(string_A[i] == string_B[j])
4243
{
43-
i++;
44-
j++;
44+
i++;
45+
j++;
4546
}
4647
else
4748
{
48-
i = i-j+1;
49-
j = 0;
49+
i = i - j + 1;
50+
j = 0;
5051
}
5152
}
5253

53-
found = (j>nc_B-1);
54+
found = (j > nc_B - 1);
5455

5556
__VERIFIER_assert(found == 0 || found == 1);
5657
}

0 commit comments

Comments
 (0)