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