1
2
3
4#line 23 "include/asm-generic/int-ll64.h"
5typedef unsigned short __u16;
6#line 26 "include/asm-generic/int-ll64.h"
7typedef unsigned int __u32;
8#line 30 "include/asm-generic/int-ll64.h"
9typedef unsigned long long __u64;
10#line 45 "include/asm-generic/int-ll64.h"
11typedef short s16;
12#line 46 "include/asm-generic/int-ll64.h"
13typedef unsigned short u16;
14#line 48 "include/asm-generic/int-ll64.h"
15typedef int s32;
16#line 49 "include/asm-generic/int-ll64.h"
17typedef unsigned int u32;
18#line 51 "include/asm-generic/int-ll64.h"
19typedef long long s64;
20#line 52 "include/asm-generic/int-ll64.h"
21typedef unsigned long long u64;
22#line 14 "include/asm-generic/posix_types.h"
23typedef long __kernel_long_t;
24#line 15 "include/asm-generic/posix_types.h"
25typedef unsigned long __kernel_ulong_t;
26#line 75 "include/asm-generic/posix_types.h"
27typedef __kernel_ulong_t __kernel_size_t;
28#line 76 "include/asm-generic/posix_types.h"
29typedef __kernel_long_t __kernel_ssize_t;
30#line 91 "include/asm-generic/posix_types.h"
31typedef long long __kernel_loff_t;
32#line 21 "include/linux/types.h"
33typedef __u32 __kernel_dev_t;
34#line 24 "include/linux/types.h"
35typedef __kernel_dev_t dev_t;
36#line 27 "include/linux/types.h"
37typedef unsigned short umode_t;
38#line 38 "include/linux/types.h"
39typedef _Bool bool;
40#line 54 "include/linux/types.h"
41typedef __kernel_loff_t loff_t;
42#line 63 "include/linux/types.h"
43typedef __kernel_size_t size_t;
44#line 68 "include/linux/types.h"
45typedef __kernel_ssize_t ssize_t;
46#line 219 "include/linux/types.h"
47struct __anonstruct_atomic_t_7 {
48 int counter ;
49};
50#line 219 "include/linux/types.h"
51typedef struct __anonstruct_atomic_t_7 atomic_t;
52#line 224 "include/linux/types.h"
53struct __anonstruct_atomic64_t_8 {
54 long counter ;
55};
56#line 224 "include/linux/types.h"
57typedef struct __anonstruct_atomic64_t_8 atomic64_t;
58#line 229 "include/linux/types.h"
59struct list_head {
60 struct list_head *next ;
61 struct list_head *prev ;
62};
63#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
64struct module;
65#line 56
66struct module;
67#line 146 "include/linux/init.h"
68typedef void (*ctor_fn_t)(void);
69#line 47 "include/linux/dynamic_debug.h"
70struct device;
71#line 47
72struct device;
73#line 135 "include/linux/kernel.h"
74struct completion;
75#line 135
76struct completion;
77#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
78struct task_struct;
79#line 20
80struct task_struct;
81#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
82struct task_struct;
83#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
84struct file;
85#line 295
86struct file;
87#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
88struct task_struct;
89#line 329
90struct arch_spinlock;
91#line 329
92struct arch_spinlock;
93#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
94struct task_struct;
95#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
96struct task_struct;
97#line 10 "include/asm-generic/bug.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 23 "include/asm-generic/atomic-long.h"
109typedef atomic64_t atomic_long_t;
110#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
111typedef u16 __ticket_t;
112#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
113typedef u32 __ticketpair_t;
114#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
115struct __raw_tickets {
116 __ticket_t head ;
117 __ticket_t tail ;
118};
119#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
120union __anonunion____missing_field_name_36 {
121 __ticketpair_t head_tail ;
122 struct __raw_tickets tickets ;
123};
124#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
125struct arch_spinlock {
126 union __anonunion____missing_field_name_36 __annonCompField17 ;
127};
128#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
129typedef struct arch_spinlock arch_spinlock_t;
130#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
131struct __anonstruct____missing_field_name_38 {
132 u32 read ;
133 s32 write ;
134};
135#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
136union __anonunion_arch_rwlock_t_37 {
137 s64 lock ;
138 struct __anonstruct____missing_field_name_38 __annonCompField18 ;
139};
140#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
141typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_t;
142#line 12 "include/linux/lockdep.h"
143struct task_struct;
144#line 20 "include/linux/spinlock_types.h"
145struct raw_spinlock {
146 arch_spinlock_t raw_lock ;
147 unsigned int magic ;
148 unsigned int owner_cpu ;
149 void *owner ;
150};
151#line 20 "include/linux/spinlock_types.h"
152typedef struct raw_spinlock raw_spinlock_t;
153#line 64 "include/linux/spinlock_types.h"
154union __anonunion____missing_field_name_39 {
155 struct raw_spinlock rlock ;
156};
157#line 64 "include/linux/spinlock_types.h"
158struct spinlock {
159 union __anonunion____missing_field_name_39 __annonCompField19 ;
160};
161#line 64 "include/linux/spinlock_types.h"
162typedef struct spinlock spinlock_t;
163#line 11 "include/linux/rwlock_types.h"
164struct __anonstruct_rwlock_t_40 {
165 arch_rwlock_t raw_lock ;
166 unsigned int magic ;
167 unsigned int owner_cpu ;
168 void *owner ;
169};
170#line 11 "include/linux/rwlock_types.h"
171typedef struct __anonstruct_rwlock_t_40 rwlock_t;
172#line 49 "include/linux/wait.h"
173struct __wait_queue_head {
174 spinlock_t lock ;
175 struct list_head task_list ;
176};
177#line 53 "include/linux/wait.h"
178typedef struct __wait_queue_head wait_queue_head_t;
179#line 55
180struct task_struct;
181#line 48 "include/linux/mutex.h"
182struct mutex {
183 atomic_t count ;
184 spinlock_t wait_lock ;
185 struct list_head wait_list ;
186 struct task_struct *owner ;
187 char const *name ;
188 void *magic ;
189};
190#line 19 "include/linux/rwsem.h"
191struct rw_semaphore;
192#line 19
193struct rw_semaphore;
194#line 25 "include/linux/rwsem.h"
195struct rw_semaphore {
196 long count ;
197 raw_spinlock_t wait_lock ;
198 struct list_head wait_list ;
199};
200#line 25 "include/linux/completion.h"
201struct completion {
202 unsigned int done ;
203 wait_queue_head_t wait ;
204};
205#line 202 "include/linux/ioport.h"
206struct device;
207#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
208struct device;
209#line 46 "include/linux/ktime.h"
210union ktime {
211 s64 tv64 ;
212};
213#line 59 "include/linux/ktime.h"
214typedef union ktime ktime_t;
215#line 10 "include/linux/timer.h"
216struct tvec_base;
217#line 10
218struct tvec_base;
219#line 12 "include/linux/timer.h"
220struct timer_list {
221 struct list_head entry ;
222 unsigned long expires ;
223 struct tvec_base *base ;
224 void (*function)(unsigned long ) ;
225 unsigned long data ;
226 int slack ;
227 int start_pid ;
228 void *start_site ;
229 char start_comm[16] ;
230};
231#line 17 "include/linux/workqueue.h"
232struct work_struct;
233#line 17
234struct work_struct;
235#line 79 "include/linux/workqueue.h"
236struct work_struct {
237 atomic_long_t data ;
238 struct list_head entry ;
239 void (*func)(struct work_struct *work ) ;
240};
241#line 42 "include/linux/pm.h"
242struct device;
243#line 50 "include/linux/pm.h"
244struct pm_message {
245 int event ;
246};
247#line 50 "include/linux/pm.h"
248typedef struct pm_message pm_message_t;
249#line 264 "include/linux/pm.h"
250struct dev_pm_ops {
251 int (*prepare)(struct device *dev ) ;
252 void (*complete)(struct device *dev ) ;
253 int (*suspend)(struct device *dev ) ;
254 int (*resume)(struct device *dev ) ;
255 int (*freeze)(struct device *dev ) ;
256 int (*thaw)(struct device *dev ) ;
257 int (*poweroff)(struct device *dev ) ;
258 int (*restore)(struct device *dev ) ;
259 int (*suspend_late)(struct device *dev ) ;
260 int (*resume_early)(struct device *dev ) ;
261 int (*freeze_late)(struct device *dev ) ;
262 int (*thaw_early)(struct device *dev ) ;
263 int (*poweroff_late)(struct device *dev ) ;
264 int (*restore_early)(struct device *dev ) ;
265 int (*suspend_noirq)(struct device *dev ) ;
266 int (*resume_noirq)(struct device *dev ) ;
267 int (*freeze_noirq)(struct device *dev ) ;
268 int (*thaw_noirq)(struct device *dev ) ;
269 int (*poweroff_noirq)(struct device *dev ) ;
270 int (*restore_noirq)(struct device *dev ) ;
271 int (*runtime_suspend)(struct device *dev ) ;
272 int (*runtime_resume)(struct device *dev ) ;
273 int (*runtime_idle)(struct device *dev ) ;
274};
275#line 458
276enum rpm_status {
277 RPM_ACTIVE = 0,
278 RPM_RESUMING = 1,
279 RPM_SUSPENDED = 2,
280 RPM_SUSPENDING = 3
281} ;
282#line 480
283enum rpm_request {
284 RPM_REQ_NONE = 0,
285 RPM_REQ_IDLE = 1,
286 RPM_REQ_SUSPEND = 2,
287 RPM_REQ_AUTOSUSPEND = 3,
288 RPM_REQ_RESUME = 4
289} ;
290#line 488
291struct wakeup_source;
292#line 488
293struct wakeup_source;
294#line 495 "include/linux/pm.h"
295struct pm_subsys_data {
296 spinlock_t lock ;
297 unsigned int refcount ;
298};
299#line 506
300struct dev_pm_qos_request;
301#line 506
302struct pm_qos_constraints;
303#line 506 "include/linux/pm.h"
304struct dev_pm_info {
305 pm_message_t power_state ;
306 unsigned int can_wakeup : 1 ;
307 unsigned int async_suspend : 1 ;
308 bool is_prepared : 1 ;
309 bool is_suspended : 1 ;
310 bool ignore_children : 1 ;
311 spinlock_t lock ;
312 struct list_head entry ;
313 struct completion completion ;
314 struct wakeup_source *wakeup ;
315 bool wakeup_path : 1 ;
316 struct timer_list suspend_timer ;
317 unsigned long timer_expires ;
318 struct work_struct work ;
319 wait_queue_head_t wait_queue ;
320 atomic_t usage_count ;
321 atomic_t child_count ;
322 unsigned int disable_depth : 3 ;
323 unsigned int idle_notification : 1 ;
324 unsigned int request_pending : 1 ;
325 unsigned int deferred_resume : 1 ;
326 unsigned int run_wake : 1 ;
327 unsigned int runtime_auto : 1 ;
328 unsigned int no_callbacks : 1 ;
329 unsigned int irq_safe : 1 ;
330 unsigned int use_autosuspend : 1 ;
331 unsigned int timer_autosuspends : 1 ;
332 enum rpm_request request ;
333 enum rpm_status runtime_status ;
334 int runtime_error ;
335 int autosuspend_delay ;
336 unsigned long last_busy ;
337 unsigned long active_jiffies ;
338 unsigned long suspended_jiffies ;
339 unsigned long accounting_timestamp ;
340 ktime_t suspend_time ;
341 s64 max_time_suspended_ns ;
342 struct dev_pm_qos_request *pq_req ;
343 struct pm_subsys_data *subsys_data ;
344 struct pm_qos_constraints *constraints ;
345};
346#line 564 "include/linux/pm.h"
347struct dev_pm_domain {
348 struct dev_pm_ops ops ;
349};
350#line 8 "include/linux/vmalloc.h"
351struct vm_area_struct;
352#line 8
353struct vm_area_struct;
354#line 10 "include/linux/gfp.h"
355struct vm_area_struct;
356#line 29 "include/linux/sysctl.h"
357struct completion;
358#line 49 "include/linux/kmod.h"
359struct file;
360#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
361struct task_struct;
362#line 18 "include/linux/elf.h"
363typedef __u64 Elf64_Addr;
364#line 19 "include/linux/elf.h"
365typedef __u16 Elf64_Half;
366#line 23 "include/linux/elf.h"
367typedef __u32 Elf64_Word;
368#line 24 "include/linux/elf.h"
369typedef __u64 Elf64_Xword;
370#line 194 "include/linux/elf.h"
371struct elf64_sym {
372 Elf64_Word st_name ;
373 unsigned char st_info ;
374 unsigned char st_other ;
375 Elf64_Half st_shndx ;
376 Elf64_Addr st_value ;
377 Elf64_Xword st_size ;
378};
379#line 194 "include/linux/elf.h"
380typedef struct elf64_sym Elf64_Sym;
381#line 438
382struct file;
383#line 20 "include/linux/kobject_ns.h"
384struct sock;
385#line 20
386struct sock;
387#line 21
388struct kobject;
389#line 21
390struct kobject;
391#line 27
392enum kobj_ns_type {
393 KOBJ_NS_TYPE_NONE = 0,
394 KOBJ_NS_TYPE_NET = 1,
395 KOBJ_NS_TYPES = 2
396} ;
397#line 40 "include/linux/kobject_ns.h"
398struct kobj_ns_type_operations {
399 enum kobj_ns_type type ;
400 void *(*grab_current_ns)(void) ;
401 void const *(*netlink_ns)(struct sock *sk ) ;
402 void const *(*initial_ns)(void) ;
403 void (*drop_ns)(void * ) ;
404};
405#line 22 "include/linux/sysfs.h"
406struct kobject;
407#line 23
408struct module;
409#line 24
410enum kobj_ns_type;
411#line 26 "include/linux/sysfs.h"
412struct attribute {
413 char const *name ;
414 umode_t mode ;
415};
416#line 56 "include/linux/sysfs.h"
417struct attribute_group {
418 char const *name ;
419 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
420 struct attribute **attrs ;
421};
422#line 85
423struct file;
424#line 86
425struct vm_area_struct;
426#line 88 "include/linux/sysfs.h"
427struct bin_attribute {
428 struct attribute attr ;
429 size_t size ;
430 void *private ;
431 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
432 loff_t , size_t ) ;
433 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
434 loff_t , size_t ) ;
435 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
436};
437#line 112 "include/linux/sysfs.h"
438struct sysfs_ops {
439 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
440 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
441 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
442};
443#line 118
444struct sysfs_dirent;
445#line 118
446struct sysfs_dirent;
447#line 22 "include/linux/kref.h"
448struct kref {
449 atomic_t refcount ;
450};
451#line 60 "include/linux/kobject.h"
452struct kset;
453#line 60
454struct kobj_type;
455#line 60 "include/linux/kobject.h"
456struct kobject {
457 char const *name ;
458 struct list_head entry ;
459 struct kobject *parent ;
460 struct kset *kset ;
461 struct kobj_type *ktype ;
462 struct sysfs_dirent *sd ;
463 struct kref kref ;
464 unsigned int state_initialized : 1 ;
465 unsigned int state_in_sysfs : 1 ;
466 unsigned int state_add_uevent_sent : 1 ;
467 unsigned int state_remove_uevent_sent : 1 ;
468 unsigned int uevent_suppress : 1 ;
469};
470#line 108 "include/linux/kobject.h"
471struct kobj_type {
472 void (*release)(struct kobject *kobj ) ;
473 struct sysfs_ops const *sysfs_ops ;
474 struct attribute **default_attrs ;
475 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
476 void const *(*namespace)(struct kobject *kobj ) ;
477};
478#line 116 "include/linux/kobject.h"
479struct kobj_uevent_env {
480 char *envp[32] ;
481 int envp_idx ;
482 char buf[2048] ;
483 int buflen ;
484};
485#line 123 "include/linux/kobject.h"
486struct kset_uevent_ops {
487 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
488 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
489 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
490};
491#line 140
492struct sock;
493#line 159 "include/linux/kobject.h"
494struct kset {
495 struct list_head list ;
496 spinlock_t list_lock ;
497 struct kobject kobj ;
498 struct kset_uevent_ops const *uevent_ops ;
499};
500#line 39 "include/linux/moduleparam.h"
501struct kernel_param;
502#line 39
503struct kernel_param;
504#line 41 "include/linux/moduleparam.h"
505struct kernel_param_ops {
506 int (*set)(char const *val , struct kernel_param const *kp ) ;
507 int (*get)(char *buffer , struct kernel_param const *kp ) ;
508 void (*free)(void *arg ) ;
509};
510#line 50
511struct kparam_string;
512#line 50
513struct kparam_array;
514#line 50 "include/linux/moduleparam.h"
515union __anonunion____missing_field_name_199 {
516 void *arg ;
517 struct kparam_string const *str ;
518 struct kparam_array const *arr ;
519};
520#line 50 "include/linux/moduleparam.h"
521struct kernel_param {
522 char const *name ;
523 struct kernel_param_ops const *ops ;
524 u16 perm ;
525 s16 level ;
526 union __anonunion____missing_field_name_199 __annonCompField32 ;
527};
528#line 63 "include/linux/moduleparam.h"
529struct kparam_string {
530 unsigned int maxlen ;
531 char *string ;
532};
533#line 69 "include/linux/moduleparam.h"
534struct kparam_array {
535 unsigned int max ;
536 unsigned int elemsize ;
537 unsigned int *num ;
538 struct kernel_param_ops const *ops ;
539 void *elem ;
540};
541#line 445
542struct module;
543#line 80 "include/linux/jump_label.h"
544struct module;
545#line 143 "include/linux/jump_label.h"
546struct static_key {
547 atomic_t enabled ;
548};
549#line 22 "include/linux/tracepoint.h"
550struct module;
551#line 23
552struct tracepoint;
553#line 23
554struct tracepoint;
555#line 25 "include/linux/tracepoint.h"
556struct tracepoint_func {
557 void *func ;
558 void *data ;
559};
560#line 30 "include/linux/tracepoint.h"
561struct tracepoint {
562 char const *name ;
563 struct static_key key ;
564 void (*regfunc)(void) ;
565 void (*unregfunc)(void) ;
566 struct tracepoint_func *funcs ;
567};
568#line 19 "include/linux/export.h"
569struct kernel_symbol {
570 unsigned long value ;
571 char const *name ;
572};
573#line 8 "include/asm-generic/module.h"
574struct mod_arch_specific {
575
576};
577#line 35 "include/linux/module.h"
578struct module;
579#line 37
580struct module_param_attrs;
581#line 37 "include/linux/module.h"
582struct module_kobject {
583 struct kobject kobj ;
584 struct module *mod ;
585 struct kobject *drivers_dir ;
586 struct module_param_attrs *mp ;
587};
588#line 44 "include/linux/module.h"
589struct module_attribute {
590 struct attribute attr ;
591 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
592 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
593 size_t count ) ;
594 void (*setup)(struct module * , char const * ) ;
595 int (*test)(struct module * ) ;
596 void (*free)(struct module * ) ;
597};
598#line 71
599struct exception_table_entry;
600#line 71
601struct exception_table_entry;
602#line 199
603enum module_state {
604 MODULE_STATE_LIVE = 0,
605 MODULE_STATE_COMING = 1,
606 MODULE_STATE_GOING = 2
607} ;
608#line 215 "include/linux/module.h"
609struct module_ref {
610 unsigned long incs ;
611 unsigned long decs ;
612} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
613#line 220
614struct module_sect_attrs;
615#line 220
616struct module_notes_attrs;
617#line 220
618struct ftrace_event_call;
619#line 220 "include/linux/module.h"
620struct module {
621 enum module_state state ;
622 struct list_head list ;
623 char name[64UL - sizeof(unsigned long )] ;
624 struct module_kobject mkobj ;
625 struct module_attribute *modinfo_attrs ;
626 char const *version ;
627 char const *srcversion ;
628 struct kobject *holders_dir ;
629 struct kernel_symbol const *syms ;
630 unsigned long const *crcs ;
631 unsigned int num_syms ;
632 struct kernel_param *kp ;
633 unsigned int num_kp ;
634 unsigned int num_gpl_syms ;
635 struct kernel_symbol const *gpl_syms ;
636 unsigned long const *gpl_crcs ;
637 struct kernel_symbol const *unused_syms ;
638 unsigned long const *unused_crcs ;
639 unsigned int num_unused_syms ;
640 unsigned int num_unused_gpl_syms ;
641 struct kernel_symbol const *unused_gpl_syms ;
642 unsigned long const *unused_gpl_crcs ;
643 struct kernel_symbol const *gpl_future_syms ;
644 unsigned long const *gpl_future_crcs ;
645 unsigned int num_gpl_future_syms ;
646 unsigned int num_exentries ;
647 struct exception_table_entry *extable ;
648 int (*init)(void) ;
649 void *module_init ;
650 void *module_core ;
651 unsigned int init_size ;
652 unsigned int core_size ;
653 unsigned int init_text_size ;
654 unsigned int core_text_size ;
655 unsigned int init_ro_size ;
656 unsigned int core_ro_size ;
657 struct mod_arch_specific arch ;
658 unsigned int taints ;
659 unsigned int num_bugs ;
660 struct list_head bug_list ;
661 struct bug_entry *bug_table ;
662 Elf64_Sym *symtab ;
663 Elf64_Sym *core_symtab ;
664 unsigned int num_symtab ;
665 unsigned int core_num_syms ;
666 char *strtab ;
667 char *core_strtab ;
668 struct module_sect_attrs *sect_attrs ;
669 struct module_notes_attrs *notes_attrs ;
670 char *args ;
671 void *percpu ;
672 unsigned int percpu_size ;
673 unsigned int num_tracepoints ;
674 struct tracepoint * const *tracepoints_ptrs ;
675 unsigned int num_trace_bprintk_fmt ;
676 char const **trace_bprintk_fmt_start ;
677 struct ftrace_event_call **trace_events ;
678 unsigned int num_trace_events ;
679 struct list_head source_list ;
680 struct list_head target_list ;
681 struct task_struct *waiter ;
682 void (*exit)(void) ;
683 struct module_ref *refptr ;
684 ctor_fn_t *ctors ;
685 unsigned int num_ctors ;
686};
687#line 20 "include/linux/leds.h"
688struct device;
689#line 25
690enum led_brightness {
691 LED_OFF = 0,
692 LED_HALF = 127,
693 LED_FULL = 255
694} ;
695#line 31
696struct led_trigger;
697#line 31 "include/linux/leds.h"
698struct led_classdev {
699 char const *name ;
700 int brightness ;
701 int max_brightness ;
702 int flags ;
703 void (*brightness_set)(struct led_classdev *led_cdev , enum led_brightness brightness ) ;
704 enum led_brightness (*brightness_get)(struct led_classdev *led_cdev ) ;
705 int (*blink_set)(struct led_classdev *led_cdev , unsigned long *delay_on , unsigned long *delay_off ) ;
706 struct device *dev ;
707 struct list_head node ;
708 char const *default_trigger ;
709 unsigned long blink_delay_on ;
710 unsigned long blink_delay_off ;
711 struct timer_list blink_timer ;
712 int blink_brightness ;
713 struct rw_semaphore trigger_lock ;
714 struct led_trigger *trigger ;
715 struct list_head trig_list ;
716 void *trigger_data ;
717};
718#line 122 "include/linux/leds.h"
719struct led_trigger {
720 char const *name ;
721 void (*activate)(struct led_classdev *led_cdev ) ;
722 void (*deactivate)(struct led_classdev *led_cdev ) ;
723 rwlock_t leddev_list_lock ;
724 struct list_head led_cdevs ;
725 struct list_head next_trig ;
726};
727#line 19 "include/linux/klist.h"
728struct klist_node;
729#line 19
730struct klist_node;
731#line 39 "include/linux/klist.h"
732struct klist_node {
733 void *n_klist ;
734 struct list_head n_node ;
735 struct kref n_ref ;
736};
737#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
738struct dma_map_ops;
739#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
740struct dev_archdata {
741 void *acpi_handle ;
742 struct dma_map_ops *dma_ops ;
743 void *iommu ;
744};
745#line 28 "include/linux/device.h"
746struct device;
747#line 29
748struct device_private;
749#line 29
750struct device_private;
751#line 30
752struct device_driver;
753#line 30
754struct device_driver;
755#line 31
756struct driver_private;
757#line 31
758struct driver_private;
759#line 32
760struct module;
761#line 33
762struct class;
763#line 33
764struct class;
765#line 34
766struct subsys_private;
767#line 34
768struct subsys_private;
769#line 35
770struct bus_type;
771#line 35
772struct bus_type;
773#line 36
774struct device_node;
775#line 36
776struct device_node;
777#line 37
778struct iommu_ops;
779#line 37
780struct iommu_ops;
781#line 39 "include/linux/device.h"
782struct bus_attribute {
783 struct attribute attr ;
784 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
785 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
786};
787#line 89
788struct device_attribute;
789#line 89
790struct driver_attribute;
791#line 89 "include/linux/device.h"
792struct bus_type {
793 char const *name ;
794 char const *dev_name ;
795 struct device *dev_root ;
796 struct bus_attribute *bus_attrs ;
797 struct device_attribute *dev_attrs ;
798 struct driver_attribute *drv_attrs ;
799 int (*match)(struct device *dev , struct device_driver *drv ) ;
800 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
801 int (*probe)(struct device *dev ) ;
802 int (*remove)(struct device *dev ) ;
803 void (*shutdown)(struct device *dev ) ;
804 int (*suspend)(struct device *dev , pm_message_t state ) ;
805 int (*resume)(struct device *dev ) ;
806 struct dev_pm_ops const *pm ;
807 struct iommu_ops *iommu_ops ;
808 struct subsys_private *p ;
809};
810#line 127
811struct device_type;
812#line 214
813struct of_device_id;
814#line 214 "include/linux/device.h"
815struct device_driver {
816 char const *name ;
817 struct bus_type *bus ;
818 struct module *owner ;
819 char const *mod_name ;
820 bool suppress_bind_attrs ;
821 struct of_device_id const *of_match_table ;
822 int (*probe)(struct device *dev ) ;
823 int (*remove)(struct device *dev ) ;
824 void (*shutdown)(struct device *dev ) ;
825 int (*suspend)(struct device *dev , pm_message_t state ) ;
826 int (*resume)(struct device *dev ) ;
827 struct attribute_group const **groups ;
828 struct dev_pm_ops const *pm ;
829 struct driver_private *p ;
830};
831#line 249 "include/linux/device.h"
832struct driver_attribute {
833 struct attribute attr ;
834 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
835 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
836};
837#line 330
838struct class_attribute;
839#line 330 "include/linux/device.h"
840struct class {
841 char const *name ;
842 struct module *owner ;
843 struct class_attribute *class_attrs ;
844 struct device_attribute *dev_attrs ;
845 struct bin_attribute *dev_bin_attrs ;
846 struct kobject *dev_kobj ;
847 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
848 char *(*devnode)(struct device *dev , umode_t *mode ) ;
849 void (*class_release)(struct class *class ) ;
850 void (*dev_release)(struct device *dev ) ;
851 int (*suspend)(struct device *dev , pm_message_t state ) ;
852 int (*resume)(struct device *dev ) ;
853 struct kobj_ns_type_operations const *ns_type ;
854 void const *(*namespace)(struct device *dev ) ;
855 struct dev_pm_ops const *pm ;
856 struct subsys_private *p ;
857};
858#line 397 "include/linux/device.h"
859struct class_attribute {
860 struct attribute attr ;
861 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
862 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
863 size_t count ) ;
864 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ;
865};
866#line 465 "include/linux/device.h"
867struct device_type {
868 char const *name ;
869 struct attribute_group const **groups ;
870 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
871 char *(*devnode)(struct device *dev , umode_t *mode ) ;
872 void (*release)(struct device *dev ) ;
873 struct dev_pm_ops const *pm ;
874};
875#line 476 "include/linux/device.h"
876struct device_attribute {
877 struct attribute attr ;
878 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
879 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
880 size_t count ) ;
881};
882#line 559 "include/linux/device.h"
883struct device_dma_parameters {
884 unsigned int max_segment_size ;
885 unsigned long segment_boundary_mask ;
886};
887#line 627
888struct dma_coherent_mem;
889#line 627 "include/linux/device.h"
890struct device {
891 struct device *parent ;
892 struct device_private *p ;
893 struct kobject kobj ;
894 char const *init_name ;
895 struct device_type const *type ;
896 struct mutex mutex ;
897 struct bus_type *bus ;
898 struct device_driver *driver ;
899 void *platform_data ;
900 struct dev_pm_info power ;
901 struct dev_pm_domain *pm_domain ;
902 int numa_node ;
903 u64 *dma_mask ;
904 u64 coherent_dma_mask ;
905 struct device_dma_parameters *dma_parms ;
906 struct list_head dma_pools ;
907 struct dma_coherent_mem *dma_mem ;
908 struct dev_archdata archdata ;
909 struct device_node *of_node ;
910 dev_t devt ;
911 u32 id ;
912 spinlock_t devres_lock ;
913 struct list_head devres_head ;
914 struct klist_node knode_class ;
915 struct class *class ;
916 struct attribute_group const **groups ;
917 void (*release)(struct device *dev ) ;
918};
919#line 43 "include/linux/pm_wakeup.h"
920struct wakeup_source {
921 char const *name ;
922 struct list_head entry ;
923 spinlock_t lock ;
924 struct timer_list timer ;
925 unsigned long timer_expires ;
926 ktime_t total_time ;
927 ktime_t max_time ;
928 ktime_t last_time ;
929 unsigned long event_count ;
930 unsigned long active_count ;
931 unsigned long relax_count ;
932 unsigned long hit_count ;
933 unsigned int active : 1 ;
934};
935#line 1 "<compiler builtins>"
936long __builtin_expect(long val , long res ) ;
937#line 152 "include/linux/mutex.h"
938void mutex_lock(struct mutex *lock ) ;
939#line 153
940int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
941#line 154
942int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
943#line 168
944int mutex_trylock(struct mutex *lock ) ;
945#line 169
946void mutex_unlock(struct mutex *lock ) ;
947#line 170
948int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
949#line 67 "include/linux/module.h"
950int init_module(void) ;
951#line 68
952void cleanup_module(void) ;
953#line 137 "include/linux/leds.h"
954extern int led_trigger_register(struct led_trigger *trigger ) ;
955#line 138
956extern void led_trigger_unregister(struct led_trigger *trigger ) ;
957#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/leds/leds.h"
958__inline static void led_set_brightness(struct led_classdev *led_cdev , enum led_brightness value ) __attribute__((__no_instrument_function__)) ;
959#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/leds/leds.h"
960__inline static void led_set_brightness(struct led_classdev *led_cdev , enum led_brightness value )
961{ unsigned long __cil_tmp3 ;
962 unsigned long __cil_tmp4 ;
963 int __cil_tmp5 ;
964 unsigned int __cil_tmp6 ;
965 unsigned int __cil_tmp7 ;
966 unsigned long __cil_tmp8 ;
967 unsigned long __cil_tmp9 ;
968 int __cil_tmp10 ;
969 unsigned long __cil_tmp11 ;
970 unsigned long __cil_tmp12 ;
971 unsigned long __cil_tmp13 ;
972 unsigned long __cil_tmp14 ;
973 int __cil_tmp15 ;
974 int __cil_tmp16 ;
975 unsigned long __cil_tmp17 ;
976 unsigned long __cil_tmp18 ;
977 void (*__cil_tmp19)(struct led_classdev *led_cdev , enum led_brightness brightness ) ;
978
979 {
980 {
981#line 23
982 __cil_tmp3 = (unsigned long )led_cdev;
983#line 23
984 __cil_tmp4 = __cil_tmp3 + 12;
985#line 23
986 __cil_tmp5 = *((int *)__cil_tmp4);
987#line 23
988 __cil_tmp6 = (unsigned int )__cil_tmp5;
989#line 23
990 __cil_tmp7 = (unsigned int )value;
991#line 23
992 if (__cil_tmp7 > __cil_tmp6) {
993#line 24
994 __cil_tmp8 = (unsigned long )led_cdev;
995#line 24
996 __cil_tmp9 = __cil_tmp8 + 12;
997#line 24
998 __cil_tmp10 = *((int *)__cil_tmp9);
999#line 24
1000 value = (enum led_brightness )__cil_tmp10;
1001 } else {
1002
1003 }
1004 }
1005#line 25
1006 __cil_tmp11 = (unsigned long )led_cdev;
1007#line 25
1008 __cil_tmp12 = __cil_tmp11 + 8;
1009#line 25
1010 *((int *)__cil_tmp12) = (int )value;
1011 {
1012#line 26
1013 __cil_tmp13 = (unsigned long )led_cdev;
1014#line 26
1015 __cil_tmp14 = __cil_tmp13 + 16;
1016#line 26
1017 __cil_tmp15 = *((int *)__cil_tmp14);
1018#line 26
1019 __cil_tmp16 = __cil_tmp15 & 1;
1020#line 26
1021 if (! __cil_tmp16) {
1022 {
1023#line 27
1024 __cil_tmp17 = (unsigned long )led_cdev;
1025#line 27
1026 __cil_tmp18 = __cil_tmp17 + 24;
1027#line 27
1028 __cil_tmp19 = *((void (**)(struct led_classdev *led_cdev , enum led_brightness brightness ))__cil_tmp18);
1029#line 27
1030 (*__cil_tmp19)(led_cdev, value);
1031 }
1032 } else {
1033
1034 }
1035 }
1036#line 28
1037 return;
1038}
1039}
1040#line 21 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1041static void defon_trig_activate(struct led_classdev *led_cdev )
1042{ unsigned long __cil_tmp2 ;
1043 unsigned long __cil_tmp3 ;
1044 int __cil_tmp4 ;
1045 enum led_brightness __cil_tmp5 ;
1046
1047 {
1048 {
1049#line 23
1050 __cil_tmp2 = (unsigned long )led_cdev;
1051#line 23
1052 __cil_tmp3 = __cil_tmp2 + 12;
1053#line 23
1054 __cil_tmp4 = *((int *)__cil_tmp3);
1055#line 23
1056 __cil_tmp5 = (enum led_brightness )__cil_tmp4;
1057#line 23
1058 led_set_brightness(led_cdev, __cil_tmp5);
1059 }
1060#line 24
1061 return;
1062}
1063}
1064#line 26 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1065static struct led_trigger defon_led_trigger = {"default-on", & defon_trig_activate, (void (*)(struct led_classdev *led_cdev ))0,
1066 {{0LL}, 0U, 0U, (void *)0}, {(struct list_head *)0, (struct list_head *)0}, {(struct list_head *)0,
1067 (struct list_head *)0}};
1068#line 31
1069static int defon_trig_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
1070#line 31 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1071static int defon_trig_init(void)
1072{ int tmp ;
1073
1074 {
1075 {
1076#line 33
1077 tmp = led_trigger_register(& defon_led_trigger);
1078 }
1079#line 33
1080 return (tmp);
1081}
1082}
1083#line 36
1084static void defon_trig_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
1085#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1086static void defon_trig_exit(void)
1087{
1088
1089 {
1090 {
1091#line 38
1092 led_trigger_unregister(& defon_led_trigger);
1093 }
1094#line 39
1095 return;
1096}
1097}
1098#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1099int init_module(void)
1100{ int tmp ;
1101
1102 {
1103 {
1104#line 41
1105 tmp = defon_trig_init();
1106 }
1107#line 41
1108 return (tmp);
1109}
1110}
1111#line 42 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1112void cleanup_module(void)
1113{
1114
1115 {
1116 {
1117#line 42
1118 defon_trig_exit();
1119 }
1120#line 42
1121 return;
1122}
1123}
1124#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1125static char const __mod_author44[45] __attribute__((__used__, __unused__, __section__(".modinfo"),
1126__aligned__(1))) =
1127#line 44
1128 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
1129 (char const )'o', (char const )'r', (char const )'=', (char const )'N',
1130 (char const )'i', (char const )'c', (char const )'k', (char const )' ',
1131 (char const )'F', (char const )'o', (char const )'r', (char const )'b',
1132 (char const )'e', (char const )'s', (char const )' ', (char const )'<',
1133 (char const )'n', (char const )'i', (char const )'c', (char const )'k',
1134 (char const )'.', (char const )'f', (char const )'o', (char const )'r',
1135 (char const )'b', (char const )'e', (char const )'s', (char const )'@',
1136 (char const )'i', (char const )'n', (char const )'c', (char const )'e',
1137 (char const )'p', (char const )'t', (char const )'a', (char const )'.',
1138 (char const )'c', (char const )'o', (char const )'m', (char const )'>',
1139 (char const )'\000'};
1140#line 45 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1141static char const __mod_description45[35] __attribute__((__used__, __unused__,
1142__section__(".modinfo"), __aligned__(1))) =
1143#line 45
1144 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
1145 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
1146 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
1147 (char const )'D', (char const )'e', (char const )'f', (char const )'a',
1148 (char const )'u', (char const )'l', (char const )'t', (char const )'-',
1149 (char const )'O', (char const )'N', (char const )' ', (char const )'L',
1150 (char const )'E', (char const )'D', (char const )' ', (char const )'t',
1151 (char const )'r', (char const )'i', (char const )'g', (char const )'g',
1152 (char const )'e', (char const )'r', (char const )'\000'};
1153#line 46 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1154static char const __mod_license46[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
1155__aligned__(1))) =
1156#line 46
1157 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
1158 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
1159 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
1160#line 64
1161void ldv_check_final_state(void) ;
1162#line 70
1163extern void ldv_initialize(void) ;
1164#line 73
1165extern int __VERIFIER_nondet_int(void) ;
1166#line 76 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1167int LDV_IN_INTERRUPT ;
1168#line 79 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1169void main(void)
1170{ struct led_classdev *var_group1 ;
1171 int tmp ;
1172 int tmp___0 ;
1173 int tmp___1 ;
1174
1175 {
1176 {
1177#line 97
1178 LDV_IN_INTERRUPT = 1;
1179#line 106
1180 ldv_initialize();
1181#line 112
1182 tmp = defon_trig_init();
1183 }
1184#line 112
1185 if (tmp) {
1186#line 113
1187 goto ldv_final;
1188 } else {
1189
1190 }
1191 {
1192#line 117
1193 while (1) {
1194 while_continue: ;
1195 {
1196#line 117
1197 tmp___1 = __VERIFIER_nondet_int();
1198 }
1199#line 117
1200 if (tmp___1) {
1201
1202 } else {
1203#line 117
1204 goto while_break;
1205 }
1206 {
1207#line 120
1208 tmp___0 = __VERIFIER_nondet_int();
1209 }
1210#line 122
1211 if (tmp___0 == 0) {
1212#line 122
1213 goto case_0;
1214 } else {
1215 {
1216#line 138
1217 goto switch_default;
1218#line 120
1219 if (0) {
1220 case_0:
1221 {
1222#line 130
1223 defon_trig_activate(var_group1);
1224 }
1225#line 137
1226 goto switch_break;
1227 switch_default:
1228#line 138
1229 goto switch_break;
1230 } else {
1231 switch_break: ;
1232 }
1233 }
1234 }
1235 }
1236 while_break: ;
1237 }
1238 {
1239#line 150
1240 defon_trig_exit();
1241 }
1242 ldv_final:
1243 {
1244#line 153
1245 ldv_check_final_state();
1246 }
1247#line 156
1248 return;
1249}
1250}
1251#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1252void ldv_blast_assert(void)
1253{
1254
1255 {
1256 ERROR:
1257#line 6
1258 goto ERROR;
1259}
1260}
1261#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1262extern int __VERIFIER_nondet_int(void) ;
1263#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1264int ldv_mutex = 1;
1265#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1266int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1267{ int nondetermined ;
1268
1269 {
1270#line 29
1271 if (ldv_mutex == 1) {
1272
1273 } else {
1274 {
1275#line 29
1276 ldv_blast_assert();
1277 }
1278 }
1279 {
1280#line 32
1281 nondetermined = __VERIFIER_nondet_int();
1282 }
1283#line 35
1284 if (nondetermined) {
1285#line 38
1286 ldv_mutex = 2;
1287#line 40
1288 return (0);
1289 } else {
1290#line 45
1291 return (-4);
1292 }
1293}
1294}
1295#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1296int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1297{ int nondetermined ;
1298
1299 {
1300#line 57
1301 if (ldv_mutex == 1) {
1302
1303 } else {
1304 {
1305#line 57
1306 ldv_blast_assert();
1307 }
1308 }
1309 {
1310#line 60
1311 nondetermined = __VERIFIER_nondet_int();
1312 }
1313#line 63
1314 if (nondetermined) {
1315#line 66
1316 ldv_mutex = 2;
1317#line 68
1318 return (0);
1319 } else {
1320#line 73
1321 return (-4);
1322 }
1323}
1324}
1325#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1326int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1327{ int atomic_value_after_dec ;
1328
1329 {
1330#line 83
1331 if (ldv_mutex == 1) {
1332
1333 } else {
1334 {
1335#line 83
1336 ldv_blast_assert();
1337 }
1338 }
1339 {
1340#line 86
1341 atomic_value_after_dec = __VERIFIER_nondet_int();
1342 }
1343#line 89
1344 if (atomic_value_after_dec == 0) {
1345#line 92
1346 ldv_mutex = 2;
1347#line 94
1348 return (1);
1349 } else {
1350
1351 }
1352#line 98
1353 return (0);
1354}
1355}
1356#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1357void mutex_lock(struct mutex *lock )
1358{
1359
1360 {
1361#line 108
1362 if (ldv_mutex == 1) {
1363
1364 } else {
1365 {
1366#line 108
1367 ldv_blast_assert();
1368 }
1369 }
1370#line 110
1371 ldv_mutex = 2;
1372#line 111
1373 return;
1374}
1375}
1376#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1377int mutex_trylock(struct mutex *lock )
1378{ int nondetermined ;
1379
1380 {
1381#line 121
1382 if (ldv_mutex == 1) {
1383
1384 } else {
1385 {
1386#line 121
1387 ldv_blast_assert();
1388 }
1389 }
1390 {
1391#line 124
1392 nondetermined = __VERIFIER_nondet_int();
1393 }
1394#line 127
1395 if (nondetermined) {
1396#line 130
1397 ldv_mutex = 2;
1398#line 132
1399 return (1);
1400 } else {
1401#line 137
1402 return (0);
1403 }
1404}
1405}
1406#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1407void mutex_unlock(struct mutex *lock )
1408{
1409
1410 {
1411#line 147
1412 if (ldv_mutex == 2) {
1413
1414 } else {
1415 {
1416#line 147
1417 ldv_blast_assert();
1418 }
1419 }
1420#line 149
1421 ldv_mutex = 1;
1422#line 150
1423 return;
1424}
1425}
1426#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1427void ldv_check_final_state(void)
1428{
1429
1430 {
1431#line 156
1432 if (ldv_mutex == 1) {
1433
1434 } else {
1435 {
1436#line 156
1437 ldv_blast_assert();
1438 }
1439 }
1440#line 157
1441 return;
1442}
1443}
1444#line 165 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12614/dscv_tempdir/dscv/ri/32_1/drivers/leds/ledtrig-default-on.c.common.c"
1445long s__builtin_expect(long val , long res )
1446{
1447
1448 {
1449#line 166
1450 return (val);
1451}
1452}