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