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 219 "include/linux/types.h"
53struct __anonstruct_atomic_t_7 {
54 int counter ;
55};
56#line 219 "include/linux/types.h"
57typedef struct __anonstruct_atomic_t_7 atomic_t;
58#line 224 "include/linux/types.h"
59struct __anonstruct_atomic64_t_8 {
60 long counter ;
61};
62#line 224 "include/linux/types.h"
63typedef struct __anonstruct_atomic64_t_8 atomic64_t;
64#line 229 "include/linux/types.h"
65struct list_head {
66 struct list_head *next ;
67 struct list_head *prev ;
68};
69#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
70struct module;
71#line 56
72struct module;
73#line 146 "include/linux/init.h"
74typedef void (*ctor_fn_t)(void);
75#line 47 "include/linux/dynamic_debug.h"
76struct device;
77#line 47
78struct device;
79#line 135 "include/linux/kernel.h"
80struct completion;
81#line 135
82struct completion;
83#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
84struct page;
85#line 18
86struct page;
87#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
88struct task_struct;
89#line 20
90struct task_struct;
91#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
92struct task_struct;
93#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
94struct file;
95#line 295
96struct file;
97#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
98struct page;
99#line 52
100struct task_struct;
101#line 329
102struct arch_spinlock;
103#line 329
104struct arch_spinlock;
105#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
106struct task_struct;
107#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
108struct task_struct;
109#line 10 "include/asm-generic/bug.h"
110struct bug_entry {
111 int bug_addr_disp ;
112 int file_disp ;
113 unsigned short line ;
114 unsigned short flags ;
115};
116#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
117struct static_key;
118#line 234
119struct static_key;
120#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
121struct kmem_cache;
122#line 23 "include/asm-generic/atomic-long.h"
123typedef atomic64_t atomic_long_t;
124#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
125typedef u16 __ticket_t;
126#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
127typedef u32 __ticketpair_t;
128#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
129struct __raw_tickets {
130 __ticket_t head ;
131 __ticket_t tail ;
132};
133#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
134union __anonunion____missing_field_name_36 {
135 __ticketpair_t head_tail ;
136 struct __raw_tickets tickets ;
137};
138#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
139struct arch_spinlock {
140 union __anonunion____missing_field_name_36 __annonCompField17 ;
141};
142#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
143typedef struct arch_spinlock arch_spinlock_t;
144#line 12 "include/linux/lockdep.h"
145struct task_struct;
146#line 391 "include/linux/lockdep.h"
147struct lock_class_key {
148
149};
150#line 20 "include/linux/spinlock_types.h"
151struct raw_spinlock {
152 arch_spinlock_t raw_lock ;
153 unsigned int magic ;
154 unsigned int owner_cpu ;
155 void *owner ;
156};
157#line 64 "include/linux/spinlock_types.h"
158union __anonunion____missing_field_name_39 {
159 struct raw_spinlock rlock ;
160};
161#line 64 "include/linux/spinlock_types.h"
162struct spinlock {
163 union __anonunion____missing_field_name_39 __annonCompField19 ;
164};
165#line 64 "include/linux/spinlock_types.h"
166typedef struct spinlock spinlock_t;
167#line 49 "include/linux/wait.h"
168struct __wait_queue_head {
169 spinlock_t lock ;
170 struct list_head task_list ;
171};
172#line 53 "include/linux/wait.h"
173typedef struct __wait_queue_head wait_queue_head_t;
174#line 55
175struct task_struct;
176#line 60 "include/linux/pageblock-flags.h"
177struct page;
178#line 48 "include/linux/mutex.h"
179struct mutex {
180 atomic_t count ;
181 spinlock_t wait_lock ;
182 struct list_head wait_list ;
183 struct task_struct *owner ;
184 char const *name ;
185 void *magic ;
186};
187#line 25 "include/linux/completion.h"
188struct completion {
189 unsigned int done ;
190 wait_queue_head_t wait ;
191};
192#line 9 "include/linux/memory_hotplug.h"
193struct page;
194#line 18 "include/linux/ioport.h"
195struct resource {
196 resource_size_t start ;
197 resource_size_t end ;
198 char const *name ;
199 unsigned long flags ;
200 struct resource *parent ;
201 struct resource *sibling ;
202 struct resource *child ;
203};
204#line 202
205struct device;
206#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
207struct device;
208#line 46 "include/linux/ktime.h"
209union ktime {
210 s64 tv64 ;
211};
212#line 59 "include/linux/ktime.h"
213typedef union ktime ktime_t;
214#line 10 "include/linux/timer.h"
215struct tvec_base;
216#line 10
217struct tvec_base;
218#line 12 "include/linux/timer.h"
219struct timer_list {
220 struct list_head entry ;
221 unsigned long expires ;
222 struct tvec_base *base ;
223 void (*function)(unsigned long ) ;
224 unsigned long data ;
225 int slack ;
226 int start_pid ;
227 void *start_site ;
228 char start_comm[16] ;
229};
230#line 17 "include/linux/workqueue.h"
231struct work_struct;
232#line 17
233struct work_struct;
234#line 79 "include/linux/workqueue.h"
235struct work_struct {
236 atomic_long_t data ;
237 struct list_head entry ;
238 void (*func)(struct work_struct *work ) ;
239};
240#line 42 "include/linux/pm.h"
241struct device;
242#line 50 "include/linux/pm.h"
243struct pm_message {
244 int event ;
245};
246#line 50 "include/linux/pm.h"
247typedef struct pm_message pm_message_t;
248#line 264 "include/linux/pm.h"
249struct dev_pm_ops {
250 int (*prepare)(struct device *dev ) ;
251 void (*complete)(struct device *dev ) ;
252 int (*suspend)(struct device *dev ) ;
253 int (*resume)(struct device *dev ) ;
254 int (*freeze)(struct device *dev ) ;
255 int (*thaw)(struct device *dev ) ;
256 int (*poweroff)(struct device *dev ) ;
257 int (*restore)(struct device *dev ) ;
258 int (*suspend_late)(struct device *dev ) ;
259 int (*resume_early)(struct device *dev ) ;
260 int (*freeze_late)(struct device *dev ) ;
261 int (*thaw_early)(struct device *dev ) ;
262 int (*poweroff_late)(struct device *dev ) ;
263 int (*restore_early)(struct device *dev ) ;
264 int (*suspend_noirq)(struct device *dev ) ;
265 int (*resume_noirq)(struct device *dev ) ;
266 int (*freeze_noirq)(struct device *dev ) ;
267 int (*thaw_noirq)(struct device *dev ) ;
268 int (*poweroff_noirq)(struct device *dev ) ;
269 int (*restore_noirq)(struct device *dev ) ;
270 int (*runtime_suspend)(struct device *dev ) ;
271 int (*runtime_resume)(struct device *dev ) ;
272 int (*runtime_idle)(struct device *dev ) ;
273};
274#line 458
275enum rpm_status {
276 RPM_ACTIVE = 0,
277 RPM_RESUMING = 1,
278 RPM_SUSPENDED = 2,
279 RPM_SUSPENDING = 3
280} ;
281#line 480
282enum rpm_request {
283 RPM_REQ_NONE = 0,
284 RPM_REQ_IDLE = 1,
285 RPM_REQ_SUSPEND = 2,
286 RPM_REQ_AUTOSUSPEND = 3,
287 RPM_REQ_RESUME = 4
288} ;
289#line 488
290struct wakeup_source;
291#line 488
292struct wakeup_source;
293#line 495 "include/linux/pm.h"
294struct pm_subsys_data {
295 spinlock_t lock ;
296 unsigned int refcount ;
297};
298#line 506
299struct dev_pm_qos_request;
300#line 506
301struct pm_qos_constraints;
302#line 506 "include/linux/pm.h"
303struct dev_pm_info {
304 pm_message_t power_state ;
305 unsigned int can_wakeup : 1 ;
306 unsigned int async_suspend : 1 ;
307 bool is_prepared : 1 ;
308 bool is_suspended : 1 ;
309 bool ignore_children : 1 ;
310 spinlock_t lock ;
311 struct list_head entry ;
312 struct completion completion ;
313 struct wakeup_source *wakeup ;
314 bool wakeup_path : 1 ;
315 struct timer_list suspend_timer ;
316 unsigned long timer_expires ;
317 struct work_struct work ;
318 wait_queue_head_t wait_queue ;
319 atomic_t usage_count ;
320 atomic_t child_count ;
321 unsigned int disable_depth : 3 ;
322 unsigned int idle_notification : 1 ;
323 unsigned int request_pending : 1 ;
324 unsigned int deferred_resume : 1 ;
325 unsigned int run_wake : 1 ;
326 unsigned int runtime_auto : 1 ;
327 unsigned int no_callbacks : 1 ;
328 unsigned int irq_safe : 1 ;
329 unsigned int use_autosuspend : 1 ;
330 unsigned int timer_autosuspends : 1 ;
331 enum rpm_request request ;
332 enum rpm_status runtime_status ;
333 int runtime_error ;
334 int autosuspend_delay ;
335 unsigned long last_busy ;
336 unsigned long active_jiffies ;
337 unsigned long suspended_jiffies ;
338 unsigned long accounting_timestamp ;
339 ktime_t suspend_time ;
340 s64 max_time_suspended_ns ;
341 struct dev_pm_qos_request *pq_req ;
342 struct pm_subsys_data *subsys_data ;
343 struct pm_qos_constraints *constraints ;
344};
345#line 564 "include/linux/pm.h"
346struct dev_pm_domain {
347 struct dev_pm_ops ops ;
348};
349#line 8 "include/linux/vmalloc.h"
350struct vm_area_struct;
351#line 8
352struct vm_area_struct;
353#line 994 "include/linux/mmzone.h"
354struct page;
355#line 10 "include/linux/gfp.h"
356struct vm_area_struct;
357#line 29 "include/linux/sysctl.h"
358struct completion;
359#line 49 "include/linux/kmod.h"
360struct file;
361#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
362struct task_struct;
363#line 18 "include/linux/elf.h"
364typedef __u64 Elf64_Addr;
365#line 19 "include/linux/elf.h"
366typedef __u16 Elf64_Half;
367#line 23 "include/linux/elf.h"
368typedef __u32 Elf64_Word;
369#line 24 "include/linux/elf.h"
370typedef __u64 Elf64_Xword;
371#line 194 "include/linux/elf.h"
372struct elf64_sym {
373 Elf64_Word st_name ;
374 unsigned char st_info ;
375 unsigned char st_other ;
376 Elf64_Half st_shndx ;
377 Elf64_Addr st_value ;
378 Elf64_Xword st_size ;
379};
380#line 194 "include/linux/elf.h"
381typedef struct elf64_sym Elf64_Sym;
382#line 438
383struct file;
384#line 20 "include/linux/kobject_ns.h"
385struct sock;
386#line 20
387struct sock;
388#line 21
389struct kobject;
390#line 21
391struct kobject;
392#line 27
393enum kobj_ns_type {
394 KOBJ_NS_TYPE_NONE = 0,
395 KOBJ_NS_TYPE_NET = 1,
396 KOBJ_NS_TYPES = 2
397} ;
398#line 40 "include/linux/kobject_ns.h"
399struct kobj_ns_type_operations {
400 enum kobj_ns_type type ;
401 void *(*grab_current_ns)(void) ;
402 void const *(*netlink_ns)(struct sock *sk ) ;
403 void const *(*initial_ns)(void) ;
404 void (*drop_ns)(void * ) ;
405};
406#line 22 "include/linux/sysfs.h"
407struct kobject;
408#line 23
409struct module;
410#line 24
411enum kobj_ns_type;
412#line 26 "include/linux/sysfs.h"
413struct attribute {
414 char const *name ;
415 umode_t mode ;
416};
417#line 56 "include/linux/sysfs.h"
418struct attribute_group {
419 char const *name ;
420 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
421 struct attribute **attrs ;
422};
423#line 85
424struct file;
425#line 86
426struct vm_area_struct;
427#line 88 "include/linux/sysfs.h"
428struct bin_attribute {
429 struct attribute attr ;
430 size_t size ;
431 void *private ;
432 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
433 loff_t , size_t ) ;
434 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
435 loff_t , size_t ) ;
436 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
437};
438#line 112 "include/linux/sysfs.h"
439struct sysfs_ops {
440 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
441 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
442 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
443};
444#line 118
445struct sysfs_dirent;
446#line 118
447struct sysfs_dirent;
448#line 22 "include/linux/kref.h"
449struct kref {
450 atomic_t refcount ;
451};
452#line 50 "include/linux/kobject.h"
453enum kobject_action {
454 KOBJ_ADD = 0,
455 KOBJ_REMOVE = 1,
456 KOBJ_CHANGE = 2,
457 KOBJ_MOVE = 3,
458 KOBJ_ONLINE = 4,
459 KOBJ_OFFLINE = 5,
460 KOBJ_MAX = 6
461} ;
462#line 60
463struct kset;
464#line 60
465struct kobj_type;
466#line 60 "include/linux/kobject.h"
467struct kobject {
468 char const *name ;
469 struct list_head entry ;
470 struct kobject *parent ;
471 struct kset *kset ;
472 struct kobj_type *ktype ;
473 struct sysfs_dirent *sd ;
474 struct kref kref ;
475 unsigned int state_initialized : 1 ;
476 unsigned int state_in_sysfs : 1 ;
477 unsigned int state_add_uevent_sent : 1 ;
478 unsigned int state_remove_uevent_sent : 1 ;
479 unsigned int uevent_suppress : 1 ;
480};
481#line 108 "include/linux/kobject.h"
482struct kobj_type {
483 void (*release)(struct kobject *kobj ) ;
484 struct sysfs_ops const *sysfs_ops ;
485 struct attribute **default_attrs ;
486 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
487 void const *(*namespace)(struct kobject *kobj ) ;
488};
489#line 116 "include/linux/kobject.h"
490struct kobj_uevent_env {
491 char *envp[32] ;
492 int envp_idx ;
493 char buf[2048] ;
494 int buflen ;
495};
496#line 123 "include/linux/kobject.h"
497struct kset_uevent_ops {
498 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
499 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
500 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
501};
502#line 140
503struct sock;
504#line 159 "include/linux/kobject.h"
505struct kset {
506 struct list_head list ;
507 spinlock_t list_lock ;
508 struct kobject kobj ;
509 struct kset_uevent_ops const *uevent_ops ;
510};
511#line 39 "include/linux/moduleparam.h"
512struct kernel_param;
513#line 39
514struct kernel_param;
515#line 41 "include/linux/moduleparam.h"
516struct kernel_param_ops {
517 int (*set)(char const *val , struct kernel_param const *kp ) ;
518 int (*get)(char *buffer , struct kernel_param const *kp ) ;
519 void (*free)(void *arg ) ;
520};
521#line 50
522struct kparam_string;
523#line 50
524struct kparam_array;
525#line 50 "include/linux/moduleparam.h"
526union __anonunion____missing_field_name_199 {
527 void *arg ;
528 struct kparam_string const *str ;
529 struct kparam_array const *arr ;
530};
531#line 50 "include/linux/moduleparam.h"
532struct kernel_param {
533 char const *name ;
534 struct kernel_param_ops const *ops ;
535 u16 perm ;
536 s16 level ;
537 union __anonunion____missing_field_name_199 __annonCompField32 ;
538};
539#line 63 "include/linux/moduleparam.h"
540struct kparam_string {
541 unsigned int maxlen ;
542 char *string ;
543};
544#line 69 "include/linux/moduleparam.h"
545struct kparam_array {
546 unsigned int max ;
547 unsigned int elemsize ;
548 unsigned int *num ;
549 struct kernel_param_ops const *ops ;
550 void *elem ;
551};
552#line 445
553struct module;
554#line 80 "include/linux/jump_label.h"
555struct module;
556#line 143 "include/linux/jump_label.h"
557struct static_key {
558 atomic_t enabled ;
559};
560#line 22 "include/linux/tracepoint.h"
561struct module;
562#line 23
563struct tracepoint;
564#line 23
565struct tracepoint;
566#line 25 "include/linux/tracepoint.h"
567struct tracepoint_func {
568 void *func ;
569 void *data ;
570};
571#line 30 "include/linux/tracepoint.h"
572struct tracepoint {
573 char const *name ;
574 struct static_key key ;
575 void (*regfunc)(void) ;
576 void (*unregfunc)(void) ;
577 struct tracepoint_func *funcs ;
578};
579#line 19 "include/linux/export.h"
580struct kernel_symbol {
581 unsigned long value ;
582 char const *name ;
583};
584#line 8 "include/asm-generic/module.h"
585struct mod_arch_specific {
586
587};
588#line 35 "include/linux/module.h"
589struct module;
590#line 37
591struct module_param_attrs;
592#line 37 "include/linux/module.h"
593struct module_kobject {
594 struct kobject kobj ;
595 struct module *mod ;
596 struct kobject *drivers_dir ;
597 struct module_param_attrs *mp ;
598};
599#line 44 "include/linux/module.h"
600struct module_attribute {
601 struct attribute attr ;
602 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
603 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
604 size_t count ) ;
605 void (*setup)(struct module * , char const * ) ;
606 int (*test)(struct module * ) ;
607 void (*free)(struct module * ) ;
608};
609#line 71
610struct exception_table_entry;
611#line 71
612struct exception_table_entry;
613#line 199
614enum module_state {
615 MODULE_STATE_LIVE = 0,
616 MODULE_STATE_COMING = 1,
617 MODULE_STATE_GOING = 2
618} ;
619#line 215 "include/linux/module.h"
620struct module_ref {
621 unsigned long incs ;
622 unsigned long decs ;
623} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
624#line 220
625struct module_sect_attrs;
626#line 220
627struct module_notes_attrs;
628#line 220
629struct ftrace_event_call;
630#line 220 "include/linux/module.h"
631struct module {
632 enum module_state state ;
633 struct list_head list ;
634 char name[64UL - sizeof(unsigned long )] ;
635 struct module_kobject mkobj ;
636 struct module_attribute *modinfo_attrs ;
637 char const *version ;
638 char const *srcversion ;
639 struct kobject *holders_dir ;
640 struct kernel_symbol const *syms ;
641 unsigned long const *crcs ;
642 unsigned int num_syms ;
643 struct kernel_param *kp ;
644 unsigned int num_kp ;
645 unsigned int num_gpl_syms ;
646 struct kernel_symbol const *gpl_syms ;
647 unsigned long const *gpl_crcs ;
648 struct kernel_symbol const *unused_syms ;
649 unsigned long const *unused_crcs ;
650 unsigned int num_unused_syms ;
651 unsigned int num_unused_gpl_syms ;
652 struct kernel_symbol const *unused_gpl_syms ;
653 unsigned long const *unused_gpl_crcs ;
654 struct kernel_symbol const *gpl_future_syms ;
655 unsigned long const *gpl_future_crcs ;
656 unsigned int num_gpl_future_syms ;
657 unsigned int num_exentries ;
658 struct exception_table_entry *extable ;
659 int (*init)(void) ;
660 void *module_init ;
661 void *module_core ;
662 unsigned int init_size ;
663 unsigned int core_size ;
664 unsigned int init_text_size ;
665 unsigned int core_text_size ;
666 unsigned int init_ro_size ;
667 unsigned int core_ro_size ;
668 struct mod_arch_specific arch ;
669 unsigned int taints ;
670 unsigned int num_bugs ;
671 struct list_head bug_list ;
672 struct bug_entry *bug_table ;
673 Elf64_Sym *symtab ;
674 Elf64_Sym *core_symtab ;
675 unsigned int num_symtab ;
676 unsigned int core_num_syms ;
677 char *strtab ;
678 char *core_strtab ;
679 struct module_sect_attrs *sect_attrs ;
680 struct module_notes_attrs *notes_attrs ;
681 char *args ;
682 void *percpu ;
683 unsigned int percpu_size ;
684 unsigned int num_tracepoints ;
685 struct tracepoint * const *tracepoints_ptrs ;
686 unsigned int num_trace_bprintk_fmt ;
687 char const **trace_bprintk_fmt_start ;
688 struct ftrace_event_call **trace_events ;
689 unsigned int num_trace_events ;
690 struct list_head source_list ;
691 struct list_head target_list ;
692 struct task_struct *waiter ;
693 void (*exit)(void) ;
694 struct module_ref *refptr ;
695 ctor_fn_t *ctors ;
696 unsigned int num_ctors ;
697};
698#line 46 "include/linux/slub_def.h"
699struct kmem_cache_cpu {
700 void **freelist ;
701 unsigned long tid ;
702 struct page *page ;
703 struct page *partial ;
704 int node ;
705 unsigned int stat[26] ;
706};
707#line 57 "include/linux/slub_def.h"
708struct kmem_cache_node {
709 spinlock_t list_lock ;
710 unsigned long nr_partial ;
711 struct list_head partial ;
712 atomic_long_t nr_slabs ;
713 atomic_long_t total_objects ;
714 struct list_head full ;
715};
716#line 73 "include/linux/slub_def.h"
717struct kmem_cache_order_objects {
718 unsigned long x ;
719};
720#line 80 "include/linux/slub_def.h"
721struct kmem_cache {
722 struct kmem_cache_cpu *cpu_slab ;
723 unsigned long flags ;
724 unsigned long min_partial ;
725 int size ;
726 int objsize ;
727 int offset ;
728 int cpu_partial ;
729 struct kmem_cache_order_objects oo ;
730 struct kmem_cache_order_objects max ;
731 struct kmem_cache_order_objects min ;
732 gfp_t allocflags ;
733 int refcount ;
734 void (*ctor)(void * ) ;
735 int inuse ;
736 int align ;
737 int reserved ;
738 char const *name ;
739 struct list_head list ;
740 struct kobject kobj ;
741 int remote_node_defrag_ratio ;
742 struct kmem_cache_node *node[1 << 10] ;
743};
744#line 10 "include/linux/irqreturn.h"
745enum irqreturn {
746 IRQ_NONE = 0,
747 IRQ_HANDLED = 1,
748 IRQ_WAKE_THREAD = 2
749} ;
750#line 16 "include/linux/irqreturn.h"
751typedef enum irqreturn irqreturn_t;
752#line 32 "include/linux/irq.h"
753struct module;
754#line 12 "include/linux/irqdesc.h"
755struct proc_dir_entry;
756#line 12
757struct proc_dir_entry;
758#line 14
759struct module;
760#line 16 "include/linux/profile.h"
761struct proc_dir_entry;
762#line 65
763struct task_struct;
764#line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess.h"
765struct exception_table_entry {
766 unsigned long insn ;
767 unsigned long fixup ;
768};
769#line 132 "include/linux/hardirq.h"
770struct task_struct;
771#line 187 "include/linux/interrupt.h"
772struct device;
773#line 19 "include/linux/klist.h"
774struct klist_node;
775#line 19
776struct klist_node;
777#line 39 "include/linux/klist.h"
778struct klist_node {
779 void *n_klist ;
780 struct list_head n_node ;
781 struct kref n_ref ;
782};
783#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
784struct dma_map_ops;
785#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
786struct dev_archdata {
787 void *acpi_handle ;
788 struct dma_map_ops *dma_ops ;
789 void *iommu ;
790};
791#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
792struct pdev_archdata {
793
794};
795#line 28 "include/linux/device.h"
796struct device;
797#line 29
798struct device_private;
799#line 29
800struct device_private;
801#line 30
802struct device_driver;
803#line 30
804struct device_driver;
805#line 31
806struct driver_private;
807#line 31
808struct driver_private;
809#line 32
810struct module;
811#line 33
812struct class;
813#line 33
814struct class;
815#line 34
816struct subsys_private;
817#line 34
818struct subsys_private;
819#line 35
820struct bus_type;
821#line 35
822struct bus_type;
823#line 36
824struct device_node;
825#line 36
826struct device_node;
827#line 37
828struct iommu_ops;
829#line 37
830struct iommu_ops;
831#line 39 "include/linux/device.h"
832struct bus_attribute {
833 struct attribute attr ;
834 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
835 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
836};
837#line 89
838struct device_attribute;
839#line 89
840struct driver_attribute;
841#line 89 "include/linux/device.h"
842struct bus_type {
843 char const *name ;
844 char const *dev_name ;
845 struct device *dev_root ;
846 struct bus_attribute *bus_attrs ;
847 struct device_attribute *dev_attrs ;
848 struct driver_attribute *drv_attrs ;
849 int (*match)(struct device *dev , struct device_driver *drv ) ;
850 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
851 int (*probe)(struct device *dev ) ;
852 int (*remove)(struct device *dev ) ;
853 void (*shutdown)(struct device *dev ) ;
854 int (*suspend)(struct device *dev , pm_message_t state ) ;
855 int (*resume)(struct device *dev ) ;
856 struct dev_pm_ops const *pm ;
857 struct iommu_ops *iommu_ops ;
858 struct subsys_private *p ;
859};
860#line 127
861struct device_type;
862#line 214
863struct of_device_id;
864#line 214 "include/linux/device.h"
865struct device_driver {
866 char const *name ;
867 struct bus_type *bus ;
868 struct module *owner ;
869 char const *mod_name ;
870 bool suppress_bind_attrs ;
871 struct of_device_id const *of_match_table ;
872 int (*probe)(struct device *dev ) ;
873 int (*remove)(struct device *dev ) ;
874 void (*shutdown)(struct device *dev ) ;
875 int (*suspend)(struct device *dev , pm_message_t state ) ;
876 int (*resume)(struct device *dev ) ;
877 struct attribute_group const **groups ;
878 struct dev_pm_ops const *pm ;
879 struct driver_private *p ;
880};
881#line 249 "include/linux/device.h"
882struct driver_attribute {
883 struct attribute attr ;
884 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
885 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
886};
887#line 330
888struct class_attribute;
889#line 330 "include/linux/device.h"
890struct class {
891 char const *name ;
892 struct module *owner ;
893 struct class_attribute *class_attrs ;
894 struct device_attribute *dev_attrs ;
895 struct bin_attribute *dev_bin_attrs ;
896 struct kobject *dev_kobj ;
897 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
898 char *(*devnode)(struct device *dev , umode_t *mode ) ;
899 void (*class_release)(struct class *class ) ;
900 void (*dev_release)(struct device *dev ) ;
901 int (*suspend)(struct device *dev , pm_message_t state ) ;
902 int (*resume)(struct device *dev ) ;
903 struct kobj_ns_type_operations const *ns_type ;
904 void const *(*namespace)(struct device *dev ) ;
905 struct dev_pm_ops const *pm ;
906 struct subsys_private *p ;
907};
908#line 397 "include/linux/device.h"
909struct class_attribute {
910 struct attribute attr ;
911 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
912 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
913 size_t count ) ;
914 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ;
915};
916#line 465 "include/linux/device.h"
917struct device_type {
918 char const *name ;
919 struct attribute_group const **groups ;
920 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
921 char *(*devnode)(struct device *dev , umode_t *mode ) ;
922 void (*release)(struct device *dev ) ;
923 struct dev_pm_ops const *pm ;
924};
925#line 476 "include/linux/device.h"
926struct device_attribute {
927 struct attribute attr ;
928 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
929 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
930 size_t count ) ;
931};
932#line 559 "include/linux/device.h"
933struct device_dma_parameters {
934 unsigned int max_segment_size ;
935 unsigned long segment_boundary_mask ;
936};
937#line 627
938struct dma_coherent_mem;
939#line 627 "include/linux/device.h"
940struct device {
941 struct device *parent ;
942 struct device_private *p ;
943 struct kobject kobj ;
944 char const *init_name ;
945 struct device_type const *type ;
946 struct mutex mutex ;
947 struct bus_type *bus ;
948 struct device_driver *driver ;
949 void *platform_data ;
950 struct dev_pm_info power ;
951 struct dev_pm_domain *pm_domain ;
952 int numa_node ;
953 u64 *dma_mask ;
954 u64 coherent_dma_mask ;
955 struct device_dma_parameters *dma_parms ;
956 struct list_head dma_pools ;
957 struct dma_coherent_mem *dma_mem ;
958 struct dev_archdata archdata ;
959 struct device_node *of_node ;
960 dev_t devt ;
961 u32 id ;
962 spinlock_t devres_lock ;
963 struct list_head devres_head ;
964 struct klist_node knode_class ;
965 struct class *class ;
966 struct attribute_group const **groups ;
967 void (*release)(struct device *dev ) ;
968};
969#line 43 "include/linux/pm_wakeup.h"
970struct wakeup_source {
971 char const *name ;
972 struct list_head entry ;
973 spinlock_t lock ;
974 struct timer_list timer ;
975 unsigned long timer_expires ;
976 ktime_t total_time ;
977 ktime_t max_time ;
978 ktime_t last_time ;
979 unsigned long event_count ;
980 unsigned long active_count ;
981 unsigned long relax_count ;
982 unsigned long hit_count ;
983 unsigned int active : 1 ;
984};
985#line 12 "include/linux/mod_devicetable.h"
986typedef unsigned long kernel_ulong_t;
987#line 219 "include/linux/mod_devicetable.h"
988struct of_device_id {
989 char name[32] ;
990 char type[32] ;
991 char compatible[128] ;
992 void *data ;
993};
994#line 506 "include/linux/mod_devicetable.h"
995struct platform_device_id {
996 char name[20] ;
997 kernel_ulong_t driver_data __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
998};
999#line 17 "include/linux/platform_device.h"
1000struct mfd_cell;
1001#line 17
1002struct mfd_cell;
1003#line 19 "include/linux/platform_device.h"
1004struct platform_device {
1005 char const *name ;
1006 int id ;
1007 struct device dev ;
1008 u32 num_resources ;
1009 struct resource *resource ;
1010 struct platform_device_id const *id_entry ;
1011 struct mfd_cell *mfd_cell ;
1012 struct pdev_archdata archdata ;
1013};
1014#line 164 "include/linux/platform_device.h"
1015struct platform_driver {
1016 int (*probe)(struct platform_device * ) ;
1017 int (*remove)(struct platform_device * ) ;
1018 void (*shutdown)(struct platform_device * ) ;
1019 int (*suspend)(struct platform_device * , pm_message_t state ) ;
1020 int (*resume)(struct platform_device * ) ;
1021 struct device_driver driver ;
1022 struct platform_device_id const *id_table ;
1023};
1024#line 17 "include/linux/hwmon.h"
1025struct device;
1026#line 28 "include/linux/of.h"
1027typedef u32 phandle;
1028#line 31 "include/linux/of.h"
1029struct property {
1030 char *name ;
1031 int length ;
1032 void *value ;
1033 struct property *next ;
1034 unsigned long _flags ;
1035 unsigned int unique_id ;
1036};
1037#line 44 "include/linux/of.h"
1038struct device_node {
1039 char const *name ;
1040 char const *type ;
1041 phandle phandle ;
1042 char *full_name ;
1043 struct property *properties ;
1044 struct property *deadprops ;
1045 struct device_node *parent ;
1046 struct device_node *child ;
1047 struct device_node *sibling ;
1048 struct device_node *next ;
1049 struct device_node *allnext ;
1050 struct proc_dir_entry *pde ;
1051 struct kref kref ;
1052 unsigned long _flags ;
1053 void *data ;
1054};
1055#line 44 "include/asm-generic/gpio.h"
1056struct device;
1057#line 47
1058struct module;
1059#line 48
1060struct device_node;
1061#line 14 "include/linux/gpio-fan.h"
1062struct gpio_fan_alarm {
1063 unsigned int gpio ;
1064 unsigned int active_low ;
1065};
1066#line 19 "include/linux/gpio-fan.h"
1067struct gpio_fan_speed {
1068 int rpm ;
1069 int ctrl_val ;
1070};
1071#line 24 "include/linux/gpio-fan.h"
1072struct gpio_fan_platform_data {
1073 int num_ctrl ;
1074 unsigned int *ctrl ;
1075 struct gpio_fan_alarm *alarm ;
1076 int num_speed ;
1077 struct gpio_fan_speed *speed ;
1078};
1079#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1080struct gpio_fan_data {
1081 struct platform_device *pdev ;
1082 struct device *hwmon_dev ;
1083 struct mutex lock ;
1084 int num_ctrl ;
1085 unsigned int *ctrl ;
1086 int num_speed ;
1087 struct gpio_fan_speed *speed ;
1088 int speed_index ;
1089 int resume_speed ;
1090 bool pwm_enable ;
1091 struct gpio_fan_alarm *alarm ;
1092 struct work_struct alarm_work ;
1093};
1094#line 1 "<compiler builtins>"
1095long __builtin_expect(long val , long res ) ;
1096#line 24 "include/linux/list.h"
1097__inline static void INIT_LIST_HEAD(struct list_head *list ) __attribute__((__no_instrument_function__)) ;
1098#line 24 "include/linux/list.h"
1099__inline static void INIT_LIST_HEAD(struct list_head *list )
1100{ unsigned long __cil_tmp2 ;
1101 unsigned long __cil_tmp3 ;
1102
1103 {
1104#line 26
1105 *((struct list_head **)list) = list;
1106#line 27
1107 __cil_tmp2 = (unsigned long )list;
1108#line 27
1109 __cil_tmp3 = __cil_tmp2 + 8;
1110#line 27
1111 *((struct list_head **)__cil_tmp3) = list;
1112#line 28
1113 return;
1114}
1115}
1116#line 215 "include/linux/kernel.h"
1117extern int __attribute__((__warn_unused_result__)) _kstrtoul(char const *s , unsigned int base ,
1118 unsigned long *res ) ;
1119#line 218
1120extern int __attribute__((__warn_unused_result__)) kstrtoull(char const *s , unsigned int base ,
1121 unsigned long long *res ) ;
1122#line 220
1123__inline static int __attribute__((__warn_unused_result__)) kstrtoul(char const *s ,
1124 unsigned int base ,
1125 unsigned long *res ) __attribute__((__no_instrument_function__)) ;
1126#line 220 "include/linux/kernel.h"
1127__inline static int __attribute__((__warn_unused_result__)) kstrtoul(char const *s ,
1128 unsigned int base ,
1129 unsigned long *res )
1130{ int tmp ;
1131 int tmp___0 ;
1132 unsigned long long *__cil_tmp6 ;
1133
1134 {
1135#line 226
1136 if (8UL == 8UL) {
1137#line 226
1138 if (8UL == 8UL) {
1139 {
1140#line 228
1141 __cil_tmp6 = (unsigned long long *)res;
1142#line 228
1143 tmp = (int )kstrtoull(s, base, __cil_tmp6);
1144 }
1145#line 228
1146 return (tmp);
1147 } else {
1148 {
1149#line 230
1150 tmp___0 = (int )_kstrtoul(s, base, res);
1151 }
1152#line 230
1153 return (tmp___0);
1154 }
1155 } else {
1156 {
1157#line 230
1158 tmp___0 = (int )_kstrtoul(s, base, res);
1159 }
1160#line 230
1161 return (tmp___0);
1162 }
1163}
1164}
1165#line 320
1166extern int ( sprintf)(char *buf , char const *fmt , ...) ;
1167#line 27 "include/linux/err.h"
1168__inline static long __attribute__((__warn_unused_result__)) PTR_ERR(void const *ptr ) __attribute__((__no_instrument_function__)) ;
1169#line 27 "include/linux/err.h"
1170__inline static long __attribute__((__warn_unused_result__)) PTR_ERR(void const *ptr )
1171{
1172
1173 {
1174#line 29
1175 return ((long )ptr);
1176}
1177}
1178#line 32
1179__inline static long __attribute__((__warn_unused_result__)) IS_ERR(void const *ptr ) __attribute__((__no_instrument_function__)) ;
1180#line 32 "include/linux/err.h"
1181__inline static long __attribute__((__warn_unused_result__)) IS_ERR(void const *ptr )
1182{ long tmp ;
1183 unsigned long __cil_tmp3 ;
1184 int __cil_tmp4 ;
1185 int __cil_tmp5 ;
1186 int __cil_tmp6 ;
1187 long __cil_tmp7 ;
1188
1189 {
1190 {
1191#line 34
1192 __cil_tmp3 = (unsigned long )ptr;
1193#line 34
1194 __cil_tmp4 = __cil_tmp3 >= 0xfffffffffffff001UL;
1195#line 34
1196 __cil_tmp5 = ! __cil_tmp4;
1197#line 34
1198 __cil_tmp6 = ! __cil_tmp5;
1199#line 34
1200 __cil_tmp7 = (long )__cil_tmp6;
1201#line 34
1202 tmp = __builtin_expect(__cil_tmp7, 0L);
1203 }
1204#line 34
1205 return (tmp);
1206}
1207}
1208#line 115 "include/linux/mutex.h"
1209extern void __mutex_init(struct mutex *lock , char const *name , struct lock_class_key *key ) ;
1210#line 152
1211void mutex_lock(struct mutex *lock ) ;
1212#line 153
1213int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
1214#line 154
1215int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
1216#line 168
1217int mutex_trylock(struct mutex *lock ) ;
1218#line 169
1219void mutex_unlock(struct mutex *lock ) ;
1220#line 170
1221int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1222#line 156 "include/linux/workqueue.h"
1223extern void __init_work(struct work_struct *work , int onstack ) ;
1224#line 380
1225extern int schedule_work(struct work_struct *work ) ;
1226#line 158 "include/linux/sysfs.h"
1227extern int __attribute__((__warn_unused_result__)) sysfs_create_group(struct kobject *kobj ,
1228 struct attribute_group const *grp ) ;
1229#line 162
1230extern void sysfs_remove_group(struct kobject *kobj , struct attribute_group const *grp ) ;
1231#line 173
1232extern void sysfs_notify(struct kobject *kobj , char const *dir , char const *attr ) ;
1233#line 207 "include/linux/kobject.h"
1234extern int kobject_uevent(struct kobject *kobj , enum kobject_action action ) ;
1235#line 67 "include/linux/module.h"
1236int init_module(void) ;
1237#line 68
1238void cleanup_module(void) ;
1239#line 161 "include/linux/slab.h"
1240extern void kfree(void const * ) ;
1241#line 221 "include/linux/slub_def.h"
1242extern void *__kmalloc(size_t size , gfp_t flags ) ;
1243#line 268
1244__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1245 gfp_t flags ) __attribute__((__no_instrument_function__)) ;
1246#line 268 "include/linux/slub_def.h"
1247__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1248 gfp_t flags )
1249{ void *tmp___2 ;
1250
1251 {
1252 {
1253#line 283
1254 tmp___2 = __kmalloc(size, flags);
1255 }
1256#line 283
1257 return (tmp___2);
1258}
1259}
1260#line 349 "include/linux/slab.h"
1261__inline static void *kzalloc(size_t size , gfp_t flags ) __attribute__((__no_instrument_function__)) ;
1262#line 349 "include/linux/slab.h"
1263__inline static void *kzalloc(size_t size , gfp_t flags )
1264{ void *tmp ;
1265 unsigned int __cil_tmp4 ;
1266
1267 {
1268 {
1269#line 351
1270 __cil_tmp4 = flags | 32768U;
1271#line 351
1272 tmp = kmalloc(size, __cil_tmp4);
1273 }
1274#line 351
1275 return (tmp);
1276}
1277}
1278#line 531 "include/linux/irq.h"
1279extern int irq_set_irq_type(unsigned int irq , unsigned int type ) ;
1280#line 126 "include/linux/interrupt.h"
1281extern int __attribute__((__warn_unused_result__)) request_threaded_irq(unsigned int irq ,
1282 irqreturn_t (*handler)(int ,
1283 void * ) ,
1284 irqreturn_t (*thread_fn)(int ,
1285 void * ) ,
1286 unsigned long flags ,
1287 char const *name ,
1288 void *dev ) ;
1289#line 131
1290__inline static int __attribute__((__warn_unused_result__)) request_irq(unsigned int irq ,
1291 irqreturn_t (*handler)(int ,
1292 void * ) ,
1293 unsigned long flags ,
1294 char const *name ,
1295 void *dev ) __attribute__((__no_instrument_function__)) ;
1296#line 131 "include/linux/interrupt.h"
1297__inline static int __attribute__((__warn_unused_result__)) request_irq(unsigned int irq ,
1298 irqreturn_t (*handler)(int ,
1299 void * ) ,
1300 unsigned long flags ,
1301 char const *name ,
1302 void *dev )
1303{ int tmp ;
1304 void *__cil_tmp7 ;
1305 irqreturn_t (*__cil_tmp8)(int , void * ) ;
1306
1307 {
1308 {
1309#line 135
1310 __cil_tmp7 = (void *)0;
1311#line 135
1312 __cil_tmp8 = (irqreturn_t (*)(int , void * ))__cil_tmp7;
1313#line 135
1314 tmp = (int )request_threaded_irq(irq, handler, __cil_tmp8, flags, name, dev);
1315 }
1316#line 135
1317 return (tmp);
1318}
1319}
1320#line 184
1321extern void free_irq(unsigned int , void * ) ;
1322#line 507 "include/linux/device.h"
1323extern int device_create_file(struct device *device , struct device_attribute const *entry ) ;
1324#line 509
1325extern void device_remove_file(struct device *dev , struct device_attribute const *attr ) ;
1326#line 792
1327extern void *dev_get_drvdata(struct device const *dev ) ;
1328#line 793
1329extern int dev_set_drvdata(struct device *dev , void *data ) ;
1330#line 893
1331extern int ( dev_warn)(struct device const *dev , char const *fmt
1332 , ...) ;
1333#line 897
1334extern int ( _dev_info)(struct device const *dev , char const *fmt
1335 , ...) ;
1336#line 174 "include/linux/platform_device.h"
1337extern int platform_driver_register(struct platform_driver * ) ;
1338#line 175
1339extern void platform_driver_unregister(struct platform_driver * ) ;
1340#line 183
1341__inline static void *platform_get_drvdata(struct platform_device const *pdev ) __attribute__((__no_instrument_function__)) ;
1342#line 183 "include/linux/platform_device.h"
1343__inline static void *platform_get_drvdata(struct platform_device const *pdev )
1344{ void *tmp ;
1345 unsigned long __cil_tmp3 ;
1346 unsigned long __cil_tmp4 ;
1347 struct device const *__cil_tmp5 ;
1348
1349 {
1350 {
1351#line 185
1352 __cil_tmp3 = (unsigned long )pdev;
1353#line 185
1354 __cil_tmp4 = __cil_tmp3 + 16;
1355#line 185
1356 __cil_tmp5 = (struct device const *)__cil_tmp4;
1357#line 185
1358 tmp = dev_get_drvdata(__cil_tmp5);
1359 }
1360#line 185
1361 return (tmp);
1362}
1363}
1364#line 188
1365__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) __attribute__((__no_instrument_function__)) ;
1366#line 188 "include/linux/platform_device.h"
1367__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
1368{ unsigned long __cil_tmp3 ;
1369 unsigned long __cil_tmp4 ;
1370 struct device *__cil_tmp5 ;
1371
1372 {
1373 {
1374#line 190
1375 __cil_tmp3 = (unsigned long )pdev;
1376#line 190
1377 __cil_tmp4 = __cil_tmp3 + 16;
1378#line 190
1379 __cil_tmp5 = (struct device *)__cil_tmp4;
1380#line 190
1381 dev_set_drvdata(__cil_tmp5, data);
1382 }
1383#line 191
1384 return;
1385}
1386}
1387#line 19 "include/linux/hwmon.h"
1388extern struct device *hwmon_device_register(struct device *dev ) ;
1389#line 21
1390extern void hwmon_device_unregister(struct device *dev ) ;
1391#line 153 "include/asm-generic/gpio.h"
1392extern int gpio_request(unsigned int gpio , char const *label ) ;
1393#line 154
1394extern void gpio_free(unsigned int gpio ) ;
1395#line 156
1396extern int gpio_direction_input(unsigned int gpio ) ;
1397#line 157
1398extern int gpio_direction_output(unsigned int gpio , int value ) ;
1399#line 169
1400extern int __gpio_get_value(unsigned int gpio ) ;
1401#line 170
1402extern void __gpio_set_value(unsigned int gpio , int value ) ;
1403#line 174
1404extern int __gpio_to_irq(unsigned int gpio ) ;
1405#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1406__inline static int gpio_get_value(unsigned int gpio ) __attribute__((__no_instrument_function__)) ;
1407#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1408__inline static int gpio_get_value(unsigned int gpio )
1409{ int tmp ;
1410
1411 {
1412 {
1413#line 28
1414 tmp = __gpio_get_value(gpio);
1415 }
1416#line 28
1417 return (tmp);
1418}
1419}
1420#line 31
1421__inline static void gpio_set_value(unsigned int gpio , int value ) __attribute__((__no_instrument_function__)) ;
1422#line 31 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1423__inline static void gpio_set_value(unsigned int gpio , int value )
1424{
1425
1426 {
1427 {
1428#line 33
1429 __gpio_set_value(gpio, value);
1430 }
1431#line 34
1432 return;
1433}
1434}
1435#line 41
1436__inline static int gpio_to_irq(unsigned int gpio ) __attribute__((__no_instrument_function__)) ;
1437#line 41 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1438__inline static int gpio_to_irq(unsigned int gpio )
1439{ int tmp ;
1440
1441 {
1442 {
1443#line 43
1444 tmp = __gpio_to_irq(gpio);
1445 }
1446#line 43
1447 return (tmp);
1448}
1449}
1450#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1451static void fan_alarm_notify(struct work_struct *ws )
1452{ struct gpio_fan_data *fan_data ;
1453 struct work_struct const *__mptr ;
1454 struct gpio_fan_data *__cil_tmp4 ;
1455 unsigned long __cil_tmp5 ;
1456 unsigned long __cil_tmp6 ;
1457 struct work_struct *__cil_tmp7 ;
1458 unsigned int __cil_tmp8 ;
1459 char *__cil_tmp9 ;
1460 char *__cil_tmp10 ;
1461 unsigned long __cil_tmp11 ;
1462 struct platform_device *__cil_tmp12 ;
1463 unsigned long __cil_tmp13 ;
1464 unsigned long __cil_tmp14 ;
1465 struct kobject *__cil_tmp15 ;
1466 void *__cil_tmp16 ;
1467 char const *__cil_tmp17 ;
1468 unsigned long __cil_tmp18 ;
1469 struct platform_device *__cil_tmp19 ;
1470 unsigned long __cil_tmp20 ;
1471 unsigned long __cil_tmp21 ;
1472 struct kobject *__cil_tmp22 ;
1473 enum kobject_action __cil_tmp23 ;
1474
1475 {
1476 {
1477#line 60
1478 __mptr = (struct work_struct const *)ws;
1479#line 60
1480 __cil_tmp4 = (struct gpio_fan_data *)0;
1481#line 60
1482 __cil_tmp5 = (unsigned long )__cil_tmp4;
1483#line 60
1484 __cil_tmp6 = __cil_tmp5 + 144;
1485#line 60
1486 __cil_tmp7 = (struct work_struct *)__cil_tmp6;
1487#line 60
1488 __cil_tmp8 = (unsigned int )__cil_tmp7;
1489#line 60
1490 __cil_tmp9 = (char *)__mptr;
1491#line 60
1492 __cil_tmp10 = __cil_tmp9 - __cil_tmp8;
1493#line 60
1494 fan_data = (struct gpio_fan_data *)__cil_tmp10;
1495#line 62
1496 __cil_tmp11 = 16 + 16;
1497#line 62
1498 __cil_tmp12 = *((struct platform_device **)fan_data);
1499#line 62
1500 __cil_tmp13 = (unsigned long )__cil_tmp12;
1501#line 62
1502 __cil_tmp14 = __cil_tmp13 + __cil_tmp11;
1503#line 62
1504 __cil_tmp15 = (struct kobject *)__cil_tmp14;
1505#line 62
1506 __cil_tmp16 = (void *)0;
1507#line 62
1508 __cil_tmp17 = (char const *)__cil_tmp16;
1509#line 62
1510 sysfs_notify(__cil_tmp15, __cil_tmp17, "fan1_alarm");
1511#line 63
1512 __cil_tmp18 = 16 + 16;
1513#line 63
1514 __cil_tmp19 = *((struct platform_device **)fan_data);
1515#line 63
1516 __cil_tmp20 = (unsigned long )__cil_tmp19;
1517#line 63
1518 __cil_tmp21 = __cil_tmp20 + __cil_tmp18;
1519#line 63
1520 __cil_tmp22 = (struct kobject *)__cil_tmp21;
1521#line 63
1522 __cil_tmp23 = (enum kobject_action )2;
1523#line 63
1524 kobject_uevent(__cil_tmp22, __cil_tmp23);
1525 }
1526#line 64
1527 return;
1528}
1529}
1530#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1531static irqreturn_t fan_alarm_irq_handler(int irq , void *dev_id )
1532{ struct gpio_fan_data *fan_data ;
1533 unsigned long __cil_tmp4 ;
1534 unsigned long __cil_tmp5 ;
1535 struct work_struct *__cil_tmp6 ;
1536
1537 {
1538 {
1539#line 68
1540 fan_data = (struct gpio_fan_data *)dev_id;
1541#line 70
1542 __cil_tmp4 = (unsigned long )fan_data;
1543#line 70
1544 __cil_tmp5 = __cil_tmp4 + 144;
1545#line 70
1546 __cil_tmp6 = (struct work_struct *)__cil_tmp5;
1547#line 70
1548 schedule_work(__cil_tmp6);
1549 }
1550#line 72
1551 return ((irqreturn_t )0);
1552}
1553}
1554#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1555static ssize_t show_fan_alarm(struct device *dev , struct device_attribute *attr ,
1556 char *buf )
1557{ struct gpio_fan_data *fan_data ;
1558 void *tmp ;
1559 struct gpio_fan_alarm *alarm ;
1560 int value ;
1561 int tmp___0 ;
1562 int tmp___1 ;
1563 struct device const *__cil_tmp10 ;
1564 unsigned long __cil_tmp11 ;
1565 unsigned long __cil_tmp12 ;
1566 unsigned int __cil_tmp13 ;
1567 unsigned long __cil_tmp14 ;
1568 unsigned long __cil_tmp15 ;
1569
1570 {
1571 {
1572#line 78
1573 __cil_tmp10 = (struct device const *)dev;
1574#line 78
1575 tmp = dev_get_drvdata(__cil_tmp10);
1576#line 78
1577 fan_data = (struct gpio_fan_data *)tmp;
1578#line 79
1579 __cil_tmp11 = (unsigned long )fan_data;
1580#line 79
1581 __cil_tmp12 = __cil_tmp11 + 136;
1582#line 79
1583 alarm = *((struct gpio_fan_alarm **)__cil_tmp12);
1584#line 80
1585 __cil_tmp13 = *((unsigned int *)alarm);
1586#line 80
1587 tmp___0 = gpio_get_value(__cil_tmp13);
1588#line 80
1589 value = tmp___0;
1590 }
1591 {
1592#line 82
1593 __cil_tmp14 = (unsigned long )alarm;
1594#line 82
1595 __cil_tmp15 = __cil_tmp14 + 4;
1596#line 82
1597 if (*((unsigned int *)__cil_tmp15)) {
1598#line 83
1599 value = ! value;
1600 } else {
1601
1602 }
1603 }
1604 {
1605#line 85
1606 tmp___1 = sprintf(buf, "%d\n", value);
1607 }
1608#line 85
1609 return ((ssize_t )tmp___1);
1610}
1611}
1612#line 88 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1613static struct device_attribute dev_attr_fan1_alarm = {{"fan1_alarm", (umode_t )292}, & show_fan_alarm, (ssize_t (*)(struct device *dev ,
1614 struct device_attribute *attr ,
1615 char const *buf ,
1616 size_t count ))((void *)0)};
1617#line 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1618static int fan_alarm_init(struct gpio_fan_data *fan_data , struct gpio_fan_alarm *alarm )
1619{ int err ;
1620 int alarm_irq ;
1621 struct platform_device *pdev ;
1622 atomic_long_t __constr_expr_0 ;
1623 unsigned long __cil_tmp7 ;
1624 unsigned long __cil_tmp8 ;
1625 unsigned int __cil_tmp9 ;
1626 unsigned int __cil_tmp10 ;
1627 unsigned long __cil_tmp11 ;
1628 unsigned long __cil_tmp12 ;
1629 struct device *__cil_tmp13 ;
1630 struct device_attribute const *__cil_tmp14 ;
1631 unsigned int __cil_tmp15 ;
1632 unsigned long __cil_tmp16 ;
1633 unsigned long __cil_tmp17 ;
1634 struct work_struct *__cil_tmp18 ;
1635 unsigned long __cil_tmp19 ;
1636 unsigned long __cil_tmp20 ;
1637 unsigned long __cil_tmp21 ;
1638 unsigned long __cil_tmp22 ;
1639 unsigned long __cil_tmp23 ;
1640 struct list_head *__cil_tmp24 ;
1641 unsigned long __cil_tmp25 ;
1642 unsigned long __cil_tmp26 ;
1643 unsigned long __cil_tmp27 ;
1644 unsigned int __cil_tmp28 ;
1645 unsigned int __cil_tmp29 ;
1646 void *__cil_tmp30 ;
1647 unsigned long __cil_tmp31 ;
1648 unsigned long __cil_tmp32 ;
1649 struct device *__cil_tmp33 ;
1650 struct device_attribute const *__cil_tmp34 ;
1651 unsigned int __cil_tmp35 ;
1652 long __constr_expr_0_counter36 ;
1653
1654 {
1655 {
1656#line 95
1657 pdev = *((struct platform_device **)fan_data);
1658#line 97
1659 __cil_tmp7 = (unsigned long )fan_data;
1660#line 97
1661 __cil_tmp8 = __cil_tmp7 + 136;
1662#line 97
1663 *((struct gpio_fan_alarm **)__cil_tmp8) = alarm;
1664#line 99
1665 __cil_tmp9 = *((unsigned int *)alarm);
1666#line 99
1667 err = gpio_request(__cil_tmp9, "GPIO fan alarm");
1668 }
1669#line 100
1670 if (err) {
1671#line 101
1672 return (err);
1673 } else {
1674
1675 }
1676 {
1677#line 103
1678 __cil_tmp10 = *((unsigned int *)alarm);
1679#line 103
1680 err = gpio_direction_input(__cil_tmp10);
1681 }
1682#line 104
1683 if (err) {
1684#line 105
1685 goto err_free_gpio;
1686 } else {
1687
1688 }
1689 {
1690#line 107
1691 __cil_tmp11 = (unsigned long )pdev;
1692#line 107
1693 __cil_tmp12 = __cil_tmp11 + 16;
1694#line 107
1695 __cil_tmp13 = (struct device *)__cil_tmp12;
1696#line 107
1697 __cil_tmp14 = (struct device_attribute const *)(& dev_attr_fan1_alarm);
1698#line 107
1699 err = device_create_file(__cil_tmp13, __cil_tmp14);
1700 }
1701#line 108
1702 if (err) {
1703#line 109
1704 goto err_free_gpio;
1705 } else {
1706
1707 }
1708 {
1709#line 115
1710 __cil_tmp15 = *((unsigned int *)alarm);
1711#line 115
1712 alarm_irq = gpio_to_irq(__cil_tmp15);
1713 }
1714#line 116
1715 if (alarm_irq < 0) {
1716#line 117
1717 return (0);
1718 } else {
1719
1720 }
1721 {
1722#line 119
1723 while (1) {
1724 while_continue: ;
1725 {
1726#line 119
1727 while (1) {
1728 while_continue___0: ;
1729 {
1730#line 119
1731 __cil_tmp16 = (unsigned long )fan_data;
1732#line 119
1733 __cil_tmp17 = __cil_tmp16 + 144;
1734#line 119
1735 __cil_tmp18 = (struct work_struct *)__cil_tmp17;
1736#line 119
1737 __init_work(__cil_tmp18, 0);
1738#line 119
1739 __constr_expr_0_counter36 = 2097664L;
1740#line 119
1741 __cil_tmp19 = (unsigned long )fan_data;
1742#line 119
1743 __cil_tmp20 = __cil_tmp19 + 144;
1744#line 119
1745 ((atomic_long_t *)__cil_tmp20)->counter = __constr_expr_0_counter36;
1746#line 119
1747 __cil_tmp21 = 144 + 8;
1748#line 119
1749 __cil_tmp22 = (unsigned long )fan_data;
1750#line 119
1751 __cil_tmp23 = __cil_tmp22 + __cil_tmp21;
1752#line 119
1753 __cil_tmp24 = (struct list_head *)__cil_tmp23;
1754#line 119
1755 INIT_LIST_HEAD(__cil_tmp24);
1756 }
1757 {
1758#line 119
1759 while (1) {
1760 while_continue___1: ;
1761#line 119
1762 __cil_tmp25 = 144 + 24;
1763#line 119
1764 __cil_tmp26 = (unsigned long )fan_data;
1765#line 119
1766 __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
1767#line 119
1768 *((void (**)(struct work_struct *work ))__cil_tmp27) = & fan_alarm_notify;
1769#line 119
1770 goto while_break___1;
1771 }
1772 while_break___1: ;
1773 }
1774#line 119
1775 goto while_break___0;
1776 }
1777 while_break___0: ;
1778 }
1779#line 119
1780 goto while_break;
1781 }
1782 while_break: ;
1783 }
1784 {
1785#line 120
1786 __cil_tmp28 = (unsigned int )alarm_irq;
1787#line 120
1788 irq_set_irq_type(__cil_tmp28, 3U);
1789#line 121
1790 __cil_tmp29 = (unsigned int )alarm_irq;
1791#line 121
1792 __cil_tmp30 = (void *)fan_data;
1793#line 121
1794 err = (int )request_irq(__cil_tmp29, & fan_alarm_irq_handler, 128UL, "GPIO fan alarm",
1795 __cil_tmp30);
1796 }
1797#line 123
1798 if (err) {
1799#line 124
1800 goto err_free_sysfs;
1801 } else {
1802
1803 }
1804#line 126
1805 return (0);
1806 err_free_sysfs:
1807 {
1808#line 129
1809 __cil_tmp31 = (unsigned long )pdev;
1810#line 129
1811 __cil_tmp32 = __cil_tmp31 + 16;
1812#line 129
1813 __cil_tmp33 = (struct device *)__cil_tmp32;
1814#line 129
1815 __cil_tmp34 = (struct device_attribute const *)(& dev_attr_fan1_alarm);
1816#line 129
1817 device_remove_file(__cil_tmp33, __cil_tmp34);
1818 }
1819 err_free_gpio:
1820 {
1821#line 131
1822 __cil_tmp35 = *((unsigned int *)alarm);
1823#line 131
1824 gpio_free(__cil_tmp35);
1825 }
1826#line 133
1827 return (err);
1828}
1829}
1830#line 136 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1831static void fan_alarm_free(struct gpio_fan_data *fan_data )
1832{ struct platform_device *pdev ;
1833 int alarm_irq ;
1834 int tmp ;
1835 unsigned long __cil_tmp5 ;
1836 unsigned long __cil_tmp6 ;
1837 struct gpio_fan_alarm *__cil_tmp7 ;
1838 unsigned int __cil_tmp8 ;
1839 unsigned int __cil_tmp9 ;
1840 void *__cil_tmp10 ;
1841 unsigned long __cil_tmp11 ;
1842 unsigned long __cil_tmp12 ;
1843 struct device *__cil_tmp13 ;
1844 struct device_attribute const *__cil_tmp14 ;
1845 unsigned long __cil_tmp15 ;
1846 unsigned long __cil_tmp16 ;
1847 struct gpio_fan_alarm *__cil_tmp17 ;
1848 unsigned int __cil_tmp18 ;
1849
1850 {
1851 {
1852#line 138
1853 pdev = *((struct platform_device **)fan_data);
1854#line 139
1855 __cil_tmp5 = (unsigned long )fan_data;
1856#line 139
1857 __cil_tmp6 = __cil_tmp5 + 136;
1858#line 139
1859 __cil_tmp7 = *((struct gpio_fan_alarm **)__cil_tmp6);
1860#line 139
1861 __cil_tmp8 = *((unsigned int *)__cil_tmp7);
1862#line 139
1863 tmp = gpio_to_irq(__cil_tmp8);
1864#line 139
1865 alarm_irq = tmp;
1866 }
1867#line 141
1868 if (alarm_irq >= 0) {
1869 {
1870#line 142
1871 __cil_tmp9 = (unsigned int )alarm_irq;
1872#line 142
1873 __cil_tmp10 = (void *)fan_data;
1874#line 142
1875 free_irq(__cil_tmp9, __cil_tmp10);
1876 }
1877 } else {
1878
1879 }
1880 {
1881#line 143
1882 __cil_tmp11 = (unsigned long )pdev;
1883#line 143
1884 __cil_tmp12 = __cil_tmp11 + 16;
1885#line 143
1886 __cil_tmp13 = (struct device *)__cil_tmp12;
1887#line 143
1888 __cil_tmp14 = (struct device_attribute const *)(& dev_attr_fan1_alarm);
1889#line 143
1890 device_remove_file(__cil_tmp13, __cil_tmp14);
1891#line 144
1892 __cil_tmp15 = (unsigned long )fan_data;
1893#line 144
1894 __cil_tmp16 = __cil_tmp15 + 136;
1895#line 144
1896 __cil_tmp17 = *((struct gpio_fan_alarm **)__cil_tmp16);
1897#line 144
1898 __cil_tmp18 = *((unsigned int *)__cil_tmp17);
1899#line 144
1900 gpio_free(__cil_tmp18);
1901 }
1902#line 145
1903 return;
1904}
1905}
1906#line 152 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1907static void __set_fan_ctrl(struct gpio_fan_data *fan_data , int ctrl_val )
1908{ int i ;
1909 unsigned long __cil_tmp4 ;
1910 unsigned long __cil_tmp5 ;
1911 int __cil_tmp6 ;
1912 unsigned long __cil_tmp7 ;
1913 unsigned long __cil_tmp8 ;
1914 unsigned int *__cil_tmp9 ;
1915 unsigned int *__cil_tmp10 ;
1916 unsigned int __cil_tmp11 ;
1917 int __cil_tmp12 ;
1918 int __cil_tmp13 ;
1919
1920 {
1921#line 156
1922 i = 0;
1923 {
1924#line 156
1925 while (1) {
1926 while_continue: ;
1927 {
1928#line 156
1929 __cil_tmp4 = (unsigned long )fan_data;
1930#line 156
1931 __cil_tmp5 = __cil_tmp4 + 88;
1932#line 156
1933 __cil_tmp6 = *((int *)__cil_tmp5);
1934#line 156
1935 if (i < __cil_tmp6) {
1936
1937 } else {
1938#line 156
1939 goto while_break;
1940 }
1941 }
1942 {
1943#line 157
1944 __cil_tmp7 = (unsigned long )fan_data;
1945#line 157
1946 __cil_tmp8 = __cil_tmp7 + 96;
1947#line 157
1948 __cil_tmp9 = *((unsigned int **)__cil_tmp8);
1949#line 157
1950 __cil_tmp10 = __cil_tmp9 + i;
1951#line 157
1952 __cil_tmp11 = *__cil_tmp10;
1953#line 157
1954 __cil_tmp12 = ctrl_val >> i;
1955#line 157
1956 __cil_tmp13 = __cil_tmp12 & 1;
1957#line 157
1958 gpio_set_value(__cil_tmp11, __cil_tmp13);
1959#line 156
1960 i = i + 1;
1961 }
1962 }
1963 while_break: ;
1964 }
1965#line 158
1966 return;
1967}
1968}
1969#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
1970static int __get_fan_ctrl(struct gpio_fan_data *fan_data )
1971{ int i ;
1972 int ctrl_val ;
1973 int value ;
1974 unsigned long __cil_tmp5 ;
1975 unsigned long __cil_tmp6 ;
1976 int __cil_tmp7 ;
1977 unsigned long __cil_tmp8 ;
1978 unsigned long __cil_tmp9 ;
1979 unsigned int *__cil_tmp10 ;
1980 unsigned int *__cil_tmp11 ;
1981 unsigned int __cil_tmp12 ;
1982 int __cil_tmp13 ;
1983
1984 {
1985#line 163
1986 ctrl_val = 0;
1987#line 165
1988 i = 0;
1989 {
1990#line 165
1991 while (1) {
1992 while_continue: ;
1993 {
1994#line 165
1995 __cil_tmp5 = (unsigned long )fan_data;
1996#line 165
1997 __cil_tmp6 = __cil_tmp5 + 88;
1998#line 165
1999 __cil_tmp7 = *((int *)__cil_tmp6);
2000#line 165
2001 if (i < __cil_tmp7) {
2002
2003 } else {
2004#line 165
2005 goto while_break;
2006 }
2007 }
2008 {
2009#line 168
2010 __cil_tmp8 = (unsigned long )fan_data;
2011#line 168
2012 __cil_tmp9 = __cil_tmp8 + 96;
2013#line 168
2014 __cil_tmp10 = *((unsigned int **)__cil_tmp9);
2015#line 168
2016 __cil_tmp11 = __cil_tmp10 + i;
2017#line 168
2018 __cil_tmp12 = *__cil_tmp11;
2019#line 168
2020 value = gpio_get_value(__cil_tmp12);
2021#line 169
2022 __cil_tmp13 = value << i;
2023#line 169
2024 ctrl_val = ctrl_val | __cil_tmp13;
2025#line 165
2026 i = i + 1;
2027 }
2028 }
2029 while_break: ;
2030 }
2031#line 171
2032 return (ctrl_val);
2033}
2034}
2035#line 175 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2036static void set_fan_speed(struct gpio_fan_data *fan_data , int speed_index )
2037{ unsigned long __cil_tmp3 ;
2038 unsigned long __cil_tmp4 ;
2039 int __cil_tmp5 ;
2040 unsigned long __cil_tmp6 ;
2041 unsigned long __cil_tmp7 ;
2042 struct gpio_fan_speed *__cil_tmp8 ;
2043 struct gpio_fan_speed *__cil_tmp9 ;
2044 unsigned long __cil_tmp10 ;
2045 unsigned long __cil_tmp11 ;
2046 int __cil_tmp12 ;
2047 unsigned long __cil_tmp13 ;
2048 unsigned long __cil_tmp14 ;
2049
2050 {
2051 {
2052#line 177
2053 __cil_tmp3 = (unsigned long )fan_data;
2054#line 177
2055 __cil_tmp4 = __cil_tmp3 + 120;
2056#line 177
2057 __cil_tmp5 = *((int *)__cil_tmp4);
2058#line 177
2059 if (__cil_tmp5 == speed_index) {
2060#line 178
2061 return;
2062 } else {
2063
2064 }
2065 }
2066 {
2067#line 180
2068 __cil_tmp6 = (unsigned long )fan_data;
2069#line 180
2070 __cil_tmp7 = __cil_tmp6 + 112;
2071#line 180
2072 __cil_tmp8 = *((struct gpio_fan_speed **)__cil_tmp7);
2073#line 180
2074 __cil_tmp9 = __cil_tmp8 + speed_index;
2075#line 180
2076 __cil_tmp10 = (unsigned long )__cil_tmp9;
2077#line 180
2078 __cil_tmp11 = __cil_tmp10 + 4;
2079#line 180
2080 __cil_tmp12 = *((int *)__cil_tmp11);
2081#line 180
2082 __set_fan_ctrl(fan_data, __cil_tmp12);
2083#line 181
2084 __cil_tmp13 = (unsigned long )fan_data;
2085#line 181
2086 __cil_tmp14 = __cil_tmp13 + 120;
2087#line 181
2088 *((int *)__cil_tmp14) = speed_index;
2089 }
2090#line 182
2091 return;
2092}
2093}
2094#line 184 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2095static int get_fan_speed_index(struct gpio_fan_data *fan_data )
2096{ int ctrl_val ;
2097 int tmp ;
2098 int i ;
2099 unsigned long __cil_tmp5 ;
2100 unsigned long __cil_tmp6 ;
2101 int __cil_tmp7 ;
2102 unsigned long __cil_tmp8 ;
2103 unsigned long __cil_tmp9 ;
2104 struct gpio_fan_speed *__cil_tmp10 ;
2105 struct gpio_fan_speed *__cil_tmp11 ;
2106 unsigned long __cil_tmp12 ;
2107 unsigned long __cil_tmp13 ;
2108 int __cil_tmp14 ;
2109 struct platform_device *__cil_tmp15 ;
2110 unsigned long __cil_tmp16 ;
2111 unsigned long __cil_tmp17 ;
2112 struct device *__cil_tmp18 ;
2113 struct device const *__cil_tmp19 ;
2114
2115 {
2116 {
2117#line 186
2118 tmp = __get_fan_ctrl(fan_data);
2119#line 186
2120 ctrl_val = tmp;
2121#line 189
2122 i = 0;
2123 }
2124 {
2125#line 189
2126 while (1) {
2127 while_continue: ;
2128 {
2129#line 189
2130 __cil_tmp5 = (unsigned long )fan_data;
2131#line 189
2132 __cil_tmp6 = __cil_tmp5 + 104;
2133#line 189
2134 __cil_tmp7 = *((int *)__cil_tmp6);
2135#line 189
2136 if (i < __cil_tmp7) {
2137
2138 } else {
2139#line 189
2140 goto while_break;
2141 }
2142 }
2143 {
2144#line 190
2145 __cil_tmp8 = (unsigned long )fan_data;
2146#line 190
2147 __cil_tmp9 = __cil_tmp8 + 112;
2148#line 190
2149 __cil_tmp10 = *((struct gpio_fan_speed **)__cil_tmp9);
2150#line 190
2151 __cil_tmp11 = __cil_tmp10 + i;
2152#line 190
2153 __cil_tmp12 = (unsigned long )__cil_tmp11;
2154#line 190
2155 __cil_tmp13 = __cil_tmp12 + 4;
2156#line 190
2157 __cil_tmp14 = *((int *)__cil_tmp13);
2158#line 190
2159 if (__cil_tmp14 == ctrl_val) {
2160#line 191
2161 return (i);
2162 } else {
2163
2164 }
2165 }
2166#line 189
2167 i = i + 1;
2168 }
2169 while_break: ;
2170 }
2171 {
2172#line 193
2173 __cil_tmp15 = *((struct platform_device **)fan_data);
2174#line 193
2175 __cil_tmp16 = (unsigned long )__cil_tmp15;
2176#line 193
2177 __cil_tmp17 = __cil_tmp16 + 16;
2178#line 193
2179 __cil_tmp18 = (struct device *)__cil_tmp17;
2180#line 193
2181 __cil_tmp19 = (struct device const *)__cil_tmp18;
2182#line 193
2183 dev_warn(__cil_tmp19, "missing speed array entry for GPIO value 0x%x\n", ctrl_val);
2184 }
2185#line 196
2186 return (-22);
2187}
2188}
2189#line 199 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2190static int rpm_to_speed_index(struct gpio_fan_data *fan_data , int rpm )
2191{ struct gpio_fan_speed *speed ;
2192 int i ;
2193 unsigned long __cil_tmp5 ;
2194 unsigned long __cil_tmp6 ;
2195 unsigned long __cil_tmp7 ;
2196 unsigned long __cil_tmp8 ;
2197 int __cil_tmp9 ;
2198 struct gpio_fan_speed *__cil_tmp10 ;
2199 int __cil_tmp11 ;
2200 unsigned long __cil_tmp12 ;
2201 unsigned long __cil_tmp13 ;
2202 int __cil_tmp14 ;
2203
2204 {
2205#line 201
2206 __cil_tmp5 = (unsigned long )fan_data;
2207#line 201
2208 __cil_tmp6 = __cil_tmp5 + 112;
2209#line 201
2210 speed = *((struct gpio_fan_speed **)__cil_tmp6);
2211#line 204
2212 i = 0;
2213 {
2214#line 204
2215 while (1) {
2216 while_continue: ;
2217 {
2218#line 204
2219 __cil_tmp7 = (unsigned long )fan_data;
2220#line 204
2221 __cil_tmp8 = __cil_tmp7 + 104;
2222#line 204
2223 __cil_tmp9 = *((int *)__cil_tmp8);
2224#line 204
2225 if (i < __cil_tmp9) {
2226
2227 } else {
2228#line 204
2229 goto while_break;
2230 }
2231 }
2232 {
2233#line 205
2234 __cil_tmp10 = speed + i;
2235#line 205
2236 __cil_tmp11 = *((int *)__cil_tmp10);
2237#line 205
2238 if (__cil_tmp11 >= rpm) {
2239#line 206
2240 return (i);
2241 } else {
2242
2243 }
2244 }
2245#line 204
2246 i = i + 1;
2247 }
2248 while_break: ;
2249 }
2250 {
2251#line 208
2252 __cil_tmp12 = (unsigned long )fan_data;
2253#line 208
2254 __cil_tmp13 = __cil_tmp12 + 104;
2255#line 208
2256 __cil_tmp14 = *((int *)__cil_tmp13);
2257#line 208
2258 return (__cil_tmp14 - 1);
2259 }
2260}
2261}
2262#line 211 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2263static ssize_t show_pwm(struct device *dev , struct device_attribute *attr , char *buf )
2264{ struct gpio_fan_data *fan_data ;
2265 void *tmp ;
2266 u8 pwm ;
2267 int tmp___0 ;
2268 struct device const *__cil_tmp8 ;
2269 unsigned long __cil_tmp9 ;
2270 unsigned long __cil_tmp10 ;
2271 int __cil_tmp11 ;
2272 int __cil_tmp12 ;
2273 unsigned long __cil_tmp13 ;
2274 unsigned long __cil_tmp14 ;
2275 int __cil_tmp15 ;
2276 int __cil_tmp16 ;
2277 int __cil_tmp17 ;
2278 int __cil_tmp18 ;
2279
2280 {
2281 {
2282#line 214
2283 __cil_tmp8 = (struct device const *)dev;
2284#line 214
2285 tmp = dev_get_drvdata(__cil_tmp8);
2286#line 214
2287 fan_data = (struct gpio_fan_data *)tmp;
2288#line 215
2289 __cil_tmp9 = (unsigned long )fan_data;
2290#line 215
2291 __cil_tmp10 = __cil_tmp9 + 104;
2292#line 215
2293 __cil_tmp11 = *((int *)__cil_tmp10);
2294#line 215
2295 __cil_tmp12 = __cil_tmp11 - 1;
2296#line 215
2297 __cil_tmp13 = (unsigned long )fan_data;
2298#line 215
2299 __cil_tmp14 = __cil_tmp13 + 120;
2300#line 215
2301 __cil_tmp15 = *((int *)__cil_tmp14);
2302#line 215
2303 __cil_tmp16 = __cil_tmp15 * 255;
2304#line 215
2305 __cil_tmp17 = __cil_tmp16 / __cil_tmp12;
2306#line 215
2307 pwm = (u8 )__cil_tmp17;
2308#line 217
2309 __cil_tmp18 = (int )pwm;
2310#line 217
2311 tmp___0 = sprintf(buf, "%d\n", __cil_tmp18);
2312 }
2313#line 217
2314 return ((ssize_t )tmp___0);
2315}
2316}
2317#line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2318static ssize_t set_pwm(struct device *dev , struct device_attribute *attr , char const *buf ,
2319 size_t count )
2320{ struct gpio_fan_data *fan_data ;
2321 void *tmp ;
2322 unsigned long pwm ;
2323 int speed_index ;
2324 int ret ;
2325 int tmp___0 ;
2326 struct device const *__cil_tmp11 ;
2327 unsigned long *__cil_tmp12 ;
2328 unsigned long __cil_tmp13 ;
2329 unsigned long __cil_tmp14 ;
2330 unsigned long __cil_tmp15 ;
2331 struct mutex *__cil_tmp16 ;
2332 unsigned long __cil_tmp17 ;
2333 unsigned long __cil_tmp18 ;
2334 bool __cil_tmp19 ;
2335 unsigned long __cil_tmp20 ;
2336 unsigned long __cil_tmp21 ;
2337 int __cil_tmp22 ;
2338 int __cil_tmp23 ;
2339 unsigned long __cil_tmp24 ;
2340 unsigned long *__cil_tmp25 ;
2341 unsigned long __cil_tmp26 ;
2342 unsigned long __cil_tmp27 ;
2343 unsigned long __cil_tmp28 ;
2344 unsigned long __cil_tmp29 ;
2345 unsigned long __cil_tmp30 ;
2346 unsigned long __cil_tmp31 ;
2347 unsigned long __cil_tmp32 ;
2348 struct mutex *__cil_tmp33 ;
2349
2350 {
2351 {
2352#line 223
2353 __cil_tmp11 = (struct device const *)dev;
2354#line 223
2355 tmp = dev_get_drvdata(__cil_tmp11);
2356#line 223
2357 fan_data = (struct gpio_fan_data *)tmp;
2358#line 226
2359 ret = (int )count;
2360#line 228
2361 tmp___0 = (int )kstrtoul(buf, 10U, & pwm);
2362 }
2363#line 228
2364 if (tmp___0) {
2365#line 229
2366 return ((ssize_t )-22);
2367 } else {
2368 {
2369#line 228
2370 __cil_tmp12 = & pwm;
2371#line 228
2372 __cil_tmp13 = *__cil_tmp12;
2373#line 228
2374 if (__cil_tmp13 > 255UL) {
2375#line 229
2376 return ((ssize_t )-22);
2377 } else {
2378
2379 }
2380 }
2381 }
2382 {
2383#line 231
2384 __cil_tmp14 = (unsigned long )fan_data;
2385#line 231
2386 __cil_tmp15 = __cil_tmp14 + 16;
2387#line 231
2388 __cil_tmp16 = (struct mutex *)__cil_tmp15;
2389#line 231
2390 mutex_lock(__cil_tmp16);
2391 }
2392 {
2393#line 233
2394 __cil_tmp17 = (unsigned long )fan_data;
2395#line 233
2396 __cil_tmp18 = __cil_tmp17 + 128;
2397#line 233
2398 __cil_tmp19 = *((bool *)__cil_tmp18);
2399#line 233
2400 if (! __cil_tmp19) {
2401#line 234
2402 ret = -1;
2403#line 235
2404 goto exit_unlock;
2405 } else {
2406
2407 }
2408 }
2409 {
2410#line 238
2411 __cil_tmp20 = (unsigned long )fan_data;
2412#line 238
2413 __cil_tmp21 = __cil_tmp20 + 104;
2414#line 238
2415 __cil_tmp22 = *((int *)__cil_tmp21);
2416#line 238
2417 __cil_tmp23 = __cil_tmp22 - 1;
2418#line 238
2419 __cil_tmp24 = (unsigned long )__cil_tmp23;
2420#line 238
2421 __cil_tmp25 = & pwm;
2422#line 238
2423 __cil_tmp26 = *__cil_tmp25;
2424#line 238
2425 __cil_tmp27 = __cil_tmp26 * __cil_tmp24;
2426#line 238
2427 __cil_tmp28 = __cil_tmp27 + 255UL;
2428#line 238
2429 __cil_tmp29 = __cil_tmp28 - 1UL;
2430#line 238
2431 __cil_tmp30 = __cil_tmp29 / 255UL;
2432#line 238
2433 speed_index = (int )__cil_tmp30;
2434#line 239
2435 set_fan_speed(fan_data, speed_index);
2436 }
2437 exit_unlock:
2438 {
2439#line 242
2440 __cil_tmp31 = (unsigned long )fan_data;
2441#line 242
2442 __cil_tmp32 = __cil_tmp31 + 16;
2443#line 242
2444 __cil_tmp33 = (struct mutex *)__cil_tmp32;
2445#line 242
2446 mutex_unlock(__cil_tmp33);
2447 }
2448#line 244
2449 return ((ssize_t )ret);
2450}
2451}
2452#line 247 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2453static ssize_t show_pwm_enable(struct device *dev , struct device_attribute *attr ,
2454 char *buf )
2455{ struct gpio_fan_data *fan_data ;
2456 void *tmp ;
2457 int tmp___0 ;
2458 struct device const *__cil_tmp7 ;
2459 unsigned long __cil_tmp8 ;
2460 unsigned long __cil_tmp9 ;
2461 bool __cil_tmp10 ;
2462 int __cil_tmp11 ;
2463
2464 {
2465 {
2466#line 250
2467 __cil_tmp7 = (struct device const *)dev;
2468#line 250
2469 tmp = dev_get_drvdata(__cil_tmp7);
2470#line 250
2471 fan_data = (struct gpio_fan_data *)tmp;
2472#line 252
2473 __cil_tmp8 = (unsigned long )fan_data;
2474#line 252
2475 __cil_tmp9 = __cil_tmp8 + 128;
2476#line 252
2477 __cil_tmp10 = *((bool *)__cil_tmp9);
2478#line 252
2479 __cil_tmp11 = (int )__cil_tmp10;
2480#line 252
2481 tmp___0 = sprintf(buf, "%d\n", __cil_tmp11);
2482 }
2483#line 252
2484 return ((ssize_t )tmp___0);
2485}
2486}
2487#line 255 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2488static ssize_t set_pwm_enable(struct device *dev , struct device_attribute *attr ,
2489 char const *buf , size_t count )
2490{ struct gpio_fan_data *fan_data ;
2491 void *tmp ;
2492 unsigned long val ;
2493 int tmp___0 ;
2494 struct device const *__cil_tmp9 ;
2495 unsigned long *__cil_tmp10 ;
2496 unsigned long __cil_tmp11 ;
2497 unsigned long *__cil_tmp12 ;
2498 unsigned long __cil_tmp13 ;
2499 unsigned long __cil_tmp14 ;
2500 unsigned long __cil_tmp15 ;
2501 bool __cil_tmp16 ;
2502 unsigned long __cil_tmp17 ;
2503 unsigned long __cil_tmp18 ;
2504 unsigned long __cil_tmp19 ;
2505 struct mutex *__cil_tmp20 ;
2506 unsigned long __cil_tmp21 ;
2507 unsigned long __cil_tmp22 ;
2508 unsigned long *__cil_tmp23 ;
2509 unsigned long __cil_tmp24 ;
2510 unsigned long *__cil_tmp25 ;
2511 unsigned long __cil_tmp26 ;
2512 unsigned long __cil_tmp27 ;
2513 unsigned long __cil_tmp28 ;
2514 int __cil_tmp29 ;
2515 int __cil_tmp30 ;
2516 unsigned long __cil_tmp31 ;
2517 unsigned long __cil_tmp32 ;
2518 struct mutex *__cil_tmp33 ;
2519
2520 {
2521 {
2522#line 258
2523 __cil_tmp9 = (struct device const *)dev;
2524#line 258
2525 tmp = dev_get_drvdata(__cil_tmp9);
2526#line 258
2527 fan_data = (struct gpio_fan_data *)tmp;
2528#line 261
2529 tmp___0 = (int )kstrtoul(buf, 10U, & val);
2530 }
2531#line 261
2532 if (tmp___0) {
2533#line 262
2534 return ((ssize_t )-22);
2535 } else {
2536 {
2537#line 261
2538 __cil_tmp10 = & val;
2539#line 261
2540 __cil_tmp11 = *__cil_tmp10;
2541#line 261
2542 if (__cil_tmp11 > 1UL) {
2543#line 262
2544 return ((ssize_t )-22);
2545 } else {
2546
2547 }
2548 }
2549 }
2550 {
2551#line 264
2552 __cil_tmp12 = & val;
2553#line 264
2554 __cil_tmp13 = *__cil_tmp12;
2555#line 264
2556 __cil_tmp14 = (unsigned long )fan_data;
2557#line 264
2558 __cil_tmp15 = __cil_tmp14 + 128;
2559#line 264
2560 __cil_tmp16 = *((bool *)__cil_tmp15);
2561#line 264
2562 __cil_tmp17 = (unsigned long )__cil_tmp16;
2563#line 264
2564 if (__cil_tmp17 == __cil_tmp13) {
2565#line 265
2566 return ((ssize_t )count);
2567 } else {
2568
2569 }
2570 }
2571 {
2572#line 267
2573 __cil_tmp18 = (unsigned long )fan_data;
2574#line 267
2575 __cil_tmp19 = __cil_tmp18 + 16;
2576#line 267
2577 __cil_tmp20 = (struct mutex *)__cil_tmp19;
2578#line 267
2579 mutex_lock(__cil_tmp20);
2580#line 269
2581 __cil_tmp21 = (unsigned long )fan_data;
2582#line 269
2583 __cil_tmp22 = __cil_tmp21 + 128;
2584#line 269
2585 __cil_tmp23 = & val;
2586#line 269
2587 __cil_tmp24 = *__cil_tmp23;
2588#line 269
2589 *((bool *)__cil_tmp22) = (bool )__cil_tmp24;
2590 }
2591 {
2592#line 272
2593 __cil_tmp25 = & val;
2594#line 272
2595 __cil_tmp26 = *__cil_tmp25;
2596#line 272
2597 if (__cil_tmp26 == 0UL) {
2598 {
2599#line 273
2600 __cil_tmp27 = (unsigned long )fan_data;
2601#line 273
2602 __cil_tmp28 = __cil_tmp27 + 104;
2603#line 273
2604 __cil_tmp29 = *((int *)__cil_tmp28);
2605#line 273
2606 __cil_tmp30 = __cil_tmp29 - 1;
2607#line 273
2608 set_fan_speed(fan_data, __cil_tmp30);
2609 }
2610 } else {
2611
2612 }
2613 }
2614 {
2615#line 275
2616 __cil_tmp31 = (unsigned long )fan_data;
2617#line 275
2618 __cil_tmp32 = __cil_tmp31 + 16;
2619#line 275
2620 __cil_tmp33 = (struct mutex *)__cil_tmp32;
2621#line 275
2622 mutex_unlock(__cil_tmp33);
2623 }
2624#line 277
2625 return ((ssize_t )count);
2626}
2627}
2628#line 280 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2629static ssize_t show_pwm_mode(struct device *dev , struct device_attribute *attr ,
2630 char *buf )
2631{ int tmp ;
2632
2633 {
2634 {
2635#line 283
2636 tmp = sprintf(buf, "0\n");
2637 }
2638#line 283
2639 return ((ssize_t )tmp);
2640}
2641}
2642#line 286 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2643static ssize_t show_rpm_min(struct device *dev , struct device_attribute *attr , char *buf )
2644{ struct gpio_fan_data *fan_data ;
2645 void *tmp ;
2646 int tmp___0 ;
2647 struct device const *__cil_tmp7 ;
2648 unsigned long __cil_tmp8 ;
2649 unsigned long __cil_tmp9 ;
2650 struct gpio_fan_speed *__cil_tmp10 ;
2651 struct gpio_fan_speed *__cil_tmp11 ;
2652 int __cil_tmp12 ;
2653
2654 {
2655 {
2656#line 289
2657 __cil_tmp7 = (struct device const *)dev;
2658#line 289
2659 tmp = dev_get_drvdata(__cil_tmp7);
2660#line 289
2661 fan_data = (struct gpio_fan_data *)tmp;
2662#line 291
2663 __cil_tmp8 = (unsigned long )fan_data;
2664#line 291
2665 __cil_tmp9 = __cil_tmp8 + 112;
2666#line 291
2667 __cil_tmp10 = *((struct gpio_fan_speed **)__cil_tmp9);
2668#line 291
2669 __cil_tmp11 = __cil_tmp10 + 0;
2670#line 291
2671 __cil_tmp12 = *((int *)__cil_tmp11);
2672#line 291
2673 tmp___0 = sprintf(buf, "%d\n", __cil_tmp12);
2674 }
2675#line 291
2676 return ((ssize_t )tmp___0);
2677}
2678}
2679#line 294 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2680static ssize_t show_rpm_max(struct device *dev , struct device_attribute *attr , char *buf )
2681{ struct gpio_fan_data *fan_data ;
2682 void *tmp ;
2683 int tmp___0 ;
2684 struct device const *__cil_tmp7 ;
2685 unsigned long __cil_tmp8 ;
2686 unsigned long __cil_tmp9 ;
2687 int __cil_tmp10 ;
2688 int __cil_tmp11 ;
2689 unsigned long __cil_tmp12 ;
2690 unsigned long __cil_tmp13 ;
2691 struct gpio_fan_speed *__cil_tmp14 ;
2692 struct gpio_fan_speed *__cil_tmp15 ;
2693 int __cil_tmp16 ;
2694
2695 {
2696 {
2697#line 297
2698 __cil_tmp7 = (struct device const *)dev;
2699#line 297
2700 tmp = dev_get_drvdata(__cil_tmp7);
2701#line 297
2702 fan_data = (struct gpio_fan_data *)tmp;
2703#line 299
2704 __cil_tmp8 = (unsigned long )fan_data;
2705#line 299
2706 __cil_tmp9 = __cil_tmp8 + 104;
2707#line 299
2708 __cil_tmp10 = *((int *)__cil_tmp9);
2709#line 299
2710 __cil_tmp11 = __cil_tmp10 - 1;
2711#line 299
2712 __cil_tmp12 = (unsigned long )fan_data;
2713#line 299
2714 __cil_tmp13 = __cil_tmp12 + 112;
2715#line 299
2716 __cil_tmp14 = *((struct gpio_fan_speed **)__cil_tmp13);
2717#line 299
2718 __cil_tmp15 = __cil_tmp14 + __cil_tmp11;
2719#line 299
2720 __cil_tmp16 = *((int *)__cil_tmp15);
2721#line 299
2722 tmp___0 = sprintf(buf, "%d\n", __cil_tmp16);
2723 }
2724#line 299
2725 return ((ssize_t )tmp___0);
2726}
2727}
2728#line 303 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2729static ssize_t show_rpm(struct device *dev , struct device_attribute *attr , char *buf )
2730{ struct gpio_fan_data *fan_data ;
2731 void *tmp ;
2732 int tmp___0 ;
2733 struct device const *__cil_tmp7 ;
2734 unsigned long __cil_tmp8 ;
2735 unsigned long __cil_tmp9 ;
2736 int __cil_tmp10 ;
2737 unsigned long __cil_tmp11 ;
2738 unsigned long __cil_tmp12 ;
2739 struct gpio_fan_speed *__cil_tmp13 ;
2740 struct gpio_fan_speed *__cil_tmp14 ;
2741 int __cil_tmp15 ;
2742
2743 {
2744 {
2745#line 306
2746 __cil_tmp7 = (struct device const *)dev;
2747#line 306
2748 tmp = dev_get_drvdata(__cil_tmp7);
2749#line 306
2750 fan_data = (struct gpio_fan_data *)tmp;
2751#line 308
2752 __cil_tmp8 = (unsigned long )fan_data;
2753#line 308
2754 __cil_tmp9 = __cil_tmp8 + 120;
2755#line 308
2756 __cil_tmp10 = *((int *)__cil_tmp9);
2757#line 308
2758 __cil_tmp11 = (unsigned long )fan_data;
2759#line 308
2760 __cil_tmp12 = __cil_tmp11 + 112;
2761#line 308
2762 __cil_tmp13 = *((struct gpio_fan_speed **)__cil_tmp12);
2763#line 308
2764 __cil_tmp14 = __cil_tmp13 + __cil_tmp10;
2765#line 308
2766 __cil_tmp15 = *((int *)__cil_tmp14);
2767#line 308
2768 tmp___0 = sprintf(buf, "%d\n", __cil_tmp15);
2769 }
2770#line 308
2771 return ((ssize_t )tmp___0);
2772}
2773}
2774#line 311 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2775static ssize_t set_rpm(struct device *dev , struct device_attribute *attr , char const *buf ,
2776 size_t count )
2777{ struct gpio_fan_data *fan_data ;
2778 void *tmp ;
2779 unsigned long rpm ;
2780 int ret ;
2781 int tmp___0 ;
2782 int tmp___1 ;
2783 struct device const *__cil_tmp11 ;
2784 unsigned long __cil_tmp12 ;
2785 unsigned long __cil_tmp13 ;
2786 struct mutex *__cil_tmp14 ;
2787 unsigned long __cil_tmp15 ;
2788 unsigned long __cil_tmp16 ;
2789 bool __cil_tmp17 ;
2790 unsigned long *__cil_tmp18 ;
2791 unsigned long __cil_tmp19 ;
2792 int __cil_tmp20 ;
2793 unsigned long __cil_tmp21 ;
2794 unsigned long __cil_tmp22 ;
2795 struct mutex *__cil_tmp23 ;
2796
2797 {
2798 {
2799#line 314
2800 __cil_tmp11 = (struct device const *)dev;
2801#line 314
2802 tmp = dev_get_drvdata(__cil_tmp11);
2803#line 314
2804 fan_data = (struct gpio_fan_data *)tmp;
2805#line 316
2806 ret = (int )count;
2807#line 318
2808 tmp___0 = (int )kstrtoul(buf, 10U, & rpm);
2809 }
2810#line 318
2811 if (tmp___0) {
2812#line 319
2813 return ((ssize_t )-22);
2814 } else {
2815
2816 }
2817 {
2818#line 321
2819 __cil_tmp12 = (unsigned long )fan_data;
2820#line 321
2821 __cil_tmp13 = __cil_tmp12 + 16;
2822#line 321
2823 __cil_tmp14 = (struct mutex *)__cil_tmp13;
2824#line 321
2825 mutex_lock(__cil_tmp14);
2826 }
2827 {
2828#line 323
2829 __cil_tmp15 = (unsigned long )fan_data;
2830#line 323
2831 __cil_tmp16 = __cil_tmp15 + 128;
2832#line 323
2833 __cil_tmp17 = *((bool *)__cil_tmp16);
2834#line 323
2835 if (! __cil_tmp17) {
2836#line 324
2837 ret = -1;
2838#line 325
2839 goto exit_unlock;
2840 } else {
2841
2842 }
2843 }
2844 {
2845#line 328
2846 __cil_tmp18 = & rpm;
2847#line 328
2848 __cil_tmp19 = *__cil_tmp18;
2849#line 328
2850 __cil_tmp20 = (int )__cil_tmp19;
2851#line 328
2852 tmp___1 = rpm_to_speed_index(fan_data, __cil_tmp20);
2853#line 328
2854 set_fan_speed(fan_data, tmp___1);
2855 }
2856 exit_unlock:
2857 {
2858#line 331
2859 __cil_tmp21 = (unsigned long )fan_data;
2860#line 331
2861 __cil_tmp22 = __cil_tmp21 + 16;
2862#line 331
2863 __cil_tmp23 = (struct mutex *)__cil_tmp22;
2864#line 331
2865 mutex_unlock(__cil_tmp23);
2866 }
2867#line 333
2868 return ((ssize_t )ret);
2869}
2870}
2871#line 336 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2872static struct device_attribute dev_attr_pwm1 = {{"pwm1", (umode_t )420}, & show_pwm, & set_pwm};
2873#line 337 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2874static struct device_attribute dev_attr_pwm1_enable = {{"pwm1_enable", (umode_t )420}, & show_pwm_enable, & set_pwm_enable};
2875#line 339 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2876static struct device_attribute dev_attr_pwm1_mode = {{"pwm1_mode", (umode_t )292}, & show_pwm_mode, (ssize_t (*)(struct device *dev ,
2877 struct device_attribute *attr ,
2878 char const *buf ,
2879 size_t count ))((void *)0)};
2880#line 340 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2881static struct device_attribute dev_attr_fan1_min = {{"fan1_min", (umode_t )292}, & show_rpm_min, (ssize_t (*)(struct device *dev ,
2882 struct device_attribute *attr ,
2883 char const *buf ,
2884 size_t count ))((void *)0)};
2885#line 341 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2886static struct device_attribute dev_attr_fan1_max = {{"fan1_max", (umode_t )292}, & show_rpm_max, (ssize_t (*)(struct device *dev ,
2887 struct device_attribute *attr ,
2888 char const *buf ,
2889 size_t count ))((void *)0)};
2890#line 342 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2891static struct device_attribute dev_attr_fan1_input = {{"fan1_input", (umode_t )292}, & show_rpm, (ssize_t (*)(struct device *dev , struct device_attribute *attr ,
2892 char const *buf , size_t count ))((void *)0)};
2893#line 343 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2894static struct device_attribute dev_attr_fan1_target = {{"fan1_target", (umode_t )420}, & show_rpm, & set_rpm};
2895#line 345 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2896static struct attribute *gpio_fan_ctrl_attributes[8] =
2897#line 345
2898 { & dev_attr_pwm1.attr, & dev_attr_pwm1_enable.attr, & dev_attr_pwm1_mode.attr, & dev_attr_fan1_input.attr,
2899 & dev_attr_fan1_target.attr, & dev_attr_fan1_min.attr, & dev_attr_fan1_max.attr, (struct attribute *)((void *)0)};
2900#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2901static struct attribute_group const gpio_fan_ctrl_group = {(char const *)0, (umode_t (*)(struct kobject * , struct attribute * , int ))0,
2902 gpio_fan_ctrl_attributes};
2903#line 360 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
2904static int fan_ctrl_init(struct gpio_fan_data *fan_data , struct gpio_fan_platform_data *pdata )
2905{ struct platform_device *pdev ;
2906 int num_ctrl ;
2907 unsigned int *ctrl ;
2908 int i ;
2909 int err ;
2910 int tmp ;
2911 unsigned long __cil_tmp9 ;
2912 unsigned long __cil_tmp10 ;
2913 unsigned int *__cil_tmp11 ;
2914 unsigned int __cil_tmp12 ;
2915 unsigned int *__cil_tmp13 ;
2916 unsigned int __cil_tmp14 ;
2917 unsigned int *__cil_tmp15 ;
2918 unsigned int __cil_tmp16 ;
2919 unsigned int *__cil_tmp17 ;
2920 unsigned int __cil_tmp18 ;
2921 unsigned long __cil_tmp19 ;
2922 unsigned long __cil_tmp20 ;
2923 unsigned long __cil_tmp21 ;
2924 unsigned long __cil_tmp22 ;
2925 unsigned long __cil_tmp23 ;
2926 unsigned long __cil_tmp24 ;
2927 unsigned long __cil_tmp25 ;
2928 unsigned long __cil_tmp26 ;
2929 unsigned long __cil_tmp27 ;
2930 unsigned long __cil_tmp28 ;
2931 unsigned long __cil_tmp29 ;
2932 unsigned long __cil_tmp30 ;
2933 unsigned long __cil_tmp31 ;
2934 unsigned long __cil_tmp32 ;
2935 unsigned long __cil_tmp33 ;
2936 unsigned long __cil_tmp34 ;
2937 unsigned long __cil_tmp35 ;
2938 unsigned long __cil_tmp36 ;
2939 int __cil_tmp37 ;
2940 unsigned long __cil_tmp38 ;
2941 unsigned long __cil_tmp39 ;
2942 unsigned long __cil_tmp40 ;
2943 struct kobject *__cil_tmp41 ;
2944 unsigned int *__cil_tmp42 ;
2945 unsigned int __cil_tmp43 ;
2946
2947 {
2948#line 363
2949 pdev = *((struct platform_device **)fan_data);
2950#line 364
2951 num_ctrl = *((int *)pdata);
2952#line 365
2953 __cil_tmp9 = (unsigned long )pdata;
2954#line 365
2955 __cil_tmp10 = __cil_tmp9 + 8;
2956#line 365
2957 ctrl = *((unsigned int **)__cil_tmp10);
2958#line 368
2959 i = 0;
2960 {
2961#line 368
2962 while (1) {
2963 while_continue: ;
2964#line 368
2965 if (i < num_ctrl) {
2966
2967 } else {
2968#line 368
2969 goto while_break;
2970 }
2971 {
2972#line 369
2973 __cil_tmp11 = ctrl + i;
2974#line 369
2975 __cil_tmp12 = *__cil_tmp11;
2976#line 369
2977 err = gpio_request(__cil_tmp12, "GPIO fan control");
2978 }
2979#line 370
2980 if (err) {
2981#line 371
2982 goto err_free_gpio;
2983 } else {
2984
2985 }
2986 {
2987#line 373
2988 __cil_tmp13 = ctrl + i;
2989#line 373
2990 __cil_tmp14 = *__cil_tmp13;
2991#line 373
2992 tmp = gpio_get_value(__cil_tmp14);
2993#line 373
2994 __cil_tmp15 = ctrl + i;
2995#line 373
2996 __cil_tmp16 = *__cil_tmp15;
2997#line 373
2998 err = gpio_direction_output(__cil_tmp16, tmp);
2999 }
3000#line 374
3001 if (err) {
3002 {
3003#line 375
3004 __cil_tmp17 = ctrl + i;
3005#line 375
3006 __cil_tmp18 = *__cil_tmp17;
3007#line 375
3008 gpio_free(__cil_tmp18);
3009 }
3010#line 376
3011 goto err_free_gpio;
3012 } else {
3013
3014 }
3015#line 368
3016 i = i + 1;
3017 }
3018 while_break: ;
3019 }
3020 {
3021#line 380
3022 __cil_tmp19 = (unsigned long )fan_data;
3023#line 380
3024 __cil_tmp20 = __cil_tmp19 + 88;
3025#line 380
3026 *((int *)__cil_tmp20) = num_ctrl;
3027#line 381
3028 __cil_tmp21 = (unsigned long )fan_data;
3029#line 381
3030 __cil_tmp22 = __cil_tmp21 + 96;
3031#line 381
3032 *((unsigned int **)__cil_tmp22) = ctrl;
3033#line 382
3034 __cil_tmp23 = (unsigned long )fan_data;
3035#line 382
3036 __cil_tmp24 = __cil_tmp23 + 104;
3037#line 382
3038 __cil_tmp25 = (unsigned long )pdata;
3039#line 382
3040 __cil_tmp26 = __cil_tmp25 + 24;
3041#line 382
3042 *((int *)__cil_tmp24) = *((int *)__cil_tmp26);
3043#line 383
3044 __cil_tmp27 = (unsigned long )fan_data;
3045#line 383
3046 __cil_tmp28 = __cil_tmp27 + 112;
3047#line 383
3048 __cil_tmp29 = (unsigned long )pdata;
3049#line 383
3050 __cil_tmp30 = __cil_tmp29 + 32;
3051#line 383
3052 *((struct gpio_fan_speed **)__cil_tmp28) = *((struct gpio_fan_speed **)__cil_tmp30);
3053#line 384
3054 __cil_tmp31 = (unsigned long )fan_data;
3055#line 384
3056 __cil_tmp32 = __cil_tmp31 + 128;
3057#line 384
3058 *((bool *)__cil_tmp32) = (bool )1;
3059#line 385
3060 __cil_tmp33 = (unsigned long )fan_data;
3061#line 385
3062 __cil_tmp34 = __cil_tmp33 + 120;
3063#line 385
3064 *((int *)__cil_tmp34) = get_fan_speed_index(fan_data);
3065 }
3066 {
3067#line 386
3068 __cil_tmp35 = (unsigned long )fan_data;
3069#line 386
3070 __cil_tmp36 = __cil_tmp35 + 120;
3071#line 386
3072 __cil_tmp37 = *((int *)__cil_tmp36);
3073#line 386
3074 if (__cil_tmp37 < 0) {
3075#line 387
3076 err = -19;
3077#line 388
3078 goto err_free_gpio;
3079 } else {
3080
3081 }
3082 }
3083 {
3084#line 391
3085 __cil_tmp38 = 16 + 16;
3086#line 391
3087 __cil_tmp39 = (unsigned long )pdev;
3088#line 391
3089 __cil_tmp40 = __cil_tmp39 + __cil_tmp38;
3090#line 391
3091 __cil_tmp41 = (struct kobject *)__cil_tmp40;
3092#line 391
3093 err = (int )sysfs_create_group(__cil_tmp41, & gpio_fan_ctrl_group);
3094 }
3095#line 392
3096 if (err) {
3097#line 393
3098 goto err_free_gpio;
3099 } else {
3100
3101 }
3102#line 395
3103 return (0);
3104 err_free_gpio:
3105#line 398
3106 i = i - 1;
3107 {
3108#line 398
3109 while (1) {
3110 while_continue___0: ;
3111#line 398
3112 if (i >= 0) {
3113
3114 } else {
3115#line 398
3116 goto while_break___0;
3117 }
3118 {
3119#line 399
3120 __cil_tmp42 = ctrl + i;
3121#line 399
3122 __cil_tmp43 = *__cil_tmp42;
3123#line 399
3124 gpio_free(__cil_tmp43);
3125#line 398
3126 i = i - 1;
3127 }
3128 }
3129 while_break___0: ;
3130 }
3131#line 401
3132 return (err);
3133}
3134}
3135#line 404 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3136static void fan_ctrl_free(struct gpio_fan_data *fan_data )
3137{ struct platform_device *pdev ;
3138 int i ;
3139 unsigned long __cil_tmp4 ;
3140 unsigned long __cil_tmp5 ;
3141 unsigned long __cil_tmp6 ;
3142 struct kobject *__cil_tmp7 ;
3143 unsigned long __cil_tmp8 ;
3144 unsigned long __cil_tmp9 ;
3145 int __cil_tmp10 ;
3146 unsigned long __cil_tmp11 ;
3147 unsigned long __cil_tmp12 ;
3148 unsigned int *__cil_tmp13 ;
3149 unsigned int *__cil_tmp14 ;
3150 unsigned int __cil_tmp15 ;
3151
3152 {
3153 {
3154#line 406
3155 pdev = *((struct platform_device **)fan_data);
3156#line 409
3157 __cil_tmp4 = 16 + 16;
3158#line 409
3159 __cil_tmp5 = (unsigned long )pdev;
3160#line 409
3161 __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
3162#line 409
3163 __cil_tmp7 = (struct kobject *)__cil_tmp6;
3164#line 409
3165 sysfs_remove_group(__cil_tmp7, & gpio_fan_ctrl_group);
3166#line 410
3167 i = 0;
3168 }
3169 {
3170#line 410
3171 while (1) {
3172 while_continue: ;
3173 {
3174#line 410
3175 __cil_tmp8 = (unsigned long )fan_data;
3176#line 410
3177 __cil_tmp9 = __cil_tmp8 + 88;
3178#line 410
3179 __cil_tmp10 = *((int *)__cil_tmp9);
3180#line 410
3181 if (i < __cil_tmp10) {
3182
3183 } else {
3184#line 410
3185 goto while_break;
3186 }
3187 }
3188 {
3189#line 411
3190 __cil_tmp11 = (unsigned long )fan_data;
3191#line 411
3192 __cil_tmp12 = __cil_tmp11 + 96;
3193#line 411
3194 __cil_tmp13 = *((unsigned int **)__cil_tmp12);
3195#line 411
3196 __cil_tmp14 = __cil_tmp13 + i;
3197#line 411
3198 __cil_tmp15 = *__cil_tmp14;
3199#line 411
3200 gpio_free(__cil_tmp15);
3201#line 410
3202 i = i + 1;
3203 }
3204 }
3205 while_break: ;
3206 }
3207#line 412
3208 return;
3209}
3210}
3211#line 418 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3212static ssize_t show_name(struct device *dev , struct device_attribute *attr , char *buf )
3213{ int tmp ;
3214
3215 {
3216 {
3217#line 421
3218 tmp = sprintf(buf, "gpio-fan\n");
3219 }
3220#line 421
3221 return ((ssize_t )tmp);
3222}
3223}
3224#line 424 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3225static struct device_attribute dev_attr_name = {{"name", (umode_t )292}, & show_name, (ssize_t (*)(struct device *dev , struct device_attribute *attr ,
3226 char const *buf , size_t count ))((void *)0)};
3227#line 441 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3228static struct lock_class_key __key___2 ;
3229#line 426
3230static int gpio_fan_probe(struct platform_device *pdev ) __attribute__((__section__(".devinit.text"),
3231__no_instrument_function__)) ;
3232#line 426 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3233static int gpio_fan_probe(struct platform_device *pdev )
3234{ int err ;
3235 struct gpio_fan_data *fan_data ;
3236 struct gpio_fan_platform_data *pdata ;
3237 void *tmp ;
3238 long tmp___0 ;
3239 long tmp___1 ;
3240 unsigned long __cil_tmp8 ;
3241 unsigned long __cil_tmp9 ;
3242 unsigned long __cil_tmp10 ;
3243 void *__cil_tmp11 ;
3244 void *__cil_tmp12 ;
3245 unsigned long __cil_tmp13 ;
3246 unsigned long __cil_tmp14 ;
3247 struct mutex *__cil_tmp15 ;
3248 unsigned long __cil_tmp16 ;
3249 unsigned long __cil_tmp17 ;
3250 unsigned long __cil_tmp18 ;
3251 unsigned long __cil_tmp19 ;
3252 struct gpio_fan_alarm *__cil_tmp20 ;
3253 unsigned long __cil_tmp21 ;
3254 unsigned long __cil_tmp22 ;
3255 int __cil_tmp23 ;
3256 unsigned long __cil_tmp24 ;
3257 unsigned long __cil_tmp25 ;
3258 struct gpio_fan_speed *__cil_tmp26 ;
3259 unsigned long __cil_tmp27 ;
3260 unsigned long __cil_tmp28 ;
3261 int __cil_tmp29 ;
3262 unsigned long __cil_tmp30 ;
3263 unsigned long __cil_tmp31 ;
3264 struct device *__cil_tmp32 ;
3265 struct device_attribute const *__cil_tmp33 ;
3266 unsigned long __cil_tmp34 ;
3267 unsigned long __cil_tmp35 ;
3268 unsigned long __cil_tmp36 ;
3269 unsigned long __cil_tmp37 ;
3270 struct device *__cil_tmp38 ;
3271 unsigned long __cil_tmp39 ;
3272 unsigned long __cil_tmp40 ;
3273 struct device *__cil_tmp41 ;
3274 void const *__cil_tmp42 ;
3275 unsigned long __cil_tmp43 ;
3276 unsigned long __cil_tmp44 ;
3277 struct device *__cil_tmp45 ;
3278 void const *__cil_tmp46 ;
3279 unsigned long __cil_tmp47 ;
3280 unsigned long __cil_tmp48 ;
3281 struct device *__cil_tmp49 ;
3282 struct device const *__cil_tmp50 ;
3283 unsigned long __cil_tmp51 ;
3284 unsigned long __cil_tmp52 ;
3285 struct device *__cil_tmp53 ;
3286 struct device_attribute const *__cil_tmp54 ;
3287 unsigned long __cil_tmp55 ;
3288 unsigned long __cil_tmp56 ;
3289 unsigned long __cil_tmp57 ;
3290 unsigned long __cil_tmp58 ;
3291 void *__cil_tmp59 ;
3292 void const *__cil_tmp60 ;
3293
3294 {
3295#line 430
3296 __cil_tmp8 = 16 + 184;
3297#line 430
3298 __cil_tmp9 = (unsigned long )pdev;
3299#line 430
3300 __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
3301#line 430
3302 __cil_tmp11 = *((void **)__cil_tmp10);
3303#line 430
3304 pdata = (struct gpio_fan_platform_data *)__cil_tmp11;
3305#line 432
3306 if (! pdata) {
3307#line 433
3308 return (-22);
3309 } else {
3310
3311 }
3312 {
3313#line 435
3314 tmp = kzalloc(176UL, 208U);
3315#line 435
3316 fan_data = (struct gpio_fan_data *)tmp;
3317 }
3318#line 436
3319 if (! fan_data) {
3320#line 437
3321 return (-12);
3322 } else {
3323
3324 }
3325 {
3326#line 439
3327 *((struct platform_device **)fan_data) = pdev;
3328#line 440
3329 __cil_tmp12 = (void *)fan_data;
3330#line 440
3331 platform_set_drvdata(pdev, __cil_tmp12);
3332 }
3333 {
3334#line 441
3335 while (1) {
3336 while_continue: ;
3337 {
3338#line 441
3339 __cil_tmp13 = (unsigned long )fan_data;
3340#line 441
3341 __cil_tmp14 = __cil_tmp13 + 16;
3342#line 441
3343 __cil_tmp15 = (struct mutex *)__cil_tmp14;
3344#line 441
3345 __mutex_init(__cil_tmp15, "&fan_data->lock", & __key___2);
3346 }
3347#line 441
3348 goto while_break;
3349 }
3350 while_break: ;
3351 }
3352 {
3353#line 444
3354 __cil_tmp16 = (unsigned long )pdata;
3355#line 444
3356 __cil_tmp17 = __cil_tmp16 + 16;
3357#line 444
3358 if (*((struct gpio_fan_alarm **)__cil_tmp17)) {
3359 {
3360#line 445
3361 __cil_tmp18 = (unsigned long )pdata;
3362#line 445
3363 __cil_tmp19 = __cil_tmp18 + 16;
3364#line 445
3365 __cil_tmp20 = *((struct gpio_fan_alarm **)__cil_tmp19);
3366#line 445
3367 err = fan_alarm_init(fan_data, __cil_tmp20);
3368 }
3369#line 446
3370 if (err) {
3371#line 447
3372 goto err_free_data;
3373 } else {
3374
3375 }
3376 } else {
3377
3378 }
3379 }
3380 {
3381#line 451
3382 __cil_tmp21 = (unsigned long )pdata;
3383#line 451
3384 __cil_tmp22 = __cil_tmp21 + 8;
3385#line 451
3386 if (*((unsigned int **)__cil_tmp22)) {
3387 {
3388#line 451
3389 __cil_tmp23 = *((int *)pdata);
3390#line 451
3391 if (__cil_tmp23 > 0) {
3392 {
3393#line 452
3394 __cil_tmp24 = (unsigned long )pdata;
3395#line 452
3396 __cil_tmp25 = __cil_tmp24 + 32;
3397#line 452
3398 __cil_tmp26 = *((struct gpio_fan_speed **)__cil_tmp25);
3399#line 452
3400 if (! __cil_tmp26) {
3401#line 453
3402 err = -22;
3403#line 454
3404 goto err_free_alarm;
3405 } else {
3406 {
3407#line 452
3408 __cil_tmp27 = (unsigned long )pdata;
3409#line 452
3410 __cil_tmp28 = __cil_tmp27 + 24;
3411#line 452
3412 __cil_tmp29 = *((int *)__cil_tmp28);
3413#line 452
3414 if (__cil_tmp29 <= 1) {
3415#line 453
3416 err = -22;
3417#line 454
3418 goto err_free_alarm;
3419 } else {
3420
3421 }
3422 }
3423 }
3424 }
3425 {
3426#line 456
3427 err = fan_ctrl_init(fan_data, pdata);
3428 }
3429#line 457
3430 if (err) {
3431#line 458
3432 goto err_free_alarm;
3433 } else {
3434
3435 }
3436 } else {
3437
3438 }
3439 }
3440 } else {
3441
3442 }
3443 }
3444 {
3445#line 461
3446 __cil_tmp30 = (unsigned long )pdev;
3447#line 461
3448 __cil_tmp31 = __cil_tmp30 + 16;
3449#line 461
3450 __cil_tmp32 = (struct device *)__cil_tmp31;
3451#line 461
3452 __cil_tmp33 = (struct device_attribute const *)(& dev_attr_name);
3453#line 461
3454 err = device_create_file(__cil_tmp32, __cil_tmp33);
3455 }
3456#line 462
3457 if (err) {
3458#line 463
3459 goto err_free_ctrl;
3460 } else {
3461
3462 }
3463 {
3464#line 466
3465 __cil_tmp34 = (unsigned long )fan_data;
3466#line 466
3467 __cil_tmp35 = __cil_tmp34 + 8;
3468#line 466
3469 __cil_tmp36 = (unsigned long )pdev;
3470#line 466
3471 __cil_tmp37 = __cil_tmp36 + 16;
3472#line 466
3473 __cil_tmp38 = (struct device *)__cil_tmp37;
3474#line 466
3475 *((struct device **)__cil_tmp35) = hwmon_device_register(__cil_tmp38);
3476#line 467
3477 __cil_tmp39 = (unsigned long )fan_data;
3478#line 467
3479 __cil_tmp40 = __cil_tmp39 + 8;
3480#line 467
3481 __cil_tmp41 = *((struct device **)__cil_tmp40);
3482#line 467
3483 __cil_tmp42 = (void const *)__cil_tmp41;
3484#line 467
3485 tmp___1 = (long )IS_ERR(__cil_tmp42);
3486 }
3487#line 467
3488 if (tmp___1) {
3489 {
3490#line 468
3491 __cil_tmp43 = (unsigned long )fan_data;
3492#line 468
3493 __cil_tmp44 = __cil_tmp43 + 8;
3494#line 468
3495 __cil_tmp45 = *((struct device **)__cil_tmp44);
3496#line 468
3497 __cil_tmp46 = (void const *)__cil_tmp45;
3498#line 468
3499 tmp___0 = (long )PTR_ERR(__cil_tmp46);
3500#line 468
3501 err = (int )tmp___0;
3502 }
3503#line 469
3504 goto err_remove_name;
3505 } else {
3506
3507 }
3508 {
3509#line 472
3510 __cil_tmp47 = (unsigned long )pdev;
3511#line 472
3512 __cil_tmp48 = __cil_tmp47 + 16;
3513#line 472
3514 __cil_tmp49 = (struct device *)__cil_tmp48;
3515#line 472
3516 __cil_tmp50 = (struct device const *)__cil_tmp49;
3517#line 472
3518 _dev_info(__cil_tmp50, "GPIO fan initialized\n");
3519 }
3520#line 474
3521 return (0);
3522 err_remove_name:
3523 {
3524#line 477
3525 __cil_tmp51 = (unsigned long )pdev;
3526#line 477
3527 __cil_tmp52 = __cil_tmp51 + 16;
3528#line 477
3529 __cil_tmp53 = (struct device *)__cil_tmp52;
3530#line 477
3531 __cil_tmp54 = (struct device_attribute const *)(& dev_attr_name);
3532#line 477
3533 device_remove_file(__cil_tmp53, __cil_tmp54);
3534 }
3535 err_free_ctrl:
3536 {
3537#line 479
3538 __cil_tmp55 = (unsigned long )fan_data;
3539#line 479
3540 __cil_tmp56 = __cil_tmp55 + 96;
3541#line 479
3542 if (*((unsigned int **)__cil_tmp56)) {
3543 {
3544#line 480
3545 fan_ctrl_free(fan_data);
3546 }
3547 } else {
3548
3549 }
3550 }
3551 err_free_alarm:
3552 {
3553#line 482
3554 __cil_tmp57 = (unsigned long )fan_data;
3555#line 482
3556 __cil_tmp58 = __cil_tmp57 + 136;
3557#line 482
3558 if (*((struct gpio_fan_alarm **)__cil_tmp58)) {
3559 {
3560#line 483
3561 fan_alarm_free(fan_data);
3562 }
3563 } else {
3564
3565 }
3566 }
3567 err_free_data:
3568 {
3569#line 485
3570 __cil_tmp59 = (void *)0;
3571#line 485
3572 platform_set_drvdata(pdev, __cil_tmp59);
3573#line 486
3574 __cil_tmp60 = (void const *)fan_data;
3575#line 486
3576 kfree(__cil_tmp60);
3577 }
3578#line 488
3579 return (err);
3580}
3581}
3582#line 491
3583static int gpio_fan_remove(struct platform_device *pdev ) __attribute__((__section__(".devexit.text"),
3584__no_instrument_function__)) ;
3585#line 491 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3586static int gpio_fan_remove(struct platform_device *pdev )
3587{ struct gpio_fan_data *fan_data ;
3588 void *tmp ;
3589 struct platform_device const *__cil_tmp4 ;
3590 unsigned long __cil_tmp5 ;
3591 unsigned long __cil_tmp6 ;
3592 struct device *__cil_tmp7 ;
3593 unsigned long __cil_tmp8 ;
3594 unsigned long __cil_tmp9 ;
3595 struct device *__cil_tmp10 ;
3596 struct device_attribute const *__cil_tmp11 ;
3597 unsigned long __cil_tmp12 ;
3598 unsigned long __cil_tmp13 ;
3599 unsigned long __cil_tmp14 ;
3600 unsigned long __cil_tmp15 ;
3601 void const *__cil_tmp16 ;
3602
3603 {
3604 {
3605#line 493
3606 __cil_tmp4 = (struct platform_device const *)pdev;
3607#line 493
3608 tmp = platform_get_drvdata(__cil_tmp4);
3609#line 493
3610 fan_data = (struct gpio_fan_data *)tmp;
3611#line 495
3612 __cil_tmp5 = (unsigned long )fan_data;
3613#line 495
3614 __cil_tmp6 = __cil_tmp5 + 8;
3615#line 495
3616 __cil_tmp7 = *((struct device **)__cil_tmp6);
3617#line 495
3618 hwmon_device_unregister(__cil_tmp7);
3619#line 496
3620 __cil_tmp8 = (unsigned long )pdev;
3621#line 496
3622 __cil_tmp9 = __cil_tmp8 + 16;
3623#line 496
3624 __cil_tmp10 = (struct device *)__cil_tmp9;
3625#line 496
3626 __cil_tmp11 = (struct device_attribute const *)(& dev_attr_name);
3627#line 496
3628 device_remove_file(__cil_tmp10, __cil_tmp11);
3629 }
3630 {
3631#line 497
3632 __cil_tmp12 = (unsigned long )fan_data;
3633#line 497
3634 __cil_tmp13 = __cil_tmp12 + 136;
3635#line 497
3636 if (*((struct gpio_fan_alarm **)__cil_tmp13)) {
3637 {
3638#line 498
3639 fan_alarm_free(fan_data);
3640 }
3641 } else {
3642
3643 }
3644 }
3645 {
3646#line 499
3647 __cil_tmp14 = (unsigned long )fan_data;
3648#line 499
3649 __cil_tmp15 = __cil_tmp14 + 96;
3650#line 499
3651 if (*((unsigned int **)__cil_tmp15)) {
3652 {
3653#line 500
3654 fan_ctrl_free(fan_data);
3655 }
3656 } else {
3657
3658 }
3659 }
3660 {
3661#line 501
3662 __cil_tmp16 = (void const *)fan_data;
3663#line 501
3664 kfree(__cil_tmp16);
3665 }
3666#line 503
3667 return (0);
3668}
3669}
3670#line 507 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3671static int gpio_fan_suspend(struct platform_device *pdev , int state_event12 )
3672{ struct gpio_fan_data *fan_data ;
3673 void *tmp ;
3674 struct platform_device const *__cil_tmp5 ;
3675 unsigned long __cil_tmp6 ;
3676 unsigned long __cil_tmp7 ;
3677 unsigned long __cil_tmp8 ;
3678 unsigned long __cil_tmp9 ;
3679 unsigned long __cil_tmp10 ;
3680 unsigned long __cil_tmp11 ;
3681
3682 {
3683 {
3684#line 509
3685 __cil_tmp5 = (struct platform_device const *)pdev;
3686#line 509
3687 tmp = platform_get_drvdata(__cil_tmp5);
3688#line 509
3689 fan_data = (struct gpio_fan_data *)tmp;
3690 }
3691 {
3692#line 511
3693 __cil_tmp6 = (unsigned long )fan_data;
3694#line 511
3695 __cil_tmp7 = __cil_tmp6 + 96;
3696#line 511
3697 if (*((unsigned int **)__cil_tmp7)) {
3698 {
3699#line 512
3700 __cil_tmp8 = (unsigned long )fan_data;
3701#line 512
3702 __cil_tmp9 = __cil_tmp8 + 124;
3703#line 512
3704 __cil_tmp10 = (unsigned long )fan_data;
3705#line 512
3706 __cil_tmp11 = __cil_tmp10 + 120;
3707#line 512
3708 *((int *)__cil_tmp9) = *((int *)__cil_tmp11);
3709#line 513
3710 set_fan_speed(fan_data, 0);
3711 }
3712 } else {
3713
3714 }
3715 }
3716#line 516
3717 return (0);
3718}
3719}
3720#line 519 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3721static int gpio_fan_resume(struct platform_device *pdev )
3722{ struct gpio_fan_data *fan_data ;
3723 void *tmp ;
3724 struct platform_device const *__cil_tmp4 ;
3725 unsigned long __cil_tmp5 ;
3726 unsigned long __cil_tmp6 ;
3727 unsigned long __cil_tmp7 ;
3728 unsigned long __cil_tmp8 ;
3729 int __cil_tmp9 ;
3730
3731 {
3732 {
3733#line 521
3734 __cil_tmp4 = (struct platform_device const *)pdev;
3735#line 521
3736 tmp = platform_get_drvdata(__cil_tmp4);
3737#line 521
3738 fan_data = (struct gpio_fan_data *)tmp;
3739 }
3740 {
3741#line 523
3742 __cil_tmp5 = (unsigned long )fan_data;
3743#line 523
3744 __cil_tmp6 = __cil_tmp5 + 96;
3745#line 523
3746 if (*((unsigned int **)__cil_tmp6)) {
3747 {
3748#line 524
3749 __cil_tmp7 = (unsigned long )fan_data;
3750#line 524
3751 __cil_tmp8 = __cil_tmp7 + 124;
3752#line 524
3753 __cil_tmp9 = *((int *)__cil_tmp8);
3754#line 524
3755 set_fan_speed(fan_data, __cil_tmp9);
3756 }
3757 } else {
3758
3759 }
3760 }
3761#line 526
3762 return (0);
3763}
3764}
3765#line 533 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3766static struct platform_driver gpio_fan_driver = {& gpio_fan_probe, & gpio_fan_remove, (void (*)(struct platform_device * ))0, & gpio_fan_suspend,
3767 & gpio_fan_resume, {"gpio-fan", (struct bus_type *)0, (struct module *)0, (char const *)0,
3768 (_Bool)0, (struct of_device_id const *)0, (int (*)(struct device *dev ))0,
3769 (int (*)(struct device *dev ))0, (void (*)(struct device *dev ))0,
3770 (int (*)(struct device *dev , pm_message_t state ))0, (int (*)(struct device *dev ))0,
3771 (struct attribute_group const **)0, (struct dev_pm_ops const *)0,
3772 (struct driver_private *)0}, (struct platform_device_id const *)0};
3773#line 543
3774static int gpio_fan_driver_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
3775#line 543 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3776static int gpio_fan_driver_init(void)
3777{ int tmp ;
3778
3779 {
3780 {
3781#line 543
3782 tmp = platform_driver_register(& gpio_fan_driver);
3783 }
3784#line 543
3785 return (tmp);
3786}
3787}
3788#line 543 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3789int init_module(void)
3790{ int tmp ;
3791
3792 {
3793 {
3794#line 543
3795 tmp = gpio_fan_driver_init();
3796 }
3797#line 543
3798 return (tmp);
3799}
3800}
3801#line 543
3802static void gpio_fan_driver_exit(void) __attribute__((__section__(".exit.text"),
3803__no_instrument_function__)) ;
3804#line 543 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3805static void gpio_fan_driver_exit(void)
3806{
3807
3808 {
3809 {
3810#line 543
3811 platform_driver_unregister(& gpio_fan_driver);
3812 }
3813#line 543
3814 return;
3815}
3816}
3817#line 543 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3818void cleanup_module(void)
3819{
3820
3821 {
3822 {
3823#line 543
3824 gpio_fan_driver_exit();
3825 }
3826#line 543
3827 return;
3828}
3829}
3830#line 545 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3831static char const __mod_author545[40] __attribute__((__used__, __unused__, __section__(".modinfo"),
3832__aligned__(1))) =
3833#line 545
3834 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
3835 (char const )'o', (char const )'r', (char const )'=', (char const )'S',
3836 (char const )'i', (char const )'m', (char const )'o', (char const )'n',
3837 (char const )' ', (char const )'G', (char const )'u', (char const )'i',
3838 (char const )'n', (char const )'o', (char const )'t', (char const )' ',
3839 (char const )'<', (char const )'s', (char const )'g', (char const )'u',
3840 (char const )'i', (char const )'n', (char const )'o', (char const )'t',
3841 (char const )'@', (char const )'l', (char const )'a', (char const )'c',
3842 (char const )'i', (char const )'e', (char const )'.', (char const )'c',
3843 (char const )'o', (char const )'m', (char const )'>', (char const )'\000'};
3844#line 546 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3845static char const __mod_description546[28] __attribute__((__used__, __unused__,
3846__section__(".modinfo"), __aligned__(1))) =
3847#line 546
3848 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
3849 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
3850 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
3851 (char const )'G', (char const )'P', (char const )'I', (char const )'O',
3852 (char const )' ', (char const )'F', (char const )'A', (char const )'N',
3853 (char const )' ', (char const )'d', (char const )'r', (char const )'i',
3854 (char const )'v', (char const )'e', (char const )'r', (char const )'\000'};
3855#line 547 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3856static char const __mod_license547[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
3857__aligned__(1))) =
3858#line 547
3859 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
3860 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
3861 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
3862#line 548 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3863static char const __mod_alias548[24] __attribute__((__used__, __unused__, __section__(".modinfo"),
3864__aligned__(1))) =
3865#line 548
3866 { (char const )'a', (char const )'l', (char const )'i', (char const )'a',
3867 (char const )'s', (char const )'=', (char const )'p', (char const )'l',
3868 (char const )'a', (char const )'t', (char const )'f', (char const )'o',
3869 (char const )'r', (char const )'m', (char const )':', (char const )'g',
3870 (char const )'p', (char const )'i', (char const )'o', (char const )'-',
3871 (char const )'f', (char const )'a', (char const )'n', (char const )'\000'};
3872#line 566
3873void ldv_check_final_state(void) ;
3874#line 569
3875extern void ldv_check_return_value(int res ) ;
3876#line 572
3877extern void ldv_initialize(void) ;
3878#line 575
3879extern int __VERIFIER_nondet_int(void) ;
3880#line 578 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3881int LDV_IN_INTERRUPT ;
3882#line 596 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3883static int res_gpio_fan_probe_22 ;
3884#line 581 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
3885void main(void)
3886{ struct platform_device *var_group1 ;
3887 pm_message_t var_gpio_fan_suspend_24_p1 ;
3888 int var_fan_alarm_irq_handler_1_p0 ;
3889 void *var_fan_alarm_irq_handler_1_p1 ;
3890 int ldv_s_gpio_fan_driver_platform_driver ;
3891 int tmp ;
3892 int tmp___0 ;
3893 int __cil_tmp8 ;
3894 int var_gpio_fan_suspend_24_p1_event9 ;
3895
3896 {
3897 {
3898#line 655
3899 LDV_IN_INTERRUPT = 1;
3900#line 664
3901 ldv_initialize();
3902#line 665
3903 ldv_s_gpio_fan_driver_platform_driver = 0;
3904 }
3905 {
3906#line 670
3907 while (1) {
3908 while_continue: ;
3909 {
3910#line 670
3911 tmp___0 = __VERIFIER_nondet_int();
3912 }
3913#line 670
3914 if (tmp___0) {
3915
3916 } else {
3917 {
3918#line 670
3919 __cil_tmp8 = ldv_s_gpio_fan_driver_platform_driver == 0;
3920#line 670
3921 if (! __cil_tmp8) {
3922
3923 } else {
3924#line 670
3925 goto while_break;
3926 }
3927 }
3928 }
3929 {
3930#line 674
3931 tmp = __VERIFIER_nondet_int();
3932 }
3933#line 676
3934 if (tmp == 0) {
3935#line 676
3936 goto case_0;
3937 } else
3938#line 705
3939 if (tmp == 1) {
3940#line 705
3941 goto case_1;
3942 } else
3943#line 731
3944 if (tmp == 2) {
3945#line 731
3946 goto case_2;
3947 } else
3948#line 757
3949 if (tmp == 3) {
3950#line 757
3951 goto case_3;
3952 } else {
3953 {
3954#line 783
3955 goto switch_default;
3956#line 674
3957 if (0) {
3958 case_0:
3959#line 679
3960 if (ldv_s_gpio_fan_driver_platform_driver == 0) {
3961 {
3962#line 687
3963 res_gpio_fan_probe_22 = gpio_fan_probe(var_group1);
3964#line 688
3965 ldv_check_return_value(res_gpio_fan_probe_22);
3966 }
3967#line 689
3968 if (res_gpio_fan_probe_22) {
3969#line 690
3970 goto ldv_module_exit;
3971 } else {
3972
3973 }
3974#line 698
3975 ldv_s_gpio_fan_driver_platform_driver = ldv_s_gpio_fan_driver_platform_driver + 1;
3976 } else {
3977
3978 }
3979#line 704
3980 goto switch_break;
3981 case_1:
3982#line 708
3983 if (ldv_s_gpio_fan_driver_platform_driver == 1) {
3984 {
3985#line 717
3986 gpio_fan_suspend(var_group1, var_gpio_fan_suspend_24_p1_event9);
3987#line 724
3988 ldv_s_gpio_fan_driver_platform_driver = ldv_s_gpio_fan_driver_platform_driver + 1;
3989 }
3990 } else {
3991
3992 }
3993#line 730
3994 goto switch_break;
3995 case_2:
3996#line 734
3997 if (ldv_s_gpio_fan_driver_platform_driver == 2) {
3998 {
3999#line 743
4000 gpio_fan_resume(var_group1);
4001#line 750
4002 ldv_s_gpio_fan_driver_platform_driver = 0;
4003 }
4004 } else {
4005
4006 }
4007#line 756
4008 goto switch_break;
4009 case_3:
4010 {
4011#line 760
4012 LDV_IN_INTERRUPT = 2;
4013#line 768
4014 fan_alarm_irq_handler(var_fan_alarm_irq_handler_1_p0, var_fan_alarm_irq_handler_1_p1);
4015#line 776
4016 LDV_IN_INTERRUPT = 1;
4017 }
4018#line 782
4019 goto switch_break;
4020 switch_default:
4021#line 783
4022 goto switch_break;
4023 } else {
4024 switch_break: ;
4025 }
4026 }
4027 }
4028 }
4029 while_break: ;
4030 }
4031 ldv_module_exit:
4032 {
4033#line 792
4034 ldv_check_final_state();
4035 }
4036#line 795
4037 return;
4038}
4039}
4040#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
4041void ldv_blast_assert(void)
4042{
4043
4044 {
4045 ERROR:
4046#line 6
4047 goto ERROR;
4048}
4049}
4050#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
4051extern int __VERIFIER_nondet_int(void) ;
4052#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4053int ldv_mutex = 1;
4054#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4055int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
4056{ int nondetermined ;
4057
4058 {
4059#line 29
4060 if (ldv_mutex == 1) {
4061
4062 } else {
4063 {
4064#line 29
4065 ldv_blast_assert();
4066 }
4067 }
4068 {
4069#line 32
4070 nondetermined = __VERIFIER_nondet_int();
4071 }
4072#line 35
4073 if (nondetermined) {
4074#line 38
4075 ldv_mutex = 2;
4076#line 40
4077 return (0);
4078 } else {
4079#line 45
4080 return (-4);
4081 }
4082}
4083}
4084#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4085int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
4086{ int nondetermined ;
4087
4088 {
4089#line 57
4090 if (ldv_mutex == 1) {
4091
4092 } else {
4093 {
4094#line 57
4095 ldv_blast_assert();
4096 }
4097 }
4098 {
4099#line 60
4100 nondetermined = __VERIFIER_nondet_int();
4101 }
4102#line 63
4103 if (nondetermined) {
4104#line 66
4105 ldv_mutex = 2;
4106#line 68
4107 return (0);
4108 } else {
4109#line 73
4110 return (-4);
4111 }
4112}
4113}
4114#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4115int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
4116{ int atomic_value_after_dec ;
4117
4118 {
4119#line 83
4120 if (ldv_mutex == 1) {
4121
4122 } else {
4123 {
4124#line 83
4125 ldv_blast_assert();
4126 }
4127 }
4128 {
4129#line 86
4130 atomic_value_after_dec = __VERIFIER_nondet_int();
4131 }
4132#line 89
4133 if (atomic_value_after_dec == 0) {
4134#line 92
4135 ldv_mutex = 2;
4136#line 94
4137 return (1);
4138 } else {
4139
4140 }
4141#line 98
4142 return (0);
4143}
4144}
4145#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4146void mutex_lock(struct mutex *lock )
4147{
4148
4149 {
4150#line 108
4151 if (ldv_mutex == 1) {
4152
4153 } else {
4154 {
4155#line 108
4156 ldv_blast_assert();
4157 }
4158 }
4159#line 110
4160 ldv_mutex = 2;
4161#line 111
4162 return;
4163}
4164}
4165#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4166int mutex_trylock(struct mutex *lock )
4167{ int nondetermined ;
4168
4169 {
4170#line 121
4171 if (ldv_mutex == 1) {
4172
4173 } else {
4174 {
4175#line 121
4176 ldv_blast_assert();
4177 }
4178 }
4179 {
4180#line 124
4181 nondetermined = __VERIFIER_nondet_int();
4182 }
4183#line 127
4184 if (nondetermined) {
4185#line 130
4186 ldv_mutex = 2;
4187#line 132
4188 return (1);
4189 } else {
4190#line 137
4191 return (0);
4192 }
4193}
4194}
4195#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4196void mutex_unlock(struct mutex *lock )
4197{
4198
4199 {
4200#line 147
4201 if (ldv_mutex == 2) {
4202
4203 } else {
4204 {
4205#line 147
4206 ldv_blast_assert();
4207 }
4208 }
4209#line 149
4210 ldv_mutex = 1;
4211#line 150
4212 return;
4213}
4214}
4215#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
4216void ldv_check_final_state(void)
4217{
4218
4219 {
4220#line 156
4221 if (ldv_mutex == 1) {
4222
4223 } else {
4224 {
4225#line 156
4226 ldv_blast_assert();
4227 }
4228 }
4229#line 157
4230 return;
4231}
4232}
4233#line 804 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/6047/dscv_tempdir/dscv/ri/32_1/drivers/hwmon/gpio-fan.c.common.c"
4234long s__builtin_expect(long val , long res )
4235{
4236
4237 {
4238#line 805
4239 return (val);
4240}
4241}