Skip to content

Commit 07c6fbd

Browse files
committed
clang-format recently moved regression tests
1 parent 98c5484 commit 07c6fbd

File tree

68 files changed

+548
-483
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

68 files changed

+548
-483
lines changed

regression/cbmc/Array_Access1/main.c

Lines changed: 8 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,16 @@
11
int a[4];
22
int *p;
33

4-
int main() {
5-
int j;
4+
int main()
5+
{
6+
int j;
67

7-
a[1] = 1;
8+
a[1] = 1;
89

9-
p = a;
10-
*p = 1;
10+
p = a;
11+
*p = 1;
1112

12-
j = a[0];
13+
j = a[0];
1314

14-
assert(j == 1);
15+
assert(j == 1);
1516
}

regression/cbmc/Array_Access2/main.c

Lines changed: 12 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,20 @@
11
int a[4];
22
int *p;
33

4-
int main() {
5-
int j;
4+
int main()
5+
{
6+
int j;
67

7-
a[1] = 1;
8+
a[1] = 1;
89

9-
p = a;
10-
p++;
11-
a[0] = 1;
12-
*p = 1;
10+
p = a;
11+
p++;
12+
a[0] = 1;
13+
*p = 1;
1314

14-
j = a[0];
15-
assert(j == 1);
15+
j = a[0];
16+
assert(j == 1);
1617

17-
j = a[1];
18-
assert(j == 1);
18+
j = a[1];
19+
assert(j == 1);
1920
}

regression/cbmc/Array_Access3/main.c

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,15 @@ int main()
66
int i;
77

88
// normal
9-
a[1]=1;
9+
a[1] = 1;
1010

1111
// not normal
12-
2[a]=2;
12+
2 [a] = 2;
1313

14-
assert(a[2]==2);
14+
assert(a[2] == 2);
1515

16-
p=a;
16+
p = a;
1717

1818
// also a bit strange
19-
assert(2[p]==2);
19+
assert(2 [p] == 2);
2020
}

regression/cbmc/Array_Pointer1/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,6 @@ int main()
1717

1818
// Assignment with (dummy) cast.
1919
// The array should be zero-initialized.
20-
p=(int *)a;
21-
assert(*p==0);
20+
p = (int *)a;
21+
assert(*p == 0);
2222
}

regression/cbmc/Array_Pointer2/main.c

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
int nums[2];
22
int *p;
33

4-
int main() {
5-
nums[1] = 999;
6-
p = &nums[0];
7-
p++;
4+
int main()
5+
{
6+
nums[1] = 999;
7+
p = &nums[0];
8+
p++;
89

9-
assert(*p == 999);
10+
assert(*p == 999);
1011
}

regression/cbmc/Array_Pointer3/main.c

Lines changed: 24 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -2,30 +2,36 @@ int x, y;
22

33
int z[10];
44

5-
void h(int w) {
5+
void h(int w)
6+
{
67
x = x + 1;
78
y = y + 1;
89
}
910

10-
_Bool strict_sorted(int a[], int len, int s) {
11+
_Bool strict_sorted(int a[], int len, int s)
12+
{
1113
int i;
12-
for (i = s; i < len-1; i++) {
13-
if (a[i] >= a[i+1])
14+
for(i = s; i < len - 1; i++)
15+
{
16+
if(a[i] >= a[i + 1])
1417
return 0;
1518
}
1619
return 1;
1720
}
1821

19-
_Bool sorted(int a[], int len, int s) {
22+
_Bool sorted(int a[], int len, int s)
23+
{
2024
int i;
21-
for (i = s; i < len-1; i++) {
22-
if (a[i] > a[i+1])
25+
for(i = s; i < len - 1; i++)
26+
{
27+
if(a[i] > a[i + 1])
2328
return 0;
2429
}
2530
return 1;
2631
}
2732

28-
int g (int w) {
33+
int g(int w)
34+
{
2935
int i;
3036
int local_arr[50];
3137
assert(w >= 1);
@@ -34,11 +40,12 @@ int g (int w) {
3440
y = w;
3541
for(i = 0; i < 10; i++)
3642
z[i] = i;
37-
assert(strict_sorted(z,10,0));
43+
assert(strict_sorted(z, 10, 0));
3844
assert(x > y);
3945
}
4046

41-
int f (int j, int k) {
47+
int f(int j, int k)
48+
{
4249
int i;
4350
assert(j > k);
4451
assert(j >= 0);
@@ -49,14 +56,15 @@ int f (int j, int k) {
4956
y = k;
5057
g(j);
5158
h(j);
52-
assert(sorted(z,10,5));
59+
assert(sorted(z, 10, 5));
5360
assert(x >= y);
5461
}
5562

56-
int main () {
63+
int main()
64+
{
5765
int x, y;
58-
__CPROVER_assume (x > y);
59-
__CPROVER_assume (x >= 0);
60-
__CPROVER_assume ((y > 15) && (y < 18));
61-
f(x,y);
66+
__CPROVER_assume(x > y);
67+
__CPROVER_assume(x >= 0);
68+
__CPROVER_assume((y > 15) && (y < 18));
69+
f(x, y);
6270
}

regression/cbmc/Array_Pointer4/main.c

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ char *(a3[10]);
99

1010
int main()
1111
{
12-
assert(sizeof(int *)==4 || sizeof(int *)==8);
13-
assert(sizeof(a1)==10*sizeof(int *));
14-
assert(sizeof(a2)==sizeof(int *));
15-
assert(sizeof(a3)==10*sizeof(int *));
12+
assert(sizeof(int *) == 4 || sizeof(int *) == 8);
13+
assert(sizeof(a1) == 10 * sizeof(int *));
14+
assert(sizeof(a2) == sizeof(int *));
15+
assert(sizeof(a3) == 10 * sizeof(int *));
1616
}

regression/cbmc/Array_Pointer5/main.c

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
typedef unsigned B[8];
22

3-
void fun(B b) {
3+
void fun(B b)
4+
{
45
}
56

67
int main(void)

regression/cbmc/Array_Pointer6/main.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,10 @@ a_type *q;
77

88
int main()
99
{
10-
p=array;
11-
q=&array;
10+
p = array;
11+
q = &array;
1212
q++;
1313
q--;
1414

15-
assert(**q==*p);
15+
assert(**q == *p);
1616
}

regression/cbmc/Array_Pointer7/main.c

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,25 +2,25 @@ void f1()
22
{
33
int array1[4];
44

5-
char *p=(char *)array1;
5+
char *p = (char *)array1;
66

7-
for(unsigned i=0; i<sizeof(array1); i++)
8-
*(p+i)=i;
7+
for(unsigned i = 0; i < sizeof(array1); i++)
8+
*(p + i) = i;
99

10-
assert(array1[0]==0x03020100);
11-
assert(array1[1]==0x07060504);
10+
assert(array1[0] == 0x03020100);
11+
assert(array1[1] == 0x07060504);
1212
}
1313

1414
void f2()
1515
{
1616
int array2[4];
1717

18-
char *p=(char *)array2;
18+
char *p = (char *)array2;
1919

20-
array2[1]=0x0200;
21-
p[4]=1;
20+
array2[1] = 0x0200;
21+
p[4] = 1;
2222

23-
assert(array2[1]==0x0201);
23+
assert(array2[1] == 0x0201);
2424
}
2525

2626
int main()

0 commit comments

Comments
 (0)