1
2
3
4#line 43 "include/asm-generic/int-ll64.h"
5typedef unsigned char u8;
6#line 46 "include/asm-generic/int-ll64.h"
7typedef unsigned short u16;
8#line 49 "include/asm-generic/int-ll64.h"
9typedef unsigned int u32;
10#line 14 "include/asm-generic/posix_types.h"
11typedef long __kernel_long_t;
12#line 15 "include/asm-generic/posix_types.h"
13typedef unsigned long __kernel_ulong_t;
14#line 75 "include/asm-generic/posix_types.h"
15typedef __kernel_ulong_t __kernel_size_t;
16#line 76 "include/asm-generic/posix_types.h"
17typedef __kernel_long_t __kernel_ssize_t;
18#line 27 "include/linux/types.h"
19typedef unsigned short umode_t;
20#line 63 "include/linux/types.h"
21typedef __kernel_size_t size_t;
22#line 68 "include/linux/types.h"
23typedef __kernel_ssize_t ssize_t;
24#line 202 "include/linux/types.h"
25typedef unsigned int gfp_t;
26#line 221 "include/linux/types.h"
27struct __anonstruct_atomic_t_6 {
28 int counter ;
29};
30#line 221 "include/linux/types.h"
31typedef struct __anonstruct_atomic_t_6 atomic_t;
32#line 226 "include/linux/types.h"
33struct __anonstruct_atomic64_t_7 {
34 long counter ;
35};
36#line 226 "include/linux/types.h"
37typedef struct __anonstruct_atomic64_t_7 atomic64_t;
38#line 227 "include/linux/types.h"
39struct list_head {
40 struct list_head *next ;
41 struct list_head *prev ;
42};
43#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
44struct page;
45#line 58
46struct page;
47#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
48struct arch_spinlock;
49#line 327
50struct arch_spinlock;
51#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
52struct kmem_cache;
53#line 23 "include/asm-generic/atomic-long.h"
54typedef atomic64_t atomic_long_t;
55#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
56typedef u16 __ticket_t;
57#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
58typedef u32 __ticketpair_t;
59#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
60struct __raw_tickets {
61 __ticket_t head ;
62 __ticket_t tail ;
63};
64#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
65union __anonunion_ldv_5907_29 {
66 __ticketpair_t head_tail ;
67 struct __raw_tickets tickets ;
68};
69#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
70struct arch_spinlock {
71 union __anonunion_ldv_5907_29 ldv_5907 ;
72};
73#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
74typedef struct arch_spinlock arch_spinlock_t;
75#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
76struct lockdep_map;
77#line 34
78struct lockdep_map;
79#line 55 "include/linux/debug_locks.h"
80struct stack_trace {
81 unsigned int nr_entries ;
82 unsigned int max_entries ;
83 unsigned long *entries ;
84 int skip ;
85};
86#line 26 "include/linux/stacktrace.h"
87struct lockdep_subclass_key {
88 char __one_byte ;
89};
90#line 53 "include/linux/lockdep.h"
91struct lock_class_key {
92 struct lockdep_subclass_key subkeys[8U] ;
93};
94#line 59 "include/linux/lockdep.h"
95struct lock_class {
96 struct list_head hash_entry ;
97 struct list_head lock_entry ;
98 struct lockdep_subclass_key *key ;
99 unsigned int subclass ;
100 unsigned int dep_gen_id ;
101 unsigned long usage_mask ;
102 struct stack_trace usage_traces[13U] ;
103 struct list_head locks_after ;
104 struct list_head locks_before ;
105 unsigned int version ;
106 unsigned long ops ;
107 char const *name ;
108 int name_version ;
109 unsigned long contention_point[4U] ;
110 unsigned long contending_point[4U] ;
111};
112#line 144 "include/linux/lockdep.h"
113struct lockdep_map {
114 struct lock_class_key *key ;
115 struct lock_class *class_cache[2U] ;
116 char const *name ;
117 int cpu ;
118 unsigned long ip ;
119};
120#line 556 "include/linux/lockdep.h"
121struct raw_spinlock {
122 arch_spinlock_t raw_lock ;
123 unsigned int magic ;
124 unsigned int owner_cpu ;
125 void *owner ;
126 struct lockdep_map dep_map ;
127};
128#line 33 "include/linux/spinlock_types.h"
129struct __anonstruct_ldv_6122_33 {
130 u8 __padding[24U] ;
131 struct lockdep_map dep_map ;
132};
133#line 33 "include/linux/spinlock_types.h"
134union __anonunion_ldv_6123_32 {
135 struct raw_spinlock rlock ;
136 struct __anonstruct_ldv_6122_33 ldv_6122 ;
137};
138#line 33 "include/linux/spinlock_types.h"
139struct spinlock {
140 union __anonunion_ldv_6123_32 ldv_6123 ;
141};
142#line 76 "include/linux/spinlock_types.h"
143typedef struct spinlock spinlock_t;
144#line 445 "include/linux/elf.h"
145struct sock;
146#line 445
147struct sock;
148#line 446
149struct kobject;
150#line 446
151struct kobject;
152#line 447
153enum kobj_ns_type {
154 KOBJ_NS_TYPE_NONE = 0,
155 KOBJ_NS_TYPE_NET = 1,
156 KOBJ_NS_TYPES = 2
157} ;
158#line 453 "include/linux/elf.h"
159struct kobj_ns_type_operations {
160 enum kobj_ns_type type ;
161 void *(*grab_current_ns)(void) ;
162 void const *(*netlink_ns)(struct sock * ) ;
163 void const *(*initial_ns)(void) ;
164 void (*drop_ns)(void * ) ;
165};
166#line 57 "include/linux/kobject_ns.h"
167struct attribute {
168 char const *name ;
169 umode_t mode ;
170 struct lock_class_key *key ;
171 struct lock_class_key skey ;
172};
173#line 98 "include/linux/sysfs.h"
174struct sysfs_ops {
175 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
176 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
177 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
178};
179#line 117
180struct sysfs_dirent;
181#line 117
182struct sysfs_dirent;
183#line 182 "include/linux/sysfs.h"
184struct kref {
185 atomic_t refcount ;
186};
187#line 49 "include/linux/kobject.h"
188struct kset;
189#line 49
190struct kobj_type;
191#line 49 "include/linux/kobject.h"
192struct kobject {
193 char const *name ;
194 struct list_head entry ;
195 struct kobject *parent ;
196 struct kset *kset ;
197 struct kobj_type *ktype ;
198 struct sysfs_dirent *sd ;
199 struct kref kref ;
200 unsigned char state_initialized : 1 ;
201 unsigned char state_in_sysfs : 1 ;
202 unsigned char state_add_uevent_sent : 1 ;
203 unsigned char state_remove_uevent_sent : 1 ;
204 unsigned char uevent_suppress : 1 ;
205};
206#line 107 "include/linux/kobject.h"
207struct kobj_type {
208 void (*release)(struct kobject * ) ;
209 struct sysfs_ops const *sysfs_ops ;
210 struct attribute **default_attrs ;
211 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
212 void const *(*namespace)(struct kobject * ) ;
213};
214#line 115 "include/linux/kobject.h"
215struct kobj_uevent_env {
216 char *envp[32U] ;
217 int envp_idx ;
218 char buf[2048U] ;
219 int buflen ;
220};
221#line 122 "include/linux/kobject.h"
222struct kset_uevent_ops {
223 int (* const filter)(struct kset * , struct kobject * ) ;
224 char const *(* const name)(struct kset * , struct kobject * ) ;
225 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
226};
227#line 139 "include/linux/kobject.h"
228struct kset {
229 struct list_head list ;
230 spinlock_t list_lock ;
231 struct kobject kobj ;
232 struct kset_uevent_ops const *uevent_ops ;
233};
234#line 88 "include/linux/kmemleak.h"
235struct kmem_cache_cpu {
236 void **freelist ;
237 unsigned long tid ;
238 struct page *page ;
239 struct page *partial ;
240 int node ;
241 unsigned int stat[26U] ;
242};
243#line 55 "include/linux/slub_def.h"
244struct kmem_cache_node {
245 spinlock_t list_lock ;
246 unsigned long nr_partial ;
247 struct list_head partial ;
248 atomic_long_t nr_slabs ;
249 atomic_long_t total_objects ;
250 struct list_head full ;
251};
252#line 66 "include/linux/slub_def.h"
253struct kmem_cache_order_objects {
254 unsigned long x ;
255};
256#line 76 "include/linux/slub_def.h"
257struct kmem_cache {
258 struct kmem_cache_cpu *cpu_slab ;
259 unsigned long flags ;
260 unsigned long min_partial ;
261 int size ;
262 int objsize ;
263 int offset ;
264 int cpu_partial ;
265 struct kmem_cache_order_objects oo ;
266 struct kmem_cache_order_objects max ;
267 struct kmem_cache_order_objects min ;
268 gfp_t allocflags ;
269 int refcount ;
270 void (*ctor)(void * ) ;
271 int inuse ;
272 int align ;
273 int reserved ;
274 char const *name ;
275 struct list_head list ;
276 struct kobject kobj ;
277 int remote_node_defrag_ratio ;
278 struct kmem_cache_node *node[1024U] ;
279};
280#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
281void ldv_spin_lock(void) ;
282#line 3
283void ldv_spin_unlock(void) ;
284#line 4
285int ldv_spin_trylock(void) ;
286#line 220 "include/linux/slub_def.h"
287extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
288#line 223
289void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
290#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
291void ldv_check_alloc_flags(gfp_t flags ) ;
292#line 12
293void ldv_check_alloc_nonatomic(void) ;
294#line 14
295struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
296#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
297static void wait_scan_exit(void)
298{
299
300 {
301#line 50
302 return;
303}
304}
305#line 75
306extern void ldv_check_final_state(void) ;
307#line 81
308extern void ldv_initialize(void) ;
309#line 84
310extern int __VERIFIER_nondet_int(void) ;
311#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
312int LDV_IN_INTERRUPT ;
313#line 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
314void main(void)
315{ int tmp ;
316 int tmp___0 ;
317
318 {
319 {
320#line 102
321 LDV_IN_INTERRUPT = 1;
322#line 111
323 ldv_initialize();
324 }
325#line 113
326 goto ldv_14949;
327 ldv_14948:
328 {
329#line 116
330 tmp = __VERIFIER_nondet_int();
331 }
332 {
333#line 118
334 goto switch_default;
335#line 116
336 if (0) {
337 switch_default: ;
338#line 118
339 goto ldv_14947;
340 } else {
341 switch_break: ;
342 }
343 }
344 ldv_14947: ;
345 ldv_14949:
346 {
347#line 113
348 tmp___0 = __VERIFIER_nondet_int();
349 }
350#line 113
351 if (tmp___0 != 0) {
352#line 114
353 goto ldv_14948;
354 } else {
355#line 116
356 goto ldv_14950;
357 }
358 ldv_14950: ;
359 {
360#line 130
361 wait_scan_exit();
362 }
363 {
364#line 133
365 ldv_check_final_state();
366 }
367#line 136
368 return;
369}
370}
371#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
372void ldv_blast_assert(void)
373{
374
375 {
376 ERROR: ;
377#line 6
378 goto ERROR;
379}
380}
381#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
382extern int __VERIFIER_nondet_int(void) ;
383#line 157 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
384int ldv_spin = 0;
385#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
386void ldv_check_alloc_flags(gfp_t flags )
387{
388
389 {
390#line 164
391 if (ldv_spin != 0) {
392#line 164
393 if (flags != 32U) {
394 {
395#line 164
396 ldv_blast_assert();
397 }
398 } else {
399
400 }
401 } else {
402
403 }
404#line 167
405 return;
406}
407}
408#line 167
409extern struct page *ldv_some_page(void) ;
410#line 170 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
411struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
412{ struct page *tmp ;
413
414 {
415#line 173
416 if (ldv_spin != 0) {
417#line 173
418 if (flags != 32U) {
419 {
420#line 173
421 ldv_blast_assert();
422 }
423 } else {
424
425 }
426 } else {
427
428 }
429 {
430#line 175
431 tmp = ldv_some_page();
432 }
433#line 175
434 return (tmp);
435}
436}
437#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
438void ldv_check_alloc_nonatomic(void)
439{
440
441 {
442#line 182
443 if (ldv_spin != 0) {
444 {
445#line 182
446 ldv_blast_assert();
447 }
448 } else {
449
450 }
451#line 185
452 return;
453}
454}
455#line 186 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
456void ldv_spin_lock(void)
457{
458
459 {
460#line 189
461 ldv_spin = 1;
462#line 190
463 return;
464}
465}
466#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
467void ldv_spin_unlock(void)
468{
469
470 {
471#line 196
472 ldv_spin = 0;
473#line 197
474 return;
475}
476}
477#line 200 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
478int ldv_spin_trylock(void)
479{ int is_lock ;
480
481 {
482 {
483#line 205
484 is_lock = __VERIFIER_nondet_int();
485 }
486#line 207
487 if (is_lock != 0) {
488#line 210
489 return (0);
490 } else {
491#line 215
492 ldv_spin = 1;
493#line 217
494 return (1);
495 }
496}
497}
498#line 384 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4019/dscv_tempdir/dscv/ri/43_1a/drivers/scsi/scsi_wait_scan.c.p"
499void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
500{
501
502 {
503 {
504#line 390
505 ldv_check_alloc_flags(ldv_func_arg2);
506#line 392
507 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
508 }
509#line 393
510 return ((void *)0);
511}
512}