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 206 "include/linux/types.h"
49typedef u64 phys_addr_t;
50#line 211 "include/linux/types.h"
51typedef phys_addr_t resource_size_t;
52#line 219 "include/linux/types.h"
53struct __anonstruct_atomic_t_7 {
54 int counter ;
55};
56#line 219 "include/linux/types.h"
57typedef struct __anonstruct_atomic_t_7 atomic_t;
58#line 224 "include/linux/types.h"
59struct __anonstruct_atomic64_t_8 {
60 long counter ;
61};
62#line 224 "include/linux/types.h"
63typedef struct __anonstruct_atomic64_t_8 atomic64_t;
64#line 229 "include/linux/types.h"
65struct list_head {
66 struct list_head *next ;
67 struct list_head *prev ;
68};
69#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
70struct module;
71#line 56
72struct module;
73#line 146 "include/linux/init.h"
74typedef void (*ctor_fn_t)(void);
75#line 47 "include/linux/dynamic_debug.h"
76struct device;
77#line 47
78struct device;
79#line 135 "include/linux/kernel.h"
80struct completion;
81#line 135
82struct completion;
83#line 18 "include/linux/ioport.h"
84struct resource {
85 resource_size_t start ;
86 resource_size_t end ;
87 char const *name ;
88 unsigned long flags ;
89 struct resource *parent ;
90 struct resource *sibling ;
91 struct resource *child ;
92};
93#line 202
94struct device;
95#line 12 "include/linux/lockdep.h"
96struct task_struct;
97#line 12
98struct task_struct;
99#line 20 "include/linux/kobject_ns.h"
100struct sock;
101#line 20
102struct sock;
103#line 21
104struct kobject;
105#line 21
106struct kobject;
107#line 27
108enum kobj_ns_type {
109 KOBJ_NS_TYPE_NONE = 0,
110 KOBJ_NS_TYPE_NET = 1,
111 KOBJ_NS_TYPES = 2
112} ;
113#line 40 "include/linux/kobject_ns.h"
114struct kobj_ns_type_operations {
115 enum kobj_ns_type type ;
116 void *(*grab_current_ns)(void) ;
117 void const *(*netlink_ns)(struct sock *sk ) ;
118 void const *(*initial_ns)(void) ;
119 void (*drop_ns)(void * ) ;
120};
121#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
122struct task_struct;
123#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
124struct file;
125#line 295
126struct file;
127#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
128struct task_struct;
129#line 329
130struct arch_spinlock;
131#line 329
132struct arch_spinlock;
133#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
134struct task_struct;
135#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
136struct task_struct;
137#line 10 "include/asm-generic/bug.h"
138struct bug_entry {
139 int bug_addr_disp ;
140 int file_disp ;
141 unsigned short line ;
142 unsigned short flags ;
143};
144#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
145struct static_key;
146#line 234
147struct static_key;
148#line 23 "include/asm-generic/atomic-long.h"
149typedef atomic64_t atomic_long_t;
150#line 22 "include/linux/sysfs.h"
151struct kobject;
152#line 23
153struct module;
154#line 24
155enum kobj_ns_type;
156#line 26 "include/linux/sysfs.h"
157struct attribute {
158 char const *name ;
159 umode_t mode ;
160};
161#line 56 "include/linux/sysfs.h"
162struct attribute_group {
163 char const *name ;
164 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
165 struct attribute **attrs ;
166};
167#line 85
168struct file;
169#line 86
170struct vm_area_struct;
171#line 86
172struct vm_area_struct;
173#line 88 "include/linux/sysfs.h"
174struct bin_attribute {
175 struct attribute attr ;
176 size_t size ;
177 void *private ;
178 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
179 loff_t , size_t ) ;
180 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
181 loff_t , size_t ) ;
182 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
183};
184#line 112 "include/linux/sysfs.h"
185struct sysfs_ops {
186 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
187 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
188 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
189};
190#line 118
191struct sysfs_dirent;
192#line 118
193struct sysfs_dirent;
194#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
195struct task_struct;
196#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
197typedef u16 __ticket_t;
198#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
199typedef u32 __ticketpair_t;
200#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
201struct __raw_tickets {
202 __ticket_t head ;
203 __ticket_t tail ;
204};
205#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
206union __anonunion____missing_field_name_36 {
207 __ticketpair_t head_tail ;
208 struct __raw_tickets tickets ;
209};
210#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
211struct arch_spinlock {
212 union __anonunion____missing_field_name_36 __annonCompField17 ;
213};
214#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
215typedef struct arch_spinlock arch_spinlock_t;
216#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
217struct __anonstruct____missing_field_name_38 {
218 u32 read ;
219 s32 write ;
220};
221#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
222union __anonunion_arch_rwlock_t_37 {
223 s64 lock ;
224 struct __anonstruct____missing_field_name_38 __annonCompField18 ;
225};
226#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
227typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
228#line 20 "include/linux/spinlock_types.h"
229struct raw_spinlock {
230 arch_spinlock_t raw_lock ;
231 unsigned int magic ;
232 unsigned int owner_cpu ;
233 void *owner ;
234};
235#line 20 "include/linux/spinlock_types.h"
236typedef struct raw_spinlock raw_spinlock_t;
237#line 64 "include/linux/spinlock_types.h"
238union __anonunion____missing_field_name_39 {
239 struct raw_spinlock rlock ;
240};
241#line 64 "include/linux/spinlock_types.h"
242struct spinlock {
243 union __anonunion____missing_field_name_39 __annonCompField19 ;
244};
245#line 64 "include/linux/spinlock_types.h"
246typedef struct spinlock spinlock_t;
247#line 11 "include/linux/rwlock_types.h"
248struct __anonstruct_rwlock_t_40 {
249 arch_rwlock_t raw_lock ;
250 unsigned int magic ;
251 unsigned int owner_cpu ;
252 void *owner ;
253};
254#line 11 "include/linux/rwlock_types.h"
255typedef struct __anonstruct_rwlock_t_40 rwlock_t;
256#line 22 "include/linux/kref.h"
257struct kref {
258 atomic_t refcount ;
259};
260#line 49 "include/linux/wait.h"
261struct __wait_queue_head {
262 spinlock_t lock ;
263 struct list_head task_list ;
264};
265#line 53 "include/linux/wait.h"
266typedef struct __wait_queue_head wait_queue_head_t;
267#line 55
268struct task_struct;
269#line 60 "include/linux/kobject.h"
270struct kset;
271#line 60
272struct kobj_type;
273#line 60 "include/linux/kobject.h"
274struct kobject {
275 char const *name ;
276 struct list_head entry ;
277 struct kobject *parent ;
278 struct kset *kset ;
279 struct kobj_type *ktype ;
280 struct sysfs_dirent *sd ;
281 struct kref kref ;
282 unsigned int state_initialized : 1 ;
283 unsigned int state_in_sysfs : 1 ;
284 unsigned int state_add_uevent_sent : 1 ;
285 unsigned int state_remove_uevent_sent : 1 ;
286 unsigned int uevent_suppress : 1 ;
287};
288#line 108 "include/linux/kobject.h"
289struct kobj_type {
290 void (*release)(struct kobject *kobj ) ;
291 struct sysfs_ops const *sysfs_ops ;
292 struct attribute **default_attrs ;
293 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
294 void const *(*namespace)(struct kobject *kobj ) ;
295};
296#line 116 "include/linux/kobject.h"
297struct kobj_uevent_env {
298 char *envp[32] ;
299 int envp_idx ;
300 char buf[2048] ;
301 int buflen ;
302};
303#line 123 "include/linux/kobject.h"
304struct kset_uevent_ops {
305 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
306 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
307 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
308};
309#line 140
310struct sock;
311#line 159 "include/linux/kobject.h"
312struct kset {
313 struct list_head list ;
314 spinlock_t list_lock ;
315 struct kobject kobj ;
316 struct kset_uevent_ops const *uevent_ops ;
317};
318#line 19 "include/linux/klist.h"
319struct klist_node;
320#line 19
321struct klist_node;
322#line 39 "include/linux/klist.h"
323struct klist_node {
324 void *n_klist ;
325 struct list_head n_node ;
326 struct kref n_ref ;
327};
328#line 48 "include/linux/mutex.h"
329struct mutex {
330 atomic_t count ;
331 spinlock_t wait_lock ;
332 struct list_head wait_list ;
333 struct task_struct *owner ;
334 char const *name ;
335 void *magic ;
336};
337#line 46 "include/linux/ktime.h"
338union ktime {
339 s64 tv64 ;
340};
341#line 59 "include/linux/ktime.h"
342typedef union ktime ktime_t;
343#line 10 "include/linux/timer.h"
344struct tvec_base;
345#line 10
346struct tvec_base;
347#line 12 "include/linux/timer.h"
348struct timer_list {
349 struct list_head entry ;
350 unsigned long expires ;
351 struct tvec_base *base ;
352 void (*function)(unsigned long ) ;
353 unsigned long data ;
354 int slack ;
355 int start_pid ;
356 void *start_site ;
357 char start_comm[16] ;
358};
359#line 17 "include/linux/workqueue.h"
360struct work_struct;
361#line 17
362struct work_struct;
363#line 79 "include/linux/workqueue.h"
364struct work_struct {
365 atomic_long_t data ;
366 struct list_head entry ;
367 void (*func)(struct work_struct *work ) ;
368};
369#line 25 "include/linux/completion.h"
370struct completion {
371 unsigned int done ;
372 wait_queue_head_t wait ;
373};
374#line 42 "include/linux/pm.h"
375struct device;
376#line 50 "include/linux/pm.h"
377struct pm_message {
378 int event ;
379};
380#line 50 "include/linux/pm.h"
381typedef struct pm_message pm_message_t;
382#line 264 "include/linux/pm.h"
383struct dev_pm_ops {
384 int (*prepare)(struct device *dev ) ;
385 void (*complete)(struct device *dev ) ;
386 int (*suspend)(struct device *dev ) ;
387 int (*resume)(struct device *dev ) ;
388 int (*freeze)(struct device *dev ) ;
389 int (*thaw)(struct device *dev ) ;
390 int (*poweroff)(struct device *dev ) ;
391 int (*restore)(struct device *dev ) ;
392 int (*suspend_late)(struct device *dev ) ;
393 int (*resume_early)(struct device *dev ) ;
394 int (*freeze_late)(struct device *dev ) ;
395 int (*thaw_early)(struct device *dev ) ;
396 int (*poweroff_late)(struct device *dev ) ;
397 int (*restore_early)(struct device *dev ) ;
398 int (*suspend_noirq)(struct device *dev ) ;
399 int (*resume_noirq)(struct device *dev ) ;
400 int (*freeze_noirq)(struct device *dev ) ;
401 int (*thaw_noirq)(struct device *dev ) ;
402 int (*poweroff_noirq)(struct device *dev ) ;
403 int (*restore_noirq)(struct device *dev ) ;
404 int (*runtime_suspend)(struct device *dev ) ;
405 int (*runtime_resume)(struct device *dev ) ;
406 int (*runtime_idle)(struct device *dev ) ;
407};
408#line 458
409enum rpm_status {
410 RPM_ACTIVE = 0,
411 RPM_RESUMING = 1,
412 RPM_SUSPENDED = 2,
413 RPM_SUSPENDING = 3
414} ;
415#line 480
416enum rpm_request {
417 RPM_REQ_NONE = 0,
418 RPM_REQ_IDLE = 1,
419 RPM_REQ_SUSPEND = 2,
420 RPM_REQ_AUTOSUSPEND = 3,
421 RPM_REQ_RESUME = 4
422} ;
423#line 488
424struct wakeup_source;
425#line 488
426struct wakeup_source;
427#line 495 "include/linux/pm.h"
428struct pm_subsys_data {
429 spinlock_t lock ;
430 unsigned int refcount ;
431};
432#line 506
433struct dev_pm_qos_request;
434#line 506
435struct pm_qos_constraints;
436#line 506 "include/linux/pm.h"
437struct dev_pm_info {
438 pm_message_t power_state ;
439 unsigned int can_wakeup : 1 ;
440 unsigned int async_suspend : 1 ;
441 bool is_prepared : 1 ;
442 bool is_suspended : 1 ;
443 bool ignore_children : 1 ;
444 spinlock_t lock ;
445 struct list_head entry ;
446 struct completion completion ;
447 struct wakeup_source *wakeup ;
448 bool wakeup_path : 1 ;
449 struct timer_list suspend_timer ;
450 unsigned long timer_expires ;
451 struct work_struct work ;
452 wait_queue_head_t wait_queue ;
453 atomic_t usage_count ;
454 atomic_t child_count ;
455 unsigned int disable_depth : 3 ;
456 unsigned int idle_notification : 1 ;
457 unsigned int request_pending : 1 ;
458 unsigned int deferred_resume : 1 ;
459 unsigned int run_wake : 1 ;
460 unsigned int runtime_auto : 1 ;
461 unsigned int no_callbacks : 1 ;
462 unsigned int irq_safe : 1 ;
463 unsigned int use_autosuspend : 1 ;
464 unsigned int timer_autosuspends : 1 ;
465 enum rpm_request request ;
466 enum rpm_status runtime_status ;
467 int runtime_error ;
468 int autosuspend_delay ;
469 unsigned long last_busy ;
470 unsigned long active_jiffies ;
471 unsigned long suspended_jiffies ;
472 unsigned long accounting_timestamp ;
473 ktime_t suspend_time ;
474 s64 max_time_suspended_ns ;
475 struct dev_pm_qos_request *pq_req ;
476 struct pm_subsys_data *subsys_data ;
477 struct pm_qos_constraints *constraints ;
478};
479#line 564 "include/linux/pm.h"
480struct dev_pm_domain {
481 struct dev_pm_ops ops ;
482};
483#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
484struct dma_map_ops;
485#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
486struct dev_archdata {
487 void *acpi_handle ;
488 struct dma_map_ops *dma_ops ;
489 void *iommu ;
490};
491#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
492struct pdev_archdata {
493
494};
495#line 28 "include/linux/device.h"
496struct device;
497#line 29
498struct device_private;
499#line 29
500struct device_private;
501#line 30
502struct device_driver;
503#line 30
504struct device_driver;
505#line 31
506struct driver_private;
507#line 31
508struct driver_private;
509#line 32
510struct module;
511#line 33
512struct class;
513#line 33
514struct class;
515#line 34
516struct subsys_private;
517#line 34
518struct subsys_private;
519#line 35
520struct bus_type;
521#line 35
522struct bus_type;
523#line 36
524struct device_node;
525#line 36
526struct device_node;
527#line 37
528struct iommu_ops;
529#line 37
530struct iommu_ops;
531#line 39 "include/linux/device.h"
532struct bus_attribute {
533 struct attribute attr ;
534 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
535 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
536};
537#line 89
538struct device_attribute;
539#line 89
540struct driver_attribute;
541#line 89 "include/linux/device.h"
542struct bus_type {
543 char const *name ;
544 char const *dev_name ;
545 struct device *dev_root ;
546 struct bus_attribute *bus_attrs ;
547 struct device_attribute *dev_attrs ;
548 struct driver_attribute *drv_attrs ;
549 int (*match)(struct device *dev , struct device_driver *drv ) ;
550 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
551 int (*probe)(struct device *dev ) ;
552 int (*remove)(struct device *dev ) ;
553 void (*shutdown)(struct device *dev ) ;
554 int (*suspend)(struct device *dev , pm_message_t state ) ;
555 int (*resume)(struct device *dev ) ;
556 struct dev_pm_ops const *pm ;
557 struct iommu_ops *iommu_ops ;
558 struct subsys_private *p ;
559};
560#line 127
561struct device_type;
562#line 214
563struct of_device_id;
564#line 214 "include/linux/device.h"
565struct device_driver {
566 char const *name ;
567 struct bus_type *bus ;
568 struct module *owner ;
569 char const *mod_name ;
570 bool suppress_bind_attrs ;
571 struct of_device_id const *of_match_table ;
572 int (*probe)(struct device *dev ) ;
573 int (*remove)(struct device *dev ) ;
574 void (*shutdown)(struct device *dev ) ;
575 int (*suspend)(struct device *dev , pm_message_t state ) ;
576 int (*resume)(struct device *dev ) ;
577 struct attribute_group const **groups ;
578 struct dev_pm_ops const *pm ;
579 struct driver_private *p ;
580};
581#line 249 "include/linux/device.h"
582struct driver_attribute {
583 struct attribute attr ;
584 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
585 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
586};
587#line 330
588struct class_attribute;
589#line 330 "include/linux/device.h"
590struct class {
591 char const *name ;
592 struct module *owner ;
593 struct class_attribute *class_attrs ;
594 struct device_attribute *dev_attrs ;
595 struct bin_attribute *dev_bin_attrs ;
596 struct kobject *dev_kobj ;
597 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
598 char *(*devnode)(struct device *dev , umode_t *mode ) ;
599 void (*class_release)(struct class *class ) ;
600 void (*dev_release)(struct device *dev ) ;
601 int (*suspend)(struct device *dev , pm_message_t state ) ;
602 int (*resume)(struct device *dev ) ;
603 struct kobj_ns_type_operations const *ns_type ;
604 void const *(*namespace)(struct device *dev ) ;
605 struct dev_pm_ops const *pm ;
606 struct subsys_private *p ;
607};
608#line 397 "include/linux/device.h"
609struct class_attribute {
610 struct attribute attr ;
611 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
612 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
613 size_t count ) ;
614 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ;
615};
616#line 465 "include/linux/device.h"
617struct device_type {
618 char const *name ;
619 struct attribute_group const **groups ;
620 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
621 char *(*devnode)(struct device *dev , umode_t *mode ) ;
622 void (*release)(struct device *dev ) ;
623 struct dev_pm_ops const *pm ;
624};
625#line 476 "include/linux/device.h"
626struct device_attribute {
627 struct attribute attr ;
628 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
629 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
630 size_t count ) ;
631};
632#line 559 "include/linux/device.h"
633struct device_dma_parameters {
634 unsigned int max_segment_size ;
635 unsigned long segment_boundary_mask ;
636};
637#line 627
638struct dma_coherent_mem;
639#line 627 "include/linux/device.h"
640struct device {
641 struct device *parent ;
642 struct device_private *p ;
643 struct kobject kobj ;
644 char const *init_name ;
645 struct device_type const *type ;
646 struct mutex mutex ;
647 struct bus_type *bus ;
648 struct device_driver *driver ;
649 void *platform_data ;
650 struct dev_pm_info power ;
651 struct dev_pm_domain *pm_domain ;
652 int numa_node ;
653 u64 *dma_mask ;
654 u64 coherent_dma_mask ;
655 struct device_dma_parameters *dma_parms ;
656 struct list_head dma_pools ;
657 struct dma_coherent_mem *dma_mem ;
658 struct dev_archdata archdata ;
659 struct device_node *of_node ;
660 dev_t devt ;
661 u32 id ;
662 spinlock_t devres_lock ;
663 struct list_head devres_head ;
664 struct klist_node knode_class ;
665 struct class *class ;
666 struct attribute_group const **groups ;
667 void (*release)(struct device *dev ) ;
668};
669#line 43 "include/linux/pm_wakeup.h"
670struct wakeup_source {
671 char const *name ;
672 struct list_head entry ;
673 spinlock_t lock ;
674 struct timer_list timer ;
675 unsigned long timer_expires ;
676 ktime_t total_time ;
677 ktime_t max_time ;
678 ktime_t last_time ;
679 unsigned long event_count ;
680 unsigned long active_count ;
681 unsigned long relax_count ;
682 unsigned long hit_count ;
683 unsigned int active : 1 ;
684};
685#line 12 "include/linux/mod_devicetable.h"
686typedef unsigned long kernel_ulong_t;
687#line 219 "include/linux/mod_devicetable.h"
688struct of_device_id {
689 char name[32] ;
690 char type[32] ;
691 char compatible[128] ;
692 void *data ;
693};
694#line 506 "include/linux/mod_devicetable.h"
695struct platform_device_id {
696 char name[20] ;
697 kernel_ulong_t driver_data __attribute__((__aligned__(sizeof(kernel_ulong_t )))) ;
698};
699#line 17 "include/linux/platform_device.h"
700struct mfd_cell;
701#line 17
702struct mfd_cell;
703#line 19 "include/linux/platform_device.h"
704struct platform_device {
705 char const *name ;
706 int id ;
707 struct device dev ;
708 u32 num_resources ;
709 struct resource *resource ;
710 struct platform_device_id const *id_entry ;
711 struct mfd_cell *mfd_cell ;
712 struct pdev_archdata archdata ;
713};
714#line 164 "include/linux/platform_device.h"
715struct platform_driver {
716 int (*probe)(struct platform_device * ) ;
717 int (*remove)(struct platform_device * ) ;
718 void (*shutdown)(struct platform_device * ) ;
719 int (*suspend)(struct platform_device * , pm_message_t state ) ;
720 int (*resume)(struct platform_device * ) ;
721 struct device_driver driver ;
722 struct platform_device_id const *id_table ;
723};
724#line 19 "include/linux/rwsem.h"
725struct rw_semaphore;
726#line 19
727struct rw_semaphore;
728#line 25 "include/linux/rwsem.h"
729struct rw_semaphore {
730 long count ;
731 raw_spinlock_t wait_lock ;
732 struct list_head wait_list ;
733};
734#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
735struct device;
736#line 8 "include/linux/vmalloc.h"
737struct vm_area_struct;
738#line 10 "include/linux/gfp.h"
739struct vm_area_struct;
740#line 20 "include/linux/leds.h"
741struct device;
742#line 25
743enum led_brightness {
744 LED_OFF = 0,
745 LED_HALF = 127,
746 LED_FULL = 255
747} ;
748#line 31
749struct led_trigger;
750#line 31 "include/linux/leds.h"
751struct led_classdev {
752 char const *name ;
753 int brightness ;
754 int max_brightness ;
755 int flags ;
756 void (*brightness_set)(struct led_classdev *led_cdev , enum led_brightness brightness ) ;
757 enum led_brightness (*brightness_get)(struct led_classdev *led_cdev ) ;
758 int (*blink_set)(struct led_classdev *led_cdev , unsigned long *delay_on , unsigned long *delay_off ) ;
759 struct device *dev ;
760 struct list_head node ;
761 char const *default_trigger ;
762 unsigned long blink_delay_on ;
763 unsigned long blink_delay_off ;
764 struct timer_list blink_timer ;
765 int blink_brightness ;
766 struct rw_semaphore trigger_lock ;
767 struct led_trigger *trigger ;
768 struct list_head trig_list ;
769 void *trigger_data ;
770};
771#line 122 "include/linux/leds.h"
772struct led_trigger {
773 char const *name ;
774 void (*activate)(struct led_classdev *led_cdev ) ;
775 void (*deactivate)(struct led_classdev *led_cdev ) ;
776 rwlock_t leddev_list_lock ;
777 struct list_head led_cdevs ;
778 struct list_head next_trig ;
779};
780#line 25 "include/linux/io.h"
781struct device;
782#line 29 "include/linux/sysctl.h"
783struct completion;
784#line 49 "include/linux/kmod.h"
785struct file;
786#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
787struct task_struct;
788#line 18 "include/linux/elf.h"
789typedef __u64 Elf64_Addr;
790#line 19 "include/linux/elf.h"
791typedef __u16 Elf64_Half;
792#line 23 "include/linux/elf.h"
793typedef __u32 Elf64_Word;
794#line 24 "include/linux/elf.h"
795typedef __u64 Elf64_Xword;
796#line 194 "include/linux/elf.h"
797struct elf64_sym {
798 Elf64_Word st_name ;
799 unsigned char st_info ;
800 unsigned char st_other ;
801 Elf64_Half st_shndx ;
802 Elf64_Addr st_value ;
803 Elf64_Xword st_size ;
804};
805#line 194 "include/linux/elf.h"
806typedef struct elf64_sym Elf64_Sym;
807#line 438
808struct file;
809#line 39 "include/linux/moduleparam.h"
810struct kernel_param;
811#line 39
812struct kernel_param;
813#line 41 "include/linux/moduleparam.h"
814struct kernel_param_ops {
815 int (*set)(char const *val , struct kernel_param const *kp ) ;
816 int (*get)(char *buffer , struct kernel_param const *kp ) ;
817 void (*free)(void *arg ) ;
818};
819#line 50
820struct kparam_string;
821#line 50
822struct kparam_array;
823#line 50 "include/linux/moduleparam.h"
824union __anonunion____missing_field_name_200 {
825 void *arg ;
826 struct kparam_string const *str ;
827 struct kparam_array const *arr ;
828};
829#line 50 "include/linux/moduleparam.h"
830struct kernel_param {
831 char const *name ;
832 struct kernel_param_ops const *ops ;
833 u16 perm ;
834 s16 level ;
835 union __anonunion____missing_field_name_200 __annonCompField32 ;
836};
837#line 63 "include/linux/moduleparam.h"
838struct kparam_string {
839 unsigned int maxlen ;
840 char *string ;
841};
842#line 69 "include/linux/moduleparam.h"
843struct kparam_array {
844 unsigned int max ;
845 unsigned int elemsize ;
846 unsigned int *num ;
847 struct kernel_param_ops const *ops ;
848 void *elem ;
849};
850#line 445
851struct module;
852#line 80 "include/linux/jump_label.h"
853struct module;
854#line 143 "include/linux/jump_label.h"
855struct static_key {
856 atomic_t enabled ;
857};
858#line 22 "include/linux/tracepoint.h"
859struct module;
860#line 23
861struct tracepoint;
862#line 23
863struct tracepoint;
864#line 25 "include/linux/tracepoint.h"
865struct tracepoint_func {
866 void *func ;
867 void *data ;
868};
869#line 30 "include/linux/tracepoint.h"
870struct tracepoint {
871 char const *name ;
872 struct static_key key ;
873 void (*regfunc)(void) ;
874 void (*unregfunc)(void) ;
875 struct tracepoint_func *funcs ;
876};
877#line 19 "include/linux/export.h"
878struct kernel_symbol {
879 unsigned long value ;
880 char const *name ;
881};
882#line 8 "include/asm-generic/module.h"
883struct mod_arch_specific {
884
885};
886#line 35 "include/linux/module.h"
887struct module;
888#line 37
889struct module_param_attrs;
890#line 37 "include/linux/module.h"
891struct module_kobject {
892 struct kobject kobj ;
893 struct module *mod ;
894 struct kobject *drivers_dir ;
895 struct module_param_attrs *mp ;
896};
897#line 44 "include/linux/module.h"
898struct module_attribute {
899 struct attribute attr ;
900 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
901 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
902 size_t count ) ;
903 void (*setup)(struct module * , char const * ) ;
904 int (*test)(struct module * ) ;
905 void (*free)(struct module * ) ;
906};
907#line 71
908struct exception_table_entry;
909#line 71
910struct exception_table_entry;
911#line 199
912enum module_state {
913 MODULE_STATE_LIVE = 0,
914 MODULE_STATE_COMING = 1,
915 MODULE_STATE_GOING = 2
916} ;
917#line 215 "include/linux/module.h"
918struct module_ref {
919 unsigned long incs ;
920 unsigned long decs ;
921} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
922#line 220
923struct module_sect_attrs;
924#line 220
925struct module_notes_attrs;
926#line 220
927struct ftrace_event_call;
928#line 220 "include/linux/module.h"
929struct module {
930 enum module_state state ;
931 struct list_head list ;
932 char name[64UL - sizeof(unsigned long )] ;
933 struct module_kobject mkobj ;
934 struct module_attribute *modinfo_attrs ;
935 char const *version ;
936 char const *srcversion ;
937 struct kobject *holders_dir ;
938 struct kernel_symbol const *syms ;
939 unsigned long const *crcs ;
940 unsigned int num_syms ;
941 struct kernel_param *kp ;
942 unsigned int num_kp ;
943 unsigned int num_gpl_syms ;
944 struct kernel_symbol const *gpl_syms ;
945 unsigned long const *gpl_crcs ;
946 struct kernel_symbol const *unused_syms ;
947 unsigned long const *unused_crcs ;
948 unsigned int num_unused_syms ;
949 unsigned int num_unused_gpl_syms ;
950 struct kernel_symbol const *unused_gpl_syms ;
951 unsigned long const *unused_gpl_crcs ;
952 struct kernel_symbol const *gpl_future_syms ;
953 unsigned long const *gpl_future_crcs ;
954 unsigned int num_gpl_future_syms ;
955 unsigned int num_exentries ;
956 struct exception_table_entry *extable ;
957 int (*init)(void) ;
958 void *module_init ;
959 void *module_core ;
960 unsigned int init_size ;
961 unsigned int core_size ;
962 unsigned int init_text_size ;
963 unsigned int core_text_size ;
964 unsigned int init_ro_size ;
965 unsigned int core_ro_size ;
966 struct mod_arch_specific arch ;
967 unsigned int taints ;
968 unsigned int num_bugs ;
969 struct list_head bug_list ;
970 struct bug_entry *bug_table ;
971 Elf64_Sym *symtab ;
972 Elf64_Sym *core_symtab ;
973 unsigned int num_symtab ;
974 unsigned int core_num_syms ;
975 char *strtab ;
976 char *core_strtab ;
977 struct module_sect_attrs *sect_attrs ;
978 struct module_notes_attrs *notes_attrs ;
979 char *args ;
980 void *percpu ;
981 unsigned int percpu_size ;
982 unsigned int num_tracepoints ;
983 struct tracepoint * const *tracepoints_ptrs ;
984 unsigned int num_trace_bprintk_fmt ;
985 char const **trace_bprintk_fmt_start ;
986 struct ftrace_event_call **trace_events ;
987 unsigned int num_trace_events ;
988 struct list_head source_list ;
989 struct list_head target_list ;
990 struct task_struct *waiter ;
991 void (*exit)(void) ;
992 struct module_ref *refptr ;
993 ctor_fn_t *ctors ;
994 unsigned int num_ctors ;
995};
996#line 20 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
997struct ot200_led {
998 struct led_classdev cdev ;
999 char const *name ;
1000 unsigned long port ;
1001 u8 mask ;
1002};
1003#line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1004struct __anonstruct_202 {
1005 int : 0 ;
1006};
1007#line 152 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1008struct __anonstruct_203 {
1009 int : 0 ;
1010};
1011#line 1 "<compiler builtins>"
1012long __builtin_expect(long val , long res ) ;
1013#line 32 "include/linux/spinlock_api_smp.h"
1014extern unsigned long _raw_spin_lock_irqsave(raw_spinlock_t *lock ) __attribute__((__section__(".spinlock.text"))) ;
1015#line 42
1016extern void _raw_spin_unlock_irqrestore(raw_spinlock_t *lock , unsigned long flags ) __attribute__((__section__(".spinlock.text"))) ;
1017#line 272 "include/linux/spinlock.h"
1018__inline static raw_spinlock_t *spinlock_check(spinlock_t *lock ) __attribute__((__no_instrument_function__)) ;
1019#line 272 "include/linux/spinlock.h"
1020__inline static raw_spinlock_t *spinlock_check(spinlock_t *lock )
1021{
1022
1023 {
1024#line 274
1025 return ((struct raw_spinlock *)lock);
1026}
1027}
1028#line 338
1029__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) __attribute__((__no_instrument_function__)) ;
1030#line 338 "include/linux/spinlock.h"
1031__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags )
1032{ struct raw_spinlock *__cil_tmp5 ;
1033
1034 {
1035 {
1036#line 340
1037 while (1) {
1038 while_continue: ;
1039 {
1040#line 340
1041 __cil_tmp5 = (struct raw_spinlock *)lock;
1042#line 340
1043 _raw_spin_unlock_irqrestore(__cil_tmp5, flags);
1044 }
1045#line 340
1046 goto while_break;
1047 }
1048 while_break: ;
1049 }
1050#line 341
1051 return;
1052}
1053}
1054#line 152 "include/linux/mutex.h"
1055void mutex_lock(struct mutex *lock ) ;
1056#line 153
1057int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
1058#line 154
1059int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
1060#line 168
1061int mutex_trylock(struct mutex *lock ) ;
1062#line 169
1063void mutex_unlock(struct mutex *lock ) ;
1064#line 170
1065int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1066#line 174 "include/linux/platform_device.h"
1067extern int platform_driver_register(struct platform_driver * ) ;
1068#line 175
1069extern void platform_driver_unregister(struct platform_driver * ) ;
1070#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1071__inline static void outb(unsigned char value , int port ) __attribute__((__no_instrument_function__)) ;
1072#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1073__inline static void outb(unsigned char value , int port )
1074{
1075
1076 {
1077#line 308
1078 __asm__ volatile ("out"
1079 "b"
1080 " %"
1081 "b"
1082 "0, %w1": : "a" (value), "Nd" (port));
1083#line 308
1084 return;
1085}
1086}
1087#line 79 "include/linux/leds.h"
1088extern int led_classdev_register(struct device *parent , struct led_classdev *led_cdev ) ;
1089#line 81
1090extern void led_classdev_unregister(struct led_classdev *led_cdev ) ;
1091#line 26 "include/linux/export.h"
1092extern struct module __this_module ;
1093#line 67 "include/linux/module.h"
1094int init_module(void) ;
1095#line 68
1096void cleanup_module(void) ;
1097#line 32 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1098static struct ot200_led leds[10] =
1099#line 32 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1100 { {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1101 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1102 unsigned long *delay_on ,
1103 unsigned long *delay_off ))0,
1104 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1105 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1106 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1107 (char)0, (char)0,
1108 (char)0, (char)0,
1109 (char)0, (char)0,
1110 (char)0, (char)0,
1111 (char)0, (char)0,
1112 (char)0, (char)0,
1113 (char)0, (char)0}},
1114 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1115 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1116 "led_run", 90UL, (u8 )1UL},
1117 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1118 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1119 unsigned long *delay_on ,
1120 unsigned long *delay_off ))0,
1121 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1122 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1123 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1124 (char)0, (char)0,
1125 (char)0, (char)0,
1126 (char)0, (char)0,
1127 (char)0, (char)0,
1128 (char)0, (char)0,
1129 (char)0, (char)0,
1130 (char)0, (char)0}},
1131 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1132 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1133 "led_init", 90UL, (u8 )(1UL << 1)},
1134 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1135 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1136 unsigned long *delay_on ,
1137 unsigned long *delay_off ))0,
1138 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1139 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1140 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1141 (char)0, (char)0,
1142 (char)0, (char)0,
1143 (char)0, (char)0,
1144 (char)0, (char)0,
1145 (char)0, (char)0,
1146 (char)0, (char)0,
1147 (char)0, (char)0}},
1148 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1149 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1150 "led_err", 90UL, (u8 )(1UL << 2)},
1151 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1152 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1153 unsigned long *delay_on ,
1154 unsigned long *delay_off ))0,
1155 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1156 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1157 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1158 (char)0, (char)0,
1159 (char)0, (char)0,
1160 (char)0, (char)0,
1161 (char)0, (char)0,
1162 (char)0, (char)0,
1163 (char)0, (char)0,
1164 (char)0, (char)0}},
1165 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1166 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1167 "led_1", 73UL, (u8 )(1UL << 7)},
1168 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1169 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1170 unsigned long *delay_on ,
1171 unsigned long *delay_off ))0,
1172 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1173 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1174 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1175 (char)0, (char)0,
1176 (char)0, (char)0,
1177 (char)0, (char)0,
1178 (char)0, (char)0,
1179 (char)0, (char)0,
1180 (char)0, (char)0,
1181 (char)0, (char)0}},
1182 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1183 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1184 "led_2", 73UL, (u8 )(1UL << 6)},
1185 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1186 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1187 unsigned long *delay_on ,
1188 unsigned long *delay_off ))0,
1189 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1190 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1191 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1192 (char)0, (char)0,
1193 (char)0, (char)0,
1194 (char)0, (char)0,
1195 (char)0, (char)0,
1196 (char)0, (char)0,
1197 (char)0, (char)0,
1198 (char)0, (char)0}},
1199 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1200 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1201 "led_3", 73UL, (u8 )(1UL << 5)},
1202 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1203 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1204 unsigned long *delay_on ,
1205 unsigned long *delay_off ))0,
1206 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1207 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1208 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1209 (char)0, (char)0,
1210 (char)0, (char)0,
1211 (char)0, (char)0,
1212 (char)0, (char)0,
1213 (char)0, (char)0,
1214 (char)0, (char)0,
1215 (char)0, (char)0}},
1216 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1217 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1218 "led_4", 73UL, (u8 )(1UL << 4)},
1219 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1220 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1221 unsigned long *delay_on ,
1222 unsigned long *delay_off ))0,
1223 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1224 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1225 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1226 (char)0, (char)0,
1227 (char)0, (char)0,
1228 (char)0, (char)0,
1229 (char)0, (char)0,
1230 (char)0, (char)0,
1231 (char)0, (char)0,
1232 (char)0, (char)0}},
1233 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1234 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1235 "led_5", 73UL, (u8 )(1UL << 3)},
1236 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1237 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1238 unsigned long *delay_on ,
1239 unsigned long *delay_off ))0,
1240 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1241 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1242 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1243 (char)0, (char)0,
1244 (char)0, (char)0,
1245 (char)0, (char)0,
1246 (char)0, (char)0,
1247 (char)0, (char)0,
1248 (char)0, (char)0,
1249 (char)0, (char)0}},
1250 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1251 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1252 "led_6", 73UL, (u8 )(1UL << 2)},
1253 {{(char const *)0, 0, 0, 0, (void (*)(struct led_classdev *led_cdev , enum led_brightness brightness ))0,
1254 (enum led_brightness (*)(struct led_classdev *led_cdev ))0, (int (*)(struct led_classdev *led_cdev ,
1255 unsigned long *delay_on ,
1256 unsigned long *delay_off ))0,
1257 (struct device *)0, {(struct list_head *)0, (struct list_head *)0}, (char const *)0,
1258 0UL, 0UL, {{(struct list_head *)0, (struct list_head *)0}, 0UL, (struct tvec_base *)0,
1259 (void (*)(unsigned long ))0, 0UL, 0, 0, (void *)0, {(char)0, (char)0,
1260 (char)0, (char)0,
1261 (char)0, (char)0,
1262 (char)0, (char)0,
1263 (char)0, (char)0,
1264 (char)0, (char)0,
1265 (char)0, (char)0,
1266 (char)0, (char)0}},
1267 0, {0L, {{{0U}}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}},
1268 (struct led_trigger *)0, {(struct list_head *)0, (struct list_head *)0}, (void *)0},
1269 "led_7", 73UL, (u8 )(1UL << 1)}};
1270#line 85 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1271static spinlock_t value_lock = {{{{{(__ticketpair_t )0}}, 3735899821U, 4294967295U, (void *)-1L}}};
1272#line 91 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1273static u8 leds_back ;
1274#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1275static u8 leds_front ;
1276#line 94 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1277static void ot200_led_brightness_set(struct led_classdev *led_cdev , enum led_brightness value )
1278{ struct ot200_led *led ;
1279 struct led_classdev const *__mptr ;
1280 u8 *val ;
1281 unsigned long flags ;
1282 raw_spinlock_t *tmp ;
1283 struct ot200_led *__cil_tmp10 ;
1284 struct led_classdev *__cil_tmp11 ;
1285 unsigned int __cil_tmp12 ;
1286 char *__cil_tmp13 ;
1287 char *__cil_tmp14 ;
1288 unsigned long __cil_tmp15 ;
1289 unsigned long __cil_tmp16 ;
1290 unsigned long __cil_tmp17 ;
1291 unsigned long __cil_tmp18 ;
1292 unsigned long __cil_tmp19 ;
1293 unsigned long __cil_tmp20 ;
1294 unsigned int __cil_tmp21 ;
1295 unsigned long __cil_tmp22 ;
1296 unsigned long __cil_tmp23 ;
1297 u8 __cil_tmp24 ;
1298 int __cil_tmp25 ;
1299 int __cil_tmp26 ;
1300 u8 __cil_tmp27 ;
1301 int __cil_tmp28 ;
1302 int __cil_tmp29 ;
1303 unsigned long __cil_tmp30 ;
1304 unsigned long __cil_tmp31 ;
1305 u8 __cil_tmp32 ;
1306 int __cil_tmp33 ;
1307 u8 __cil_tmp34 ;
1308 int __cil_tmp35 ;
1309 int __cil_tmp36 ;
1310 u8 __cil_tmp37 ;
1311 unsigned long __cil_tmp38 ;
1312 unsigned long __cil_tmp39 ;
1313 unsigned long __cil_tmp40 ;
1314 int __cil_tmp41 ;
1315
1316 {
1317#line 97
1318 __mptr = (struct led_classdev const *)led_cdev;
1319#line 97
1320 __cil_tmp10 = (struct ot200_led *)0;
1321#line 97
1322 __cil_tmp11 = (struct led_classdev *)__cil_tmp10;
1323#line 97
1324 __cil_tmp12 = (unsigned int )__cil_tmp11;
1325#line 97
1326 __cil_tmp13 = (char *)__mptr;
1327#line 97
1328 __cil_tmp14 = __cil_tmp13 - __cil_tmp12;
1329#line 97
1330 led = (struct ot200_led *)__cil_tmp14;
1331 {
1332#line 101
1333 while (1) {
1334 while_continue: ;
1335 {
1336#line 101
1337 while (1) {
1338 while_continue___0: ;
1339 {
1340#line 101
1341 tmp = spinlock_check(& value_lock);
1342#line 101
1343 flags = _raw_spin_lock_irqsave(tmp);
1344 }
1345#line 101
1346 goto while_break___0;
1347 }
1348 while_break___0: ;
1349 }
1350#line 101
1351 goto while_break;
1352 }
1353 while_break: ;
1354 }
1355 {
1356#line 103
1357 __cil_tmp15 = (unsigned long )led;
1358#line 103
1359 __cil_tmp16 = __cil_tmp15 + 272;
1360#line 103
1361 __cil_tmp17 = *((unsigned long *)__cil_tmp16);
1362#line 103
1363 if (__cil_tmp17 == 73UL) {
1364#line 104
1365 val = & leds_front;
1366 } else {
1367 {
1368#line 105
1369 __cil_tmp18 = (unsigned long )led;
1370#line 105
1371 __cil_tmp19 = __cil_tmp18 + 272;
1372#line 105
1373 __cil_tmp20 = *((unsigned long *)__cil_tmp19);
1374#line 105
1375 if (__cil_tmp20 == 90UL) {
1376#line 106
1377 val = & leds_back;
1378 } else {
1379 {
1380#line 108
1381 while (1) {
1382 while_continue___1: ;
1383#line 108
1384 __asm__ volatile ("1:\tud2\n"
1385 ".pushsection __bug_table,\"a\"\n"
1386 "2:\t.long 1b - 2b, %c0 - 2b\n"
1387 "\t.word %c1, 0\n"
1388 "\t.org 2b+%c2\n"
1389 ".popsection": : "i" ("/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"),
1390 "i" (108), "i" (12UL));
1391 {
1392#line 108
1393 while (1) {
1394 while_continue___2: ;
1395 }
1396 while_break___2: ;
1397 }
1398#line 108
1399 goto while_break___1;
1400 }
1401 while_break___1: ;
1402 }
1403 }
1404 }
1405 }
1406 }
1407 {
1408#line 110
1409 __cil_tmp21 = (unsigned int )value;
1410#line 110
1411 if (__cil_tmp21 == 0U) {
1412#line 111
1413 __cil_tmp22 = (unsigned long )led;
1414#line 111
1415 __cil_tmp23 = __cil_tmp22 + 280;
1416#line 111
1417 __cil_tmp24 = *((u8 *)__cil_tmp23);
1418#line 111
1419 __cil_tmp25 = (int )__cil_tmp24;
1420#line 111
1421 __cil_tmp26 = ~ __cil_tmp25;
1422#line 111
1423 __cil_tmp27 = *val;
1424#line 111
1425 __cil_tmp28 = (int )__cil_tmp27;
1426#line 111
1427 __cil_tmp29 = __cil_tmp28 & __cil_tmp26;
1428#line 111
1429 *val = (u8 )__cil_tmp29;
1430 } else {
1431#line 113
1432 __cil_tmp30 = (unsigned long )led;
1433#line 113
1434 __cil_tmp31 = __cil_tmp30 + 280;
1435#line 113
1436 __cil_tmp32 = *((u8 *)__cil_tmp31);
1437#line 113
1438 __cil_tmp33 = (int )__cil_tmp32;
1439#line 113
1440 __cil_tmp34 = *val;
1441#line 113
1442 __cil_tmp35 = (int )__cil_tmp34;
1443#line 113
1444 __cil_tmp36 = __cil_tmp35 | __cil_tmp33;
1445#line 113
1446 *val = (u8 )__cil_tmp36;
1447 }
1448 }
1449 {
1450#line 115
1451 __cil_tmp37 = *val;
1452#line 115
1453 __cil_tmp38 = (unsigned long )led;
1454#line 115
1455 __cil_tmp39 = __cil_tmp38 + 272;
1456#line 115
1457 __cil_tmp40 = *((unsigned long *)__cil_tmp39);
1458#line 115
1459 __cil_tmp41 = (int )__cil_tmp40;
1460#line 115
1461 outb(__cil_tmp37, __cil_tmp41);
1462#line 116
1463 spin_unlock_irqrestore(& value_lock, flags);
1464 }
1465#line 117
1466 return;
1467}
1468}
1469#line 119
1470static int ot200_led_probe(struct platform_device *pdev ) __attribute__((__section__(".devinit.text"),
1471__no_instrument_function__)) ;
1472#line 119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1473static int ot200_led_probe(struct platform_device *pdev )
1474{ int i ;
1475 int ret ;
1476 unsigned long __cil_tmp4 ;
1477 unsigned long __cil_tmp5 ;
1478 unsigned long __cil_tmp6 ;
1479 unsigned long __cil_tmp7 ;
1480 unsigned long __cil_tmp8 ;
1481 unsigned long __cil_tmp9 ;
1482 unsigned long __cil_tmp10 ;
1483 unsigned long __cil_tmp11 ;
1484 unsigned long __cil_tmp12 ;
1485 unsigned long __cil_tmp13 ;
1486 unsigned long __cil_tmp14 ;
1487 unsigned long __cil_tmp15 ;
1488 unsigned long __cil_tmp16 ;
1489 unsigned long __cil_tmp17 ;
1490 struct device *__cil_tmp18 ;
1491 unsigned long __cil_tmp19 ;
1492 unsigned long __cil_tmp20 ;
1493 struct led_classdev *__cil_tmp21 ;
1494 u8 *__cil_tmp22 ;
1495 u8 *__cil_tmp23 ;
1496 unsigned long __cil_tmp24 ;
1497 u8 *__cil_tmp25 ;
1498 u8 __cil_tmp26 ;
1499 u8 *__cil_tmp27 ;
1500 u8 __cil_tmp28 ;
1501 unsigned long __cil_tmp29 ;
1502 unsigned long __cil_tmp30 ;
1503 struct led_classdev *__cil_tmp31 ;
1504
1505 {
1506#line 124
1507 i = 0;
1508 {
1509#line 124
1510 while (1) {
1511 while_continue: ;
1512 {
1513#line 124
1514 __cil_tmp4 = 2880UL / 288UL;
1515#line 124
1516 __cil_tmp5 = __cil_tmp4 + 0UL;
1517#line 124
1518 __cil_tmp6 = (unsigned long )i;
1519#line 124
1520 if (__cil_tmp6 < __cil_tmp5) {
1521
1522 } else {
1523#line 124
1524 goto while_break;
1525 }
1526 }
1527 {
1528#line 126
1529 __cil_tmp7 = i * 288UL;
1530#line 126
1531 __cil_tmp8 = (unsigned long )(leds) + __cil_tmp7;
1532#line 126
1533 __cil_tmp9 = i * 288UL;
1534#line 126
1535 __cil_tmp10 = __cil_tmp9 + 264;
1536#line 126
1537 __cil_tmp11 = (unsigned long )(leds) + __cil_tmp10;
1538#line 126
1539 *((char const **)__cil_tmp8) = *((char const **)__cil_tmp11);
1540#line 127
1541 __cil_tmp12 = 0 + 24;
1542#line 127
1543 __cil_tmp13 = i * 288UL;
1544#line 127
1545 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
1546#line 127
1547 __cil_tmp15 = (unsigned long )(leds) + __cil_tmp14;
1548#line 127
1549 *((void (**)(struct led_classdev *led_cdev , enum led_brightness brightness ))__cil_tmp15) = & ot200_led_brightness_set;
1550#line 129
1551 __cil_tmp16 = (unsigned long )pdev;
1552#line 129
1553 __cil_tmp17 = __cil_tmp16 + 16;
1554#line 129
1555 __cil_tmp18 = (struct device *)__cil_tmp17;
1556#line 129
1557 __cil_tmp19 = i * 288UL;
1558#line 129
1559 __cil_tmp20 = (unsigned long )(leds) + __cil_tmp19;
1560#line 129
1561 __cil_tmp21 = (struct led_classdev *)__cil_tmp20;
1562#line 129
1563 ret = led_classdev_register(__cil_tmp18, __cil_tmp21);
1564 }
1565#line 130
1566 if (ret < 0) {
1567#line 131
1568 goto err;
1569 } else {
1570
1571 }
1572#line 124
1573 i = i + 1;
1574 }
1575 while_break: ;
1576 }
1577 {
1578#line 134
1579 __cil_tmp22 = & leds_front;
1580#line 134
1581 *__cil_tmp22 = (u8 )0;
1582#line 135
1583 __cil_tmp23 = & leds_back;
1584#line 135
1585 __cil_tmp24 = 1UL << 1;
1586#line 135
1587 *__cil_tmp23 = (u8 )__cil_tmp24;
1588#line 136
1589 __cil_tmp25 = & leds_front;
1590#line 136
1591 __cil_tmp26 = *__cil_tmp25;
1592#line 136
1593 outb(__cil_tmp26, 73);
1594#line 137
1595 __cil_tmp27 = & leds_back;
1596#line 137
1597 __cil_tmp28 = *__cil_tmp27;
1598#line 137
1599 outb(__cil_tmp28, 90);
1600 }
1601#line 139
1602 return (0);
1603 err:
1604#line 142
1605 i = i - 1;
1606 {
1607#line 142
1608 while (1) {
1609 while_continue___0: ;
1610#line 142
1611 if (i >= 0) {
1612
1613 } else {
1614#line 142
1615 goto while_break___0;
1616 }
1617 {
1618#line 143
1619 __cil_tmp29 = i * 288UL;
1620#line 143
1621 __cil_tmp30 = (unsigned long )(leds) + __cil_tmp29;
1622#line 143
1623 __cil_tmp31 = (struct led_classdev *)__cil_tmp30;
1624#line 143
1625 led_classdev_unregister(__cil_tmp31);
1626#line 142
1627 i = i - 1;
1628 }
1629 }
1630 while_break___0: ;
1631 }
1632#line 145
1633 return (ret);
1634}
1635}
1636#line 148
1637static int ot200_led_remove(struct platform_device *pdev ) __attribute__((__section__(".devexit.text"),
1638__no_instrument_function__)) ;
1639#line 148 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1640static int ot200_led_remove(struct platform_device *pdev )
1641{ int i ;
1642 unsigned long __cil_tmp3 ;
1643 unsigned long __cil_tmp4 ;
1644 unsigned long __cil_tmp5 ;
1645 unsigned long __cil_tmp6 ;
1646 unsigned long __cil_tmp7 ;
1647 struct led_classdev *__cil_tmp8 ;
1648
1649 {
1650#line 152
1651 i = 0;
1652 {
1653#line 152
1654 while (1) {
1655 while_continue: ;
1656 {
1657#line 152
1658 __cil_tmp3 = 2880UL / 288UL;
1659#line 152
1660 __cil_tmp4 = __cil_tmp3 + 0UL;
1661#line 152
1662 __cil_tmp5 = (unsigned long )i;
1663#line 152
1664 if (__cil_tmp5 < __cil_tmp4) {
1665
1666 } else {
1667#line 152
1668 goto while_break;
1669 }
1670 }
1671 {
1672#line 153
1673 __cil_tmp6 = i * 288UL;
1674#line 153
1675 __cil_tmp7 = (unsigned long )(leds) + __cil_tmp6;
1676#line 153
1677 __cil_tmp8 = (struct led_classdev *)__cil_tmp7;
1678#line 153
1679 led_classdev_unregister(__cil_tmp8);
1680#line 152
1681 i = i + 1;
1682 }
1683 }
1684 while_break: ;
1685 }
1686#line 155
1687 return (0);
1688}
1689}
1690#line 158 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1691static struct platform_driver ot200_led_driver = {& ot200_led_probe, & ot200_led_remove, (void (*)(struct platform_device * ))0,
1692 (int (*)(struct platform_device * , pm_message_t state ))0, (int (*)(struct platform_device * ))0,
1693 {"leds-ot200", (struct bus_type *)0, & __this_module, (char const *)0, (_Bool)0,
1694 (struct of_device_id const *)0, (int (*)(struct device *dev ))0, (int (*)(struct device *dev ))0,
1695 (void (*)(struct device *dev ))0, (int (*)(struct device *dev , pm_message_t state ))0,
1696 (int (*)(struct device *dev ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0,
1697 (struct driver_private *)0}, (struct platform_device_id const *)0};
1698#line 167
1699static int ot200_led_driver_init(void) __attribute__((__section__(".init.text"),
1700__no_instrument_function__)) ;
1701#line 167 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1702static int ot200_led_driver_init(void)
1703{ int tmp ;
1704
1705 {
1706 {
1707#line 167
1708 tmp = platform_driver_register(& ot200_led_driver);
1709 }
1710#line 167
1711 return (tmp);
1712}
1713}
1714#line 167 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1715int init_module(void)
1716{ int tmp ;
1717
1718 {
1719 {
1720#line 167
1721 tmp = ot200_led_driver_init();
1722 }
1723#line 167
1724 return (tmp);
1725}
1726}
1727#line 167
1728static void ot200_led_driver_exit(void) __attribute__((__section__(".exit.text"),
1729__no_instrument_function__)) ;
1730#line 167 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1731static void ot200_led_driver_exit(void)
1732{
1733
1734 {
1735 {
1736#line 167
1737 platform_driver_unregister(& ot200_led_driver);
1738 }
1739#line 167
1740 return;
1741}
1742}
1743#line 167 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1744void cleanup_module(void)
1745{
1746
1747 {
1748 {
1749#line 167
1750 ot200_led_driver_exit();
1751 }
1752#line 167
1753 return;
1754}
1755}
1756#line 169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1757static char const __mod_author169[52] __attribute__((__used__, __unused__, __section__(".modinfo"),
1758__aligned__(1))) =
1759#line 169
1760 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
1761 (char const )'o', (char const )'r', (char const )'=', (char const )'S',
1762 (char const )'e', (char const )'b', (char const )'a', (char const )'s',
1763 (char const )'t', (char const )'i', (char const )'a', (char const )'n',
1764 (char const )' ', (char const )'A', (char const )'.', (char const )' ',
1765 (char const )'S', (char const )'i', (char const )'e', (char const )'w',
1766 (char const )'i', (char const )'o', (char const )'r', (char const )' ',
1767 (char const )'<', (char const )'b', (char const )'i', (char const )'g',
1768 (char const )'e', (char const )'a', (char const )'s', (char const )'y',
1769 (char const )'@', (char const )'l', (char const )'i', (char const )'n',
1770 (char const )'u', (char const )'t', (char const )'r', (char const )'o',
1771 (char const )'n', (char const )'i', (char const )'x', (char const )'.',
1772 (char const )'d', (char const )'e', (char const )'>', (char const )'\000'};
1773#line 170 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1774static char const __mod_description170[29] __attribute__((__used__, __unused__,
1775__section__(".modinfo"), __aligned__(1))) =
1776#line 170
1777 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
1778 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
1779 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
1780 (char const )'o', (char const )'t', (char const )'2', (char const )'0',
1781 (char const )'0', (char const )' ', (char const )'L', (char const )'E',
1782 (char const )'D', (char const )' ', (char const )'d', (char const )'r',
1783 (char const )'i', (char const )'v', (char const )'e', (char const )'r',
1784 (char const )'\000'};
1785#line 171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1786static char const __mod_license171[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
1787__aligned__(1))) =
1788#line 171
1789 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
1790 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
1791 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
1792#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1793static char const __mod_alias172[26] __attribute__((__used__, __unused__, __section__(".modinfo"),
1794__aligned__(1))) =
1795#line 172
1796 { (char const )'a', (char const )'l', (char const )'i', (char const )'a',
1797 (char const )'s', (char const )'=', (char const )'p', (char const )'l',
1798 (char const )'a', (char const )'t', (char const )'f', (char const )'o',
1799 (char const )'r', (char const )'m', (char const )':', (char const )'l',
1800 (char const )'e', (char const )'d', (char const )'s', (char const )'-',
1801 (char const )'o', (char const )'t', (char const )'2', (char const )'0',
1802 (char const )'0', (char const )'\000'};
1803#line 190
1804void ldv_check_final_state(void) ;
1805#line 193
1806extern void ldv_check_return_value(int res ) ;
1807#line 196
1808extern void ldv_initialize(void) ;
1809#line 199
1810extern int __VERIFIER_nondet_int(void) ;
1811#line 202 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1812int LDV_IN_INTERRUPT ;
1813#line 217 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1814static int res_ot200_led_probe_1 ;
1815#line 205 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
1816void main(void)
1817{ struct platform_device *var_group1 ;
1818 int ldv_s_ot200_led_driver_platform_driver ;
1819 int tmp ;
1820 int tmp___0 ;
1821 int __cil_tmp5 ;
1822
1823 {
1824 {
1825#line 225
1826 LDV_IN_INTERRUPT = 1;
1827#line 234
1828 ldv_initialize();
1829#line 235
1830 ldv_s_ot200_led_driver_platform_driver = 0;
1831 }
1832 {
1833#line 238
1834 while (1) {
1835 while_continue: ;
1836 {
1837#line 238
1838 tmp___0 = __VERIFIER_nondet_int();
1839 }
1840#line 238
1841 if (tmp___0) {
1842
1843 } else {
1844 {
1845#line 238
1846 __cil_tmp5 = ldv_s_ot200_led_driver_platform_driver == 0;
1847#line 238
1848 if (! __cil_tmp5) {
1849
1850 } else {
1851#line 238
1852 goto while_break;
1853 }
1854 }
1855 }
1856 {
1857#line 242
1858 tmp = __VERIFIER_nondet_int();
1859 }
1860#line 244
1861 if (tmp == 0) {
1862#line 244
1863 goto case_0;
1864 } else {
1865 {
1866#line 263
1867 goto switch_default;
1868#line 242
1869 if (0) {
1870 case_0:
1871#line 247
1872 if (ldv_s_ot200_led_driver_platform_driver == 0) {
1873 {
1874#line 252
1875 res_ot200_led_probe_1 = ot200_led_probe(var_group1);
1876#line 253
1877 ldv_check_return_value(res_ot200_led_probe_1);
1878 }
1879#line 254
1880 if (res_ot200_led_probe_1) {
1881#line 255
1882 goto ldv_module_exit;
1883 } else {
1884
1885 }
1886#line 256
1887 ldv_s_ot200_led_driver_platform_driver = 0;
1888 } else {
1889
1890 }
1891#line 262
1892 goto switch_break;
1893 switch_default:
1894#line 263
1895 goto switch_break;
1896 } else {
1897 switch_break: ;
1898 }
1899 }
1900 }
1901 }
1902 while_break: ;
1903 }
1904 ldv_module_exit:
1905 {
1906#line 272
1907 ldv_check_final_state();
1908 }
1909#line 275
1910 return;
1911}
1912}
1913#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1914void ldv_blast_assert(void)
1915{
1916
1917 {
1918 ERROR:
1919#line 6
1920 goto ERROR;
1921}
1922}
1923#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1924extern int __VERIFIER_nondet_int(void) ;
1925#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1926int ldv_mutex = 1;
1927#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1928int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1929{ int nondetermined ;
1930
1931 {
1932#line 29
1933 if (ldv_mutex == 1) {
1934
1935 } else {
1936 {
1937#line 29
1938 ldv_blast_assert();
1939 }
1940 }
1941 {
1942#line 32
1943 nondetermined = __VERIFIER_nondet_int();
1944 }
1945#line 35
1946 if (nondetermined) {
1947#line 38
1948 ldv_mutex = 2;
1949#line 40
1950 return (0);
1951 } else {
1952#line 45
1953 return (-4);
1954 }
1955}
1956}
1957#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1958int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1959{ int nondetermined ;
1960
1961 {
1962#line 57
1963 if (ldv_mutex == 1) {
1964
1965 } else {
1966 {
1967#line 57
1968 ldv_blast_assert();
1969 }
1970 }
1971 {
1972#line 60
1973 nondetermined = __VERIFIER_nondet_int();
1974 }
1975#line 63
1976 if (nondetermined) {
1977#line 66
1978 ldv_mutex = 2;
1979#line 68
1980 return (0);
1981 } else {
1982#line 73
1983 return (-4);
1984 }
1985}
1986}
1987#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1988int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1989{ int atomic_value_after_dec ;
1990
1991 {
1992#line 83
1993 if (ldv_mutex == 1) {
1994
1995 } else {
1996 {
1997#line 83
1998 ldv_blast_assert();
1999 }
2000 }
2001 {
2002#line 86
2003 atomic_value_after_dec = __VERIFIER_nondet_int();
2004 }
2005#line 89
2006 if (atomic_value_after_dec == 0) {
2007#line 92
2008 ldv_mutex = 2;
2009#line 94
2010 return (1);
2011 } else {
2012
2013 }
2014#line 98
2015 return (0);
2016}
2017}
2018#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2019void mutex_lock(struct mutex *lock )
2020{
2021
2022 {
2023#line 108
2024 if (ldv_mutex == 1) {
2025
2026 } else {
2027 {
2028#line 108
2029 ldv_blast_assert();
2030 }
2031 }
2032#line 110
2033 ldv_mutex = 2;
2034#line 111
2035 return;
2036}
2037}
2038#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2039int mutex_trylock(struct mutex *lock )
2040{ int nondetermined ;
2041
2042 {
2043#line 121
2044 if (ldv_mutex == 1) {
2045
2046 } else {
2047 {
2048#line 121
2049 ldv_blast_assert();
2050 }
2051 }
2052 {
2053#line 124
2054 nondetermined = __VERIFIER_nondet_int();
2055 }
2056#line 127
2057 if (nondetermined) {
2058#line 130
2059 ldv_mutex = 2;
2060#line 132
2061 return (1);
2062 } else {
2063#line 137
2064 return (0);
2065 }
2066}
2067}
2068#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2069void mutex_unlock(struct mutex *lock )
2070{
2071
2072 {
2073#line 147
2074 if (ldv_mutex == 2) {
2075
2076 } else {
2077 {
2078#line 147
2079 ldv_blast_assert();
2080 }
2081 }
2082#line 149
2083 ldv_mutex = 1;
2084#line 150
2085 return;
2086}
2087}
2088#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2089void ldv_check_final_state(void)
2090{
2091
2092 {
2093#line 156
2094 if (ldv_mutex == 1) {
2095
2096 } else {
2097 {
2098#line 156
2099 ldv_blast_assert();
2100 }
2101 }
2102#line 157
2103 return;
2104}
2105}
2106#line 284 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12605/dscv_tempdir/dscv/ri/32_1/drivers/leds/leds-ot200.c.common.c"
2107long s__builtin_expect(long val , long res )
2108{
2109
2110 {
2111#line 285
2112 return (val);
2113}
2114}