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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
/* run.config
PLUGIN: @EVA_PLUGINS@
EXIT: 1
STDOPT: #"-cpp-extra-args=-DBITFIELD"
STDOPT: #"-cpp-extra-args=-DARRAY_DECL"
STDOPT: #"-cpp-extra-args=-DCASE_RANGE"
STDOPT: #"-cpp-extra-args=-DCASE_RANGE2"
STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR"
STDOPT: #"-cpp-extra-args=-DINIT_DESIGNATOR2"
STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR"
STDOPT: #"-cpp-extra-args=-DRANGE_DESIGNATOR2"
STDOPT: #"-cpp-extra-args=-DATTRIBUTE_CONSTANT"
STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT"
STDOPT: #"-cpp-extra-args=-DLOGIC_CONSTANT_OCTAL"
STDOPT: #"-cpp-extra-args=-DEVA_UNROLL -eva -kernel-warn-key annot-error=error"
STDOPT: #"-cpp-extra-args=-DCABS_DOWHILE"
STDOPT: #"-cpp-extra-args=-DARRAY_INIT1"
STDOPT: #"-cpp-extra-args=-DARRAY_INIT2"
STDOPT: #"-cpp-extra-args=-DARRAY_INIT3"
STDOPT: #"-cpp-extra-args=-DARRAY_INIT4"
EXIT: 0
STDOPT: #"-cpp-extra-args=-DUNROLL_PRAGMA"
*/
// Lines intentionally left blank to minimize future oracle changes
volatile int nondet;
#ifdef BITFIELD
struct st {
int bf:(999999999999999999U+9999999999999999999U);
};
#endif
#ifdef ARRAY_DECL
int arr[9999999999999999999U+18000000000000000000U];
char arr1[99999999999999999999U];
#endif
#ifdef CASE_RANGE
unsigned long nondetul;
void case_range() {
switch (nondetul)
case 0 ... 9999999999999999999U:;
case 0 ... 199999999999999999U:;
}
#endif
#ifdef CASE_RANGE2
void case_range2() {
switch (nondet)
case 0 ... 10000000U:;
}
#endif
#ifdef INIT_DESIGNATOR
int arr2[9999999999999999999U] = { [9999999999999999999U] = 42 };
#endif
#ifdef INIT_DESIGNATOR2
int arr3[1] = { [9999999999999999999U] = 42 };
#endif
#ifdef RANGE_DESIGNATOR
int arr4[1] = { [-9999999999999999999U ... 9999999999999999999U] = 42 };
#endif
#ifdef RANGE_DESIGNATOR2
int widths[] = { [99999999999999999 ... 999999999999999999] = 2 };
#endif
#ifdef ATTRIBUTE_CONSTANT
struct acst {
int a __attribute__((aligned(0x80000000000000000)));
};
#endif
typedef struct {
char a;
int b __attribute__((aligned(0x8000000000000000)));
double c __attribute__((aligned(0x8000000000000000+0x8000000000000000)));
} stt ;
//@ logic integer too_large_integer = 9999999999999999999;
#ifdef LOGIC_CONSTANT
//@ type too_large_logic_array = int[9999999999999999999U];
#endif
#ifdef LOGIC_CONSTANT_OCTAL
//@ type too_large_logic_array_octal = int[09876543210];
#endif
#ifdef ARRAY_INIT1
// Previously caused Invalid_argument(Array.make)
int a1[] = {[72057594037927936] = 0};
#endif
#ifdef ARRAY_INIT2
struct arri2 {
int a[7205759403792795];
};
struct st {
struct arri2 a;
};
// Previously caused Out of memory
struct st s = {
{{[7205759403792793 ... 7205759403792793] = 0}}
};
#endif
#ifdef ARRAY_INIT3
int ai3[] = {0xdead, [72057594037927936] = 0xbeef};
#endif
#ifdef ARRAY_INIT4
// Previously caused Out of memory
int ai4[] = {1, [7205759403792793] = 11};
#endif
int main() {
#ifdef EVA_UNROLL
//@ loop unroll (-9999999999999999999); // IntLimit
while (nondet);
//@ loop unroll too_large_integer; // ExpLimit
while (nondet);
//@ slevel 9999999999999999999;
while (nondet);
#endif
#ifdef CABS_DOWHILE
do { } while (09);
#endif
#ifdef UNROLL_PRAGMA
//@ loop pragma UNROLL 99999999999999999999;
#endif
while (nondet);
return 0;
}
|
