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 206 "include/linux/types.h"
51typedef u64 phys_addr_t;
52#line 211 "include/linux/types.h"
53typedef phys_addr_t resource_size_t;
54#line 221 "include/linux/types.h"
55struct __anonstruct_atomic_t_6 {
56 int counter ;
57};
58#line 221 "include/linux/types.h"
59typedef struct __anonstruct_atomic_t_6 atomic_t;
60#line 226 "include/linux/types.h"
61struct __anonstruct_atomic64_t_7 {
62 long counter ;
63};
64#line 226 "include/linux/types.h"
65typedef struct __anonstruct_atomic64_t_7 atomic64_t;
66#line 227 "include/linux/types.h"
67struct list_head {
68 struct list_head *next ;
69 struct list_head *prev ;
70};
71#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
72struct module;
73#line 55
74struct module;
75#line 146 "include/linux/init.h"
76typedef void (*ctor_fn_t)(void);
77#line 46 "include/linux/dynamic_debug.h"
78struct device;
79#line 46
80struct device;
81#line 57
82struct completion;
83#line 57
84struct completion;
85#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
86struct page;
87#line 58
88struct page;
89#line 26 "include/asm-generic/getorder.h"
90struct task_struct;
91#line 26
92struct task_struct;
93#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
94struct file;
95#line 290
96struct file;
97#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
98struct arch_spinlock;
99#line 327
100struct arch_spinlock;
101#line 306 "include/linux/bitmap.h"
102struct bug_entry {
103 int bug_addr_disp ;
104 int file_disp ;
105 unsigned short line ;
106 unsigned short flags ;
107};
108#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
109struct static_key;
110#line 234
111struct static_key;
112#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
113struct kmem_cache;
114#line 23 "include/asm-generic/atomic-long.h"
115typedef atomic64_t atomic_long_t;
116#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
117typedef u16 __ticket_t;
118#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
119typedef u32 __ticketpair_t;
120#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
121struct __raw_tickets {
122 __ticket_t head ;
123 __ticket_t tail ;
124};
125#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
126union __anonunion_ldv_5907_29 {
127 __ticketpair_t head_tail ;
128 struct __raw_tickets tickets ;
129};
130#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
131struct arch_spinlock {
132 union __anonunion_ldv_5907_29 ldv_5907 ;
133};
134#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
135typedef struct arch_spinlock arch_spinlock_t;
136#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
137struct __anonstruct_ldv_5914_31 {
138 u32 read ;
139 s32 write ;
140};
141#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
142union __anonunion_arch_rwlock_t_30 {
143 s64 lock ;
144 struct __anonstruct_ldv_5914_31 ldv_5914 ;
145};
146#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
147typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
148#line 34
149struct lockdep_map;
150#line 34
151struct lockdep_map;
152#line 55 "include/linux/debug_locks.h"
153struct stack_trace {
154 unsigned int nr_entries ;
155 unsigned int max_entries ;
156 unsigned long *entries ;
157 int skip ;
158};
159#line 26 "include/linux/stacktrace.h"
160struct lockdep_subclass_key {
161 char __one_byte ;
162};
163#line 53 "include/linux/lockdep.h"
164struct lock_class_key {
165 struct lockdep_subclass_key subkeys[8U] ;
166};
167#line 59 "include/linux/lockdep.h"
168struct lock_class {
169 struct list_head hash_entry ;
170 struct list_head lock_entry ;
171 struct lockdep_subclass_key *key ;
172 unsigned int subclass ;
173 unsigned int dep_gen_id ;
174 unsigned long usage_mask ;
175 struct stack_trace usage_traces[13U] ;
176 struct list_head locks_after ;
177 struct list_head locks_before ;
178 unsigned int version ;
179 unsigned long ops ;
180 char const *name ;
181 int name_version ;
182 unsigned long contention_point[4U] ;
183 unsigned long contending_point[4U] ;
184};
185#line 144 "include/linux/lockdep.h"
186struct lockdep_map {
187 struct lock_class_key *key ;
188 struct lock_class *class_cache[2U] ;
189 char const *name ;
190 int cpu ;
191 unsigned long ip ;
192};
193#line 556 "include/linux/lockdep.h"
194struct raw_spinlock {
195 arch_spinlock_t raw_lock ;
196 unsigned int magic ;
197 unsigned int owner_cpu ;
198 void *owner ;
199 struct lockdep_map dep_map ;
200};
201#line 32 "include/linux/spinlock_types.h"
202typedef struct raw_spinlock raw_spinlock_t;
203#line 33 "include/linux/spinlock_types.h"
204struct __anonstruct_ldv_6122_33 {
205 u8 __padding[24U] ;
206 struct lockdep_map dep_map ;
207};
208#line 33 "include/linux/spinlock_types.h"
209union __anonunion_ldv_6123_32 {
210 struct raw_spinlock rlock ;
211 struct __anonstruct_ldv_6122_33 ldv_6122 ;
212};
213#line 33 "include/linux/spinlock_types.h"
214struct spinlock {
215 union __anonunion_ldv_6123_32 ldv_6123 ;
216};
217#line 76 "include/linux/spinlock_types.h"
218typedef struct spinlock spinlock_t;
219#line 23 "include/linux/rwlock_types.h"
220struct __anonstruct_rwlock_t_34 {
221 arch_rwlock_t raw_lock ;
222 unsigned int magic ;
223 unsigned int owner_cpu ;
224 void *owner ;
225 struct lockdep_map dep_map ;
226};
227#line 23 "include/linux/rwlock_types.h"
228typedef struct __anonstruct_rwlock_t_34 rwlock_t;
229#line 48 "include/linux/wait.h"
230struct __wait_queue_head {
231 spinlock_t lock ;
232 struct list_head task_list ;
233};
234#line 53 "include/linux/wait.h"
235typedef struct __wait_queue_head wait_queue_head_t;
236#line 670 "include/linux/mmzone.h"
237struct mutex {
238 atomic_t count ;
239 spinlock_t wait_lock ;
240 struct list_head wait_list ;
241 struct task_struct *owner ;
242 char const *name ;
243 void *magic ;
244 struct lockdep_map dep_map ;
245};
246#line 171 "include/linux/mutex.h"
247struct rw_semaphore;
248#line 171
249struct rw_semaphore;
250#line 172 "include/linux/mutex.h"
251struct rw_semaphore {
252 long count ;
253 raw_spinlock_t wait_lock ;
254 struct list_head wait_list ;
255 struct lockdep_map dep_map ;
256};
257#line 128 "include/linux/rwsem.h"
258struct completion {
259 unsigned int done ;
260 wait_queue_head_t wait ;
261};
262#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
263struct resource {
264 resource_size_t start ;
265 resource_size_t end ;
266 char const *name ;
267 unsigned long flags ;
268 struct resource *parent ;
269 struct resource *sibling ;
270 struct resource *child ;
271};
272#line 312 "include/linux/jiffies.h"
273union ktime {
274 s64 tv64 ;
275};
276#line 59 "include/linux/ktime.h"
277typedef union ktime ktime_t;
278#line 341
279struct tvec_base;
280#line 341
281struct tvec_base;
282#line 342 "include/linux/ktime.h"
283struct timer_list {
284 struct list_head entry ;
285 unsigned long expires ;
286 struct tvec_base *base ;
287 void (*function)(unsigned long ) ;
288 unsigned long data ;
289 int slack ;
290 int start_pid ;
291 void *start_site ;
292 char start_comm[16U] ;
293 struct lockdep_map lockdep_map ;
294};
295#line 302 "include/linux/timer.h"
296struct work_struct;
297#line 302
298struct work_struct;
299#line 45 "include/linux/workqueue.h"
300struct work_struct {
301 atomic_long_t data ;
302 struct list_head entry ;
303 void (*func)(struct work_struct * ) ;
304 struct lockdep_map lockdep_map ;
305};
306#line 46 "include/linux/pm.h"
307struct pm_message {
308 int event ;
309};
310#line 52 "include/linux/pm.h"
311typedef struct pm_message pm_message_t;
312#line 53 "include/linux/pm.h"
313struct dev_pm_ops {
314 int (*prepare)(struct device * ) ;
315 void (*complete)(struct device * ) ;
316 int (*suspend)(struct device * ) ;
317 int (*resume)(struct device * ) ;
318 int (*freeze)(struct device * ) ;
319 int (*thaw)(struct device * ) ;
320 int (*poweroff)(struct device * ) ;
321 int (*restore)(struct device * ) ;
322 int (*suspend_late)(struct device * ) ;
323 int (*resume_early)(struct device * ) ;
324 int (*freeze_late)(struct device * ) ;
325 int (*thaw_early)(struct device * ) ;
326 int (*poweroff_late)(struct device * ) ;
327 int (*restore_early)(struct device * ) ;
328 int (*suspend_noirq)(struct device * ) ;
329 int (*resume_noirq)(struct device * ) ;
330 int (*freeze_noirq)(struct device * ) ;
331 int (*thaw_noirq)(struct device * ) ;
332 int (*poweroff_noirq)(struct device * ) ;
333 int (*restore_noirq)(struct device * ) ;
334 int (*runtime_suspend)(struct device * ) ;
335 int (*runtime_resume)(struct device * ) ;
336 int (*runtime_idle)(struct device * ) ;
337};
338#line 289
339enum rpm_status {
340 RPM_ACTIVE = 0,
341 RPM_RESUMING = 1,
342 RPM_SUSPENDED = 2,
343 RPM_SUSPENDING = 3
344} ;
345#line 296
346enum rpm_request {
347 RPM_REQ_NONE = 0,
348 RPM_REQ_IDLE = 1,
349 RPM_REQ_SUSPEND = 2,
350 RPM_REQ_AUTOSUSPEND = 3,
351 RPM_REQ_RESUME = 4
352} ;
353#line 304
354struct wakeup_source;
355#line 304
356struct wakeup_source;
357#line 494 "include/linux/pm.h"
358struct pm_subsys_data {
359 spinlock_t lock ;
360 unsigned int refcount ;
361};
362#line 499
363struct dev_pm_qos_request;
364#line 499
365struct pm_qos_constraints;
366#line 499 "include/linux/pm.h"
367struct dev_pm_info {
368 pm_message_t power_state ;
369 unsigned char can_wakeup : 1 ;
370 unsigned char async_suspend : 1 ;
371 bool is_prepared ;
372 bool is_suspended ;
373 bool ignore_children ;
374 spinlock_t lock ;
375 struct list_head entry ;
376 struct completion completion ;
377 struct wakeup_source *wakeup ;
378 bool wakeup_path ;
379 struct timer_list suspend_timer ;
380 unsigned long timer_expires ;
381 struct work_struct work ;
382 wait_queue_head_t wait_queue ;
383 atomic_t usage_count ;
384 atomic_t child_count ;
385 unsigned char disable_depth : 3 ;
386 unsigned char idle_notification : 1 ;
387 unsigned char request_pending : 1 ;
388 unsigned char deferred_resume : 1 ;
389 unsigned char run_wake : 1 ;
390 unsigned char runtime_auto : 1 ;
391 unsigned char no_callbacks : 1 ;
392 unsigned char irq_safe : 1 ;
393 unsigned char use_autosuspend : 1 ;
394 unsigned char timer_autosuspends : 1 ;
395 enum rpm_request request ;
396 enum rpm_status runtime_status ;
397 int runtime_error ;
398 int autosuspend_delay ;
399 unsigned long last_busy ;
400 unsigned long active_jiffies ;
401 unsigned long suspended_jiffies ;
402 unsigned long accounting_timestamp ;
403 ktime_t suspend_time ;
404 s64 max_time_suspended_ns ;
405 struct dev_pm_qos_request *pq_req ;
406 struct pm_subsys_data *subsys_data ;
407 struct pm_qos_constraints *constraints ;
408};
409#line 558 "include/linux/pm.h"
410struct dev_pm_domain {
411 struct dev_pm_ops ops ;
412};
413#line 18 "include/asm-generic/pci_iomap.h"
414struct vm_area_struct;
415#line 18
416struct vm_area_struct;
417#line 18 "include/linux/elf.h"
418typedef __u64 Elf64_Addr;
419#line 19 "include/linux/elf.h"
420typedef __u16 Elf64_Half;
421#line 23 "include/linux/elf.h"
422typedef __u32 Elf64_Word;
423#line 24 "include/linux/elf.h"
424typedef __u64 Elf64_Xword;
425#line 193 "include/linux/elf.h"
426struct elf64_sym {
427 Elf64_Word st_name ;
428 unsigned char st_info ;
429 unsigned char st_other ;
430 Elf64_Half st_shndx ;
431 Elf64_Addr st_value ;
432 Elf64_Xword st_size ;
433};
434#line 201 "include/linux/elf.h"
435typedef struct elf64_sym Elf64_Sym;
436#line 445
437struct sock;
438#line 445
439struct sock;
440#line 446
441struct kobject;
442#line 446
443struct kobject;
444#line 447
445enum kobj_ns_type {
446 KOBJ_NS_TYPE_NONE = 0,
447 KOBJ_NS_TYPE_NET = 1,
448 KOBJ_NS_TYPES = 2
449} ;
450#line 453 "include/linux/elf.h"
451struct kobj_ns_type_operations {
452 enum kobj_ns_type type ;
453 void *(*grab_current_ns)(void) ;
454 void const *(*netlink_ns)(struct sock * ) ;
455 void const *(*initial_ns)(void) ;
456 void (*drop_ns)(void * ) ;
457};
458#line 57 "include/linux/kobject_ns.h"
459struct attribute {
460 char const *name ;
461 umode_t mode ;
462 struct lock_class_key *key ;
463 struct lock_class_key skey ;
464};
465#line 33 "include/linux/sysfs.h"
466struct attribute_group {
467 char const *name ;
468 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
469 struct attribute **attrs ;
470};
471#line 62 "include/linux/sysfs.h"
472struct bin_attribute {
473 struct attribute attr ;
474 size_t size ;
475 void *private ;
476 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
477 loff_t , size_t ) ;
478 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
479 loff_t , size_t ) ;
480 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
481};
482#line 98 "include/linux/sysfs.h"
483struct sysfs_ops {
484 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
485 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
486 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
487};
488#line 117
489struct sysfs_dirent;
490#line 117
491struct sysfs_dirent;
492#line 182 "include/linux/sysfs.h"
493struct kref {
494 atomic_t refcount ;
495};
496#line 49 "include/linux/kobject.h"
497struct kset;
498#line 49
499struct kobj_type;
500#line 49 "include/linux/kobject.h"
501struct kobject {
502 char const *name ;
503 struct list_head entry ;
504 struct kobject *parent ;
505 struct kset *kset ;
506 struct kobj_type *ktype ;
507 struct sysfs_dirent *sd ;
508 struct kref kref ;
509 unsigned char state_initialized : 1 ;
510 unsigned char state_in_sysfs : 1 ;
511 unsigned char state_add_uevent_sent : 1 ;
512 unsigned char state_remove_uevent_sent : 1 ;
513 unsigned char uevent_suppress : 1 ;
514};
515#line 107 "include/linux/kobject.h"
516struct kobj_type {
517 void (*release)(struct kobject * ) ;
518 struct sysfs_ops const *sysfs_ops ;
519 struct attribute **default_attrs ;
520 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
521 void const *(*namespace)(struct kobject * ) ;
522};
523#line 115 "include/linux/kobject.h"
524struct kobj_uevent_env {
525 char *envp[32U] ;
526 int envp_idx ;
527 char buf[2048U] ;
528 int buflen ;
529};
530#line 122 "include/linux/kobject.h"
531struct kset_uevent_ops {
532 int (* const filter)(struct kset * , struct kobject * ) ;
533 char const *(* const name)(struct kset * , struct kobject * ) ;
534 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
535};
536#line 139 "include/linux/kobject.h"
537struct kset {
538 struct list_head list ;
539 spinlock_t list_lock ;
540 struct kobject kobj ;
541 struct kset_uevent_ops const *uevent_ops ;
542};
543#line 215
544struct kernel_param;
545#line 215
546struct kernel_param;
547#line 216 "include/linux/kobject.h"
548struct kernel_param_ops {
549 int (*set)(char const * , struct kernel_param const * ) ;
550 int (*get)(char * , struct kernel_param const * ) ;
551 void (*free)(void * ) ;
552};
553#line 49 "include/linux/moduleparam.h"
554struct kparam_string;
555#line 49
556struct kparam_array;
557#line 49 "include/linux/moduleparam.h"
558union __anonunion_ldv_13363_134 {
559 void *arg ;
560 struct kparam_string const *str ;
561 struct kparam_array const *arr ;
562};
563#line 49 "include/linux/moduleparam.h"
564struct kernel_param {
565 char const *name ;
566 struct kernel_param_ops const *ops ;
567 u16 perm ;
568 s16 level ;
569 union __anonunion_ldv_13363_134 ldv_13363 ;
570};
571#line 61 "include/linux/moduleparam.h"
572struct kparam_string {
573 unsigned int maxlen ;
574 char *string ;
575};
576#line 67 "include/linux/moduleparam.h"
577struct kparam_array {
578 unsigned int max ;
579 unsigned int elemsize ;
580 unsigned int *num ;
581 struct kernel_param_ops const *ops ;
582 void *elem ;
583};
584#line 458 "include/linux/moduleparam.h"
585struct static_key {
586 atomic_t enabled ;
587};
588#line 225 "include/linux/jump_label.h"
589struct tracepoint;
590#line 225
591struct tracepoint;
592#line 226 "include/linux/jump_label.h"
593struct tracepoint_func {
594 void *func ;
595 void *data ;
596};
597#line 29 "include/linux/tracepoint.h"
598struct tracepoint {
599 char const *name ;
600 struct static_key key ;
601 void (*regfunc)(void) ;
602 void (*unregfunc)(void) ;
603 struct tracepoint_func *funcs ;
604};
605#line 86 "include/linux/tracepoint.h"
606struct kernel_symbol {
607 unsigned long value ;
608 char const *name ;
609};
610#line 27 "include/linux/export.h"
611struct mod_arch_specific {
612
613};
614#line 34 "include/linux/module.h"
615struct module_param_attrs;
616#line 34 "include/linux/module.h"
617struct module_kobject {
618 struct kobject kobj ;
619 struct module *mod ;
620 struct kobject *drivers_dir ;
621 struct module_param_attrs *mp ;
622};
623#line 43 "include/linux/module.h"
624struct module_attribute {
625 struct attribute attr ;
626 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
627 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
628 size_t ) ;
629 void (*setup)(struct module * , char const * ) ;
630 int (*test)(struct module * ) ;
631 void (*free)(struct module * ) ;
632};
633#line 69
634struct exception_table_entry;
635#line 69
636struct exception_table_entry;
637#line 198
638enum module_state {
639 MODULE_STATE_LIVE = 0,
640 MODULE_STATE_COMING = 1,
641 MODULE_STATE_GOING = 2
642} ;
643#line 204 "include/linux/module.h"
644struct module_ref {
645 unsigned long incs ;
646 unsigned long decs ;
647};
648#line 219
649struct module_sect_attrs;
650#line 219
651struct module_notes_attrs;
652#line 219
653struct ftrace_event_call;
654#line 219 "include/linux/module.h"
655struct module {
656 enum module_state state ;
657 struct list_head list ;
658 char name[56U] ;
659 struct module_kobject mkobj ;
660 struct module_attribute *modinfo_attrs ;
661 char const *version ;
662 char const *srcversion ;
663 struct kobject *holders_dir ;
664 struct kernel_symbol const *syms ;
665 unsigned long const *crcs ;
666 unsigned int num_syms ;
667 struct kernel_param *kp ;
668 unsigned int num_kp ;
669 unsigned int num_gpl_syms ;
670 struct kernel_symbol const *gpl_syms ;
671 unsigned long const *gpl_crcs ;
672 struct kernel_symbol const *unused_syms ;
673 unsigned long const *unused_crcs ;
674 unsigned int num_unused_syms ;
675 unsigned int num_unused_gpl_syms ;
676 struct kernel_symbol const *unused_gpl_syms ;
677 unsigned long const *unused_gpl_crcs ;
678 struct kernel_symbol const *gpl_future_syms ;
679 unsigned long const *gpl_future_crcs ;
680 unsigned int num_gpl_future_syms ;
681 unsigned int num_exentries ;
682 struct exception_table_entry *extable ;
683 int (*init)(void) ;
684 void *module_init ;
685 void *module_core ;
686 unsigned int init_size ;
687 unsigned int core_size ;
688 unsigned int init_text_size ;
689 unsigned int core_text_size ;
690 unsigned int init_ro_size ;
691 unsigned int core_ro_size ;
692 struct mod_arch_specific arch ;
693 unsigned int taints ;
694 unsigned int num_bugs ;
695 struct list_head bug_list ;
696 struct bug_entry *bug_table ;
697 Elf64_Sym *symtab ;
698 Elf64_Sym *core_symtab ;
699 unsigned int num_symtab ;
700 unsigned int core_num_syms ;
701 char *strtab ;
702 char *core_strtab ;
703 struct module_sect_attrs *sect_attrs ;
704 struct module_notes_attrs *notes_attrs ;
705 char *args ;
706 void *percpu ;
707 unsigned int percpu_size ;
708 unsigned int num_tracepoints ;
709 struct tracepoint * const *tracepoints_ptrs ;
710 unsigned int num_trace_bprintk_fmt ;
711 char const **trace_bprintk_fmt_start ;
712 struct ftrace_event_call **trace_events ;
713 unsigned int num_trace_events ;
714 struct list_head source_list ;
715 struct list_head target_list ;
716 struct task_struct *waiter ;
717 void (*exit)(void) ;
718 struct module_ref *refptr ;
719 ctor_fn_t (**ctors)(void) ;
720 unsigned int num_ctors ;
721};
722#line 88 "include/linux/kmemleak.h"
723struct kmem_cache_cpu {
724 void **freelist ;
725 unsigned long tid ;
726 struct page *page ;
727 struct page *partial ;
728 int node ;
729 unsigned int stat[26U] ;
730};
731#line 55 "include/linux/slub_def.h"
732struct kmem_cache_node {
733 spinlock_t list_lock ;
734 unsigned long nr_partial ;
735 struct list_head partial ;
736 atomic_long_t nr_slabs ;
737 atomic_long_t total_objects ;
738 struct list_head full ;
739};
740#line 66 "include/linux/slub_def.h"
741struct kmem_cache_order_objects {
742 unsigned long x ;
743};
744#line 76 "include/linux/slub_def.h"
745struct kmem_cache {
746 struct kmem_cache_cpu *cpu_slab ;
747 unsigned long flags ;
748 unsigned long min_partial ;
749 int size ;
750 int objsize ;
751 int offset ;
752 int cpu_partial ;
753 struct kmem_cache_order_objects oo ;
754 struct kmem_cache_order_objects max ;
755 struct kmem_cache_order_objects min ;
756 gfp_t allocflags ;
757 int refcount ;
758 void (*ctor)(void * ) ;
759 int inuse ;
760 int align ;
761 int reserved ;
762 char const *name ;
763 struct list_head list ;
764 struct kobject kobj ;
765 int remote_node_defrag_ratio ;
766 struct kmem_cache_node *node[1024U] ;
767};
768#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
769struct klist_node;
770#line 15
771struct klist_node;
772#line 37 "include/linux/klist.h"
773struct klist_node {
774 void *n_klist ;
775 struct list_head n_node ;
776 struct kref n_ref ;
777};
778#line 67
779struct dma_map_ops;
780#line 67 "include/linux/klist.h"
781struct dev_archdata {
782 void *acpi_handle ;
783 struct dma_map_ops *dma_ops ;
784 void *iommu ;
785};
786#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
787struct pdev_archdata {
788
789};
790#line 17
791struct device_private;
792#line 17
793struct device_private;
794#line 18
795struct device_driver;
796#line 18
797struct device_driver;
798#line 19
799struct driver_private;
800#line 19
801struct driver_private;
802#line 20
803struct class;
804#line 20
805struct class;
806#line 21
807struct subsys_private;
808#line 21
809struct subsys_private;
810#line 22
811struct bus_type;
812#line 22
813struct bus_type;
814#line 23
815struct device_node;
816#line 23
817struct device_node;
818#line 24
819struct iommu_ops;
820#line 24
821struct iommu_ops;
822#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
823struct bus_attribute {
824 struct attribute attr ;
825 ssize_t (*show)(struct bus_type * , char * ) ;
826 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
827};
828#line 51 "include/linux/device.h"
829struct device_attribute;
830#line 51
831struct driver_attribute;
832#line 51 "include/linux/device.h"
833struct bus_type {
834 char const *name ;
835 char const *dev_name ;
836 struct device *dev_root ;
837 struct bus_attribute *bus_attrs ;
838 struct device_attribute *dev_attrs ;
839 struct driver_attribute *drv_attrs ;
840 int (*match)(struct device * , struct device_driver * ) ;
841 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
842 int (*probe)(struct device * ) ;
843 int (*remove)(struct device * ) ;
844 void (*shutdown)(struct device * ) ;
845 int (*suspend)(struct device * , pm_message_t ) ;
846 int (*resume)(struct device * ) ;
847 struct dev_pm_ops const *pm ;
848 struct iommu_ops *iommu_ops ;
849 struct subsys_private *p ;
850};
851#line 125
852struct device_type;
853#line 182
854struct of_device_id;
855#line 182 "include/linux/device.h"
856struct device_driver {
857 char const *name ;
858 struct bus_type *bus ;
859 struct module *owner ;
860 char const *mod_name ;
861 bool suppress_bind_attrs ;
862 struct of_device_id const *of_match_table ;
863 int (*probe)(struct device * ) ;
864 int (*remove)(struct device * ) ;
865 void (*shutdown)(struct device * ) ;
866 int (*suspend)(struct device * , pm_message_t ) ;
867 int (*resume)(struct device * ) ;
868 struct attribute_group const **groups ;
869 struct dev_pm_ops const *pm ;
870 struct driver_private *p ;
871};
872#line 245 "include/linux/device.h"
873struct driver_attribute {
874 struct attribute attr ;
875 ssize_t (*show)(struct device_driver * , char * ) ;
876 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
877};
878#line 299
879struct class_attribute;
880#line 299 "include/linux/device.h"
881struct class {
882 char const *name ;
883 struct module *owner ;
884 struct class_attribute *class_attrs ;
885 struct device_attribute *dev_attrs ;
886 struct bin_attribute *dev_bin_attrs ;
887 struct kobject *dev_kobj ;
888 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
889 char *(*devnode)(struct device * , umode_t * ) ;
890 void (*class_release)(struct class * ) ;
891 void (*dev_release)(struct device * ) ;
892 int (*suspend)(struct device * , pm_message_t ) ;
893 int (*resume)(struct device * ) ;
894 struct kobj_ns_type_operations const *ns_type ;
895 void const *(*namespace)(struct device * ) ;
896 struct dev_pm_ops const *pm ;
897 struct subsys_private *p ;
898};
899#line 394 "include/linux/device.h"
900struct class_attribute {
901 struct attribute attr ;
902 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
903 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
904 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
905};
906#line 447 "include/linux/device.h"
907struct device_type {
908 char const *name ;
909 struct attribute_group const **groups ;
910 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
911 char *(*devnode)(struct device * , umode_t * ) ;
912 void (*release)(struct device * ) ;
913 struct dev_pm_ops const *pm ;
914};
915#line 474 "include/linux/device.h"
916struct device_attribute {
917 struct attribute attr ;
918 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
919 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
920 size_t ) ;
921};
922#line 557 "include/linux/device.h"
923struct device_dma_parameters {
924 unsigned int max_segment_size ;
925 unsigned long segment_boundary_mask ;
926};
927#line 567
928struct dma_coherent_mem;
929#line 567 "include/linux/device.h"
930struct device {
931 struct device *parent ;
932 struct device_private *p ;
933 struct kobject kobj ;
934 char const *init_name ;
935 struct device_type const *type ;
936 struct mutex mutex ;
937 struct bus_type *bus ;
938 struct device_driver *driver ;
939 void *platform_data ;
940 struct dev_pm_info power ;
941 struct dev_pm_domain *pm_domain ;
942 int numa_node ;
943 u64 *dma_mask ;
944 u64 coherent_dma_mask ;
945 struct device_dma_parameters *dma_parms ;
946 struct list_head dma_pools ;
947 struct dma_coherent_mem *dma_mem ;
948 struct dev_archdata archdata ;
949 struct device_node *of_node ;
950 dev_t devt ;
951 u32 id ;
952 spinlock_t devres_lock ;
953 struct list_head devres_head ;
954 struct klist_node knode_class ;
955 struct class *class ;
956 struct attribute_group const **groups ;
957 void (*release)(struct device * ) ;
958};
959#line 681 "include/linux/device.h"
960struct wakeup_source {
961 char const *name ;
962 struct list_head entry ;
963 spinlock_t lock ;
964 struct timer_list timer ;
965 unsigned long timer_expires ;
966 ktime_t total_time ;
967 ktime_t max_time ;
968 ktime_t last_time ;
969 unsigned long event_count ;
970 unsigned long active_count ;
971 unsigned long relax_count ;
972 unsigned long hit_count ;
973 unsigned char active : 1 ;
974};
975#line 12 "include/linux/mod_devicetable.h"
976typedef unsigned long kernel_ulong_t;
977#line 215 "include/linux/mod_devicetable.h"
978struct of_device_id {
979 char name[32U] ;
980 char type[32U] ;
981 char compatible[128U] ;
982 void *data ;
983};
984#line 492 "include/linux/mod_devicetable.h"
985struct platform_device_id {
986 char name[20U] ;
987 kernel_ulong_t driver_data ;
988};
989#line 584
990struct mfd_cell;
991#line 584
992struct mfd_cell;
993#line 585 "include/linux/mod_devicetable.h"
994struct platform_device {
995 char const *name ;
996 int id ;
997 struct device dev ;
998 u32 num_resources ;
999 struct resource *resource ;
1000 struct platform_device_id const *id_entry ;
1001 struct mfd_cell *mfd_cell ;
1002 struct pdev_archdata archdata ;
1003};
1004#line 272 "include/linux/platform_device.h"
1005enum led_brightness {
1006 LED_OFF = 0,
1007 LED_HALF = 127,
1008 LED_FULL = 255
1009} ;
1010#line 278
1011struct led_trigger;
1012#line 278 "include/linux/platform_device.h"
1013struct led_classdev {
1014 char const *name ;
1015 int brightness ;
1016 int max_brightness ;
1017 int flags ;
1018 void (*brightness_set)(struct led_classdev * , enum led_brightness ) ;
1019 enum led_brightness (*brightness_get)(struct led_classdev * ) ;
1020 int (*blink_set)(struct led_classdev * , unsigned long * , unsigned long * ) ;
1021 struct device *dev ;
1022 struct list_head node ;
1023 char const *default_trigger ;
1024 unsigned long blink_delay_on ;
1025 unsigned long blink_delay_off ;
1026 struct timer_list blink_timer ;
1027 int blink_brightness ;
1028 struct rw_semaphore trigger_lock ;
1029 struct led_trigger *trigger ;
1030 struct list_head trig_list ;
1031 void *trigger_data ;
1032};
1033#line 113 "include/linux/leds.h"
1034struct led_trigger {
1035 char const *name ;
1036 void (*activate)(struct led_classdev * ) ;
1037 void (*deactivate)(struct led_classdev * ) ;
1038 rwlock_t leddev_list_lock ;
1039 struct list_head led_cdevs ;
1040 struct list_head next_trig ;
1041};
1042#line 69 "include/linux/io.h"
1043struct ot200_led {
1044 struct led_classdev cdev ;
1045 char const *name ;
1046 unsigned long port ;
1047 u8 mask ;
1048};
1049#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1050void ldv_spin_lock(void) ;
1051#line 3
1052void ldv_spin_unlock(void) ;
1053#line 4
1054int ldv_spin_trylock(void) ;
1055#line 43 "include/linux/spinlock_api_smp.h"
1056extern void _raw_spin_unlock_irqrestore(raw_spinlock_t * , unsigned long ) ;
1057#line 350 "include/linux/spinlock.h"
1058__inline static void ldv_spin_unlock_irqrestore_8(spinlock_t *lock , unsigned long flags )
1059{ struct raw_spinlock *__cil_tmp5 ;
1060
1061 {
1062 {
1063#line 352
1064 __cil_tmp5 = (struct raw_spinlock *)lock;
1065#line 352
1066 _raw_spin_unlock_irqrestore(__cil_tmp5, flags);
1067 }
1068#line 353
1069 return;
1070}
1071}
1072#line 350
1073__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) ;
1074#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1075__inline static void outb(unsigned char value , int port )
1076{
1077
1078 {
1079#line 308
1080 __asm__ volatile ("outb %b0, %w1": : "a" (value), "Nd" (port));
1081#line 309
1082 return;
1083}
1084}
1085#line 220 "include/linux/slub_def.h"
1086extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1087#line 223
1088void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1089#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1090void ldv_check_alloc_flags(gfp_t flags ) ;
1091#line 12
1092void ldv_check_alloc_nonatomic(void) ;
1093#line 14
1094struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1095#line 79 "include/linux/leds.h"
1096extern int led_classdev_register(struct device * , struct led_classdev * ) ;
1097#line 81
1098extern void led_classdev_unregister(struct led_classdev * ) ;
1099#line 46 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1100static struct ot200_led leds[10U] =
1101#line 46 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1102 { {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1103 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1104 unsigned long * ,
1105 unsigned long * ))0,
1106 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1107 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1108 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1109 (char)0, (char)0,
1110 (char)0, (char)0,
1111 (char)0, (char)0,
1112 (char)0, (char)0,
1113 (char)0, (char)0,
1114 (char)0, (char)0,
1115 (char)0, (char)0},
1116 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1117 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1118 {(struct lock_class_key *)0,
1119 {(struct lock_class *)0,
1120 (struct lock_class *)0},
1121 (char const *)0, 0, 0UL}},
1122 {(struct list_head *)0, (struct list_head *)0},
1123 {(struct lock_class_key *)0, {(struct lock_class *)0,
1124 (struct lock_class *)0},
1125 (char const *)0, 0, 0UL}},
1126 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1127 "led_run", 90UL, (u8 )1U},
1128 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1129 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1130 unsigned long * ,
1131 unsigned long * ))0,
1132 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1133 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1134 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1135 (char)0, (char)0,
1136 (char)0, (char)0,
1137 (char)0, (char)0,
1138 (char)0, (char)0,
1139 (char)0, (char)0,
1140 (char)0, (char)0,
1141 (char)0, (char)0},
1142 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1143 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1144 {(struct lock_class_key *)0,
1145 {(struct lock_class *)0,
1146 (struct lock_class *)0},
1147 (char const *)0, 0, 0UL}},
1148 {(struct list_head *)0, (struct list_head *)0},
1149 {(struct lock_class_key *)0, {(struct lock_class *)0,
1150 (struct lock_class *)0},
1151 (char const *)0, 0, 0UL}},
1152 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1153 "led_init", 90UL, (u8 )2U},
1154 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1155 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1156 unsigned long * ,
1157 unsigned long * ))0,
1158 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1159 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1160 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1161 (char)0, (char)0,
1162 (char)0, (char)0,
1163 (char)0, (char)0,
1164 (char)0, (char)0,
1165 (char)0, (char)0,
1166 (char)0, (char)0,
1167 (char)0, (char)0},
1168 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1169 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1170 {(struct lock_class_key *)0,
1171 {(struct lock_class *)0,
1172 (struct lock_class *)0},
1173 (char const *)0, 0, 0UL}},
1174 {(struct list_head *)0, (struct list_head *)0},
1175 {(struct lock_class_key *)0, {(struct lock_class *)0,
1176 (struct lock_class *)0},
1177 (char const *)0, 0, 0UL}},
1178 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1179 "led_err", 90UL, (u8 )4U},
1180 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1181 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1182 unsigned long * ,
1183 unsigned long * ))0,
1184 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1185 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1186 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1187 (char)0, (char)0,
1188 (char)0, (char)0,
1189 (char)0, (char)0,
1190 (char)0, (char)0,
1191 (char)0, (char)0,
1192 (char)0, (char)0,
1193 (char)0, (char)0},
1194 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1195 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1196 {(struct lock_class_key *)0,
1197 {(struct lock_class *)0,
1198 (struct lock_class *)0},
1199 (char const *)0, 0, 0UL}},
1200 {(struct list_head *)0, (struct list_head *)0},
1201 {(struct lock_class_key *)0, {(struct lock_class *)0,
1202 (struct lock_class *)0},
1203 (char const *)0, 0, 0UL}},
1204 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1205 "led_1", 73UL, (u8 )128U},
1206 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1207 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1208 unsigned long * ,
1209 unsigned long * ))0,
1210 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1211 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1212 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1213 (char)0, (char)0,
1214 (char)0, (char)0,
1215 (char)0, (char)0,
1216 (char)0, (char)0,
1217 (char)0, (char)0,
1218 (char)0, (char)0,
1219 (char)0, (char)0},
1220 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1221 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1222 {(struct lock_class_key *)0,
1223 {(struct lock_class *)0,
1224 (struct lock_class *)0},
1225 (char const *)0, 0, 0UL}},
1226 {(struct list_head *)0, (struct list_head *)0},
1227 {(struct lock_class_key *)0, {(struct lock_class *)0,
1228 (struct lock_class *)0},
1229 (char const *)0, 0, 0UL}},
1230 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1231 "led_2", 73UL, (u8 )64U},
1232 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1233 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1234 unsigned long * ,
1235 unsigned long * ))0,
1236 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1237 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1238 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1239 (char)0, (char)0,
1240 (char)0, (char)0,
1241 (char)0, (char)0,
1242 (char)0, (char)0,
1243 (char)0, (char)0,
1244 (char)0, (char)0,
1245 (char)0, (char)0},
1246 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1247 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1248 {(struct lock_class_key *)0,
1249 {(struct lock_class *)0,
1250 (struct lock_class *)0},
1251 (char const *)0, 0, 0UL}},
1252 {(struct list_head *)0, (struct list_head *)0},
1253 {(struct lock_class_key *)0, {(struct lock_class *)0,
1254 (struct lock_class *)0},
1255 (char const *)0, 0, 0UL}},
1256 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1257 "led_3", 73UL, (u8 )32U},
1258 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1259 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1260 unsigned long * ,
1261 unsigned long * ))0,
1262 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1263 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1264 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1265 (char)0, (char)0,
1266 (char)0, (char)0,
1267 (char)0, (char)0,
1268 (char)0, (char)0,
1269 (char)0, (char)0,
1270 (char)0, (char)0,
1271 (char)0, (char)0},
1272 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1273 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1274 {(struct lock_class_key *)0,
1275 {(struct lock_class *)0,
1276 (struct lock_class *)0},
1277 (char const *)0, 0, 0UL}},
1278 {(struct list_head *)0, (struct list_head *)0},
1279 {(struct lock_class_key *)0, {(struct lock_class *)0,
1280 (struct lock_class *)0},
1281 (char const *)0, 0, 0UL}},
1282 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1283 "led_4", 73UL, (u8 )16U},
1284 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1285 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1286 unsigned long * ,
1287 unsigned long * ))0,
1288 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1289 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1290 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1291 (char)0, (char)0,
1292 (char)0, (char)0,
1293 (char)0, (char)0,
1294 (char)0, (char)0,
1295 (char)0, (char)0,
1296 (char)0, (char)0,
1297 (char)0, (char)0},
1298 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1299 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1300 {(struct lock_class_key *)0,
1301 {(struct lock_class *)0,
1302 (struct lock_class *)0},
1303 (char const *)0, 0, 0UL}},
1304 {(struct list_head *)0, (struct list_head *)0},
1305 {(struct lock_class_key *)0, {(struct lock_class *)0,
1306 (struct lock_class *)0},
1307 (char const *)0, 0, 0UL}},
1308 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1309 "led_5", 73UL, (u8 )8U},
1310 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1311 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1312 unsigned long * ,
1313 unsigned long * ))0,
1314 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1315 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1316 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1317 (char)0, (char)0,
1318 (char)0, (char)0,
1319 (char)0, (char)0,
1320 (char)0, (char)0,
1321 (char)0, (char)0,
1322 (char)0, (char)0,
1323 (char)0, (char)0},
1324 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1325 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1326 {(struct lock_class_key *)0,
1327 {(struct lock_class *)0,
1328 (struct lock_class *)0},
1329 (char const *)0, 0, 0UL}},
1330 {(struct list_head *)0, (struct list_head *)0},
1331 {(struct lock_class_key *)0, {(struct lock_class *)0,
1332 (struct lock_class *)0},
1333 (char const *)0, 0, 0UL}},
1334 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1335 "led_6", 73UL, (u8 )4U},
1336 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev * , enum led_brightness ))0,
1337 (enum led_brightness (*)(struct led_classdev * ))0, (int (*)(struct led_classdev * ,
1338 unsigned long * ,
1339 unsigned long * ))0,
1340 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1341 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1342 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1343 (char)0, (char)0,
1344 (char)0, (char)0,
1345 (char)0, (char)0,
1346 (char)0, (char)0,
1347 (char)0, (char)0,
1348 (char)0, (char)0,
1349 (char)0, (char)0},
1350 {(struct lock_class_key *)0, {(struct lock_class *)0, (struct lock_class *)0},
1351 (char const *)0, 0, 0UL}}, 0, {0L, {{{0U}}, 0U, 0U, (void *)0,
1352 {(struct lock_class_key *)0,
1353 {(struct lock_class *)0,
1354 (struct lock_class *)0},
1355 (char const *)0, 0, 0UL}},
1356 {(struct list_head *)0, (struct list_head *)0},
1357 {(struct lock_class_key *)0, {(struct lock_class *)0,
1358 (struct lock_class *)0},
1359 (char const *)0, 0, 0UL}},
1360 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1361 "led_7", 73UL, (u8 )2U}};
1362#line 99 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1363static spinlock_t value_lock = {{{{{0U}}, 3735899821U, 4294967295U, (void *)0xffffffffffffffffUL, {(struct lock_class_key *)0,
1364 {(struct lock_class *)0,
1365 (struct lock_class *)0},
1366 "value_lock",
1367 0, 0UL}}}};
1368#line 105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1369static u8 leds_back ;
1370#line 106 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1371static u8 leds_front ;
1372#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1373static void ot200_led_brightness_set(struct led_classdev *led_cdev , enum led_brightness value )
1374{ struct ot200_led *led ;
1375 struct led_classdev const *__mptr ;
1376 u8 *val ;
1377 unsigned long flags ;
1378 unsigned long __cil_tmp7 ;
1379 unsigned long __cil_tmp8 ;
1380 unsigned long __cil_tmp9 ;
1381 unsigned long __cil_tmp10 ;
1382 unsigned long __cil_tmp11 ;
1383 unsigned long __cil_tmp12 ;
1384 unsigned int __cil_tmp13 ;
1385 unsigned long __cil_tmp14 ;
1386 unsigned long __cil_tmp15 ;
1387 u8 __cil_tmp16 ;
1388 signed char __cil_tmp17 ;
1389 int __cil_tmp18 ;
1390 int __cil_tmp19 ;
1391 u8 __cil_tmp20 ;
1392 signed char __cil_tmp21 ;
1393 int __cil_tmp22 ;
1394 int __cil_tmp23 ;
1395 unsigned long __cil_tmp24 ;
1396 unsigned long __cil_tmp25 ;
1397 u8 __cil_tmp26 ;
1398 int __cil_tmp27 ;
1399 u8 __cil_tmp28 ;
1400 int __cil_tmp29 ;
1401 int __cil_tmp30 ;
1402 u8 __cil_tmp31 ;
1403 int __cil_tmp32 ;
1404 unsigned char __cil_tmp33 ;
1405 unsigned long __cil_tmp34 ;
1406 unsigned long __cil_tmp35 ;
1407 unsigned long __cil_tmp36 ;
1408 int __cil_tmp37 ;
1409
1410 {
1411 {
1412#line 111
1413 __mptr = (struct led_classdev const *)led_cdev;
1414#line 111
1415 led = (struct ot200_led *)__mptr;
1416#line 115
1417 ldv_spin_lock();
1418 }
1419 {
1420#line 117
1421 __cil_tmp7 = (unsigned long )led;
1422#line 117
1423 __cil_tmp8 = __cil_tmp7 + 416;
1424#line 117
1425 __cil_tmp9 = *((unsigned long *)__cil_tmp8);
1426#line 117
1427 if (__cil_tmp9 == 73UL) {
1428#line 118
1429 val = & leds_front;
1430 } else {
1431 {
1432#line 119
1433 __cil_tmp10 = (unsigned long )led;
1434#line 119
1435 __cil_tmp11 = __cil_tmp10 + 416;
1436#line 119
1437 __cil_tmp12 = *((unsigned long *)__cil_tmp11);
1438#line 119
1439 if (__cil_tmp12 == 90UL) {
1440#line 120
1441 val = & leds_back;
1442 } else {
1443#line 122
1444 __asm__ volatile ("1:\tud2\n.pushsection __bug_table,\"a\"\n2:\t.long 1b - 2b, %c0 - 2b\n\t.word %c1, 0\n\t.org 2b+%c2\n.popsection": : "i" ((char *)"/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"),
1445 "i" (122), "i" (12UL));
1446 ldv_15421: ;
1447#line 122
1448 goto ldv_15421;
1449 }
1450 }
1451 }
1452 }
1453 {
1454#line 124
1455 __cil_tmp13 = (unsigned int )value;
1456#line 124
1457 if (__cil_tmp13 == 0U) {
1458#line 125
1459 __cil_tmp14 = (unsigned long )led;
1460#line 125
1461 __cil_tmp15 = __cil_tmp14 + 424;
1462#line 125
1463 __cil_tmp16 = *((u8 *)__cil_tmp15);
1464#line 125
1465 __cil_tmp17 = (signed char )__cil_tmp16;
1466#line 125
1467 __cil_tmp18 = (int )__cil_tmp17;
1468#line 125
1469 __cil_tmp19 = ~ __cil_tmp18;
1470#line 125
1471 __cil_tmp20 = *val;
1472#line 125
1473 __cil_tmp21 = (signed char )__cil_tmp20;
1474#line 125
1475 __cil_tmp22 = (int )__cil_tmp21;
1476#line 125
1477 __cil_tmp23 = __cil_tmp22 & __cil_tmp19;
1478#line 125
1479 *val = (u8 )__cil_tmp23;
1480 } else {
1481#line 127
1482 __cil_tmp24 = (unsigned long )led;
1483#line 127
1484 __cil_tmp25 = __cil_tmp24 + 424;
1485#line 127
1486 __cil_tmp26 = *((u8 *)__cil_tmp25);
1487#line 127
1488 __cil_tmp27 = (int )__cil_tmp26;
1489#line 127
1490 __cil_tmp28 = *val;
1491#line 127
1492 __cil_tmp29 = (int )__cil_tmp28;
1493#line 127
1494 __cil_tmp30 = __cil_tmp29 | __cil_tmp27;
1495#line 127
1496 *val = (u8 )__cil_tmp30;
1497 }
1498 }
1499 {
1500#line 129
1501 __cil_tmp31 = *val;
1502#line 129
1503 __cil_tmp32 = (int )__cil_tmp31;
1504#line 129
1505 __cil_tmp33 = (unsigned char )__cil_tmp32;
1506#line 129
1507 __cil_tmp34 = (unsigned long )led;
1508#line 129
1509 __cil_tmp35 = __cil_tmp34 + 416;
1510#line 129
1511 __cil_tmp36 = *((unsigned long *)__cil_tmp35);
1512#line 129
1513 __cil_tmp37 = (int )__cil_tmp36;
1514#line 129
1515 outb(__cil_tmp33, __cil_tmp37);
1516#line 130
1517 spin_unlock_irqrestore(& value_lock, flags);
1518 }
1519#line 131
1520 return;
1521}
1522}
1523#line 133 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1524static int ot200_led_probe(struct platform_device *pdev )
1525{ int i ;
1526 int ret ;
1527 unsigned long __cil_tmp4 ;
1528 unsigned long __cil_tmp5 ;
1529 unsigned long __cil_tmp6 ;
1530 unsigned long __cil_tmp7 ;
1531 unsigned long __cil_tmp8 ;
1532 unsigned long __cil_tmp9 ;
1533 unsigned long __cil_tmp10 ;
1534 unsigned long __cil_tmp11 ;
1535 unsigned long __cil_tmp12 ;
1536 unsigned long __cil_tmp13 ;
1537 unsigned long __cil_tmp14 ;
1538 struct device *__cil_tmp15 ;
1539 unsigned long __cil_tmp16 ;
1540 unsigned long __cil_tmp17 ;
1541 struct led_classdev *__cil_tmp18 ;
1542 unsigned int __cil_tmp19 ;
1543 u8 *__cil_tmp20 ;
1544 u8 *__cil_tmp21 ;
1545 u8 *__cil_tmp22 ;
1546 u8 __cil_tmp23 ;
1547 int __cil_tmp24 ;
1548 unsigned char __cil_tmp25 ;
1549 u8 *__cil_tmp26 ;
1550 u8 __cil_tmp27 ;
1551 int __cil_tmp28 ;
1552 unsigned char __cil_tmp29 ;
1553 unsigned long __cil_tmp30 ;
1554 unsigned long __cil_tmp31 ;
1555 struct led_classdev *__cil_tmp32 ;
1556
1557 {
1558#line 138
1559 i = 0;
1560#line 138
1561 goto ldv_15431;
1562 ldv_15430:
1563 {
1564#line 140
1565 __cil_tmp4 = i * 432UL;
1566#line 140
1567 __cil_tmp5 = (unsigned long )(leds) + __cil_tmp4;
1568#line 140
1569 __cil_tmp6 = i * 432UL;
1570#line 140
1571 __cil_tmp7 = __cil_tmp6 + 408;
1572#line 140
1573 __cil_tmp8 = (unsigned long )(leds) + __cil_tmp7;
1574#line 140
1575 *((char const **)__cil_tmp5) = *((char const **)__cil_tmp8);
1576#line 141
1577 __cil_tmp9 = 0 + 24;
1578#line 141
1579 __cil_tmp10 = i * 432UL;
1580#line 141
1581 __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
1582#line 141
1583 __cil_tmp12 = (unsigned long )(leds) + __cil_tmp11;
1584#line 141
1585 *((void (**)(struct led_classdev * , enum led_brightness ))__cil_tmp12) = & ot200_led_brightness_set;
1586#line 143
1587 __cil_tmp13 = (unsigned long )pdev;
1588#line 143
1589 __cil_tmp14 = __cil_tmp13 + 16;
1590#line 143
1591 __cil_tmp15 = (struct device *)__cil_tmp14;
1592#line 143
1593 __cil_tmp16 = i * 432UL;
1594#line 143
1595 __cil_tmp17 = (unsigned long )(leds) + __cil_tmp16;
1596#line 143
1597 __cil_tmp18 = (struct led_classdev *)__cil_tmp17;
1598#line 143
1599 ret = led_classdev_register(__cil_tmp15, __cil_tmp18);
1600 }
1601#line 144
1602 if (ret < 0) {
1603#line 145
1604 goto err;
1605 } else {
1606
1607 }
1608#line 138
1609 i = i + 1;
1610 ldv_15431: ;
1611 {
1612#line 138
1613 __cil_tmp19 = (unsigned int )i;
1614#line 138
1615 if (__cil_tmp19 <= 9U) {
1616#line 139
1617 goto ldv_15430;
1618 } else {
1619#line 141
1620 goto ldv_15432;
1621 }
1622 }
1623 ldv_15432:
1624 {
1625#line 148
1626 __cil_tmp20 = & leds_front;
1627#line 148
1628 *__cil_tmp20 = (u8 )0U;
1629#line 149
1630 __cil_tmp21 = & leds_back;
1631#line 149
1632 *__cil_tmp21 = (u8 )2U;
1633#line 150
1634 __cil_tmp22 = & leds_front;
1635#line 150
1636 __cil_tmp23 = *__cil_tmp22;
1637#line 150
1638 __cil_tmp24 = (int )__cil_tmp23;
1639#line 150
1640 __cil_tmp25 = (unsigned char )__cil_tmp24;
1641#line 150
1642 outb(__cil_tmp25, 73);
1643#line 151
1644 __cil_tmp26 = & leds_back;
1645#line 151
1646 __cil_tmp27 = *__cil_tmp26;
1647#line 151
1648 __cil_tmp28 = (int )__cil_tmp27;
1649#line 151
1650 __cil_tmp29 = (unsigned char )__cil_tmp28;
1651#line 151
1652 outb(__cil_tmp29, 90);
1653 }
1654#line 153
1655 return (0);
1656 err:
1657#line 156
1658 i = i + -1;
1659#line 156
1660 goto ldv_15434;
1661 ldv_15433:
1662 {
1663#line 157
1664 __cil_tmp30 = i * 432UL;
1665#line 157
1666 __cil_tmp31 = (unsigned long )(leds) + __cil_tmp30;
1667#line 157
1668 __cil_tmp32 = (struct led_classdev *)__cil_tmp31;
1669#line 157
1670 led_classdev_unregister(__cil_tmp32);
1671#line 156
1672 i = i - 1;
1673 }
1674 ldv_15434: ;
1675#line 156
1676 if (i >= 0) {
1677#line 157
1678 goto ldv_15433;
1679 } else {
1680#line 159
1681 goto ldv_15435;
1682 }
1683 ldv_15435: ;
1684#line 159
1685 return (ret);
1686}
1687}
1688#line 204
1689extern void ldv_check_final_state(void) ;
1690#line 207
1691extern void ldv_check_return_value(int ) ;
1692#line 210
1693extern void ldv_initialize(void) ;
1694#line 213
1695extern int __VERIFIER_nondet_int(void) ;
1696#line 216 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1697int LDV_IN_INTERRUPT ;
1698#line 219 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1699void main(void)
1700{ struct platform_device *var_group1 ;
1701 int res_ot200_led_probe_1 ;
1702 int ldv_s_ot200_led_driver_platform_driver ;
1703 int tmp ;
1704 int tmp___0 ;
1705
1706 {
1707 {
1708#line 249
1709 ldv_s_ot200_led_driver_platform_driver = 0;
1710#line 239
1711 LDV_IN_INTERRUPT = 1;
1712#line 248
1713 ldv_initialize();
1714 }
1715#line 252
1716 goto ldv_15486;
1717 ldv_15485:
1718 {
1719#line 256
1720 tmp = __VERIFIER_nondet_int();
1721 }
1722#line 258
1723 if (tmp == 0) {
1724#line 258
1725 goto case_0;
1726 } else {
1727 {
1728#line 277
1729 goto switch_default;
1730#line 256
1731 if (0) {
1732 case_0: ;
1733#line 261
1734 if (ldv_s_ot200_led_driver_platform_driver == 0) {
1735 {
1736#line 266
1737 res_ot200_led_probe_1 = ot200_led_probe(var_group1);
1738#line 267
1739 ldv_check_return_value(res_ot200_led_probe_1);
1740 }
1741#line 268
1742 if (res_ot200_led_probe_1 != 0) {
1743#line 269
1744 goto ldv_module_exit;
1745 } else {
1746
1747 }
1748#line 270
1749 ldv_s_ot200_led_driver_platform_driver = 0;
1750 } else {
1751
1752 }
1753#line 276
1754 goto ldv_15483;
1755 switch_default: ;
1756#line 277
1757 goto ldv_15483;
1758 } else {
1759 switch_break: ;
1760 }
1761 }
1762 }
1763 ldv_15483: ;
1764 ldv_15486:
1765 {
1766#line 252
1767 tmp___0 = __VERIFIER_nondet_int();
1768 }
1769#line 252
1770 if (tmp___0 != 0) {
1771#line 254
1772 goto ldv_15485;
1773 } else
1774#line 252
1775 if (ldv_s_ot200_led_driver_platform_driver != 0) {
1776#line 254
1777 goto ldv_15485;
1778 } else {
1779#line 256
1780 goto ldv_15487;
1781 }
1782 ldv_15487: ;
1783 ldv_module_exit: ;
1784 {
1785#line 286
1786 ldv_check_final_state();
1787 }
1788#line 289
1789 return;
1790}
1791}
1792#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1793void ldv_blast_assert(void)
1794{
1795
1796 {
1797 ERROR: ;
1798#line 6
1799 goto ERROR;
1800}
1801}
1802#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1803extern int __VERIFIER_nondet_int(void) ;
1804#line 310 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1805int ldv_spin = 0;
1806#line 314 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1807void ldv_check_alloc_flags(gfp_t flags )
1808{
1809
1810 {
1811#line 317
1812 if (ldv_spin != 0) {
1813#line 317
1814 if (flags != 32U) {
1815 {
1816#line 317
1817 ldv_blast_assert();
1818 }
1819 } else {
1820
1821 }
1822 } else {
1823
1824 }
1825#line 320
1826 return;
1827}
1828}
1829#line 320
1830extern struct page *ldv_some_page(void) ;
1831#line 323 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1832struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1833{ struct page *tmp ;
1834
1835 {
1836#line 326
1837 if (ldv_spin != 0) {
1838#line 326
1839 if (flags != 32U) {
1840 {
1841#line 326
1842 ldv_blast_assert();
1843 }
1844 } else {
1845
1846 }
1847 } else {
1848
1849 }
1850 {
1851#line 328
1852 tmp = ldv_some_page();
1853 }
1854#line 328
1855 return (tmp);
1856}
1857}
1858#line 332 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1859void ldv_check_alloc_nonatomic(void)
1860{
1861
1862 {
1863#line 335
1864 if (ldv_spin != 0) {
1865 {
1866#line 335
1867 ldv_blast_assert();
1868 }
1869 } else {
1870
1871 }
1872#line 338
1873 return;
1874}
1875}
1876#line 339 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1877void ldv_spin_lock(void)
1878{
1879
1880 {
1881#line 342
1882 ldv_spin = 1;
1883#line 343
1884 return;
1885}
1886}
1887#line 346 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1888void ldv_spin_unlock(void)
1889{
1890
1891 {
1892#line 349
1893 ldv_spin = 0;
1894#line 350
1895 return;
1896}
1897}
1898#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1899int ldv_spin_trylock(void)
1900{ int is_lock ;
1901
1902 {
1903 {
1904#line 358
1905 is_lock = __VERIFIER_nondet_int();
1906 }
1907#line 360
1908 if (is_lock != 0) {
1909#line 363
1910 return (0);
1911 } else {
1912#line 368
1913 ldv_spin = 1;
1914#line 370
1915 return (1);
1916 }
1917}
1918}
1919#line 446 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1920__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags )
1921{
1922
1923 {
1924 {
1925#line 452
1926 ldv_spin_unlock();
1927#line 454
1928 ldv_spin_unlock_irqrestore_8(lock, flags);
1929 }
1930#line 455
1931 return;
1932}
1933}
1934#line 537 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/12450/dscv_tempdir/dscv/ri/43_1a/drivers/leds/leds-ot200.c.p"
1935void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1936{
1937
1938 {
1939 {
1940#line 543
1941 ldv_check_alloc_flags(ldv_func_arg2);
1942#line 545
1943 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1944 }
1945#line 546
1946 return ((void *)0);
1947}
1948}