This repository has been archived by the owner on Oct 3, 2021. It is now read-only.
/
mbpr4_true-unreach-call.i
92 lines (82 loc) · 1.76 KB
/
mbpr4_true-unreach-call.i
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
extern void __VERIFIER_error() __attribute__ ((__noreturn__));
extern void __VERIFIER_assume(int);
void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: __VERIFIER_error(); } }
extern int __VERIFIER_nondet_int(void);
int CELLCOUNT;
int main()
{
CELLCOUNT = __VERIFIER_nondet_int();
if(CELLCOUNT > 1)
{
int MINVAL=2;
int i;
int volArray[CELLCOUNT];
int CCCELVOL4 = 5;
int CCCELVOL3 = 7;
int CCCELVOL2 = 3;
int CCCELVOL1 = 1;
if(CELLCOUNT % 4 != 0) { return 1; }
__VERIFIER_assume(CELLCOUNT % 4 == 0);
for(i = 1; i <= CELLCOUNT/4; i++)
{
if(CCCELVOL4 >= MINVAL)
{
volArray[i*4 - 4] = CCCELVOL4;
}
else
{
volArray[i*4 - 4] = 0;
}
volArray[i*4 - 3] = volArray[i*4 - 3];
volArray[i*4 - 2] = volArray[i*4 - 2];
volArray[i*4 - 1] = volArray[i*4 - 1];
}
for(i = 1; i <= CELLCOUNT/4; i++)
{
if(CCCELVOL3 >= MINVAL)
{
volArray[i*4 - 3] = CCCELVOL3;
}
else
{
volArray[i*4 - 3] = 0;
}
volArray[i*4 - 4] = volArray[i*4 - 4];
volArray[i*4 - 2] = volArray[i*4 - 2];
volArray[i*4 - 1] = volArray[i*4 - 1];
}
for(i = 1; i <= CELLCOUNT/4; i++)
{
if(CCCELVOL2 >= MINVAL)
{
volArray[i*4 - 2] = CCCELVOL2;
}
else
{
volArray[i*4 - 2] = 0;
}
volArray[i*4 - 4] = volArray[i*4 - 4];
volArray[i*4 - 3] = volArray[i*4 - 3];
volArray[i*4 - 1] = volArray[i*4 - 1];
}
for(i = 1; i <= CELLCOUNT/4; i++)
{
if(CCCELVOL1 >= MINVAL)
{
volArray[i*4 - 1] = CCCELVOL1;
}
else
{
volArray[i*4 - 1] = 0;
}
volArray[i*4 - 4] = volArray[i*4 - 4];
volArray[i*4 - 3] = volArray[i*4 - 3];
volArray[i*4 - 2] = volArray[i*4 - 2];
}
for(i = 0; i < CELLCOUNT; i++)
{
__VERIFIER_assert(volArray[i] >= MINVAL || volArray[i] == 0 );
}
}
return 1;
}