source: CIVL/mods/dev.civl.com/examples/svcomp17/assume_with_disjuncts.c@ cb4d4f4

main test-branch
Last change on this file since cb4d4f4 was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 8.2 KB
Line 
1int num_of_inputs_at_223 = 5; int INPUTS_at_223[5]; int input_at_223_counter = 0;int LbranchIdx = 0;int Lbranch[12] = {1,1,1,1,1,1,0,0,0,0,0,0};
2extern void __VERIFIER_error () __attribute__ ((__noreturn__));
3extern void __VERIFIER_assume (int);
4extern int __VERIFIER_nondet_int ();
5
6void error (void) {
7 {
8__VERIFIER_assume(!((0 == INPUTS_at_223[0]) || (0 == INPUTS_at_223[1]) || (0 == INPUTS_at_223[2]) || (0 == INPUTS_at_223[3]) || (0 == INPUTS_at_223[4])));__VERIFIER_error ();
9 return;
10 }
11}
12
13int q_buf_0;
14int q_free;
15int q_read_ev;
16int q_write_ev;
17int p_num_write;
18int p_last_write;
19int p_dw_st;
20int p_dw_pc;
21int p_dw_i;
22int c_num_read;
23int c_last_read;
24int c_dr_st;
25int c_dr_pc;
26int c_dr_i;
27
28int is_do_write_p_triggered (void) {
29 int __retres1;
30 {
31 if ((int) p_dw_pc == 1) {
32 if ((int) q_read_ev == 1) {
33 __retres1 = 1;
34 goto return_label;
35 }
36 else {
37 }
38 }
39 else {
40 }
41 __retres1 = 0;
42 return_label : return (__retres1);
43 }
44}
45
46int is_do_read_c_triggered (void) {
47 int __retres1;
48 {
49 if ((int) c_dr_pc == 1) {
50 if ((int) q_write_ev == 1) {
51 __retres1 = 1;
52 goto return_label;
53 }
54 else {
55 }
56 }
57 else {
58 }
59 __retres1 = 0;
60 return_label : return (__retres1);
61 }
62}
63
64void immediate_notify_threads (void) {
65 int tmp;
66 int tmp___0;
67 {
68 {
69 tmp = is_do_write_p_triggered ();
70 }
71 if (tmp) {
72 p_dw_st = 0;
73 }
74 else {
75 }
76 {
77 tmp___0 = is_do_read_c_triggered ();
78 }
79 if (tmp___0) {
80 c_dr_st = 0;
81 }
82 else {
83 }
84 return;
85 }
86}
87
88void do_write_p (void) {
89 {
90 if ((int) p_dw_pc == 0) {
91 goto DW_ENTRY;
92 }
93 else {
94 if ((int) p_dw_pc == 1) {
95 goto DW_WAIT_READ;
96 }
97 else {
98 }
99 }
100 DW_ENTRY : {
101 while (1) {
102 while_0_continue :;
103 if ((int) q_free == 0) {
104 p_dw_st = 2;
105 p_dw_pc = 1;
106 goto return_label;
107 DW_WAIT_READ :;
108 }
109 else {
110 }
111 {
112 q_buf_0 = __VERIFIER_nondet_int ();
113 p_last_write = q_buf_0;
114 p_num_write += 1;
115 q_free = 0;
116 q_write_ev = 1;
117 immediate_notify_threads ();
118 q_write_ev = 2;
119 }
120 }
121 while_0_break :;
122 }
123 return_label : return;
124 }
125}
126
127static int a_t;
128
129void do_read_c (void) {
130 int a;
131 {
132 if ((int) c_dr_pc == 0) {
133 goto DR_ENTRY;
134 }
135 else {
136 if ((int) c_dr_pc == 1) {
137 goto DR_WAIT_WRITE;
138 }
139 else {
140 }
141 }
142 DR_ENTRY : {
143 while (1) {
144 while_1_continue :;
145 if ((int) q_free == 1) {
146 c_dr_st = 2;
147 c_dr_pc = 1;
148 a_t = a;
149 goto return_label;
150 DR_WAIT_WRITE : a = a_t;
151 }
152 else {
153 }
154 {
155 a = q_buf_0;
156 c_last_read = a;
157 c_num_read += 1;
158 q_free = 1;
159 q_read_ev = 1;
160 immediate_notify_threads ();
161 q_read_ev = 2;
162 }
163 if (p_last_write == c_last_read) {
164 if (p_num_write == c_num_read) {
165 }
166 else {
167 {
168 error ();
169 }
170 }
171 }
172 else {
173 {
174 error ();
175 }
176 }
177 }
178 while_1_break :;
179 }
180 return_label : return;
181 }
182}
183
184void init_threads (void) {
185 {
186 __VERIFIER_assume (Lbranch [LbranchIdx ++] ? (int) p_dw_i == 1 : ! ((int) p_dw_i == 1)); if ((int) p_dw_i == 1) {
187 p_dw_st = 0;
188 }
189 else {
190 p_dw_st = 2;
191 }
192 __VERIFIER_assume (Lbranch [LbranchIdx ++] ? (int) c_dr_i == 1 : ! ((int) c_dr_i == 1)); if ((int) c_dr_i == 1) {
193 c_dr_st = 0;
194 }
195 else {
196 c_dr_st = 2;
197 }
198 return;
199 }
200}
201
202int exists_runnable_thread (void) {
203 int __retres1;
204 {
205 __VERIFIER_assume (Lbranch [LbranchIdx ++] ? (int) p_dw_st == 0 : ! ((int) p_dw_st == 0)); if ((int) p_dw_st == 0) {
206 __retres1 = 1;
207 goto return_label;
208 }
209 else {
210 if ((int) c_dr_st == 0) {
211 __retres1 = 1;
212 goto return_label;
213 }
214 else {
215 }
216 }
217 __retres1 = 0;
218 return_label : return (__retres1);
219 }
220}
221
222void eval (void) {
223 int tmp;
224 int tmp___0;
225 int tmp___1;
226 {
227 {
228 while (1) {
229 while_2_continue :;
230 {
231 tmp___1 = exists_runnable_thread ();
232 }
233 __VERIFIER_assume (Lbranch [LbranchIdx ++] ? tmp___1 : ! (tmp___1)); if (tmp___1) {
234 }
235 else {
236 goto while_2_break;
237 }
238 __VERIFIER_assume (Lbranch [LbranchIdx ++] ? (int) p_dw_st == 0 : ! ((int) p_dw_st == 0)); if ((int) p_dw_st == 0) {
239 {
240 tmp = __VERIFIER_nondet_int ();
241 }
242 __VERIFIER_assume (Lbranch [LbranchIdx ++] ? tmp : ! (tmp)); if (tmp) {
243 {
244 p_dw_st = 1;
245 do_write_p ();
246 }
247 }
248 else {
249 error ();
250 }
251 }
252 else {
253 }
254 if ((int) c_dr_st == 0) {
255 {
256 tmp___0 = __VERIFIER_nondet_int ();
257 }
258 if (tmp___0) {
259 {
260 c_dr_st = 1;
261 do_read_c ();
262 }
263 }
264 else {
265 }
266 }
267 else {
268 }
269 }
270 while_2_break :;
271 }
272 return;
273 }
274}
275
276int stop_simulation (void) {
277 int tmp;
278 int __retres2;
279 {
280 {
281 tmp = exists_runnable_thread ();
282 }
283 if (tmp) {
284 __retres2 = 0;
285 goto return_label;
286 }
287 else {
288 }
289 __retres2 = 1;
290 return_label : return (__retres2);
291 }
292}
293
294void start_simulation (void) {
295 int kernel_st;
296 int tmp;
297 {
298 {
299 kernel_st = 0;
300 init_threads ();
301 }
302 {
303 int foo = 1;
304 while (1) {__VERIFIER_assume (Lbranch [LbranchIdx ++] ? foo : ! (foo)); if (! (foo)) break; {
305 while_3_continue :;
306 {
307 kernel_st = 1;
308 eval ();
309 tmp = stop_simulation ();
310 }
311 if (tmp) {
312 goto while_3_break;
313 }
314 else {
315 }
316 }}
317 while_3_break :;
318 }
319 return;
320 }
321}
322
323void init_model (void) {
324 {
325 q_free = 1;
326 q_write_ev = 2;
327 q_read_ev = q_write_ev;
328 p_num_write = 0;
329 p_dw_pc = 0;
330 p_dw_i = 1;
331 c_num_read = 0;
332 c_dr_pc = 0;
333 c_dr_i = 1;
334 return;
335 }
336}
337
338int initialize_reads () {
339 for (int instrumentation_index=0; instrumentation_index<5; instrumentation_index++) INPUTS_at_223[instrumentation_index] = __VERIFIER_nondet_int();
340}
341
342int main (void) {
343 initialize_reads ();
344 int __retres1;
345 {
346 {
347 init_model ();
348 start_simulation ();
349 }
350 __retres1 = 0;
351 return (__retres1);
352 }
353}
354
Note: See TracBrowser for help on using the repository browser.