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