1
2
3
4#line 46 "include/asm-generic/int-ll64.h"
5typedef unsigned short u16;
6#line 49 "include/asm-generic/int-ll64.h"
7typedef unsigned int u32;
8#line 219 "include/linux/types.h"
9struct __anonstruct_atomic_t_7 {
10 int counter ;
11};
12#line 219 "include/linux/types.h"
13typedef struct __anonstruct_atomic_t_7 atomic_t;
14#line 229 "include/linux/types.h"
15struct list_head {
16 struct list_head *next ;
17 struct list_head *prev ;
18};
19#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
20struct task_struct;
21#line 20
22struct task_struct;
23#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
24struct task_struct;
25#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
26struct task_struct;
27#line 329
28struct arch_spinlock;
29#line 329
30struct arch_spinlock;
31#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
32struct task_struct;
33#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
34struct task_struct;
35#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
36typedef u16 __ticket_t;
37#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
38typedef u32 __ticketpair_t;
39#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
40struct __raw_tickets {
41 __ticket_t head ;
42 __ticket_t tail ;
43};
44#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
45union __anonunion____missing_field_name_36 {
46 __ticketpair_t head_tail ;
47 struct __raw_tickets tickets ;
48};
49#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
50struct arch_spinlock {
51 union __anonunion____missing_field_name_36 __annonCompField17 ;
52};
53#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
54typedef struct arch_spinlock arch_spinlock_t;
55#line 12 "include/linux/lockdep.h"
56struct task_struct;
57#line 20 "include/linux/spinlock_types.h"
58struct raw_spinlock {
59 arch_spinlock_t raw_lock ;
60 unsigned int magic ;
61 unsigned int owner_cpu ;
62 void *owner ;
63};
64#line 64 "include/linux/spinlock_types.h"
65union __anonunion____missing_field_name_39 {
66 struct raw_spinlock rlock ;
67};
68#line 64 "include/linux/spinlock_types.h"
69struct spinlock {
70 union __anonunion____missing_field_name_39 __annonCompField19 ;
71};
72#line 64 "include/linux/spinlock_types.h"
73typedef struct spinlock spinlock_t;
74#line 55 "include/linux/wait.h"
75struct task_struct;
76#line 48 "include/linux/mutex.h"
77struct mutex {
78 atomic_t count ;
79 spinlock_t wait_lock ;
80 struct list_head wait_list ;
81 struct task_struct *owner ;
82 char const *name ;
83 void *magic ;
84};
85#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
86struct task_struct;
87#line 1 "<compiler builtins>"
88long __builtin_expect(long val , long res ) ;
89#line 152 "include/linux/mutex.h"
90void mutex_lock(struct mutex *lock ) ;
91#line 153
92int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
93#line 154
94int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
95#line 168
96int mutex_trylock(struct mutex *lock ) ;
97#line 169
98void mutex_unlock(struct mutex *lock ) ;
99#line 170
100int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
101#line 67 "include/linux/module.h"
102int init_module(void) ;
103#line 68
104void cleanup_module(void) ;
105#line 244 "include/linux/device.h"
106extern void wait_for_device_probe(void) ;
107#line 8 "include/scsi/scsi_scan.h"
108__inline static int scsi_complete_async_scans(void) __attribute__((__no_instrument_function__)) ;
109#line 8 "include/scsi/scsi_scan.h"
110__inline static int scsi_complete_async_scans(void)
111{
112
113 {
114#line 8
115 return (0);
116}
117}
118#line 18 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
119static int wait_scan_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
120#line 18 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
121static int wait_scan_init(void)
122{
123
124 {
125 {
126#line 25
127 wait_for_device_probe();
128#line 30
129 scsi_complete_async_scans();
130 }
131#line 31
132 return (0);
133}
134}
135#line 34
136static void wait_scan_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
137#line 34 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
138static void wait_scan_exit(void)
139{
140
141 {
142#line 36
143 return;
144}
145}
146#line 38 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
147static char const __mod_description38[32] __attribute__((__used__, __unused__,
148__section__(".modinfo"), __aligned__(1))) =
149#line 38
150 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
151 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
152 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
153 (char const )'S', (char const )'C', (char const )'S', (char const )'I',
154 (char const )' ', (char const )'w', (char const )'a', (char const )'i',
155 (char const )'t', (char const )' ', (char const )'f', (char const )'o',
156 (char const )'r', (char const )' ', (char const )'s', (char const )'c',
157 (char const )'a', (char const )'n', (char const )'s', (char const )'\000'};
158#line 39 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
159static char const __mod_author39[23] __attribute__((__used__, __unused__, __section__(".modinfo"),
160__aligned__(1))) =
161#line 39
162 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
163 (char const )'o', (char const )'r', (char const )'=', (char const )'J',
164 (char const )'a', (char const )'m', (char const )'e', (char const )'s',
165 (char const )' ', (char const )'B', (char const )'o', (char const )'t',
166 (char const )'t', (char const )'o', (char const )'m', (char const )'l',
167 (char const )'e', (char const )'y', (char const )'\000'};
168#line 40 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
169static char const __mod_license40[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
170__aligned__(1))) =
171#line 40
172 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
173 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
174 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
175#line 42 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
176int init_module(void)
177{ int tmp ;
178
179 {
180 {
181#line 42
182 tmp = wait_scan_init();
183 }
184#line 42
185 return (tmp);
186}
187}
188#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
189void cleanup_module(void)
190{
191
192 {
193 {
194#line 43
195 wait_scan_exit();
196 }
197#line 43
198 return;
199}
200}
201#line 61
202void ldv_check_final_state(void) ;
203#line 67
204extern void ldv_initialize(void) ;
205#line 70
206extern int __VERIFIER_nondet_int(void) ;
207#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
208int LDV_IN_INTERRUPT ;
209#line 76 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
210void main(void)
211{ int tmp ;
212 int tmp___0 ;
213
214 {
215 {
216#line 88
217 LDV_IN_INTERRUPT = 1;
218#line 97
219 ldv_initialize();
220 }
221 {
222#line 99
223 while (1) {
224 while_continue: ;
225 {
226#line 99
227 tmp___0 = __VERIFIER_nondet_int();
228 }
229#line 99
230 if (tmp___0) {
231
232 } else {
233#line 99
234 goto while_break;
235 }
236 {
237#line 102
238 tmp = __VERIFIER_nondet_int();
239 }
240 {
241#line 104
242 goto switch_default;
243#line 102
244 if (0) {
245 switch_default:
246#line 104
247 goto switch_break;
248 } else {
249 switch_break: ;
250 }
251 }
252 }
253 while_break: ;
254 }
255 {
256#line 116
257 wait_scan_exit();
258 }
259 {
260#line 119
261 ldv_check_final_state();
262 }
263#line 122
264 return;
265}
266}
267#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
268void ldv_blast_assert(void)
269{
270
271 {
272 ERROR:
273#line 6
274 goto ERROR;
275}
276}
277#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
278extern int __VERIFIER_nondet_int(void) ;
279#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
280int ldv_mutex = 1;
281#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
282int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
283{ int nondetermined ;
284
285 {
286#line 29
287 if (ldv_mutex == 1) {
288
289 } else {
290 {
291#line 29
292 ldv_blast_assert();
293 }
294 }
295 {
296#line 32
297 nondetermined = __VERIFIER_nondet_int();
298 }
299#line 35
300 if (nondetermined) {
301#line 38
302 ldv_mutex = 2;
303#line 40
304 return (0);
305 } else {
306#line 45
307 return (-4);
308 }
309}
310}
311#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
312int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
313{ int nondetermined ;
314
315 {
316#line 57
317 if (ldv_mutex == 1) {
318
319 } else {
320 {
321#line 57
322 ldv_blast_assert();
323 }
324 }
325 {
326#line 60
327 nondetermined = __VERIFIER_nondet_int();
328 }
329#line 63
330 if (nondetermined) {
331#line 66
332 ldv_mutex = 2;
333#line 68
334 return (0);
335 } else {
336#line 73
337 return (-4);
338 }
339}
340}
341#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
342int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
343{ int atomic_value_after_dec ;
344
345 {
346#line 83
347 if (ldv_mutex == 1) {
348
349 } else {
350 {
351#line 83
352 ldv_blast_assert();
353 }
354 }
355 {
356#line 86
357 atomic_value_after_dec = __VERIFIER_nondet_int();
358 }
359#line 89
360 if (atomic_value_after_dec == 0) {
361#line 92
362 ldv_mutex = 2;
363#line 94
364 return (1);
365 } else {
366
367 }
368#line 98
369 return (0);
370}
371}
372#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
373void mutex_lock(struct mutex *lock )
374{
375
376 {
377#line 108
378 if (ldv_mutex == 1) {
379
380 } else {
381 {
382#line 108
383 ldv_blast_assert();
384 }
385 }
386#line 110
387 ldv_mutex = 2;
388#line 111
389 return;
390}
391}
392#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
393int mutex_trylock(struct mutex *lock )
394{ int nondetermined ;
395
396 {
397#line 121
398 if (ldv_mutex == 1) {
399
400 } else {
401 {
402#line 121
403 ldv_blast_assert();
404 }
405 }
406 {
407#line 124
408 nondetermined = __VERIFIER_nondet_int();
409 }
410#line 127
411 if (nondetermined) {
412#line 130
413 ldv_mutex = 2;
414#line 132
415 return (1);
416 } else {
417#line 137
418 return (0);
419 }
420}
421}
422#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
423void mutex_unlock(struct mutex *lock )
424{
425
426 {
427#line 147
428 if (ldv_mutex == 2) {
429
430 } else {
431 {
432#line 147
433 ldv_blast_assert();
434 }
435 }
436#line 149
437 ldv_mutex = 1;
438#line 150
439 return;
440}
441}
442#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
443void ldv_check_final_state(void)
444{
445
446 {
447#line 156
448 if (ldv_mutex == 1) {
449
450 } else {
451 {
452#line 156
453 ldv_blast_assert();
454 }
455 }
456#line 157
457 return;
458}
459}
460#line 131 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/977/dscv_tempdir/dscv/ri/32_1/drivers/scsi/scsi_wait_scan.c.common.c"
461long s__builtin_expect(long val , long res )
462{
463
464 {
465#line 132
466 return (val);
467}
468}