1
2
3
4#line 23 "include/asm-generic/int-ll64.h"
5typedef unsigned short __u16;
6#line 26 "include/asm-generic/int-ll64.h"
7typedef unsigned int __u32;
8#line 30 "include/asm-generic/int-ll64.h"
9typedef unsigned long long __u64;
10#line 43 "include/asm-generic/int-ll64.h"
11typedef unsigned char u8;
12#line 45 "include/asm-generic/int-ll64.h"
13typedef short s16;
14#line 46 "include/asm-generic/int-ll64.h"
15typedef unsigned short u16;
16#line 48 "include/asm-generic/int-ll64.h"
17typedef int s32;
18#line 49 "include/asm-generic/int-ll64.h"
19typedef unsigned int u32;
20#line 51 "include/asm-generic/int-ll64.h"
21typedef long long s64;
22#line 52 "include/asm-generic/int-ll64.h"
23typedef unsigned long long u64;
24#line 14 "include/asm-generic/posix_types.h"
25typedef long __kernel_long_t;
26#line 15 "include/asm-generic/posix_types.h"
27typedef unsigned long __kernel_ulong_t;
28#line 75 "include/asm-generic/posix_types.h"
29typedef __kernel_ulong_t __kernel_size_t;
30#line 76 "include/asm-generic/posix_types.h"
31typedef __kernel_long_t __kernel_ssize_t;
32#line 91 "include/asm-generic/posix_types.h"
33typedef long long __kernel_loff_t;
34#line 21 "include/linux/types.h"
35typedef __u32 __kernel_dev_t;
36#line 24 "include/linux/types.h"
37typedef __kernel_dev_t dev_t;
38#line 27 "include/linux/types.h"
39typedef unsigned short umode_t;
40#line 38 "include/linux/types.h"
41typedef _Bool bool;
42#line 54 "include/linux/types.h"
43typedef __kernel_loff_t loff_t;
44#line 63 "include/linux/types.h"
45typedef __kernel_size_t size_t;
46#line 68 "include/linux/types.h"
47typedef __kernel_ssize_t ssize_t;
48#line 202 "include/linux/types.h"
49typedef unsigned int gfp_t;
50#line 221 "include/linux/types.h"
51struct __anonstruct_atomic_t_6 {
52 int counter ;
53};
54#line 221 "include/linux/types.h"
55typedef struct __anonstruct_atomic_t_6 atomic_t;
56#line 226 "include/linux/types.h"
57struct __anonstruct_atomic64_t_7 {
58 long counter ;
59};
60#line 226 "include/linux/types.h"
61typedef struct __anonstruct_atomic64_t_7 atomic64_t;
62#line 227 "include/linux/types.h"
63struct list_head {
64 struct list_head *next ;
65 struct list_head *prev ;
66};
67#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
68struct module;
69#line 55
70struct module;
71#line 146 "include/linux/init.h"
72typedef void (*ctor_fn_t)(void);
73#line 46 "include/linux/dynamic_debug.h"
74struct device;
75#line 46
76struct device;
77#line 57
78struct completion;
79#line 57
80struct completion;
81#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
82struct page;
83#line 58
84struct page;
85#line 26 "include/asm-generic/getorder.h"
86struct task_struct;
87#line 26
88struct task_struct;
89#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
90struct file;
91#line 290
92struct file;
93#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
94struct arch_spinlock;
95#line 327
96struct arch_spinlock;
97#line 306 "include/linux/bitmap.h"
98struct bug_entry {
99 int bug_addr_disp ;
100 int file_disp ;
101 unsigned short line ;
102 unsigned short flags ;
103};
104#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
105struct static_key;
106#line 234
107struct static_key;
108#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
109struct kmem_cache;
110#line 23 "include/asm-generic/atomic-long.h"
111typedef atomic64_t atomic_long_t;
112#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
113typedef u16 __ticket_t;
114#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
115typedef u32 __ticketpair_t;
116#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
117struct __raw_tickets {
118 __ticket_t head ;
119 __ticket_t tail ;
120};
121#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
122union __anonunion_ldv_5907_29 {
123 __ticketpair_t head_tail ;
124 struct __raw_tickets tickets ;
125};
126#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
127struct arch_spinlock {
128 union __anonunion_ldv_5907_29 ldv_5907 ;
129};
130#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
131typedef struct arch_spinlock arch_spinlock_t;
132#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
133struct __anonstruct_ldv_5914_31 {
134 u32 read ;
135 s32 write ;
136};
137#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
138union __anonunion_arch_rwlock_t_30 {
139 s64 lock ;
140 struct __anonstruct_ldv_5914_31 ldv_5914 ;
141};
142#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
143typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
144#line 34
145struct lockdep_map;
146#line 34
147struct lockdep_map;
148#line 55 "include/linux/debug_locks.h"
149struct stack_trace {
150 unsigned int nr_entries ;
151 unsigned int max_entries ;
152 unsigned long *entries ;
153 int skip ;
154};
155#line 26 "include/linux/stacktrace.h"
156struct lockdep_subclass_key {
157 char __one_byte ;
158};
159#line 53 "include/linux/lockdep.h"
160struct lock_class_key {
161 struct lockdep_subclass_key subkeys[8U] ;
162};
163#line 59 "include/linux/lockdep.h"
164struct lock_class {
165 struct list_head hash_entry ;
166 struct list_head lock_entry ;
167 struct lockdep_subclass_key *key ;
168 unsigned int subclass ;
169 unsigned int dep_gen_id ;
170 unsigned long usage_mask ;
171 struct stack_trace usage_traces[13U] ;
172 struct list_head locks_after ;
173 struct list_head locks_before ;
174 unsigned int version ;
175 unsigned long ops ;
176 char const *name ;
177 int name_version ;
178 unsigned long contention_point[4U] ;
179 unsigned long contending_point[4U] ;
180};
181#line 144 "include/linux/lockdep.h"
182struct lockdep_map {
183 struct lock_class_key *key ;
184 struct lock_class *class_cache[2U] ;
185 char const *name ;
186 int cpu ;
187 unsigned long ip ;
188};
189#line 556 "include/linux/lockdep.h"
190struct raw_spinlock {
191 arch_spinlock_t raw_lock ;
192 unsigned int magic ;
193 unsigned int owner_cpu ;
194 void *owner ;
195 struct lockdep_map dep_map ;
196};
197#line 32 "include/linux/spinlock_types.h"
198typedef struct raw_spinlock raw_spinlock_t;
199#line 33 "include/linux/spinlock_types.h"
200struct __anonstruct_ldv_6122_33 {
201 u8 __padding[24U] ;
202 struct lockdep_map dep_map ;
203};
204#line 33 "include/linux/spinlock_types.h"
205union __anonunion_ldv_6123_32 {
206 struct raw_spinlock rlock ;
207 struct __anonstruct_ldv_6122_33 ldv_6122 ;
208};
209#line 33 "include/linux/spinlock_types.h"
210struct spinlock {
211 union __anonunion_ldv_6123_32 ldv_6123 ;
212};
213#line 76 "include/linux/spinlock_types.h"
214typedef struct spinlock spinlock_t;
215#line 23 "include/linux/rwlock_types.h"
216struct __anonstruct_rwlock_t_34 {
217 arch_rwlock_t raw_lock ;
218 unsigned int magic ;
219 unsigned int owner_cpu ;
220 void *owner ;
221 struct lockdep_map dep_map ;
222};
223#line 23 "include/linux/rwlock_types.h"
224typedef struct __anonstruct_rwlock_t_34 rwlock_t;
225#line 48 "include/linux/wait.h"
226struct __wait_queue_head {
227 spinlock_t lock ;
228 struct list_head task_list ;
229};
230#line 53 "include/linux/wait.h"
231typedef struct __wait_queue_head wait_queue_head_t;
232#line 670 "include/linux/mmzone.h"
233struct mutex {
234 atomic_t count ;
235 spinlock_t wait_lock ;
236 struct list_head wait_list ;
237 struct task_struct *owner ;
238 char const *name ;
239 void *magic ;
240 struct lockdep_map dep_map ;
241};
242#line 171 "include/linux/mutex.h"
243struct rw_semaphore;
244#line 171
245struct rw_semaphore;
246#line 172 "include/linux/mutex.h"
247struct rw_semaphore {
248 long count ;
249 raw_spinlock_t wait_lock ;
250 struct list_head wait_list ;
251 struct lockdep_map dep_map ;
252};
253#line 128 "include/linux/rwsem.h"
254struct completion {
255 unsigned int done ;
256 wait_queue_head_t wait ;
257};
258#line 312 "include/linux/jiffies.h"
259union ktime {
260 s64 tv64 ;
261};
262#line 59 "include/linux/ktime.h"
263typedef union ktime ktime_t;
264#line 341
265struct tvec_base;
266#line 341
267struct tvec_base;
268#line 342 "include/linux/ktime.h"
269struct timer_list {
270 struct list_head entry ;
271 unsigned long expires ;
272 struct tvec_base *base ;
273 void (*function)(unsigned long ) ;
274 unsigned long data ;
275 int slack ;
276 int start_pid ;
277 void *start_site ;
278 char start_comm[16U] ;
279 struct lockdep_map lockdep_map ;
280};
281#line 302 "include/linux/timer.h"
282struct work_struct;
283#line 302
284struct work_struct;
285#line 45 "include/linux/workqueue.h"
286struct work_struct {
287 atomic_long_t data ;
288 struct list_head entry ;
289 void (*func)(struct work_struct * ) ;
290 struct lockdep_map lockdep_map ;
291};
292#line 46 "include/linux/pm.h"
293struct pm_message {
294 int event ;
295};
296#line 52 "include/linux/pm.h"
297typedef struct pm_message pm_message_t;
298#line 53 "include/linux/pm.h"
299struct dev_pm_ops {
300 int (*prepare)(struct device * ) ;
301 void (*complete)(struct device * ) ;
302 int (*suspend)(struct device * ) ;
303 int (*resume)(struct device * ) ;
304 int (*freeze)(struct device * ) ;
305 int (*thaw)(struct device * ) ;
306 int (*poweroff)(struct device * ) ;
307 int (*restore)(struct device * ) ;
308 int (*suspend_late)(struct device * ) ;
309 int (*resume_early)(struct device * ) ;
310 int (*freeze_late)(struct device * ) ;
311 int (*thaw_early)(struct device * ) ;
312 int (*poweroff_late)(struct device * ) ;
313 int (*restore_early)(struct device * ) ;
314 int (*suspend_noirq)(struct device * ) ;
315 int (*resume_noirq)(struct device * ) ;
316 int (*freeze_noirq)(struct device * ) ;
317 int (*thaw_noirq)(struct device * ) ;
318 int (*poweroff_noirq)(struct device * ) ;
319 int (*restore_noirq)(struct device * ) ;
320 int (*runtime_suspend)(struct device * ) ;
321 int (*runtime_resume)(struct device * ) ;
322 int (*runtime_idle)(struct device * ) ;
323};
324#line 289
325enum rpm_status {
326 RPM_ACTIVE = 0,
327 RPM_RESUMING = 1,
328 RPM_SUSPENDED = 2,
329 RPM_SUSPENDING = 3
330} ;
331#line 296
332enum rpm_request {
333 RPM_REQ_NONE = 0,
334 RPM_REQ_IDLE = 1,
335 RPM_REQ_SUSPEND = 2,
336 RPM_REQ_AUTOSUSPEND = 3,
337 RPM_REQ_RESUME = 4
338} ;
339#line 304
340struct wakeup_source;
341#line 304
342struct wakeup_source;
343#line 494 "include/linux/pm.h"
344struct pm_subsys_data {
345 spinlock_t lock ;
346 unsigned int refcount ;
347};
348#line 499
349struct dev_pm_qos_request;
350#line 499
351struct pm_qos_constraints;
352#line 499 "include/linux/pm.h"
353struct dev_pm_info {
354 pm_message_t power_state ;
355 unsigned char can_wakeup : 1 ;
356 unsigned char async_suspend : 1 ;
357 bool is_prepared ;
358 bool is_suspended ;
359 bool ignore_children ;
360 spinlock_t lock ;
361 struct list_head entry ;
362 struct completion completion ;
363 struct wakeup_source *wakeup ;
364 bool wakeup_path ;
365 struct timer_list suspend_timer ;
366 unsigned long timer_expires ;
367 struct work_struct work ;
368 wait_queue_head_t wait_queue ;
369 atomic_t usage_count ;
370 atomic_t child_count ;
371 unsigned char disable_depth : 3 ;
372 unsigned char idle_notification : 1 ;
373 unsigned char request_pending : 1 ;
374 unsigned char deferred_resume : 1 ;
375 unsigned char run_wake : 1 ;
376 unsigned char runtime_auto : 1 ;
377 unsigned char no_callbacks : 1 ;
378 unsigned char irq_safe : 1 ;
379 unsigned char use_autosuspend : 1 ;
380 unsigned char timer_autosuspends : 1 ;
381 enum rpm_request request ;
382 enum rpm_status runtime_status ;
383 int runtime_error ;
384 int autosuspend_delay ;
385 unsigned long last_busy ;
386 unsigned long active_jiffies ;
387 unsigned long suspended_jiffies ;
388 unsigned long accounting_timestamp ;
389 ktime_t suspend_time ;
390 s64 max_time_suspended_ns ;
391 struct dev_pm_qos_request *pq_req ;
392 struct pm_subsys_data *subsys_data ;
393 struct pm_qos_constraints *constraints ;
394};
395#line 558 "include/linux/pm.h"
396struct dev_pm_domain {
397 struct dev_pm_ops ops ;
398};
399#line 18 "include/asm-generic/pci_iomap.h"
400struct vm_area_struct;
401#line 18
402struct vm_area_struct;
403#line 18 "include/linux/elf.h"
404typedef __u64 Elf64_Addr;
405#line 19 "include/linux/elf.h"
406typedef __u16 Elf64_Half;
407#line 23 "include/linux/elf.h"
408typedef __u32 Elf64_Word;
409#line 24 "include/linux/elf.h"
410typedef __u64 Elf64_Xword;
411#line 193 "include/linux/elf.h"
412struct elf64_sym {
413 Elf64_Word st_name ;
414 unsigned char st_info ;
415 unsigned char st_other ;
416 Elf64_Half st_shndx ;
417 Elf64_Addr st_value ;
418 Elf64_Xword st_size ;
419};
420#line 201 "include/linux/elf.h"
421typedef struct elf64_sym Elf64_Sym;
422#line 445
423struct sock;
424#line 445
425struct sock;
426#line 446
427struct kobject;
428#line 446
429struct kobject;
430#line 447
431enum kobj_ns_type {
432 KOBJ_NS_TYPE_NONE = 0,
433 KOBJ_NS_TYPE_NET = 1,
434 KOBJ_NS_TYPES = 2
435} ;
436#line 453 "include/linux/elf.h"
437struct kobj_ns_type_operations {
438 enum kobj_ns_type type ;
439 void *(*grab_current_ns)(void) ;
440 void const *(*netlink_ns)(struct sock * ) ;
441 void const *(*initial_ns)(void) ;
442 void (*drop_ns)(void * ) ;
443};
444#line 57 "include/linux/kobject_ns.h"
445struct attribute {
446 char const *name ;
447 umode_t mode ;
448 struct lock_class_key *key ;
449 struct lock_class_key skey ;
450};
451#line 33 "include/linux/sysfs.h"
452struct attribute_group {
453 char const *name ;
454 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
455 struct attribute **attrs ;
456};
457#line 62 "include/linux/sysfs.h"
458struct bin_attribute {
459 struct attribute attr ;
460 size_t size ;
461 void *private ;
462 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
463 loff_t , size_t ) ;
464 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
465 loff_t , size_t ) ;
466 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
467};
468#line 98 "include/linux/sysfs.h"
469struct sysfs_ops {
470 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
471 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
472 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
473};
474#line 117
475struct sysfs_dirent;
476#line 117
477struct sysfs_dirent;
478#line 182 "include/linux/sysfs.h"
479struct kref {
480 atomic_t refcount ;
481};
482#line 49 "include/linux/kobject.h"
483struct kset;
484#line 49
485struct kobj_type;
486#line 49 "include/linux/kobject.h"
487struct kobject {
488 char const *name ;
489 struct list_head entry ;
490 struct kobject *parent ;
491 struct kset *kset ;
492 struct kobj_type *ktype ;
493 struct sysfs_dirent *sd ;
494 struct kref kref ;
495 unsigned char state_initialized : 1 ;
496 unsigned char state_in_sysfs : 1 ;
497 unsigned char state_add_uevent_sent : 1 ;
498 unsigned char state_remove_uevent_sent : 1 ;
499 unsigned char uevent_suppress : 1 ;
500};
501#line 107 "include/linux/kobject.h"
502struct kobj_type {
503 void (*release)(struct kobject * ) ;
504 struct sysfs_ops const *sysfs_ops ;
505 struct attribute **default_attrs ;
506 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
507 void const *(*namespace)(struct kobject * ) ;
508};
509#line 115 "include/linux/kobject.h"
510struct kobj_uevent_env {
511 char *envp[32U] ;
512 int envp_idx ;
513 char buf[2048U] ;
514 int buflen ;
515};
516#line 122 "include/linux/kobject.h"
517struct kset_uevent_ops {
518 int (* const filter)(struct kset * , struct kobject * ) ;
519 char const *(* const name)(struct kset * , struct kobject * ) ;
520 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
521};
522#line 139 "include/linux/kobject.h"
523struct kset {
524 struct list_head list ;
525 spinlock_t list_lock ;
526 struct kobject kobj ;
527 struct kset_uevent_ops const *uevent_ops ;
528};
529#line 215
530struct kernel_param;
531#line 215
532struct kernel_param;
533#line 216 "include/linux/kobject.h"
534struct kernel_param_ops {
535 int (*set)(char const * , struct kernel_param const * ) ;
536 int (*get)(char * , struct kernel_param const * ) ;
537 void (*free)(void * ) ;
538};
539#line 49 "include/linux/moduleparam.h"
540struct kparam_string;
541#line 49
542struct kparam_array;
543#line 49 "include/linux/moduleparam.h"
544union __anonunion_ldv_13363_134 {
545 void *arg ;
546 struct kparam_string const *str ;
547 struct kparam_array const *arr ;
548};
549#line 49 "include/linux/moduleparam.h"
550struct kernel_param {
551 char const *name ;
552 struct kernel_param_ops const *ops ;
553 u16 perm ;
554 s16 level ;
555 union __anonunion_ldv_13363_134 ldv_13363 ;
556};
557#line 61 "include/linux/moduleparam.h"
558struct kparam_string {
559 unsigned int maxlen ;
560 char *string ;
561};
562#line 67 "include/linux/moduleparam.h"
563struct kparam_array {
564 unsigned int max ;
565 unsigned int elemsize ;
566 unsigned int *num ;
567 struct kernel_param_ops const *ops ;
568 void *elem ;
569};
570#line 458 "include/linux/moduleparam.h"
571struct static_key {
572 atomic_t enabled ;
573};
574#line 225 "include/linux/jump_label.h"
575struct tracepoint;
576#line 225
577struct tracepoint;
578#line 226 "include/linux/jump_label.h"
579struct tracepoint_func {
580 void *func ;
581 void *data ;
582};
583#line 29 "include/linux/tracepoint.h"
584struct tracepoint {
585 char const *name ;
586 struct static_key key ;
587 void (*regfunc)(void) ;
588 void (*unregfunc)(void) ;
589 struct tracepoint_func *funcs ;
590};
591#line 86 "include/linux/tracepoint.h"
592struct kernel_symbol {
593 unsigned long value ;
594 char const *name ;
595};
596#line 27 "include/linux/export.h"
597struct mod_arch_specific {
598
599};
600#line 34 "include/linux/module.h"
601struct module_param_attrs;
602#line 34 "include/linux/module.h"
603struct module_kobject {
604 struct kobject kobj ;
605 struct module *mod ;
606 struct kobject *drivers_dir ;
607 struct module_param_attrs *mp ;
608};
609#line 43 "include/linux/module.h"
610struct module_attribute {
611 struct attribute attr ;
612 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
613 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
614 size_t ) ;
615 void (*setup)(struct module * , char const * ) ;
616 int (*test)(struct module * ) ;
617 void (*free)(struct module * ) ;
618};
619#line 69
620struct exception_table_entry;
621#line 69
622struct exception_table_entry;
623#line 198
624enum module_state {
625 MODULE_STATE_LIVE = 0,
626 MODULE_STATE_COMING = 1,
627 MODULE_STATE_GOING = 2
628} ;
629#line 204 "include/linux/module.h"
630struct module_ref {
631 unsigned long incs ;
632 unsigned long decs ;
633};
634#line 219
635struct module_sect_attrs;
636#line 219
637struct module_notes_attrs;
638#line 219
639struct ftrace_event_call;
640#line 219 "include/linux/module.h"
641struct module {
642 enum module_state state ;
643 struct list_head list ;
644 char name[56U] ;
645 struct module_kobject mkobj ;
646 struct module_attribute *modinfo_attrs ;
647 char const *version ;
648 char const *srcversion ;
649 struct kobject *holders_dir ;
650 struct kernel_symbol const *syms ;
651 unsigned long const *crcs ;
652 unsigned int num_syms ;
653 struct kernel_param *kp ;
654 unsigned int num_kp ;
655 unsigned int num_gpl_syms ;
656 struct kernel_symbol const *gpl_syms ;
657 unsigned long const *gpl_crcs ;
658 struct kernel_symbol const *unused_syms ;
659 unsigned long const *unused_crcs ;
660 unsigned int num_unused_syms ;
661 unsigned int num_unused_gpl_syms ;
662 struct kernel_symbol const *unused_gpl_syms ;
663 unsigned long const *unused_gpl_crcs ;
664 struct kernel_symbol const *gpl_future_syms ;
665 unsigned long const *gpl_future_crcs ;
666 unsigned int num_gpl_future_syms ;
667 unsigned int num_exentries ;
668 struct exception_table_entry *extable ;
669 int (*init)(void) ;
670 void *module_init ;
671 void *module_core ;
672 unsigned int init_size ;
673 unsigned int core_size ;
674 unsigned int init_text_size ;
675 unsigned int core_text_size ;
676 unsigned int init_ro_size ;
677 unsigned int core_ro_size ;
678 struct mod_arch_specific arch ;
679 unsigned int taints ;
680 unsigned int num_bugs ;
681 struct list_head bug_list ;
682 struct bug_entry *bug_table ;
683 Elf64_Sym *symtab ;
684 Elf64_Sym *core_symtab ;
685 unsigned int num_symtab ;
686 unsigned int core_num_syms ;
687 char *strtab ;
688 char *core_strtab ;
689 struct module_sect_attrs *sect_attrs ;
690 struct module_notes_attrs *notes_attrs ;
691 char *args ;
692 void *percpu ;
693 unsigned int percpu_size ;
694 unsigned int num_tracepoints ;
695 struct tracepoint * const *tracepoints_ptrs ;
696 unsigned int num_trace_bprintk_fmt ;
697 char const **trace_bprintk_fmt_start ;
698 struct ftrace_event_call **trace_events ;
699 unsigned int num_trace_events ;
700 struct list_head source_list ;
701 struct list_head target_list ;
702 struct task_struct *waiter ;
703 void (*exit)(void) ;
704 struct module_ref *refptr ;
705 ctor_fn_t (**ctors)(void) ;
706 unsigned int num_ctors ;
707};
708#line 88 "include/linux/kmemleak.h"
709struct kmem_cache_cpu {
710 void **freelist ;
711 unsigned long tid ;
712 struct page *page ;
713 struct page *partial ;
714 int node ;
715 unsigned int stat[26U] ;
716};
717#line 55 "include/linux/slub_def.h"
718struct kmem_cache_node {
719 spinlock_t list_lock ;
720 unsigned long nr_partial ;
721 struct list_head partial ;
722 atomic_long_t nr_slabs ;
723 atomic_long_t total_objects ;
724 struct list_head full ;
725};
726#line 66 "include/linux/slub_def.h"
727struct kmem_cache_order_objects {
728 unsigned long x ;
729};
730#line 76 "include/linux/slub_def.h"
731struct kmem_cache {
732 struct kmem_cache_cpu *cpu_slab ;
733 unsigned long flags ;
734 unsigned long min_partial ;
735 int size ;
736 int objsize ;
737 int offset ;
738 int cpu_partial ;
739 struct kmem_cache_order_objects oo ;
740 struct kmem_cache_order_objects max ;
741 struct kmem_cache_order_objects min ;
742 gfp_t allocflags ;
743 int refcount ;
744 void (*ctor)(void * ) ;
745 int inuse ;
746 int align ;
747 int reserved ;
748 char const *name ;
749 struct list_head list ;
750 struct kobject kobj ;
751 int remote_node_defrag_ratio ;
752 struct kmem_cache_node *node[1024U] ;
753};
754#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
755enum led_brightness {
756 LED_OFF = 0,
757 LED_HALF = 127,
758 LED_FULL = 255
759} ;
760#line 21
761struct led_trigger;
762#line 21 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
763struct led_classdev {
764 char const *name ;
765 int brightness ;
766 int max_brightness ;
767 int flags ;
768 void (*brightness_set)(struct led_classdev * , enum led_brightness ) ;
769 enum led_brightness (*brightness_get)(struct led_classdev * ) ;
770 int (*blink_set)(struct led_classdev * , unsigned long * , unsigned long * ) ;
771 struct device *dev ;
772 struct list_head node ;
773 char const *default_trigger ;
774 unsigned long blink_delay_on ;
775 unsigned long blink_delay_off ;
776 struct timer_list blink_timer ;
777 int blink_brightness ;
778 struct rw_semaphore trigger_lock ;
779 struct led_trigger *trigger ;
780 struct list_head trig_list ;
781 void *trigger_data ;
782};
783#line 113 "include/linux/leds.h"
784struct led_trigger {
785 char const *name ;
786 void (*activate)(struct led_classdev * ) ;
787 void (*deactivate)(struct led_classdev * ) ;
788 rwlock_t leddev_list_lock ;
789 struct list_head led_cdevs ;
790 struct list_head next_trig ;
791};
792#line 211
793struct klist_node;
794#line 211
795struct klist_node;
796#line 37 "include/linux/klist.h"
797struct klist_node {
798 void *n_klist ;
799 struct list_head n_node ;
800 struct kref n_ref ;
801};
802#line 67
803struct dma_map_ops;
804#line 67 "include/linux/klist.h"
805struct dev_archdata {
806 void *acpi_handle ;
807 struct dma_map_ops *dma_ops ;
808 void *iommu ;
809};
810#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
811struct device_private;
812#line 17
813struct device_private;
814#line 18
815struct device_driver;
816#line 18
817struct device_driver;
818#line 19
819struct driver_private;
820#line 19
821struct driver_private;
822#line 20
823struct class;
824#line 20
825struct class;
826#line 21
827struct subsys_private;
828#line 21
829struct subsys_private;
830#line 22
831struct bus_type;
832#line 22
833struct bus_type;
834#line 23
835struct device_node;
836#line 23
837struct device_node;
838#line 24
839struct iommu_ops;
840#line 24
841struct iommu_ops;
842#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
843struct bus_attribute {
844 struct attribute attr ;
845 ssize_t (*show)(struct bus_type * , char * ) ;
846 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
847};
848#line 51 "include/linux/device.h"
849struct device_attribute;
850#line 51
851struct driver_attribute;
852#line 51 "include/linux/device.h"
853struct bus_type {
854 char const *name ;
855 char const *dev_name ;
856 struct device *dev_root ;
857 struct bus_attribute *bus_attrs ;
858 struct device_attribute *dev_attrs ;
859 struct driver_attribute *drv_attrs ;
860 int (*match)(struct device * , struct device_driver * ) ;
861 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
862 int (*probe)(struct device * ) ;
863 int (*remove)(struct device * ) ;
864 void (*shutdown)(struct device * ) ;
865 int (*suspend)(struct device * , pm_message_t ) ;
866 int (*resume)(struct device * ) ;
867 struct dev_pm_ops const *pm ;
868 struct iommu_ops *iommu_ops ;
869 struct subsys_private *p ;
870};
871#line 125
872struct device_type;
873#line 182
874struct of_device_id;
875#line 182 "include/linux/device.h"
876struct device_driver {
877 char const *name ;
878 struct bus_type *bus ;
879 struct module *owner ;
880 char const *mod_name ;
881 bool suppress_bind_attrs ;
882 struct of_device_id const *of_match_table ;
883 int (*probe)(struct device * ) ;
884 int (*remove)(struct device * ) ;
885 void (*shutdown)(struct device * ) ;
886 int (*suspend)(struct device * , pm_message_t ) ;
887 int (*resume)(struct device * ) ;
888 struct attribute_group const **groups ;
889 struct dev_pm_ops const *pm ;
890 struct driver_private *p ;
891};
892#line 245 "include/linux/device.h"
893struct driver_attribute {
894 struct attribute attr ;
895 ssize_t (*show)(struct device_driver * , char * ) ;
896 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
897};
898#line 299
899struct class_attribute;
900#line 299 "include/linux/device.h"
901struct class {
902 char const *name ;
903 struct module *owner ;
904 struct class_attribute *class_attrs ;
905 struct device_attribute *dev_attrs ;
906 struct bin_attribute *dev_bin_attrs ;
907 struct kobject *dev_kobj ;
908 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
909 char *(*devnode)(struct device * , umode_t * ) ;
910 void (*class_release)(struct class * ) ;
911 void (*dev_release)(struct device * ) ;
912 int (*suspend)(struct device * , pm_message_t ) ;
913 int (*resume)(struct device * ) ;
914 struct kobj_ns_type_operations const *ns_type ;
915 void const *(*namespace)(struct device * ) ;
916 struct dev_pm_ops const *pm ;
917 struct subsys_private *p ;
918};
919#line 394 "include/linux/device.h"
920struct class_attribute {
921 struct attribute attr ;
922 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
923 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
924 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
925};
926#line 447 "include/linux/device.h"
927struct device_type {
928 char const *name ;
929 struct attribute_group const **groups ;
930 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
931 char *(*devnode)(struct device * , umode_t * ) ;
932 void (*release)(struct device * ) ;
933 struct dev_pm_ops const *pm ;
934};
935#line 474 "include/linux/device.h"
936struct device_attribute {
937 struct attribute attr ;
938 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
939 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
940 size_t ) ;
941};
942#line 557 "include/linux/device.h"
943struct device_dma_parameters {
944 unsigned int max_segment_size ;
945 unsigned long segment_boundary_mask ;
946};
947#line 567
948struct dma_coherent_mem;
949#line 567 "include/linux/device.h"
950struct device {
951 struct device *parent ;
952 struct device_private *p ;
953 struct kobject kobj ;
954 char const *init_name ;
955 struct device_type const *type ;
956 struct mutex mutex ;
957 struct bus_type *bus ;
958 struct device_driver *driver ;
959 void *platform_data ;
960 struct dev_pm_info power ;
961 struct dev_pm_domain *pm_domain ;
962 int numa_node ;
963 u64 *dma_mask ;
964 u64 coherent_dma_mask ;
965 struct device_dma_parameters *dma_parms ;
966 struct list_head dma_pools ;
967 struct dma_coherent_mem *dma_mem ;
968 struct dev_archdata archdata ;
969 struct device_node *of_node ;
970 dev_t devt ;
971 u32 id ;
972 spinlock_t devres_lock ;
973 struct list_head devres_head ;
974 struct klist_node knode_class ;
975 struct class *class ;
976 struct attribute_group const **groups ;
977 void (*release)(struct device * ) ;
978};
979#line 681 "include/linux/device.h"
980struct wakeup_source {
981 char const *name ;
982 struct list_head entry ;
983 spinlock_t lock ;
984 struct timer_list timer ;
985 unsigned long timer_expires ;
986 ktime_t total_time ;
987 ktime_t max_time ;
988 ktime_t last_time ;
989 unsigned long event_count ;
990 unsigned long active_count ;
991 unsigned long relax_count ;
992 unsigned long hit_count ;
993 unsigned char active : 1 ;
994};
995#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
996void ldv_spin_lock(void) ;
997#line 3
998void ldv_spin_unlock(void) ;
999#line 4
1000int ldv_spin_trylock(void) ;
1001#line 220 "include/linux/slub_def.h"
1002extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1003#line 223
1004void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1005#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1006void ldv_check_alloc_flags(gfp_t flags ) ;
1007#line 12
1008void ldv_check_alloc_nonatomic(void) ;
1009#line 14
1010struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1011#line 137 "include/linux/leds.h"
1012extern int led_trigger_register(struct led_trigger * ) ;
1013#line 138
1014extern void led_trigger_unregister(struct led_trigger * ) ;
1015#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/leds/leds.h"
1016__inline static void led_set_brightness(struct led_classdev *led_cdev , enum led_brightness value )
1017{ unsigned int __cil_tmp3 ;
1018 unsigned long __cil_tmp4 ;
1019 unsigned long __cil_tmp5 ;
1020 int __cil_tmp6 ;
1021 unsigned int __cil_tmp7 ;
1022 unsigned long __cil_tmp8 ;
1023 unsigned long __cil_tmp9 ;
1024 int __cil_tmp10 ;
1025 unsigned long __cil_tmp11 ;
1026 unsigned long __cil_tmp12 ;
1027 unsigned long __cil_tmp13 ;
1028 unsigned long __cil_tmp14 ;
1029 int __cil_tmp15 ;
1030 int __cil_tmp16 ;
1031 unsigned long __cil_tmp17 ;
1032 unsigned long __cil_tmp18 ;
1033 void (*__cil_tmp19)(struct led_classdev * , enum led_brightness ) ;
1034
1035 {
1036 {
1037#line 23
1038 __cil_tmp3 = (unsigned int )value;
1039#line 23
1040 __cil_tmp4 = (unsigned long )led_cdev;
1041#line 23
1042 __cil_tmp5 = __cil_tmp4 + 12;
1043#line 23
1044 __cil_tmp6 = *((int *)__cil_tmp5);
1045#line 23
1046 __cil_tmp7 = (unsigned int )__cil_tmp6;
1047#line 23
1048 if (__cil_tmp7 < __cil_tmp3) {
1049#line 24
1050 __cil_tmp8 = (unsigned long )led_cdev;
1051#line 24
1052 __cil_tmp9 = __cil_tmp8 + 12;
1053#line 24
1054 __cil_tmp10 = *((int *)__cil_tmp9);
1055#line 24
1056 value = (enum led_brightness )__cil_tmp10;
1057 } else {
1058
1059 }
1060 }
1061#line 25
1062 __cil_tmp11 = (unsigned long )led_cdev;
1063#line 25
1064 __cil_tmp12 = __cil_tmp11 + 8;
1065#line 25
1066 *((int *)__cil_tmp12) = (int )value;
1067 {
1068#line 26
1069 __cil_tmp13 = (unsigned long )led_cdev;
1070#line 26
1071 __cil_tmp14 = __cil_tmp13 + 16;
1072#line 26
1073 __cil_tmp15 = *((int *)__cil_tmp14);
1074#line 26
1075 __cil_tmp16 = __cil_tmp15 & 1;
1076#line 26
1077 if (__cil_tmp16 == 0) {
1078 {
1079#line 27
1080 __cil_tmp17 = (unsigned long )led_cdev;
1081#line 27
1082 __cil_tmp18 = __cil_tmp17 + 24;
1083#line 27
1084 __cil_tmp19 = *((void (**)(struct led_classdev * , enum led_brightness ))__cil_tmp18);
1085#line 27
1086 (*__cil_tmp19)(led_cdev, value);
1087 }
1088 } else {
1089
1090 }
1091 }
1092#line 28
1093 return;
1094}
1095}
1096#line 35 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1097static void defon_trig_activate(struct led_classdev *led_cdev )
1098{ unsigned long __cil_tmp2 ;
1099 unsigned long __cil_tmp3 ;
1100 int __cil_tmp4 ;
1101 enum led_brightness __cil_tmp5 ;
1102
1103 {
1104 {
1105#line 37
1106 __cil_tmp2 = (unsigned long )led_cdev;
1107#line 37
1108 __cil_tmp3 = __cil_tmp2 + 12;
1109#line 37
1110 __cil_tmp4 = *((int *)__cil_tmp3);
1111#line 37
1112 __cil_tmp5 = (enum led_brightness )__cil_tmp4;
1113#line 37
1114 led_set_brightness(led_cdev, __cil_tmp5);
1115 }
1116#line 38
1117 return;
1118}
1119}
1120#line 40 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1121static struct led_trigger defon_led_trigger = {"default-on", & defon_trig_activate, (void (*)(struct led_classdev * ))0, {{0LL},
1122 0U,
1123 0U,
1124 (void *)0,
1125 {(struct lock_class_key *)0,
1126 {(struct lock_class *)0,
1127 (struct lock_class *)0},
1128 (char const *)0,
1129 0,
1130 0UL}},
1131 {(struct list_head *)0, (struct list_head *)0}, {(struct list_head *)0, (struct list_head *)0}};
1132#line 45 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1133static int defon_trig_init(void)
1134{ int tmp ;
1135
1136 {
1137 {
1138#line 47
1139 tmp = led_trigger_register(& defon_led_trigger);
1140 }
1141#line 47
1142 return (tmp);
1143}
1144}
1145#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1146static void defon_trig_exit(void)
1147{
1148
1149 {
1150 {
1151#line 52
1152 led_trigger_unregister(& defon_led_trigger);
1153 }
1154#line 53
1155 return;
1156}
1157}
1158#line 78
1159extern void ldv_check_final_state(void) ;
1160#line 84
1161extern void ldv_initialize(void) ;
1162#line 87
1163extern int __VERIFIER_nondet_int(void) ;
1164#line 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1165int LDV_IN_INTERRUPT ;
1166#line 93 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1167void main(void)
1168{ struct led_classdev *var_group1 ;
1169 int tmp ;
1170 int tmp___0 ;
1171 int tmp___1 ;
1172
1173 {
1174 {
1175#line 111
1176 LDV_IN_INTERRUPT = 1;
1177#line 120
1178 ldv_initialize();
1179#line 126
1180 tmp = defon_trig_init();
1181 }
1182#line 126
1183 if (tmp != 0) {
1184#line 127
1185 goto ldv_final;
1186 } else {
1187
1188 }
1189#line 131
1190 goto ldv_15079;
1191 ldv_15078:
1192 {
1193#line 134
1194 tmp___0 = __VERIFIER_nondet_int();
1195 }
1196#line 136
1197 if (tmp___0 == 0) {
1198#line 136
1199 goto case_0;
1200 } else {
1201 {
1202#line 152
1203 goto switch_default;
1204#line 134
1205 if (0) {
1206 case_0:
1207 {
1208#line 144
1209 defon_trig_activate(var_group1);
1210 }
1211#line 151
1212 goto ldv_15076;
1213 switch_default: ;
1214#line 152
1215 goto ldv_15076;
1216 } else {
1217 switch_break: ;
1218 }
1219 }
1220 }
1221 ldv_15076: ;
1222 ldv_15079:
1223 {
1224#line 131
1225 tmp___1 = __VERIFIER_nondet_int();
1226 }
1227#line 131
1228 if (tmp___1 != 0) {
1229#line 132
1230 goto ldv_15078;
1231 } else {
1232#line 134
1233 goto ldv_15080;
1234 }
1235 ldv_15080: ;
1236 {
1237#line 164
1238 defon_trig_exit();
1239 }
1240 ldv_final:
1241 {
1242#line 167
1243 ldv_check_final_state();
1244 }
1245#line 170
1246 return;
1247}
1248}
1249#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1250void ldv_blast_assert(void)
1251{
1252
1253 {
1254 ERROR: ;
1255#line 6
1256 goto ERROR;
1257}
1258}
1259#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1260extern int __VERIFIER_nondet_int(void) ;
1261#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1262int ldv_spin = 0;
1263#line 195 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1264void ldv_check_alloc_flags(gfp_t flags )
1265{
1266
1267 {
1268#line 198
1269 if (ldv_spin != 0) {
1270#line 198
1271 if (flags != 32U) {
1272 {
1273#line 198
1274 ldv_blast_assert();
1275 }
1276 } else {
1277
1278 }
1279 } else {
1280
1281 }
1282#line 201
1283 return;
1284}
1285}
1286#line 201
1287extern struct page *ldv_some_page(void) ;
1288#line 204 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1289struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1290{ struct page *tmp ;
1291
1292 {
1293#line 207
1294 if (ldv_spin != 0) {
1295#line 207
1296 if (flags != 32U) {
1297 {
1298#line 207
1299 ldv_blast_assert();
1300 }
1301 } else {
1302
1303 }
1304 } else {
1305
1306 }
1307 {
1308#line 209
1309 tmp = ldv_some_page();
1310 }
1311#line 209
1312 return (tmp);
1313}
1314}
1315#line 213 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1316void ldv_check_alloc_nonatomic(void)
1317{
1318
1319 {
1320#line 216
1321 if (ldv_spin != 0) {
1322 {
1323#line 216
1324 ldv_blast_assert();
1325 }
1326 } else {
1327
1328 }
1329#line 219
1330 return;
1331}
1332}
1333#line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1334void ldv_spin_lock(void)
1335{
1336
1337 {
1338#line 223
1339 ldv_spin = 1;
1340#line 224
1341 return;
1342}
1343}
1344#line 227 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1345void ldv_spin_unlock(void)
1346{
1347
1348 {
1349#line 230
1350 ldv_spin = 0;
1351#line 231
1352 return;
1353}
1354}
1355#line 234 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1356int ldv_spin_trylock(void)
1357{ int is_lock ;
1358
1359 {
1360 {
1361#line 239
1362 is_lock = __VERIFIER_nondet_int();
1363 }
1364#line 241
1365 if (is_lock != 0) {
1366#line 244
1367 return (0);
1368 } else {
1369#line 249
1370 ldv_spin = 1;
1371#line 251
1372 return (1);
1373 }
1374}
1375}
1376#line 418 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12459/dscv_tempdir/dscv/ri/43_1a/drivers/leds/ledtrig-default-on.c.p"
1377void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1378{
1379
1380 {
1381 {
1382#line 424
1383 ldv_check_alloc_flags(ldv_func_arg2);
1384#line 426
1385 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1386 }
1387#line 427
1388 return ((void *)0);
1389}
1390}