Skip to content

Commit 9055029

Browse files
peterschrammelpeterschrammel
committed
Clang-format cbmc-incr-oneloop tests
1 parent 2916d91 commit 9055029

File tree

32 files changed

+1760
-1176
lines changed

32 files changed

+1760
-1176
lines changed

‎regression/cbmc-incr-oneloop/alarm1/main.c

Lines changed: 455 additions & 320 deletions
Large diffs are not rendered by default.

‎regression/cbmc-incr-oneloop/alarm2/main.c

Lines changed: 454 additions & 320 deletions
Large diffs are not rendered by default.

‎regression/cbmc-incr-oneloop/alarm3/main.c

Lines changed: 455 additions & 320 deletions
Large diffs are not rendered by default.

‎regression/cbmc-incr-oneloop/arrays2/main.c

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,13 @@ int main()
22
{
33
int a[5], b[5];
44
int x;
5-
for(unsigned i = 0;i<5;i++) {
5+
for(unsigned i = 0; i < 5; i++)
6+
{
67
a[i] = b[i];
7-
if(i==3) b[i] = x;
8-
if(i>0) assert(a[i-1]==b[i-1]);
8+
if(i == 3)
9+
b[i] = x;
10+
if(i > 0)
11+
assert(a[i - 1] == b[i - 1]);
912
}
10-
assert(a[4]==b[4]);
13+
assert(a[4] == b[4]);
1114
}

‎regression/cbmc-incr-oneloop/arrays3/main.c

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,14 @@
11
int main()
22
{
33
int a[5], b[5];
4-
int x,z;
4+
int x, z;
55
unsigned y;
6-
__CPROVER_assume(2<=y && y<=3);
7-
for(unsigned i = 0;i<5;i++) {
6+
__CPROVER_assume(2 <= y && y <= 3);
7+
for(unsigned i = 0; i < 5; i++)
8+
{
89
a[i] = b[i];
9-
if(z) a[y] = x;
10-
assert(a[i]==b[i] || a[i]==x);
10+
if(z)
11+
a[y] = x;
12+
assert(a[i] == b[i] || a[i] == x);
1113
}
1214
}

‎regression/cbmc-incr-oneloop/arrays4/main.c

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,14 @@ int main()
22
{
33
int a[10], b[10];
44
int x;
5-
unsigned y,z;
6-
__CPROVER_assume(2<=y && y<=4);
7-
__CPROVER_assume(6<=z && z<=8);
5+
unsigned y, z;
6+
__CPROVER_assume(2 <= y && y <= 4);
7+
__CPROVER_assume(6 <= z && z <= 8);
88
b[y] = x;
99
b[z] = x;
10-
for(unsigned i = 0;i<10;i++) {
10+
for(unsigned i = 0; i < 10; i++)
11+
{
1112
a[i] = b[i];
1213
}
13-
assert(a[y]==a[z]);
14+
assert(a[y] == a[z]);
1415
}

‎regression/cbmc-incr-oneloop/arrays5/main.c

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,11 @@ int a[5], b[5];
33
int main()
44
{
55
unsigned x;
6-
__CPROVER_assume(0<=x && x<=4);
6+
__CPROVER_assume(0 <= x && x <= 4);
77
b[x] = x;
8-
for(unsigned i=0;i<5;i++) {
8+
for(unsigned i = 0; i < 5; i++)
9+
{
910
a[i] = b[i];
1011
}
11-
assert(a[x]==b[x]);
12+
assert(a[x] == b[x]);
1213
}

‎regression/cbmc-incr-oneloop/assertion-after-loop1/main.c

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,10 @@ extern int nondet_int();
22
int main()
33
{
44
int x = nondet_int();
5-
__CPROVER_assume(0<=x && x<=1);
6-
while(x<4) {
7-
x=x+1;
5+
__CPROVER_assume(0 <= x && x <= 1);
6+
while(x < 4)
7+
{
8+
x = x + 1;
89
}
9-
assert(x<4);
10+
assert(x < 4);
1011
}

‎regression/cbmc-incr-oneloop/assertion-after-loop2/main.c

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,10 @@ extern int nondet_int();
22
int main()
33
{
44
int x = nondet_int();
5-
__CPROVER_assume(0<=x && x<=1);
6-
while(x<4) {
7-
x=x+1;
5+
__CPROVER_assume(0 <= x && x <= 1);
6+
while(x < 4)
7+
{
8+
x = x + 1;
89
}
9-
assert(x<=4);
10+
assert(x <= 4);
1011
}

‎regression/cbmc-incr-oneloop/cruise1/main.c

Lines changed: 100 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,12 @@
1010
LNCS Volume 8254, 2013, pp 133-148 */
1111
/*******************************************************************************/
1212

13+
#include <assert.h>
1314
#include <stdio.h>
1415
#include <stdlib.h>
15-
#include <assert.h>
1616

17-
typedef struct state {
17+
typedef struct state
18+
{
1819
int mode;
1920
int speed;
2021
int button;
@@ -26,65 +27,126 @@ typedef struct state {
2627
#define I_GAS 4
2728
#define I_BRAKE 5
2829

29-
typedef struct input {
30+
typedef struct input
31+
{
3032
int signal;
3133
} t_input;
3234

33-
void init(t_state *s) {
35+
void init(t_state *s)
36+
{
3437
s->mode = 0;
3538
s->speed = 0;
3639
s->button = 0;
3740
}
3841

39-
void compute(t_input* i, t_state *s) {
40-
if((s->mode==0) && (s->speed==0) && (s->button==0)) {
41-
if((i->signal==I_ACC)||(i->signal==I_GAS)) s->speed=1;
42-
else if(i->signal==I_BUTTON) s->button=1;
42+
void compute(t_input *i, t_state *s)
43+
{
44+
if((s->mode == 0) && (s->speed == 0) && (s->button == 0))
45+
{
46+
if((i->signal == I_ACC) || (i->signal == I_GAS))
47+
s->speed = 1;
48+
else if(i->signal == I_BUTTON)
49+
s->button = 1;
4350
}
44-
else if((s->mode==0) && (s->speed==1) && (s->button==0)) {
45-
if((i->signal==I_BRAKE)||(i->signal==I_DEC)) s->speed=0;
46-
else if((i->signal==I_GAS)||(i->signal==I_ACC)) s->speed=2;
47-
else if(i->signal==I_BUTTON) { s->button=1; s->mode=1; }
51+
else if((s->mode == 0) && (s->speed == 1) && (s->button == 0))
52+
{
53+
if((i->signal == I_BRAKE) || (i->signal == I_DEC))
54+
s->speed = 0;
55+
else if((i->signal == I_GAS) || (i->signal == I_ACC))
56+
s->speed = 2;
57+
else if(i->signal == I_BUTTON)
58+
{
59+
s->button = 1;
60+
s->mode = 1;
61+
}
4862
}
49-
else if((s->mode==0) && (s->speed==0) && (s->button==1)) {
50-
if((i->signal==I_GAS)||(i->signal==I_ACC)) {s->speed=1; s->mode=1; }
51-
else if(i->signal==I_BUTTON) s->button=0;
63+
else if((s->mode == 0) && (s->speed == 0) && (s->button == 1))
64+
{
65+
if((i->signal == I_GAS) || (i->signal == I_ACC))
66+
{
67+
s->speed = 1;
68+
s->mode = 1;
69+
}
70+
else if(i->signal == I_BUTTON)
71+
s->button = 0;
5272
}
53-
else if((s->mode==1) && (s->speed==1) && (s->button==1)) {
54-
if(i->signal==I_GAS) { s->speed=2; s->mode=2; }
55-
else if(i->signal==I_BRAKE) { s->speed=0; s->mode=2; }
56-
else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; }
73+
else if((s->mode == 1) && (s->speed == 1) && (s->button == 1))
74+
{
75+
if(i->signal == I_GAS)
76+
{
77+
s->speed = 2;
78+
s->mode = 2;
79+
}
80+
else if(i->signal == I_BRAKE)
81+
{
82+
s->speed = 0;
83+
s->mode = 2;
84+
}
85+
else if(i->signal == I_BUTTON)
86+
{
87+
s->mode = 0;
88+
s->button = 0;
89+
}
5790
}
58-
else if((s->mode==2) && (s->speed==2) && (s->button==1)) {
59-
if((i->signal==I_BRAKE)||(i->signal==I_DEC)) { s->speed=1; s->mode=1; }
60-
else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; }
91+
else if((s->mode == 2) && (s->speed == 2) && (s->button == 1))
92+
{
93+
if((i->signal == I_BRAKE) || (i->signal == I_DEC))
94+
{
95+
s->speed = 1;
96+
s->mode = 1;
97+
}
98+
else if(i->signal == I_BUTTON)
99+
{
100+
s->mode = 0;
101+
s->button = 0;
102+
}
61103
}
62-
else if((s->mode==2) && (s->speed==0) && (s->button==1)) {
63-
if((i->signal==I_GAS)||(i->signal==I_ACC)) { s->speed=1; s->mode=1; }
64-
else if(i->signal==I_BUTTON) { s->mode=0; s->button=0; }
104+
else if((s->mode == 2) && (s->speed == 0) && (s->button == 1))
105+
{
106+
if((i->signal == I_GAS) || (i->signal == I_ACC))
107+
{
108+
s->speed = 1;
109+
s->mode = 1;
110+
}
111+
else if(i->signal == I_BUTTON)
112+
{
113+
s->mode = 0;
114+
s->button = 0;
115+
}
65116
}
66-
else if((s->mode==0) && (s->speed==2) && (s->button==0)) {
67-
if((i->signal==I_BRAKE)||(i->signal==I_DEC)) s->speed=1;
68-
else if(i->signal==I_BUTTON) s->button=1;
117+
else if((s->mode == 0) && (s->speed == 2) && (s->button == 0))
118+
{
119+
if((i->signal == I_BRAKE) || (i->signal == I_DEC))
120+
s->speed = 1;
121+
else if(i->signal == I_BUTTON)
122+
s->button = 1;
69123
}
70-
else if((s->mode==0) && (s->speed==2) && (s->button==1)) {
71-
if((i->signal==I_BRAKE)||(i->signal==I_DEC)) { s->speed=1; s->mode=1; }
72-
else if(i->signal==I_BUTTON) s->button=0;
124+
else if((s->mode == 0) && (s->speed == 2) && (s->button == 1))
125+
{
126+
if((i->signal == I_BRAKE) || (i->signal == I_DEC))
127+
{
128+
s->speed = 1;
129+
s->mode = 1;
130+
}
131+
else if(i->signal == I_BUTTON)
132+
s->button = 0;
73133
}
74134
}
75135

76-
77136
extern t_input nondet_input();
78137

79-
void main() {
138+
void main()
139+
{
80140
t_state s;
81141
init(&s);
82-
while(1) {
142+
while(1)
143+
{
83144
t_input i = nondet_input();
84-
__CPROVER_assume((1<=i.signal) && (i.signal<=5));
145+
__CPROVER_assume((1 <= i.signal) && (i.signal <= 5));
85146
t_state s_old = s;
86-
compute(&i,&s);
87-
assert(!(s_old.mode==2 && s_old.speed==2 && i.signal==I_DEC) ||
88-
s.mode==1);
147+
compute(&i, &s);
148+
assert(
149+
!(s_old.mode == 2 && s_old.speed == 2 && i.signal == I_DEC) ||
150+
s.mode == 1);
89151
}
90152
}

0 commit comments

Comments
 (0)