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 45 "include/asm-generic/int-ll64.h"
11typedef short s16;
12#line 46 "include/asm-generic/int-ll64.h"
13typedef unsigned short u16;
14#line 48 "include/asm-generic/int-ll64.h"
15typedef int s32;
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 219 "include/linux/types.h"
49struct __anonstruct_atomic_t_7 {
50 int counter ;
51};
52#line 219 "include/linux/types.h"
53typedef struct __anonstruct_atomic_t_7 atomic_t;
54#line 224 "include/linux/types.h"
55struct __anonstruct_atomic64_t_8 {
56 long counter ;
57};
58#line 224 "include/linux/types.h"
59typedef struct __anonstruct_atomic64_t_8 atomic64_t;
60#line 229 "include/linux/types.h"
61struct list_head {
62 struct list_head *next ;
63 struct list_head *prev ;
64};
65#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
66struct module;
67#line 56
68struct module;
69#line 146 "include/linux/init.h"
70typedef void (*ctor_fn_t)(void);
71#line 47 "include/linux/dynamic_debug.h"
72struct device;
73#line 47
74struct device;
75#line 135 "include/linux/kernel.h"
76struct completion;
77#line 135
78struct completion;
79#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
80struct page;
81#line 18
82struct page;
83#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
84struct task_struct;
85#line 20
86struct task_struct;
87#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
88struct task_struct;
89#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
90struct file;
91#line 295
92struct file;
93#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
94struct page;
95#line 52
96struct task_struct;
97#line 329
98struct arch_spinlock;
99#line 329
100struct arch_spinlock;
101#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
102struct task_struct;
103#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
104struct task_struct;
105#line 10 "include/asm-generic/bug.h"
106struct bug_entry {
107 int bug_addr_disp ;
108 int file_disp ;
109 unsigned short line ;
110 unsigned short flags ;
111};
112#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
113struct static_key;
114#line 234
115struct static_key;
116#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
117struct kmem_cache;
118#line 23 "include/asm-generic/atomic-long.h"
119typedef atomic64_t atomic_long_t;
120#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
121typedef u16 __ticket_t;
122#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
123typedef u32 __ticketpair_t;
124#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
125struct __raw_tickets {
126 __ticket_t head ;
127 __ticket_t tail ;
128};
129#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
130union __anonunion____missing_field_name_36 {
131 __ticketpair_t head_tail ;
132 struct __raw_tickets tickets ;
133};
134#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
135struct arch_spinlock {
136 union __anonunion____missing_field_name_36 __annonCompField17 ;
137};
138#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
139typedef struct arch_spinlock arch_spinlock_t;
140#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
141struct __anonstruct____missing_field_name_38 {
142 u32 read ;
143 s32 write ;
144};
145#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
146union __anonunion_arch_rwlock_t_37 {
147 s64 lock ;
148 struct __anonstruct____missing_field_name_38 __annonCompField18 ;
149};
150#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
151typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
152#line 12 "include/linux/lockdep.h"
153struct task_struct;
154#line 20 "include/linux/spinlock_types.h"
155struct raw_spinlock {
156 arch_spinlock_t raw_lock ;
157 unsigned int magic ;
158 unsigned int owner_cpu ;
159 void *owner ;
160};
161#line 20 "include/linux/spinlock_types.h"
162typedef struct raw_spinlock raw_spinlock_t;
163#line 64 "include/linux/spinlock_types.h"
164union __anonunion____missing_field_name_39 {
165 struct raw_spinlock rlock ;
166};
167#line 64 "include/linux/spinlock_types.h"
168struct spinlock {
169 union __anonunion____missing_field_name_39 __annonCompField19 ;
170};
171#line 64 "include/linux/spinlock_types.h"
172typedef struct spinlock spinlock_t;
173#line 11 "include/linux/rwlock_types.h"
174struct __anonstruct_rwlock_t_40 {
175 arch_rwlock_t raw_lock ;
176 unsigned int magic ;
177 unsigned int owner_cpu ;
178 void *owner ;
179};
180#line 11 "include/linux/rwlock_types.h"
181typedef struct __anonstruct_rwlock_t_40 rwlock_t;
182#line 49 "include/linux/wait.h"
183struct __wait_queue_head {
184 spinlock_t lock ;
185 struct list_head task_list ;
186};
187#line 53 "include/linux/wait.h"
188typedef struct __wait_queue_head wait_queue_head_t;
189#line 55
190struct task_struct;
191#line 60 "include/linux/pageblock-flags.h"
192struct page;
193#line 48 "include/linux/mutex.h"
194struct mutex {
195 atomic_t count ;
196 spinlock_t wait_lock ;
197 struct list_head wait_list ;
198 struct task_struct *owner ;
199 char const *name ;
200 void *magic ;
201};
202#line 19 "include/linux/rwsem.h"
203struct rw_semaphore;
204#line 19
205struct rw_semaphore;
206#line 25 "include/linux/rwsem.h"
207struct rw_semaphore {
208 long count ;
209 raw_spinlock_t wait_lock ;
210 struct list_head wait_list ;
211};
212#line 25 "include/linux/completion.h"
213struct completion {
214 unsigned int done ;
215 wait_queue_head_t wait ;
216};
217#line 9 "include/linux/memory_hotplug.h"
218struct page;
219#line 202 "include/linux/ioport.h"
220struct device;
221#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
222struct device;
223#line 46 "include/linux/ktime.h"
224union ktime {
225 s64 tv64 ;
226};
227#line 59 "include/linux/ktime.h"
228typedef union ktime ktime_t;
229#line 10 "include/linux/timer.h"
230struct tvec_base;
231#line 10
232struct tvec_base;
233#line 12 "include/linux/timer.h"
234struct timer_list {
235 struct list_head entry ;
236 unsigned long expires ;
237 struct tvec_base *base ;
238 void (*function)(unsigned long ) ;
239 unsigned long data ;
240 int slack ;
241 int start_pid ;
242 void *start_site ;
243 char start_comm[16] ;
244};
245#line 17 "include/linux/workqueue.h"
246struct work_struct;
247#line 17
248struct work_struct;
249#line 79 "include/linux/workqueue.h"
250struct work_struct {
251 atomic_long_t data ;
252 struct list_head entry ;
253 void (*func)(struct work_struct *work ) ;
254};
255#line 42 "include/linux/pm.h"
256struct device;
257#line 50 "include/linux/pm.h"
258struct pm_message {
259 int event ;
260};
261#line 50 "include/linux/pm.h"
262typedef struct pm_message pm_message_t;
263#line 264 "include/linux/pm.h"
264struct dev_pm_ops {
265 int (*prepare)(struct device *dev ) ;
266 void (*complete)(struct device *dev ) ;
267 int (*suspend)(struct device *dev ) ;
268 int (*resume)(struct device *dev ) ;
269 int (*freeze)(struct device *dev ) ;
270 int (*thaw)(struct device *dev ) ;
271 int (*poweroff)(struct device *dev ) ;
272 int (*restore)(struct device *dev ) ;
273 int (*suspend_late)(struct device *dev ) ;
274 int (*resume_early)(struct device *dev ) ;
275 int (*freeze_late)(struct device *dev ) ;
276 int (*thaw_early)(struct device *dev ) ;
277 int (*poweroff_late)(struct device *dev ) ;
278 int (*restore_early)(struct device *dev ) ;
279 int (*suspend_noirq)(struct device *dev ) ;
280 int (*resume_noirq)(struct device *dev ) ;
281 int (*freeze_noirq)(struct device *dev ) ;
282 int (*thaw_noirq)(struct device *dev ) ;
283 int (*poweroff_noirq)(struct device *dev ) ;
284 int (*restore_noirq)(struct device *dev ) ;
285 int (*runtime_suspend)(struct device *dev ) ;
286 int (*runtime_resume)(struct device *dev ) ;
287 int (*runtime_idle)(struct device *dev ) ;
288};
289#line 458
290enum rpm_status {
291 RPM_ACTIVE = 0,
292 RPM_RESUMING = 1,
293 RPM_SUSPENDED = 2,
294 RPM_SUSPENDING = 3
295} ;
296#line 480
297enum rpm_request {
298 RPM_REQ_NONE = 0,
299 RPM_REQ_IDLE = 1,
300 RPM_REQ_SUSPEND = 2,
301 RPM_REQ_AUTOSUSPEND = 3,
302 RPM_REQ_RESUME = 4
303} ;
304#line 488
305struct wakeup_source;
306#line 488
307struct wakeup_source;
308#line 495 "include/linux/pm.h"
309struct pm_subsys_data {
310 spinlock_t lock ;
311 unsigned int refcount ;
312};
313#line 506
314struct dev_pm_qos_request;
315#line 506
316struct pm_qos_constraints;
317#line 506 "include/linux/pm.h"
318struct dev_pm_info {
319 pm_message_t power_state ;
320 unsigned int can_wakeup : 1 ;
321 unsigned int async_suspend : 1 ;
322 bool is_prepared : 1 ;
323 bool is_suspended : 1 ;
324 bool ignore_children : 1 ;
325 spinlock_t lock ;
326 struct list_head entry ;
327 struct completion completion ;
328 struct wakeup_source *wakeup ;
329 bool wakeup_path : 1 ;
330 struct timer_list suspend_timer ;
331 unsigned long timer_expires ;
332 struct work_struct work ;
333 wait_queue_head_t wait_queue ;
334 atomic_t usage_count ;
335 atomic_t child_count ;
336 unsigned int disable_depth : 3 ;
337 unsigned int idle_notification : 1 ;
338 unsigned int request_pending : 1 ;
339 unsigned int deferred_resume : 1 ;
340 unsigned int run_wake : 1 ;
341 unsigned int runtime_auto : 1 ;
342 unsigned int no_callbacks : 1 ;
343 unsigned int irq_safe : 1 ;
344 unsigned int use_autosuspend : 1 ;
345 unsigned int timer_autosuspends : 1 ;
346 enum rpm_request request ;
347 enum rpm_status runtime_status ;
348 int runtime_error ;
349 int autosuspend_delay ;
350 unsigned long last_busy ;
351 unsigned long active_jiffies ;
352 unsigned long suspended_jiffies ;
353 unsigned long accounting_timestamp ;
354 ktime_t suspend_time ;
355 s64 max_time_suspended_ns ;
356 struct dev_pm_qos_request *pq_req ;
357 struct pm_subsys_data *subsys_data ;
358 struct pm_qos_constraints *constraints ;
359};
360#line 564 "include/linux/pm.h"
361struct dev_pm_domain {
362 struct dev_pm_ops ops ;
363};
364#line 8 "include/linux/vmalloc.h"
365struct vm_area_struct;
366#line 8
367struct vm_area_struct;
368#line 994 "include/linux/mmzone.h"
369struct page;
370#line 10 "include/linux/gfp.h"
371struct vm_area_struct;
372#line 29 "include/linux/sysctl.h"
373struct completion;
374#line 49 "include/linux/kmod.h"
375struct file;
376#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
377struct task_struct;
378#line 18 "include/linux/elf.h"
379typedef __u64 Elf64_Addr;
380#line 19 "include/linux/elf.h"
381typedef __u16 Elf64_Half;
382#line 23 "include/linux/elf.h"
383typedef __u32 Elf64_Word;
384#line 24 "include/linux/elf.h"
385typedef __u64 Elf64_Xword;
386#line 194 "include/linux/elf.h"
387struct elf64_sym {
388 Elf64_Word st_name ;
389 unsigned char st_info ;
390 unsigned char st_other ;
391 Elf64_Half st_shndx ;
392 Elf64_Addr st_value ;
393 Elf64_Xword st_size ;
394};
395#line 194 "include/linux/elf.h"
396typedef struct elf64_sym Elf64_Sym;
397#line 438
398struct file;
399#line 20 "include/linux/kobject_ns.h"
400struct sock;
401#line 20
402struct sock;
403#line 21
404struct kobject;
405#line 21
406struct kobject;
407#line 27
408enum kobj_ns_type {
409 KOBJ_NS_TYPE_NONE = 0,
410 KOBJ_NS_TYPE_NET = 1,
411 KOBJ_NS_TYPES = 2
412} ;
413#line 40 "include/linux/kobject_ns.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 *sk ) ;
418 void const *(*initial_ns)(void) ;
419 void (*drop_ns)(void * ) ;
420};
421#line 22 "include/linux/sysfs.h"
422struct kobject;
423#line 23
424struct module;
425#line 24
426enum kobj_ns_type;
427#line 26 "include/linux/sysfs.h"
428struct attribute {
429 char const *name ;
430 umode_t mode ;
431};
432#line 56 "include/linux/sysfs.h"
433struct attribute_group {
434 char const *name ;
435 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
436 struct attribute **attrs ;
437};
438#line 85
439struct file;
440#line 86
441struct vm_area_struct;
442#line 88 "include/linux/sysfs.h"
443struct bin_attribute {
444 struct attribute attr ;
445 size_t size ;
446 void *private ;
447 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
448 loff_t , size_t ) ;
449 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
450 loff_t , size_t ) ;
451 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
452};
453#line 112 "include/linux/sysfs.h"
454struct sysfs_ops {
455 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
456 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
457 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
458};
459#line 118
460struct sysfs_dirent;
461#line 118
462struct sysfs_dirent;
463#line 22 "include/linux/kref.h"
464struct kref {
465 atomic_t refcount ;
466};
467#line 60 "include/linux/kobject.h"
468struct kset;
469#line 60
470struct kobj_type;
471#line 60 "include/linux/kobject.h"
472struct kobject {
473 char const *name ;
474 struct list_head entry ;
475 struct kobject *parent ;
476 struct kset *kset ;
477 struct kobj_type *ktype ;
478 struct sysfs_dirent *sd ;
479 struct kref kref ;
480 unsigned int state_initialized : 1 ;
481 unsigned int state_in_sysfs : 1 ;
482 unsigned int state_add_uevent_sent : 1 ;
483 unsigned int state_remove_uevent_sent : 1 ;
484 unsigned int uevent_suppress : 1 ;
485};
486#line 108 "include/linux/kobject.h"
487struct kobj_type {
488 void (*release)(struct kobject *kobj ) ;
489 struct sysfs_ops const *sysfs_ops ;
490 struct attribute **default_attrs ;
491 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
492 void const *(*namespace)(struct kobject *kobj ) ;
493};
494#line 116 "include/linux/kobject.h"
495struct kobj_uevent_env {
496 char *envp[32] ;
497 int envp_idx ;
498 char buf[2048] ;
499 int buflen ;
500};
501#line 123 "include/linux/kobject.h"
502struct kset_uevent_ops {
503 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
504 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
505 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
506};
507#line 140
508struct sock;
509#line 159 "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 39 "include/linux/moduleparam.h"
517struct kernel_param;
518#line 39
519struct kernel_param;
520#line 41 "include/linux/moduleparam.h"
521struct kernel_param_ops {
522 int (*set)(char const *val , struct kernel_param const *kp ) ;
523 int (*get)(char *buffer , struct kernel_param const *kp ) ;
524 void (*free)(void *arg ) ;
525};
526#line 50
527struct kparam_string;
528#line 50
529struct kparam_array;
530#line 50 "include/linux/moduleparam.h"
531union __anonunion____missing_field_name_199 {
532 void *arg ;
533 struct kparam_string const *str ;
534 struct kparam_array const *arr ;
535};
536#line 50 "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____missing_field_name_199 __annonCompField32 ;
543};
544#line 63 "include/linux/moduleparam.h"
545struct kparam_string {
546 unsigned int maxlen ;
547 char *string ;
548};
549#line 69 "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 445
558struct module;
559#line 80 "include/linux/jump_label.h"
560struct module;
561#line 143 "include/linux/jump_label.h"
562struct static_key {
563 atomic_t enabled ;
564};
565#line 22 "include/linux/tracepoint.h"
566struct module;
567#line 23
568struct tracepoint;
569#line 23
570struct tracepoint;
571#line 25 "include/linux/tracepoint.h"
572struct tracepoint_func {
573 void *func ;
574 void *data ;
575};
576#line 30 "include/linux/tracepoint.h"
577struct tracepoint {
578 char const *name ;
579 struct static_key key ;
580 void (*regfunc)(void) ;
581 void (*unregfunc)(void) ;
582 struct tracepoint_func *funcs ;
583};
584#line 19 "include/linux/export.h"
585struct kernel_symbol {
586 unsigned long value ;
587 char const *name ;
588};
589#line 8 "include/asm-generic/module.h"
590struct mod_arch_specific {
591
592};
593#line 35 "include/linux/module.h"
594struct module;
595#line 37
596struct module_param_attrs;
597#line 37 "include/linux/module.h"
598struct module_kobject {
599 struct kobject kobj ;
600 struct module *mod ;
601 struct kobject *drivers_dir ;
602 struct module_param_attrs *mp ;
603};
604#line 44 "include/linux/module.h"
605struct module_attribute {
606 struct attribute attr ;
607 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
608 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
609 size_t count ) ;
610 void (*setup)(struct module * , char const * ) ;
611 int (*test)(struct module * ) ;
612 void (*free)(struct module * ) ;
613};
614#line 71
615struct exception_table_entry;
616#line 71
617struct exception_table_entry;
618#line 199
619enum module_state {
620 MODULE_STATE_LIVE = 0,
621 MODULE_STATE_COMING = 1,
622 MODULE_STATE_GOING = 2
623} ;
624#line 215 "include/linux/module.h"
625struct module_ref {
626 unsigned long incs ;
627 unsigned long decs ;
628} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
629#line 220
630struct module_sect_attrs;
631#line 220
632struct module_notes_attrs;
633#line 220
634struct ftrace_event_call;
635#line 220 "include/linux/module.h"
636struct module {
637 enum module_state state ;
638 struct list_head list ;
639 char name[64UL - sizeof(unsigned long )] ;
640 struct module_kobject mkobj ;
641 struct module_attribute *modinfo_attrs ;
642 char const *version ;
643 char const *srcversion ;
644 struct kobject *holders_dir ;
645 struct kernel_symbol const *syms ;
646 unsigned long const *crcs ;
647 unsigned int num_syms ;
648 struct kernel_param *kp ;
649 unsigned int num_kp ;
650 unsigned int num_gpl_syms ;
651 struct kernel_symbol const *gpl_syms ;
652 unsigned long const *gpl_crcs ;
653 struct kernel_symbol const *unused_syms ;
654 unsigned long const *unused_crcs ;
655 unsigned int num_unused_syms ;
656 unsigned int num_unused_gpl_syms ;
657 struct kernel_symbol const *unused_gpl_syms ;
658 unsigned long const *unused_gpl_crcs ;
659 struct kernel_symbol const *gpl_future_syms ;
660 unsigned long const *gpl_future_crcs ;
661 unsigned int num_gpl_future_syms ;
662 unsigned int num_exentries ;
663 struct exception_table_entry *extable ;
664 int (*init)(void) ;
665 void *module_init ;
666 void *module_core ;
667 unsigned int init_size ;
668 unsigned int core_size ;
669 unsigned int init_text_size ;
670 unsigned int core_text_size ;
671 unsigned int init_ro_size ;
672 unsigned int core_ro_size ;
673 struct mod_arch_specific arch ;
674 unsigned int taints ;
675 unsigned int num_bugs ;
676 struct list_head bug_list ;
677 struct bug_entry *bug_table ;
678 Elf64_Sym *symtab ;
679 Elf64_Sym *core_symtab ;
680 unsigned int num_symtab ;
681 unsigned int core_num_syms ;
682 char *strtab ;
683 char *core_strtab ;
684 struct module_sect_attrs *sect_attrs ;
685 struct module_notes_attrs *notes_attrs ;
686 char *args ;
687 void *percpu ;
688 unsigned int percpu_size ;
689 unsigned int num_tracepoints ;
690 struct tracepoint * const *tracepoints_ptrs ;
691 unsigned int num_trace_bprintk_fmt ;
692 char const **trace_bprintk_fmt_start ;
693 struct ftrace_event_call **trace_events ;
694 unsigned int num_trace_events ;
695 struct list_head source_list ;
696 struct list_head target_list ;
697 struct task_struct *waiter ;
698 void (*exit)(void) ;
699 struct module_ref *refptr ;
700 ctor_fn_t *ctors ;
701 unsigned int num_ctors ;
702};
703#line 219 "include/linux/mod_devicetable.h"
704struct of_device_id {
705 char name[32] ;
706 char type[32] ;
707 char compatible[128] ;
708 void *data ;
709};
710#line 28 "include/linux/of.h"
711typedef u32 phandle;
712#line 31 "include/linux/of.h"
713struct property {
714 char *name ;
715 int length ;
716 void *value ;
717 struct property *next ;
718 unsigned long _flags ;
719 unsigned int unique_id ;
720};
721#line 44
722struct proc_dir_entry;
723#line 44 "include/linux/of.h"
724struct device_node {
725 char const *name ;
726 char const *type ;
727 phandle phandle ;
728 char *full_name ;
729 struct property *properties ;
730 struct property *deadprops ;
731 struct device_node *parent ;
732 struct device_node *child ;
733 struct device_node *sibling ;
734 struct device_node *next ;
735 struct device_node *allnext ;
736 struct proc_dir_entry *pde ;
737 struct kref kref ;
738 unsigned long _flags ;
739 void *data ;
740};
741#line 44 "include/asm-generic/gpio.h"
742struct device;
743#line 47
744struct module;
745#line 48
746struct device_node;
747#line 10 "include/linux/irqreturn.h"
748enum irqreturn {
749 IRQ_NONE = 0,
750 IRQ_HANDLED = 1,
751 IRQ_WAKE_THREAD = 2
752} ;
753#line 16 "include/linux/irqreturn.h"
754typedef enum irqreturn irqreturn_t;
755#line 32 "include/linux/irq.h"
756struct module;
757#line 12 "include/linux/irqdesc.h"
758struct proc_dir_entry;
759#line 14
760struct module;
761#line 16 "include/linux/profile.h"
762struct proc_dir_entry;
763#line 65
764struct task_struct;
765#line 94 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess.h"
766struct exception_table_entry {
767 unsigned long insn ;
768 unsigned long fixup ;
769};
770#line 132 "include/linux/hardirq.h"
771struct task_struct;
772#line 187 "include/linux/interrupt.h"
773struct device;
774#line 20 "include/linux/leds.h"
775struct device;
776#line 25
777enum led_brightness {
778 LED_OFF = 0,
779 LED_HALF = 127,
780 LED_FULL = 255
781} ;
782#line 31
783struct led_trigger;
784#line 31 "include/linux/leds.h"
785struct led_classdev {
786 char const *name ;
787 int brightness ;
788 int max_brightness ;
789 int flags ;
790 void (*brightness_set)(struct led_classdev *led_cdev , enum led_brightness brightness ) ;
791 enum led_brightness (*brightness_get)(struct led_classdev *led_cdev ) ;
792 int (*blink_set)(struct led_classdev *led_cdev , unsigned long *delay_on , unsigned long *delay_off ) ;
793 struct device *dev ;
794 struct list_head node ;
795 char const *default_trigger ;
796 unsigned long blink_delay_on ;
797 unsigned long blink_delay_off ;
798 struct timer_list blink_timer ;
799 int blink_brightness ;
800 struct rw_semaphore trigger_lock ;
801 struct led_trigger *trigger ;
802 struct list_head trig_list ;
803 void *trigger_data ;
804};
805#line 122 "include/linux/leds.h"
806struct led_trigger {
807 char const *name ;
808 void (*activate)(struct led_classdev *led_cdev ) ;
809 void (*deactivate)(struct led_classdev *led_cdev ) ;
810 rwlock_t leddev_list_lock ;
811 struct list_head led_cdevs ;
812 struct list_head next_trig ;
813};
814#line 46 "include/linux/slub_def.h"
815struct kmem_cache_cpu {
816 void **freelist ;
817 unsigned long tid ;
818 struct page *page ;
819 struct page *partial ;
820 int node ;
821 unsigned int stat[26] ;
822};
823#line 57 "include/linux/slub_def.h"
824struct kmem_cache_node {
825 spinlock_t list_lock ;
826 unsigned long nr_partial ;
827 struct list_head partial ;
828 atomic_long_t nr_slabs ;
829 atomic_long_t total_objects ;
830 struct list_head full ;
831};
832#line 73 "include/linux/slub_def.h"
833struct kmem_cache_order_objects {
834 unsigned long x ;
835};
836#line 80 "include/linux/slub_def.h"
837struct kmem_cache {
838 struct kmem_cache_cpu *cpu_slab ;
839 unsigned long flags ;
840 unsigned long min_partial ;
841 int size ;
842 int objsize ;
843 int offset ;
844 int cpu_partial ;
845 struct kmem_cache_order_objects oo ;
846 struct kmem_cache_order_objects max ;
847 struct kmem_cache_order_objects min ;
848 gfp_t allocflags ;
849 int refcount ;
850 void (*ctor)(void * ) ;
851 int inuse ;
852 int align ;
853 int reserved ;
854 char const *name ;
855 struct list_head list ;
856 struct kobject kobj ;
857 int remote_node_defrag_ratio ;
858 struct kmem_cache_node *node[1 << 10] ;
859};
860#line 19 "include/linux/klist.h"
861struct klist_node;
862#line 19
863struct klist_node;
864#line 39 "include/linux/klist.h"
865struct klist_node {
866 void *n_klist ;
867 struct list_head n_node ;
868 struct kref n_ref ;
869};
870#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
871struct dma_map_ops;
872#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
873struct dev_archdata {
874 void *acpi_handle ;
875 struct dma_map_ops *dma_ops ;
876 void *iommu ;
877};
878#line 28 "include/linux/device.h"
879struct device;
880#line 29
881struct device_private;
882#line 29
883struct device_private;
884#line 30
885struct device_driver;
886#line 30
887struct device_driver;
888#line 31
889struct driver_private;
890#line 31
891struct driver_private;
892#line 32
893struct module;
894#line 33
895struct class;
896#line 33
897struct class;
898#line 34
899struct subsys_private;
900#line 34
901struct subsys_private;
902#line 35
903struct bus_type;
904#line 35
905struct bus_type;
906#line 36
907struct device_node;
908#line 37
909struct iommu_ops;
910#line 37
911struct iommu_ops;
912#line 39 "include/linux/device.h"
913struct bus_attribute {
914 struct attribute attr ;
915 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
916 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
917};
918#line 89
919struct device_attribute;
920#line 89
921struct driver_attribute;
922#line 89 "include/linux/device.h"
923struct bus_type {
924 char const *name ;
925 char const *dev_name ;
926 struct device *dev_root ;
927 struct bus_attribute *bus_attrs ;
928 struct device_attribute *dev_attrs ;
929 struct driver_attribute *drv_attrs ;
930 int (*match)(struct device *dev , struct device_driver *drv ) ;
931 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
932 int (*probe)(struct device *dev ) ;
933 int (*remove)(struct device *dev ) ;
934 void (*shutdown)(struct device *dev ) ;
935 int (*suspend)(struct device *dev , pm_message_t state ) ;
936 int (*resume)(struct device *dev ) ;
937 struct dev_pm_ops const *pm ;
938 struct iommu_ops *iommu_ops ;
939 struct subsys_private *p ;
940};
941#line 127
942struct device_type;
943#line 214 "include/linux/device.h"
944struct device_driver {
945 char const *name ;
946 struct bus_type *bus ;
947 struct module *owner ;
948 char const *mod_name ;
949 bool suppress_bind_attrs ;
950 struct of_device_id const *of_match_table ;
951 int (*probe)(struct device *dev ) ;
952 int (*remove)(struct device *dev ) ;
953 void (*shutdown)(struct device *dev ) ;
954 int (*suspend)(struct device *dev , pm_message_t state ) ;
955 int (*resume)(struct device *dev ) ;
956 struct attribute_group const **groups ;
957 struct dev_pm_ops const *pm ;
958 struct driver_private *p ;
959};
960#line 249 "include/linux/device.h"
961struct driver_attribute {
962 struct attribute attr ;
963 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
964 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
965};
966#line 330
967struct class_attribute;
968#line 330 "include/linux/device.h"
969struct class {
970 char const *name ;
971 struct module *owner ;
972 struct class_attribute *class_attrs ;
973 struct device_attribute *dev_attrs ;
974 struct bin_attribute *dev_bin_attrs ;
975 struct kobject *dev_kobj ;
976 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
977 char *(*devnode)(struct device *dev , umode_t *mode ) ;
978 void (*class_release)(struct class *class ) ;
979 void (*dev_release)(struct device *dev ) ;
980 int (*suspend)(struct device *dev , pm_message_t state ) ;
981 int (*resume)(struct device *dev ) ;
982 struct kobj_ns_type_operations const *ns_type ;
983 void const *(*namespace)(struct device *dev ) ;
984 struct dev_pm_ops const *pm ;
985 struct subsys_private *p ;
986};
987#line 397 "include/linux/device.h"
988struct class_attribute {
989 struct attribute attr ;
990 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
991 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
992 size_t count ) ;
993 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ;
994};
995#line 465 "include/linux/device.h"
996struct device_type {
997 char const *name ;
998 struct attribute_group const **groups ;
999 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
1000 char *(*devnode)(struct device *dev , umode_t *mode ) ;
1001 void (*release)(struct device *dev ) ;
1002 struct dev_pm_ops const *pm ;
1003};
1004#line 476 "include/linux/device.h"
1005struct device_attribute {
1006 struct attribute attr ;
1007 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
1008 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
1009 size_t count ) ;
1010};
1011#line 559 "include/linux/device.h"
1012struct device_dma_parameters {
1013 unsigned int max_segment_size ;
1014 unsigned long segment_boundary_mask ;
1015};
1016#line 627
1017struct dma_coherent_mem;
1018#line 627 "include/linux/device.h"
1019struct device {
1020 struct device *parent ;
1021 struct device_private *p ;
1022 struct kobject kobj ;
1023 char const *init_name ;
1024 struct device_type const *type ;
1025 struct mutex mutex ;
1026 struct bus_type *bus ;
1027 struct device_driver *driver ;
1028 void *platform_data ;
1029 struct dev_pm_info power ;
1030 struct dev_pm_domain *pm_domain ;
1031 int numa_node ;
1032 u64 *dma_mask ;
1033 u64 coherent_dma_mask ;
1034 struct device_dma_parameters *dma_parms ;
1035 struct list_head dma_pools ;
1036 struct dma_coherent_mem *dma_mem ;
1037 struct dev_archdata archdata ;
1038 struct device_node *of_node ;
1039 dev_t devt ;
1040 u32 id ;
1041 spinlock_t devres_lock ;
1042 struct list_head devres_head ;
1043 struct klist_node knode_class ;
1044 struct class *class ;
1045 struct attribute_group const **groups ;
1046 void (*release)(struct device *dev ) ;
1047};
1048#line 43 "include/linux/pm_wakeup.h"
1049struct wakeup_source {
1050 char const *name ;
1051 struct list_head entry ;
1052 spinlock_t lock ;
1053 struct timer_list timer ;
1054 unsigned long timer_expires ;
1055 ktime_t total_time ;
1056 ktime_t max_time ;
1057 ktime_t last_time ;
1058 unsigned long event_count ;
1059 unsigned long active_count ;
1060 unsigned long relax_count ;
1061 unsigned long hit_count ;
1062 unsigned int active : 1 ;
1063};
1064#line 23 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1065struct gpio_trig_data {
1066 struct led_classdev *led ;
1067 struct work_struct work ;
1068 unsigned int desired_brightness ;
1069 unsigned int inverted ;
1070 unsigned int gpio ;
1071};
1072#line 1 "<compiler builtins>"
1073long __builtin_expect(long val , long res ) ;
1074#line 24 "include/linux/list.h"
1075__inline static void INIT_LIST_HEAD(struct list_head *list ) __attribute__((__no_instrument_function__)) ;
1076#line 24 "include/linux/list.h"
1077__inline static void INIT_LIST_HEAD(struct list_head *list )
1078{ unsigned long __cil_tmp2 ;
1079 unsigned long __cil_tmp3 ;
1080
1081 {
1082#line 26
1083 *((struct list_head **)list) = list;
1084#line 27
1085 __cil_tmp2 = (unsigned long )list;
1086#line 27
1087 __cil_tmp3 = __cil_tmp2 + 8;
1088#line 27
1089 *((struct list_head **)__cil_tmp3) = list;
1090#line 28
1091 return;
1092}
1093}
1094#line 215 "include/linux/kernel.h"
1095extern int __attribute__((__warn_unused_result__)) _kstrtoul(char const *s , unsigned int base ,
1096 unsigned long *res ) ;
1097#line 218
1098extern int __attribute__((__warn_unused_result__)) kstrtoull(char const *s , unsigned int base ,
1099 unsigned long long *res ) ;
1100#line 220
1101__inline static int __attribute__((__warn_unused_result__)) kstrtoul(char const *s ,
1102 unsigned int base ,
1103 unsigned long *res ) __attribute__((__no_instrument_function__)) ;
1104#line 220 "include/linux/kernel.h"
1105__inline static int __attribute__((__warn_unused_result__)) kstrtoul(char const *s ,
1106 unsigned int base ,
1107 unsigned long *res )
1108{ int tmp ;
1109 int tmp___0 ;
1110 unsigned long long *__cil_tmp6 ;
1111
1112 {
1113#line 226
1114 if (8UL == 8UL) {
1115#line 226
1116 if (8UL == 8UL) {
1117 {
1118#line 228
1119 __cil_tmp6 = (unsigned long long *)res;
1120#line 228
1121 tmp = (int )kstrtoull(s, base, __cil_tmp6);
1122 }
1123#line 228
1124 return (tmp);
1125 } else {
1126 {
1127#line 230
1128 tmp___0 = (int )_kstrtoul(s, base, res);
1129 }
1130#line 230
1131 return (tmp___0);
1132 }
1133 } else {
1134 {
1135#line 230
1136 tmp___0 = (int )_kstrtoul(s, base, res);
1137 }
1138#line 230
1139 return (tmp___0);
1140 }
1141}
1142}
1143#line 320
1144extern int ( sprintf)(char *buf , char const *fmt , ...) ;
1145#line 334
1146extern int ( sscanf)(char const * , char const * , ...) ;
1147#line 152 "include/linux/mutex.h"
1148void mutex_lock(struct mutex *lock ) ;
1149#line 153
1150int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
1151#line 154
1152int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
1153#line 168
1154int mutex_trylock(struct mutex *lock ) ;
1155#line 169
1156void mutex_unlock(struct mutex *lock ) ;
1157#line 170
1158int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1159#line 156 "include/linux/workqueue.h"
1160extern void __init_work(struct work_struct *work , int onstack ) ;
1161#line 380
1162extern int schedule_work(struct work_struct *work ) ;
1163#line 390
1164extern bool flush_work(struct work_struct *work ) ;
1165#line 67 "include/linux/module.h"
1166int init_module(void) ;
1167#line 68
1168void cleanup_module(void) ;
1169#line 169 "include/asm-generic/gpio.h"
1170extern int __gpio_get_value(unsigned int gpio ) ;
1171#line 174
1172extern int __gpio_to_irq(unsigned int gpio ) ;
1173#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1174__inline static int gpio_get_value(unsigned int gpio ) __attribute__((__no_instrument_function__)) ;
1175#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1176__inline static int gpio_get_value(unsigned int gpio )
1177{ int tmp ;
1178
1179 {
1180 {
1181#line 28
1182 tmp = __gpio_get_value(gpio);
1183 }
1184#line 28
1185 return (tmp);
1186}
1187}
1188#line 41
1189__inline static int gpio_to_irq(unsigned int gpio ) __attribute__((__no_instrument_function__)) ;
1190#line 41 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
1191__inline static int gpio_to_irq(unsigned int gpio )
1192{ int tmp ;
1193
1194 {
1195 {
1196#line 43
1197 tmp = __gpio_to_irq(gpio);
1198 }
1199#line 43
1200 return (tmp);
1201}
1202}
1203#line 126 "include/linux/interrupt.h"
1204extern int __attribute__((__warn_unused_result__)) request_threaded_irq(unsigned int irq ,
1205 irqreturn_t (*handler)(int ,
1206 void * ) ,
1207 irqreturn_t (*thread_fn)(int ,
1208 void * ) ,
1209 unsigned long flags ,
1210 char const *name ,
1211 void *dev ) ;
1212#line 131
1213__inline static int __attribute__((__warn_unused_result__)) request_irq(unsigned int irq ,
1214 irqreturn_t (*handler)(int ,
1215 void * ) ,
1216 unsigned long flags ,
1217 char const *name ,
1218 void *dev ) __attribute__((__no_instrument_function__)) ;
1219#line 131 "include/linux/interrupt.h"
1220__inline static int __attribute__((__warn_unused_result__)) request_irq(unsigned int irq ,
1221 irqreturn_t (*handler)(int ,
1222 void * ) ,
1223 unsigned long flags ,
1224 char const *name ,
1225 void *dev )
1226{ int tmp ;
1227 void *__cil_tmp7 ;
1228 irqreturn_t (*__cil_tmp8)(int , void * ) ;
1229
1230 {
1231 {
1232#line 135
1233 __cil_tmp7 = (void *)0;
1234#line 135
1235 __cil_tmp8 = (irqreturn_t (*)(int , void * ))__cil_tmp7;
1236#line 135
1237 tmp = (int )request_threaded_irq(irq, handler, __cil_tmp8, flags, name, dev);
1238 }
1239#line 135
1240 return (tmp);
1241}
1242}
1243#line 184
1244extern void free_irq(unsigned int , void * ) ;
1245#line 137 "include/linux/leds.h"
1246extern int led_trigger_register(struct led_trigger *trigger ) ;
1247#line 138
1248extern void led_trigger_unregister(struct led_trigger *trigger ) ;
1249#line 161 "include/linux/slab.h"
1250extern void kfree(void const * ) ;
1251#line 221 "include/linux/slub_def.h"
1252extern void *__kmalloc(size_t size , gfp_t flags ) ;
1253#line 268
1254__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1255 gfp_t flags ) __attribute__((__no_instrument_function__)) ;
1256#line 268 "include/linux/slub_def.h"
1257__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1258 gfp_t flags )
1259{ void *tmp___2 ;
1260
1261 {
1262 {
1263#line 283
1264 tmp___2 = __kmalloc(size, flags);
1265 }
1266#line 283
1267 return (tmp___2);
1268}
1269}
1270#line 349 "include/linux/slab.h"
1271__inline static void *kzalloc(size_t size , gfp_t flags ) __attribute__((__no_instrument_function__)) ;
1272#line 349 "include/linux/slab.h"
1273__inline static void *kzalloc(size_t size , gfp_t flags )
1274{ void *tmp ;
1275 unsigned int __cil_tmp4 ;
1276
1277 {
1278 {
1279#line 351
1280 __cil_tmp4 = flags | 32768U;
1281#line 351
1282 tmp = kmalloc(size, __cil_tmp4);
1283 }
1284#line 351
1285 return (tmp);
1286}
1287}
1288#line 507 "include/linux/device.h"
1289extern int device_create_file(struct device *device , struct device_attribute const *entry ) ;
1290#line 509
1291extern void device_remove_file(struct device *dev , struct device_attribute const *attr ) ;
1292#line 792
1293extern void *dev_get_drvdata(struct device const *dev ) ;
1294#line 891
1295extern int ( dev_err)(struct device const *dev , char const *fmt
1296 , ...) ;
1297#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/leds/leds.h"
1298__inline static void led_set_brightness(struct led_classdev *led_cdev , enum led_brightness value ) __attribute__((__no_instrument_function__)) ;
1299#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/leds/leds.h"
1300__inline static void led_set_brightness(struct led_classdev *led_cdev , enum led_brightness value )
1301{ unsigned long __cil_tmp3 ;
1302 unsigned long __cil_tmp4 ;
1303 int __cil_tmp5 ;
1304 unsigned int __cil_tmp6 ;
1305 unsigned int __cil_tmp7 ;
1306 unsigned long __cil_tmp8 ;
1307 unsigned long __cil_tmp9 ;
1308 int __cil_tmp10 ;
1309 unsigned long __cil_tmp11 ;
1310 unsigned long __cil_tmp12 ;
1311 unsigned long __cil_tmp13 ;
1312 unsigned long __cil_tmp14 ;
1313 int __cil_tmp15 ;
1314 int __cil_tmp16 ;
1315 unsigned long __cil_tmp17 ;
1316 unsigned long __cil_tmp18 ;
1317 void (*__cil_tmp19)(struct led_classdev *led_cdev , enum led_brightness brightness ) ;
1318
1319 {
1320 {
1321#line 23
1322 __cil_tmp3 = (unsigned long )led_cdev;
1323#line 23
1324 __cil_tmp4 = __cil_tmp3 + 12;
1325#line 23
1326 __cil_tmp5 = *((int *)__cil_tmp4);
1327#line 23
1328 __cil_tmp6 = (unsigned int )__cil_tmp5;
1329#line 23
1330 __cil_tmp7 = (unsigned int )value;
1331#line 23
1332 if (__cil_tmp7 > __cil_tmp6) {
1333#line 24
1334 __cil_tmp8 = (unsigned long )led_cdev;
1335#line 24
1336 __cil_tmp9 = __cil_tmp8 + 12;
1337#line 24
1338 __cil_tmp10 = *((int *)__cil_tmp9);
1339#line 24
1340 value = (enum led_brightness )__cil_tmp10;
1341 } else {
1342
1343 }
1344 }
1345#line 25
1346 __cil_tmp11 = (unsigned long )led_cdev;
1347#line 25
1348 __cil_tmp12 = __cil_tmp11 + 8;
1349#line 25
1350 *((int *)__cil_tmp12) = (int )value;
1351 {
1352#line 26
1353 __cil_tmp13 = (unsigned long )led_cdev;
1354#line 26
1355 __cil_tmp14 = __cil_tmp13 + 16;
1356#line 26
1357 __cil_tmp15 = *((int *)__cil_tmp14);
1358#line 26
1359 __cil_tmp16 = __cil_tmp15 & 1;
1360#line 26
1361 if (! __cil_tmp16) {
1362 {
1363#line 27
1364 __cil_tmp17 = (unsigned long )led_cdev;
1365#line 27
1366 __cil_tmp18 = __cil_tmp17 + 24;
1367#line 27
1368 __cil_tmp19 = *((void (**)(struct led_classdev *led_cdev , enum led_brightness brightness ))__cil_tmp18);
1369#line 27
1370 (*__cil_tmp19)(led_cdev, value);
1371 }
1372 } else {
1373
1374 }
1375 }
1376#line 28
1377 return;
1378}
1379}
1380#line 32 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1381static irqreturn_t gpio_trig_irq(int irq , void *_led )
1382{ struct led_classdev *led ;
1383 struct gpio_trig_data *gpio_data ;
1384 unsigned long __cil_tmp5 ;
1385 unsigned long __cil_tmp6 ;
1386 void *__cil_tmp7 ;
1387 unsigned long __cil_tmp8 ;
1388 unsigned long __cil_tmp9 ;
1389 struct work_struct *__cil_tmp10 ;
1390
1391 {
1392 {
1393#line 34
1394 led = (struct led_classdev *)_led;
1395#line 35
1396 __cil_tmp5 = (unsigned long )led;
1397#line 35
1398 __cil_tmp6 = __cil_tmp5 + 256;
1399#line 35
1400 __cil_tmp7 = *((void **)__cil_tmp6);
1401#line 35
1402 gpio_data = (struct gpio_trig_data *)__cil_tmp7;
1403#line 38
1404 __cil_tmp8 = (unsigned long )gpio_data;
1405#line 38
1406 __cil_tmp9 = __cil_tmp8 + 8;
1407#line 38
1408 __cil_tmp10 = (struct work_struct *)__cil_tmp9;
1409#line 38
1410 schedule_work(__cil_tmp10);
1411 }
1412#line 40
1413 return ((irqreturn_t )1);
1414}
1415}
1416#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1417static void gpio_trig_work(struct work_struct *work )
1418{ struct gpio_trig_data *gpio_data ;
1419 struct work_struct const *__mptr ;
1420 int tmp ;
1421 struct gpio_trig_data *__cil_tmp5 ;
1422 unsigned long __cil_tmp6 ;
1423 unsigned long __cil_tmp7 ;
1424 struct work_struct *__cil_tmp8 ;
1425 unsigned int __cil_tmp9 ;
1426 char *__cil_tmp10 ;
1427 char *__cil_tmp11 ;
1428 unsigned long __cil_tmp12 ;
1429 unsigned long __cil_tmp13 ;
1430 unsigned int __cil_tmp14 ;
1431 unsigned long __cil_tmp15 ;
1432 unsigned long __cil_tmp16 ;
1433 unsigned int __cil_tmp17 ;
1434 unsigned long __cil_tmp18 ;
1435 unsigned long __cil_tmp19 ;
1436 unsigned long __cil_tmp20 ;
1437 unsigned long __cil_tmp21 ;
1438 struct led_classdev *__cil_tmp22 ;
1439 unsigned long __cil_tmp23 ;
1440 unsigned long __cil_tmp24 ;
1441 unsigned int __cil_tmp25 ;
1442 enum led_brightness __cil_tmp26 ;
1443 struct led_classdev *__cil_tmp27 ;
1444 enum led_brightness __cil_tmp28 ;
1445 struct led_classdev *__cil_tmp29 ;
1446 enum led_brightness __cil_tmp30 ;
1447
1448 {
1449#line 45
1450 __mptr = (struct work_struct const *)work;
1451#line 45
1452 __cil_tmp5 = (struct gpio_trig_data *)0;
1453#line 45
1454 __cil_tmp6 = (unsigned long )__cil_tmp5;
1455#line 45
1456 __cil_tmp7 = __cil_tmp6 + 8;
1457#line 45
1458 __cil_tmp8 = (struct work_struct *)__cil_tmp7;
1459#line 45
1460 __cil_tmp9 = (unsigned int )__cil_tmp8;
1461#line 45
1462 __cil_tmp10 = (char *)__mptr;
1463#line 45
1464 __cil_tmp11 = __cil_tmp10 - __cil_tmp9;
1465#line 45
1466 gpio_data = (struct gpio_trig_data *)__cil_tmp11;
1467 {
1468#line 49
1469 __cil_tmp12 = (unsigned long )gpio_data;
1470#line 49
1471 __cil_tmp13 = __cil_tmp12 + 48;
1472#line 49
1473 __cil_tmp14 = *((unsigned int *)__cil_tmp13);
1474#line 49
1475 if (! __cil_tmp14) {
1476#line 50
1477 return;
1478 } else {
1479
1480 }
1481 }
1482 {
1483#line 52
1484 __cil_tmp15 = (unsigned long )gpio_data;
1485#line 52
1486 __cil_tmp16 = __cil_tmp15 + 48;
1487#line 52
1488 __cil_tmp17 = *((unsigned int *)__cil_tmp16);
1489#line 52
1490 tmp = gpio_get_value(__cil_tmp17);
1491 }
1492 {
1493#line 53
1494 __cil_tmp18 = (unsigned long )gpio_data;
1495#line 53
1496 __cil_tmp19 = __cil_tmp18 + 44;
1497#line 53
1498 if (*((unsigned int *)__cil_tmp19)) {
1499#line 54
1500 tmp = ! tmp;
1501 } else {
1502
1503 }
1504 }
1505#line 56
1506 if (tmp) {
1507 {
1508#line 57
1509 __cil_tmp20 = (unsigned long )gpio_data;
1510#line 57
1511 __cil_tmp21 = __cil_tmp20 + 40;
1512#line 57
1513 if (*((unsigned int *)__cil_tmp21)) {
1514 {
1515#line 58
1516 __cil_tmp22 = *((struct led_classdev **)gpio_data);
1517#line 58
1518 __cil_tmp23 = (unsigned long )gpio_data;
1519#line 58
1520 __cil_tmp24 = __cil_tmp23 + 40;
1521#line 58
1522 __cil_tmp25 = *((unsigned int *)__cil_tmp24);
1523#line 58
1524 __cil_tmp26 = (enum led_brightness )__cil_tmp25;
1525#line 58
1526 led_set_brightness(__cil_tmp22, __cil_tmp26);
1527 }
1528 } else {
1529 {
1530#line 61
1531 __cil_tmp27 = *((struct led_classdev **)gpio_data);
1532#line 61
1533 __cil_tmp28 = (enum led_brightness )255;
1534#line 61
1535 led_set_brightness(__cil_tmp27, __cil_tmp28);
1536 }
1537 }
1538 }
1539 } else {
1540 {
1541#line 63
1542 __cil_tmp29 = *((struct led_classdev **)gpio_data);
1543#line 63
1544 __cil_tmp30 = (enum led_brightness )0;
1545#line 63
1546 led_set_brightness(__cil_tmp29, __cil_tmp30);
1547 }
1548 }
1549#line 65
1550 return;
1551}
1552}
1553#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1554static ssize_t gpio_trig_brightness_show(struct device *dev , struct device_attribute *attr ,
1555 char *buf )
1556{ struct led_classdev *led ;
1557 void *tmp ;
1558 struct gpio_trig_data *gpio_data ;
1559 int tmp___0 ;
1560 struct device const *__cil_tmp8 ;
1561 unsigned long __cil_tmp9 ;
1562 unsigned long __cil_tmp10 ;
1563 void *__cil_tmp11 ;
1564 unsigned long __cil_tmp12 ;
1565 unsigned long __cil_tmp13 ;
1566 unsigned int __cil_tmp14 ;
1567
1568 {
1569 {
1570#line 70
1571 __cil_tmp8 = (struct device const *)dev;
1572#line 70
1573 tmp = dev_get_drvdata(__cil_tmp8);
1574#line 70
1575 led = (struct led_classdev *)tmp;
1576#line 71
1577 __cil_tmp9 = (unsigned long )led;
1578#line 71
1579 __cil_tmp10 = __cil_tmp9 + 256;
1580#line 71
1581 __cil_tmp11 = *((void **)__cil_tmp10);
1582#line 71
1583 gpio_data = (struct gpio_trig_data *)__cil_tmp11;
1584#line 73
1585 __cil_tmp12 = (unsigned long )gpio_data;
1586#line 73
1587 __cil_tmp13 = __cil_tmp12 + 40;
1588#line 73
1589 __cil_tmp14 = *((unsigned int *)__cil_tmp13);
1590#line 73
1591 tmp___0 = sprintf(buf, "%u\n", __cil_tmp14);
1592 }
1593#line 73
1594 return ((ssize_t )tmp___0);
1595}
1596}
1597#line 76 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1598static ssize_t gpio_trig_brightness_store(struct device *dev , struct device_attribute *attr ,
1599 char const *buf , size_t n )
1600{ struct led_classdev *led ;
1601 void *tmp ;
1602 struct gpio_trig_data *gpio_data ;
1603 unsigned int desired_brightness ;
1604 int ret ;
1605 struct device const *__cil_tmp10 ;
1606 unsigned long __cil_tmp11 ;
1607 unsigned long __cil_tmp12 ;
1608 void *__cil_tmp13 ;
1609 struct device const *__cil_tmp14 ;
1610 unsigned int *__cil_tmp15 ;
1611 unsigned int __cil_tmp16 ;
1612 struct device const *__cil_tmp17 ;
1613 unsigned long __cil_tmp18 ;
1614 unsigned long __cil_tmp19 ;
1615 unsigned int *__cil_tmp20 ;
1616
1617 {
1618 {
1619#line 79
1620 __cil_tmp10 = (struct device const *)dev;
1621#line 79
1622 tmp = dev_get_drvdata(__cil_tmp10);
1623#line 79
1624 led = (struct led_classdev *)tmp;
1625#line 80
1626 __cil_tmp11 = (unsigned long )led;
1627#line 80
1628 __cil_tmp12 = __cil_tmp11 + 256;
1629#line 80
1630 __cil_tmp13 = *((void **)__cil_tmp12);
1631#line 80
1632 gpio_data = (struct gpio_trig_data *)__cil_tmp13;
1633#line 84
1634 ret = sscanf(buf, "%u", & desired_brightness);
1635 }
1636#line 85
1637 if (ret < 1) {
1638 {
1639#line 86
1640 __cil_tmp14 = (struct device const *)dev;
1641#line 86
1642 dev_err(__cil_tmp14, "invalid value\n");
1643 }
1644#line 87
1645 return ((ssize_t )-22);
1646 } else {
1647 {
1648#line 85
1649 __cil_tmp15 = & desired_brightness;
1650#line 85
1651 __cil_tmp16 = *__cil_tmp15;
1652#line 85
1653 if (__cil_tmp16 > 255U) {
1654 {
1655#line 86
1656 __cil_tmp17 = (struct device const *)dev;
1657#line 86
1658 dev_err(__cil_tmp17, "invalid value\n");
1659 }
1660#line 87
1661 return ((ssize_t )-22);
1662 } else {
1663
1664 }
1665 }
1666 }
1667#line 90
1668 __cil_tmp18 = (unsigned long )gpio_data;
1669#line 90
1670 __cil_tmp19 = __cil_tmp18 + 40;
1671#line 90
1672 __cil_tmp20 = & desired_brightness;
1673#line 90
1674 *((unsigned int *)__cil_tmp19) = *__cil_tmp20;
1675#line 92
1676 return ((ssize_t )n);
1677}
1678}
1679#line 94 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1680static struct device_attribute dev_attr_desired_brightness = {{"desired_brightness", (umode_t )420}, & gpio_trig_brightness_show, & gpio_trig_brightness_store};
1681#line 97 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1682static ssize_t gpio_trig_inverted_show(struct device *dev , struct device_attribute *attr ,
1683 char *buf )
1684{ struct led_classdev *led ;
1685 void *tmp ;
1686 struct gpio_trig_data *gpio_data ;
1687 int tmp___0 ;
1688 struct device const *__cil_tmp8 ;
1689 unsigned long __cil_tmp9 ;
1690 unsigned long __cil_tmp10 ;
1691 void *__cil_tmp11 ;
1692 unsigned long __cil_tmp12 ;
1693 unsigned long __cil_tmp13 ;
1694 unsigned int __cil_tmp14 ;
1695
1696 {
1697 {
1698#line 100
1699 __cil_tmp8 = (struct device const *)dev;
1700#line 100
1701 tmp = dev_get_drvdata(__cil_tmp8);
1702#line 100
1703 led = (struct led_classdev *)tmp;
1704#line 101
1705 __cil_tmp9 = (unsigned long )led;
1706#line 101
1707 __cil_tmp10 = __cil_tmp9 + 256;
1708#line 101
1709 __cil_tmp11 = *((void **)__cil_tmp10);
1710#line 101
1711 gpio_data = (struct gpio_trig_data *)__cil_tmp11;
1712#line 103
1713 __cil_tmp12 = (unsigned long )gpio_data;
1714#line 103
1715 __cil_tmp13 = __cil_tmp12 + 44;
1716#line 103
1717 __cil_tmp14 = *((unsigned int *)__cil_tmp13);
1718#line 103
1719 tmp___0 = sprintf(buf, "%u\n", __cil_tmp14);
1720 }
1721#line 103
1722 return ((ssize_t )tmp___0);
1723}
1724}
1725#line 106 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1726static ssize_t gpio_trig_inverted_store(struct device *dev , struct device_attribute *attr ,
1727 char const *buf , size_t n )
1728{ struct led_classdev *led ;
1729 void *tmp ;
1730 struct gpio_trig_data *gpio_data ;
1731 unsigned long inverted ;
1732 int ret ;
1733 struct device const *__cil_tmp10 ;
1734 unsigned long __cil_tmp11 ;
1735 unsigned long __cil_tmp12 ;
1736 void *__cil_tmp13 ;
1737 unsigned long *__cil_tmp14 ;
1738 unsigned long __cil_tmp15 ;
1739 unsigned long __cil_tmp16 ;
1740 unsigned long __cil_tmp17 ;
1741 unsigned long *__cil_tmp18 ;
1742 unsigned long __cil_tmp19 ;
1743 unsigned long __cil_tmp20 ;
1744 unsigned long __cil_tmp21 ;
1745 struct work_struct *__cil_tmp22 ;
1746
1747 {
1748 {
1749#line 109
1750 __cil_tmp10 = (struct device const *)dev;
1751#line 109
1752 tmp = dev_get_drvdata(__cil_tmp10);
1753#line 109
1754 led = (struct led_classdev *)tmp;
1755#line 110
1756 __cil_tmp11 = (unsigned long )led;
1757#line 110
1758 __cil_tmp12 = __cil_tmp11 + 256;
1759#line 110
1760 __cil_tmp13 = *((void **)__cil_tmp12);
1761#line 110
1762 gpio_data = (struct gpio_trig_data *)__cil_tmp13;
1763#line 114
1764 ret = (int )kstrtoul(buf, 10U, & inverted);
1765 }
1766#line 115
1767 if (ret < 0) {
1768#line 116
1769 return ((ssize_t )ret);
1770 } else {
1771
1772 }
1773 {
1774#line 118
1775 __cil_tmp14 = & inverted;
1776#line 118
1777 __cil_tmp15 = *__cil_tmp14;
1778#line 118
1779 if (__cil_tmp15 > 1UL) {
1780#line 119
1781 return ((ssize_t )-22);
1782 } else {
1783
1784 }
1785 }
1786 {
1787#line 121
1788 __cil_tmp16 = (unsigned long )gpio_data;
1789#line 121
1790 __cil_tmp17 = __cil_tmp16 + 44;
1791#line 121
1792 __cil_tmp18 = & inverted;
1793#line 121
1794 __cil_tmp19 = *__cil_tmp18;
1795#line 121
1796 *((unsigned int *)__cil_tmp17) = (unsigned int )__cil_tmp19;
1797#line 124
1798 __cil_tmp20 = (unsigned long )gpio_data;
1799#line 124
1800 __cil_tmp21 = __cil_tmp20 + 8;
1801#line 124
1802 __cil_tmp22 = (struct work_struct *)__cil_tmp21;
1803#line 124
1804 schedule_work(__cil_tmp22);
1805 }
1806#line 126
1807 return ((ssize_t )n);
1808}
1809}
1810#line 128 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1811static struct device_attribute dev_attr_inverted = {{"inverted", (umode_t )420}, & gpio_trig_inverted_show, & gpio_trig_inverted_store};
1812#line 131 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1813static ssize_t gpio_trig_gpio_show(struct device *dev , struct device_attribute *attr ,
1814 char *buf )
1815{ struct led_classdev *led ;
1816 void *tmp ;
1817 struct gpio_trig_data *gpio_data ;
1818 int tmp___0 ;
1819 struct device const *__cil_tmp8 ;
1820 unsigned long __cil_tmp9 ;
1821 unsigned long __cil_tmp10 ;
1822 void *__cil_tmp11 ;
1823 unsigned long __cil_tmp12 ;
1824 unsigned long __cil_tmp13 ;
1825 unsigned int __cil_tmp14 ;
1826
1827 {
1828 {
1829#line 134
1830 __cil_tmp8 = (struct device const *)dev;
1831#line 134
1832 tmp = dev_get_drvdata(__cil_tmp8);
1833#line 134
1834 led = (struct led_classdev *)tmp;
1835#line 135
1836 __cil_tmp9 = (unsigned long )led;
1837#line 135
1838 __cil_tmp10 = __cil_tmp9 + 256;
1839#line 135
1840 __cil_tmp11 = *((void **)__cil_tmp10);
1841#line 135
1842 gpio_data = (struct gpio_trig_data *)__cil_tmp11;
1843#line 137
1844 __cil_tmp12 = (unsigned long )gpio_data;
1845#line 137
1846 __cil_tmp13 = __cil_tmp12 + 48;
1847#line 137
1848 __cil_tmp14 = *((unsigned int *)__cil_tmp13);
1849#line 137
1850 tmp___0 = sprintf(buf, "%u\n", __cil_tmp14);
1851 }
1852#line 137
1853 return ((ssize_t )tmp___0);
1854}
1855}
1856#line 140 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
1857static ssize_t gpio_trig_gpio_store(struct device *dev , struct device_attribute *attr ,
1858 char const *buf , size_t n )
1859{ struct led_classdev *led ;
1860 void *tmp ;
1861 struct gpio_trig_data *gpio_data ;
1862 unsigned int gpio ;
1863 int ret ;
1864 int tmp___0 ;
1865 int tmp___1 ;
1866 int tmp___2 ;
1867 size_t tmp___3 ;
1868 struct device const *__cil_tmp14 ;
1869 unsigned long __cil_tmp15 ;
1870 unsigned long __cil_tmp16 ;
1871 void *__cil_tmp17 ;
1872 struct device const *__cil_tmp18 ;
1873 unsigned long __cil_tmp19 ;
1874 unsigned long __cil_tmp20 ;
1875 struct work_struct *__cil_tmp21 ;
1876 unsigned int *__cil_tmp22 ;
1877 unsigned int __cil_tmp23 ;
1878 unsigned long __cil_tmp24 ;
1879 unsigned long __cil_tmp25 ;
1880 unsigned int __cil_tmp26 ;
1881 unsigned int *__cil_tmp27 ;
1882 unsigned int __cil_tmp28 ;
1883 unsigned long __cil_tmp29 ;
1884 unsigned long __cil_tmp30 ;
1885 unsigned int __cil_tmp31 ;
1886 unsigned long __cil_tmp32 ;
1887 unsigned long __cil_tmp33 ;
1888 unsigned int __cil_tmp34 ;
1889 unsigned int __cil_tmp35 ;
1890 void *__cil_tmp36 ;
1891 unsigned long __cil_tmp37 ;
1892 unsigned long __cil_tmp38 ;
1893 unsigned int *__cil_tmp39 ;
1894 unsigned int __cil_tmp40 ;
1895 unsigned int __cil_tmp41 ;
1896 void *__cil_tmp42 ;
1897 struct device const *__cil_tmp43 ;
1898 unsigned long __cil_tmp44 ;
1899 unsigned long __cil_tmp45 ;
1900 unsigned int __cil_tmp46 ;
1901 unsigned long __cil_tmp47 ;
1902 unsigned long __cil_tmp48 ;
1903 unsigned int __cil_tmp49 ;
1904 unsigned int __cil_tmp50 ;
1905 void *__cil_tmp51 ;
1906 unsigned long __cil_tmp52 ;
1907 unsigned long __cil_tmp53 ;
1908 unsigned int *__cil_tmp54 ;
1909
1910 {
1911 {
1912#line 143
1913 __cil_tmp14 = (struct device const *)dev;
1914#line 143
1915 tmp = dev_get_drvdata(__cil_tmp14);
1916#line 143
1917 led = (struct led_classdev *)tmp;
1918#line 144
1919 __cil_tmp15 = (unsigned long )led;
1920#line 144
1921 __cil_tmp16 = __cil_tmp15 + 256;
1922#line 144
1923 __cil_tmp17 = *((void **)__cil_tmp16);
1924#line 144
1925 gpio_data = (struct gpio_trig_data *)__cil_tmp17;
1926#line 148
1927 ret = sscanf(buf, "%u", & gpio);
1928 }
1929#line 149
1930 if (ret < 1) {
1931 {
1932#line 150
1933 __cil_tmp18 = (struct device const *)dev;
1934#line 150
1935 dev_err(__cil_tmp18, "couldn\'t read gpio number\n");
1936#line 151
1937 __cil_tmp19 = (unsigned long )gpio_data;
1938#line 151
1939 __cil_tmp20 = __cil_tmp19 + 8;
1940#line 151
1941 __cil_tmp21 = (struct work_struct *)__cil_tmp20;
1942#line 151
1943 flush_work(__cil_tmp21);
1944 }
1945#line 152
1946 return ((ssize_t )-22);
1947 } else {
1948
1949 }
1950 {
1951#line 155
1952 __cil_tmp22 = & gpio;
1953#line 155
1954 __cil_tmp23 = *__cil_tmp22;
1955#line 155
1956 __cil_tmp24 = (unsigned long )gpio_data;
1957#line 155
1958 __cil_tmp25 = __cil_tmp24 + 48;
1959#line 155
1960 __cil_tmp26 = *((unsigned int *)__cil_tmp25);
1961#line 155
1962 if (__cil_tmp26 == __cil_tmp23) {
1963#line 156
1964 return ((ssize_t )n);
1965 } else {
1966
1967 }
1968 }
1969 {
1970#line 158
1971 __cil_tmp27 = & gpio;
1972#line 158
1973 __cil_tmp28 = *__cil_tmp27;
1974#line 158
1975 if (! __cil_tmp28) {
1976 {
1977#line 159
1978 __cil_tmp29 = (unsigned long )gpio_data;
1979#line 159
1980 __cil_tmp30 = __cil_tmp29 + 48;
1981#line 159
1982 __cil_tmp31 = *((unsigned int *)__cil_tmp30);
1983#line 159
1984 if (__cil_tmp31 != 0U) {
1985 {
1986#line 160
1987 __cil_tmp32 = (unsigned long )gpio_data;
1988#line 160
1989 __cil_tmp33 = __cil_tmp32 + 48;
1990#line 160
1991 __cil_tmp34 = *((unsigned int *)__cil_tmp33);
1992#line 160
1993 tmp___0 = gpio_to_irq(__cil_tmp34);
1994#line 160
1995 __cil_tmp35 = (unsigned int )tmp___0;
1996#line 160
1997 __cil_tmp36 = (void *)led;
1998#line 160
1999 free_irq(__cil_tmp35, __cil_tmp36);
2000 }
2001 } else {
2002
2003 }
2004 }
2005#line 161
2006 __cil_tmp37 = (unsigned long )gpio_data;
2007#line 161
2008 __cil_tmp38 = __cil_tmp37 + 48;
2009#line 161
2010 *((unsigned int *)__cil_tmp38) = 0U;
2011#line 162
2012 return ((ssize_t )n);
2013 } else {
2014
2015 }
2016 }
2017 {
2018#line 165
2019 __cil_tmp39 = & gpio;
2020#line 165
2021 __cil_tmp40 = *__cil_tmp39;
2022#line 165
2023 tmp___1 = gpio_to_irq(__cil_tmp40);
2024#line 165
2025 __cil_tmp41 = (unsigned int )tmp___1;
2026#line 165
2027 __cil_tmp42 = (void *)led;
2028#line 165
2029 ret = (int )request_irq(__cil_tmp41, & gpio_trig_irq, 131UL, "ledtrig-gpio", __cil_tmp42);
2030 }
2031#line 168
2032 if (ret) {
2033 {
2034#line 169
2035 __cil_tmp43 = (struct device const *)dev;
2036#line 169
2037 dev_err(__cil_tmp43, "request_irq failed with error %d\n", ret);
2038 }
2039 } else {
2040 {
2041#line 171
2042 __cil_tmp44 = (unsigned long )gpio_data;
2043#line 171
2044 __cil_tmp45 = __cil_tmp44 + 48;
2045#line 171
2046 __cil_tmp46 = *((unsigned int *)__cil_tmp45);
2047#line 171
2048 if (__cil_tmp46 != 0U) {
2049 {
2050#line 172
2051 __cil_tmp47 = (unsigned long )gpio_data;
2052#line 172
2053 __cil_tmp48 = __cil_tmp47 + 48;
2054#line 172
2055 __cil_tmp49 = *((unsigned int *)__cil_tmp48);
2056#line 172
2057 tmp___2 = gpio_to_irq(__cil_tmp49);
2058#line 172
2059 __cil_tmp50 = (unsigned int )tmp___2;
2060#line 172
2061 __cil_tmp51 = (void *)led;
2062#line 172
2063 free_irq(__cil_tmp50, __cil_tmp51);
2064 }
2065 } else {
2066
2067 }
2068 }
2069#line 173
2070 __cil_tmp52 = (unsigned long )gpio_data;
2071#line 173
2072 __cil_tmp53 = __cil_tmp52 + 48;
2073#line 173
2074 __cil_tmp54 = & gpio;
2075#line 173
2076 *((unsigned int *)__cil_tmp53) = *__cil_tmp54;
2077 }
2078#line 176
2079 if (ret) {
2080#line 176
2081 tmp___3 = (size_t )ret;
2082 } else {
2083#line 176
2084 tmp___3 = n;
2085 }
2086#line 176
2087 return ((ssize_t )tmp___3);
2088}
2089}
2090#line 178 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2091static struct device_attribute dev_attr_gpio = {{"gpio", (umode_t )420}, & gpio_trig_gpio_show, & gpio_trig_gpio_store};
2092#line 180 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2093static void gpio_trig_activate(struct led_classdev *led )
2094{ struct gpio_trig_data *gpio_data ;
2095 int ret ;
2096 void *tmp ;
2097 atomic_long_t __constr_expr_0 ;
2098 unsigned long __cil_tmp6 ;
2099 unsigned long __cil_tmp7 ;
2100 struct device *__cil_tmp8 ;
2101 struct device_attribute const *__cil_tmp9 ;
2102 unsigned long __cil_tmp10 ;
2103 unsigned long __cil_tmp11 ;
2104 struct device *__cil_tmp12 ;
2105 struct device_attribute const *__cil_tmp13 ;
2106 unsigned long __cil_tmp14 ;
2107 unsigned long __cil_tmp15 ;
2108 struct device *__cil_tmp16 ;
2109 struct device_attribute const *__cil_tmp17 ;
2110 unsigned long __cil_tmp18 ;
2111 unsigned long __cil_tmp19 ;
2112 unsigned long __cil_tmp20 ;
2113 unsigned long __cil_tmp21 ;
2114 struct work_struct *__cil_tmp22 ;
2115 unsigned long __cil_tmp23 ;
2116 unsigned long __cil_tmp24 ;
2117 unsigned long __cil_tmp25 ;
2118 unsigned long __cil_tmp26 ;
2119 unsigned long __cil_tmp27 ;
2120 struct list_head *__cil_tmp28 ;
2121 unsigned long __cil_tmp29 ;
2122 unsigned long __cil_tmp30 ;
2123 unsigned long __cil_tmp31 ;
2124 unsigned long __cil_tmp32 ;
2125 unsigned long __cil_tmp33 ;
2126 struct device *__cil_tmp34 ;
2127 struct device_attribute const *__cil_tmp35 ;
2128 unsigned long __cil_tmp36 ;
2129 unsigned long __cil_tmp37 ;
2130 struct device *__cil_tmp38 ;
2131 struct device_attribute const *__cil_tmp39 ;
2132 void const *__cil_tmp40 ;
2133 long __constr_expr_0_counter41 ;
2134
2135 {
2136 {
2137#line 185
2138 tmp = kzalloc(56UL, 208U);
2139#line 185
2140 gpio_data = (struct gpio_trig_data *)tmp;
2141 }
2142#line 186
2143 if (! gpio_data) {
2144#line 187
2145 return;
2146 } else {
2147
2148 }
2149 {
2150#line 189
2151 __cil_tmp6 = (unsigned long )led;
2152#line 189
2153 __cil_tmp7 = __cil_tmp6 + 48;
2154#line 189
2155 __cil_tmp8 = *((struct device **)__cil_tmp7);
2156#line 189
2157 __cil_tmp9 = (struct device_attribute const *)(& dev_attr_gpio);
2158#line 189
2159 ret = device_create_file(__cil_tmp8, __cil_tmp9);
2160 }
2161#line 190
2162 if (ret) {
2163#line 191
2164 goto err_gpio;
2165 } else {
2166
2167 }
2168 {
2169#line 193
2170 __cil_tmp10 = (unsigned long )led;
2171#line 193
2172 __cil_tmp11 = __cil_tmp10 + 48;
2173#line 193
2174 __cil_tmp12 = *((struct device **)__cil_tmp11);
2175#line 193
2176 __cil_tmp13 = (struct device_attribute const *)(& dev_attr_inverted);
2177#line 193
2178 ret = device_create_file(__cil_tmp12, __cil_tmp13);
2179 }
2180#line 194
2181 if (ret) {
2182#line 195
2183 goto err_inverted;
2184 } else {
2185
2186 }
2187 {
2188#line 197
2189 __cil_tmp14 = (unsigned long )led;
2190#line 197
2191 __cil_tmp15 = __cil_tmp14 + 48;
2192#line 197
2193 __cil_tmp16 = *((struct device **)__cil_tmp15);
2194#line 197
2195 __cil_tmp17 = (struct device_attribute const *)(& dev_attr_desired_brightness);
2196#line 197
2197 ret = device_create_file(__cil_tmp16, __cil_tmp17);
2198 }
2199#line 198
2200 if (ret) {
2201#line 199
2202 goto err_brightness;
2203 } else {
2204
2205 }
2206#line 201
2207 *((struct led_classdev **)gpio_data) = led;
2208#line 202
2209 __cil_tmp18 = (unsigned long )led;
2210#line 202
2211 __cil_tmp19 = __cil_tmp18 + 256;
2212#line 202
2213 *((void **)__cil_tmp19) = (void *)gpio_data;
2214 {
2215#line 203
2216 while (1) {
2217 while_continue: ;
2218 {
2219#line 203
2220 while (1) {
2221 while_continue___0: ;
2222 {
2223#line 203
2224 __cil_tmp20 = (unsigned long )gpio_data;
2225#line 203
2226 __cil_tmp21 = __cil_tmp20 + 8;
2227#line 203
2228 __cil_tmp22 = (struct work_struct *)__cil_tmp21;
2229#line 203
2230 __init_work(__cil_tmp22, 0);
2231#line 203
2232 __constr_expr_0_counter41 = 2097664L;
2233#line 203
2234 __cil_tmp23 = (unsigned long )gpio_data;
2235#line 203
2236 __cil_tmp24 = __cil_tmp23 + 8;
2237#line 203
2238 ((atomic_long_t *)__cil_tmp24)->counter = __constr_expr_0_counter41;
2239#line 203
2240 __cil_tmp25 = 8 + 8;
2241#line 203
2242 __cil_tmp26 = (unsigned long )gpio_data;
2243#line 203
2244 __cil_tmp27 = __cil_tmp26 + __cil_tmp25;
2245#line 203
2246 __cil_tmp28 = (struct list_head *)__cil_tmp27;
2247#line 203
2248 INIT_LIST_HEAD(__cil_tmp28);
2249 }
2250 {
2251#line 203
2252 while (1) {
2253 while_continue___1: ;
2254#line 203
2255 __cil_tmp29 = 8 + 24;
2256#line 203
2257 __cil_tmp30 = (unsigned long )gpio_data;
2258#line 203
2259 __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
2260#line 203
2261 *((void (**)(struct work_struct *work ))__cil_tmp31) = & gpio_trig_work;
2262#line 203
2263 goto while_break___1;
2264 }
2265 while_break___1: ;
2266 }
2267#line 203
2268 goto while_break___0;
2269 }
2270 while_break___0: ;
2271 }
2272#line 203
2273 goto while_break;
2274 }
2275 while_break: ;
2276 }
2277#line 205
2278 return;
2279 err_brightness:
2280 {
2281#line 208
2282 __cil_tmp32 = (unsigned long )led;
2283#line 208
2284 __cil_tmp33 = __cil_tmp32 + 48;
2285#line 208
2286 __cil_tmp34 = *((struct device **)__cil_tmp33);
2287#line 208
2288 __cil_tmp35 = (struct device_attribute const *)(& dev_attr_inverted);
2289#line 208
2290 device_remove_file(__cil_tmp34, __cil_tmp35);
2291 }
2292 err_inverted:
2293 {
2294#line 211
2295 __cil_tmp36 = (unsigned long )led;
2296#line 211
2297 __cil_tmp37 = __cil_tmp36 + 48;
2298#line 211
2299 __cil_tmp38 = *((struct device **)__cil_tmp37);
2300#line 211
2301 __cil_tmp39 = (struct device_attribute const *)(& dev_attr_gpio);
2302#line 211
2303 device_remove_file(__cil_tmp38, __cil_tmp39);
2304 }
2305 err_gpio:
2306 {
2307#line 214
2308 __cil_tmp40 = (void const *)gpio_data;
2309#line 214
2310 kfree(__cil_tmp40);
2311 }
2312#line 215
2313 return;
2314}
2315}
2316#line 217 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2317static void gpio_trig_deactivate(struct led_classdev *led )
2318{ struct gpio_trig_data *gpio_data ;
2319 int tmp ;
2320 unsigned long __cil_tmp4 ;
2321 unsigned long __cil_tmp5 ;
2322 void *__cil_tmp6 ;
2323 unsigned long __cil_tmp7 ;
2324 unsigned long __cil_tmp8 ;
2325 struct device *__cil_tmp9 ;
2326 struct device_attribute const *__cil_tmp10 ;
2327 unsigned long __cil_tmp11 ;
2328 unsigned long __cil_tmp12 ;
2329 struct device *__cil_tmp13 ;
2330 struct device_attribute const *__cil_tmp14 ;
2331 unsigned long __cil_tmp15 ;
2332 unsigned long __cil_tmp16 ;
2333 struct device *__cil_tmp17 ;
2334 struct device_attribute const *__cil_tmp18 ;
2335 unsigned long __cil_tmp19 ;
2336 unsigned long __cil_tmp20 ;
2337 struct work_struct *__cil_tmp21 ;
2338 unsigned long __cil_tmp22 ;
2339 unsigned long __cil_tmp23 ;
2340 unsigned int __cil_tmp24 ;
2341 unsigned long __cil_tmp25 ;
2342 unsigned long __cil_tmp26 ;
2343 unsigned int __cil_tmp27 ;
2344 unsigned int __cil_tmp28 ;
2345 void *__cil_tmp29 ;
2346 void const *__cil_tmp30 ;
2347
2348 {
2349#line 219
2350 __cil_tmp4 = (unsigned long )led;
2351#line 219
2352 __cil_tmp5 = __cil_tmp4 + 256;
2353#line 219
2354 __cil_tmp6 = *((void **)__cil_tmp5);
2355#line 219
2356 gpio_data = (struct gpio_trig_data *)__cil_tmp6;
2357#line 221
2358 if (gpio_data) {
2359 {
2360#line 222
2361 __cil_tmp7 = (unsigned long )led;
2362#line 222
2363 __cil_tmp8 = __cil_tmp7 + 48;
2364#line 222
2365 __cil_tmp9 = *((struct device **)__cil_tmp8);
2366#line 222
2367 __cil_tmp10 = (struct device_attribute const *)(& dev_attr_gpio);
2368#line 222
2369 device_remove_file(__cil_tmp9, __cil_tmp10);
2370#line 223
2371 __cil_tmp11 = (unsigned long )led;
2372#line 223
2373 __cil_tmp12 = __cil_tmp11 + 48;
2374#line 223
2375 __cil_tmp13 = *((struct device **)__cil_tmp12);
2376#line 223
2377 __cil_tmp14 = (struct device_attribute const *)(& dev_attr_inverted);
2378#line 223
2379 device_remove_file(__cil_tmp13, __cil_tmp14);
2380#line 224
2381 __cil_tmp15 = (unsigned long )led;
2382#line 224
2383 __cil_tmp16 = __cil_tmp15 + 48;
2384#line 224
2385 __cil_tmp17 = *((struct device **)__cil_tmp16);
2386#line 224
2387 __cil_tmp18 = (struct device_attribute const *)(& dev_attr_desired_brightness);
2388#line 224
2389 device_remove_file(__cil_tmp17, __cil_tmp18);
2390#line 225
2391 __cil_tmp19 = (unsigned long )gpio_data;
2392#line 225
2393 __cil_tmp20 = __cil_tmp19 + 8;
2394#line 225
2395 __cil_tmp21 = (struct work_struct *)__cil_tmp20;
2396#line 225
2397 flush_work(__cil_tmp21);
2398 }
2399 {
2400#line 226
2401 __cil_tmp22 = (unsigned long )gpio_data;
2402#line 226
2403 __cil_tmp23 = __cil_tmp22 + 48;
2404#line 226
2405 __cil_tmp24 = *((unsigned int *)__cil_tmp23);
2406#line 226
2407 if (__cil_tmp24 != 0U) {
2408 {
2409#line 227
2410 __cil_tmp25 = (unsigned long )gpio_data;
2411#line 227
2412 __cil_tmp26 = __cil_tmp25 + 48;
2413#line 227
2414 __cil_tmp27 = *((unsigned int *)__cil_tmp26);
2415#line 227
2416 tmp = gpio_to_irq(__cil_tmp27);
2417#line 227
2418 __cil_tmp28 = (unsigned int )tmp;
2419#line 227
2420 __cil_tmp29 = (void *)led;
2421#line 227
2422 free_irq(__cil_tmp28, __cil_tmp29);
2423 }
2424 } else {
2425
2426 }
2427 }
2428 {
2429#line 228
2430 __cil_tmp30 = (void const *)gpio_data;
2431#line 228
2432 kfree(__cil_tmp30);
2433 }
2434 } else {
2435
2436 }
2437#line 230
2438 return;
2439}
2440}
2441#line 232 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2442static struct led_trigger gpio_led_trigger = {"gpio", & gpio_trig_activate, & gpio_trig_deactivate, {{0LL}, 0U, 0U, (void *)0},
2443 {(struct list_head *)0, (struct list_head *)0}, {(struct list_head *)0, (struct list_head *)0}};
2444#line 238
2445static int gpio_trig_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
2446#line 238 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2447static int gpio_trig_init(void)
2448{ int tmp ;
2449
2450 {
2451 {
2452#line 240
2453 tmp = led_trigger_register(& gpio_led_trigger);
2454 }
2455#line 240
2456 return (tmp);
2457}
2458}
2459#line 242 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2460int init_module(void)
2461{ int tmp ;
2462
2463 {
2464 {
2465#line 242
2466 tmp = gpio_trig_init();
2467 }
2468#line 242
2469 return (tmp);
2470}
2471}
2472#line 244
2473static void gpio_trig_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
2474#line 244 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2475static void gpio_trig_exit(void)
2476{
2477
2478 {
2479 {
2480#line 246
2481 led_trigger_unregister(& gpio_led_trigger);
2482 }
2483#line 247
2484 return;
2485}
2486}
2487#line 248 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2488void cleanup_module(void)
2489{
2490
2491 {
2492 {
2493#line 248
2494 gpio_trig_exit();
2495 }
2496#line 248
2497 return;
2498}
2499}
2500#line 250 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2501static char const __mod_author250[41] __attribute__((__used__, __unused__, __section__(".modinfo"),
2502__aligned__(1))) =
2503#line 250
2504 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
2505 (char const )'o', (char const )'r', (char const )'=', (char const )'F',
2506 (char const )'e', (char const )'l', (char const )'i', (char const )'p',
2507 (char const )'e', (char const )' ', (char const )'B', (char const )'a',
2508 (char const )'l', (char const )'b', (char const )'i', (char const )' ',
2509 (char const )'<', (char const )'m', (char const )'e', (char const )'@',
2510 (char const )'f', (char const )'e', (char const )'l', (char const )'i',
2511 (char const )'p', (char const )'e', (char const )'b', (char const )'a',
2512 (char const )'l', (char const )'b', (char const )'i', (char const )'.',
2513 (char const )'c', (char const )'o', (char const )'m', (char const )'>',
2514 (char const )'\000'};
2515#line 251 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2516static char const __mod_description251[29] __attribute__((__used__, __unused__,
2517__section__(".modinfo"), __aligned__(1))) =
2518#line 251
2519 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
2520 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
2521 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
2522 (char const )'G', (char const )'P', (char const )'I', (char const )'O',
2523 (char const )' ', (char const )'L', (char const )'E', (char const )'D',
2524 (char const )' ', (char const )'t', (char const )'r', (char const )'i',
2525 (char const )'g', (char const )'g', (char const )'e', (char const )'r',
2526 (char const )'\000'};
2527#line 252 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2528static char const __mod_license252[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
2529__aligned__(1))) =
2530#line 252
2531 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
2532 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
2533 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
2534#line 270
2535void ldv_check_final_state(void) ;
2536#line 276
2537extern void ldv_initialize(void) ;
2538#line 279
2539extern int __VERIFIER_nondet_int(void) ;
2540#line 282 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2541int LDV_IN_INTERRUPT ;
2542#line 285 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2543void main(void)
2544{ struct led_classdev *var_group1 ;
2545 int var_gpio_trig_irq_0_p0 ;
2546 void *var_gpio_trig_irq_0_p1 ;
2547 int tmp ;
2548 int tmp___0 ;
2549 int tmp___1 ;
2550
2551 {
2552 {
2553#line 313
2554 LDV_IN_INTERRUPT = 1;
2555#line 322
2556 ldv_initialize();
2557#line 328
2558 tmp = gpio_trig_init();
2559 }
2560#line 328
2561 if (tmp) {
2562#line 329
2563 goto ldv_final;
2564 } else {
2565
2566 }
2567 {
2568#line 335
2569 while (1) {
2570 while_continue: ;
2571 {
2572#line 335
2573 tmp___1 = __VERIFIER_nondet_int();
2574 }
2575#line 335
2576 if (tmp___1) {
2577
2578 } else {
2579#line 335
2580 goto while_break;
2581 }
2582 {
2583#line 338
2584 tmp___0 = __VERIFIER_nondet_int();
2585 }
2586#line 340
2587 if (tmp___0 == 0) {
2588#line 340
2589 goto case_0;
2590 } else
2591#line 356
2592 if (tmp___0 == 1) {
2593#line 356
2594 goto case_1;
2595 } else
2596#line 372
2597 if (tmp___0 == 2) {
2598#line 372
2599 goto case_2;
2600 } else {
2601 {
2602#line 388
2603 goto switch_default;
2604#line 338
2605 if (0) {
2606 case_0:
2607 {
2608#line 348
2609 gpio_trig_activate(var_group1);
2610 }
2611#line 355
2612 goto switch_break;
2613 case_1:
2614 {
2615#line 364
2616 gpio_trig_deactivate(var_group1);
2617 }
2618#line 371
2619 goto switch_break;
2620 case_2:
2621 {
2622#line 375
2623 LDV_IN_INTERRUPT = 2;
2624#line 380
2625 gpio_trig_irq(var_gpio_trig_irq_0_p0, var_gpio_trig_irq_0_p1);
2626#line 381
2627 LDV_IN_INTERRUPT = 1;
2628 }
2629#line 387
2630 goto switch_break;
2631 switch_default:
2632#line 388
2633 goto switch_break;
2634 } else {
2635 switch_break: ;
2636 }
2637 }
2638 }
2639 }
2640 while_break: ;
2641 }
2642 {
2643#line 400
2644 gpio_trig_exit();
2645 }
2646 ldv_final:
2647 {
2648#line 403
2649 ldv_check_final_state();
2650 }
2651#line 406
2652 return;
2653}
2654}
2655#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
2656void ldv_blast_assert(void)
2657{
2658
2659 {
2660 ERROR:
2661#line 6
2662 goto ERROR;
2663}
2664}
2665#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
2666extern int __VERIFIER_nondet_int(void) ;
2667#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2668int ldv_mutex = 1;
2669#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2670int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
2671{ int nondetermined ;
2672
2673 {
2674#line 29
2675 if (ldv_mutex == 1) {
2676
2677 } else {
2678 {
2679#line 29
2680 ldv_blast_assert();
2681 }
2682 }
2683 {
2684#line 32
2685 nondetermined = __VERIFIER_nondet_int();
2686 }
2687#line 35
2688 if (nondetermined) {
2689#line 38
2690 ldv_mutex = 2;
2691#line 40
2692 return (0);
2693 } else {
2694#line 45
2695 return (-4);
2696 }
2697}
2698}
2699#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2700int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
2701{ int nondetermined ;
2702
2703 {
2704#line 57
2705 if (ldv_mutex == 1) {
2706
2707 } else {
2708 {
2709#line 57
2710 ldv_blast_assert();
2711 }
2712 }
2713 {
2714#line 60
2715 nondetermined = __VERIFIER_nondet_int();
2716 }
2717#line 63
2718 if (nondetermined) {
2719#line 66
2720 ldv_mutex = 2;
2721#line 68
2722 return (0);
2723 } else {
2724#line 73
2725 return (-4);
2726 }
2727}
2728}
2729#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2730int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
2731{ int atomic_value_after_dec ;
2732
2733 {
2734#line 83
2735 if (ldv_mutex == 1) {
2736
2737 } else {
2738 {
2739#line 83
2740 ldv_blast_assert();
2741 }
2742 }
2743 {
2744#line 86
2745 atomic_value_after_dec = __VERIFIER_nondet_int();
2746 }
2747#line 89
2748 if (atomic_value_after_dec == 0) {
2749#line 92
2750 ldv_mutex = 2;
2751#line 94
2752 return (1);
2753 } else {
2754
2755 }
2756#line 98
2757 return (0);
2758}
2759}
2760#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2761void mutex_lock(struct mutex *lock )
2762{
2763
2764 {
2765#line 108
2766 if (ldv_mutex == 1) {
2767
2768 } else {
2769 {
2770#line 108
2771 ldv_blast_assert();
2772 }
2773 }
2774#line 110
2775 ldv_mutex = 2;
2776#line 111
2777 return;
2778}
2779}
2780#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2781int mutex_trylock(struct mutex *lock )
2782{ int nondetermined ;
2783
2784 {
2785#line 121
2786 if (ldv_mutex == 1) {
2787
2788 } else {
2789 {
2790#line 121
2791 ldv_blast_assert();
2792 }
2793 }
2794 {
2795#line 124
2796 nondetermined = __VERIFIER_nondet_int();
2797 }
2798#line 127
2799 if (nondetermined) {
2800#line 130
2801 ldv_mutex = 2;
2802#line 132
2803 return (1);
2804 } else {
2805#line 137
2806 return (0);
2807 }
2808}
2809}
2810#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2811void mutex_unlock(struct mutex *lock )
2812{
2813
2814 {
2815#line 147
2816 if (ldv_mutex == 2) {
2817
2818 } else {
2819 {
2820#line 147
2821 ldv_blast_assert();
2822 }
2823 }
2824#line 149
2825 ldv_mutex = 1;
2826#line 150
2827 return;
2828}
2829}
2830#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2831void ldv_check_final_state(void)
2832{
2833
2834 {
2835#line 156
2836 if (ldv_mutex == 1) {
2837
2838 } else {
2839 {
2840#line 156
2841 ldv_blast_assert();
2842 }
2843 }
2844#line 157
2845 return;
2846}
2847}
2848#line 415 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12615/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-gpio.c.common.c"
2849long s__builtin_expect(long val , long res )
2850{
2851
2852 {
2853#line 416
2854 return (val);
2855}
2856}