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