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 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 9 "include/linux/dynamic_debug.h"
70struct _ddebug {
71 char const *modname ;
72 char const *function ;
73 char const *filename ;
74 char const *format ;
75 unsigned int lineno : 18 ;
76 unsigned int flags : 8 ;
77} __attribute__((__aligned__(8))) ;
78#line 47
79struct device;
80#line 47
81struct device;
82#line 135 "include/linux/kernel.h"
83struct completion;
84#line 135
85struct completion;
86#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
87struct task_struct;
88#line 20
89struct task_struct;
90#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
91struct task_struct;
92#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
93struct file;
94#line 295
95struct file;
96#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
97struct task_struct;
98#line 329
99struct arch_spinlock;
100#line 329
101struct arch_spinlock;
102#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
103struct task_struct;
104#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
105struct task_struct;
106#line 10 "include/asm-generic/bug.h"
107struct bug_entry {
108 int bug_addr_disp ;
109 int file_disp ;
110 unsigned short line ;
111 unsigned short flags ;
112};
113#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
114struct static_key;
115#line 234
116struct static_key;
117#line 23 "include/asm-generic/atomic-long.h"
118typedef atomic64_t atomic_long_t;
119#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
120typedef u16 __ticket_t;
121#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
122typedef u32 __ticketpair_t;
123#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
124struct __raw_tickets {
125 __ticket_t head ;
126 __ticket_t tail ;
127};
128#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
129union __anonunion____missing_field_name_36 {
130 __ticketpair_t head_tail ;
131 struct __raw_tickets tickets ;
132};
133#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
134struct arch_spinlock {
135 union __anonunion____missing_field_name_36 __annonCompField17 ;
136};
137#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
138typedef struct arch_spinlock arch_spinlock_t;
139#line 12 "include/linux/lockdep.h"
140struct task_struct;
141#line 20 "include/linux/spinlock_types.h"
142struct raw_spinlock {
143 arch_spinlock_t raw_lock ;
144 unsigned int magic ;
145 unsigned int owner_cpu ;
146 void *owner ;
147};
148#line 64 "include/linux/spinlock_types.h"
149union __anonunion____missing_field_name_39 {
150 struct raw_spinlock rlock ;
151};
152#line 64 "include/linux/spinlock_types.h"
153struct spinlock {
154 union __anonunion____missing_field_name_39 __annonCompField19 ;
155};
156#line 64 "include/linux/spinlock_types.h"
157typedef struct spinlock spinlock_t;
158#line 49 "include/linux/wait.h"
159struct __wait_queue_head {
160 spinlock_t lock ;
161 struct list_head task_list ;
162};
163#line 53 "include/linux/wait.h"
164typedef struct __wait_queue_head wait_queue_head_t;
165#line 55
166struct task_struct;
167#line 48 "include/linux/mutex.h"
168struct mutex {
169 atomic_t count ;
170 spinlock_t wait_lock ;
171 struct list_head wait_list ;
172 struct task_struct *owner ;
173 char const *name ;
174 void *magic ;
175};
176#line 25 "include/linux/completion.h"
177struct completion {
178 unsigned int done ;
179 wait_queue_head_t wait ;
180};
181#line 202 "include/linux/ioport.h"
182struct device;
183#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
184struct device;
185#line 46 "include/linux/ktime.h"
186union ktime {
187 s64 tv64 ;
188};
189#line 59 "include/linux/ktime.h"
190typedef union ktime ktime_t;
191#line 10 "include/linux/timer.h"
192struct tvec_base;
193#line 10
194struct tvec_base;
195#line 12 "include/linux/timer.h"
196struct timer_list {
197 struct list_head entry ;
198 unsigned long expires ;
199 struct tvec_base *base ;
200 void (*function)(unsigned long ) ;
201 unsigned long data ;
202 int slack ;
203 int start_pid ;
204 void *start_site ;
205 char start_comm[16] ;
206};
207#line 17 "include/linux/workqueue.h"
208struct work_struct;
209#line 17
210struct work_struct;
211#line 79 "include/linux/workqueue.h"
212struct work_struct {
213 atomic_long_t data ;
214 struct list_head entry ;
215 void (*func)(struct work_struct *work ) ;
216};
217#line 42 "include/linux/pm.h"
218struct device;
219#line 50 "include/linux/pm.h"
220struct pm_message {
221 int event ;
222};
223#line 50 "include/linux/pm.h"
224typedef struct pm_message pm_message_t;
225#line 264 "include/linux/pm.h"
226struct dev_pm_ops {
227 int (*prepare)(struct device *dev ) ;
228 void (*complete)(struct device *dev ) ;
229 int (*suspend)(struct device *dev ) ;
230 int (*resume)(struct device *dev ) ;
231 int (*freeze)(struct device *dev ) ;
232 int (*thaw)(struct device *dev ) ;
233 int (*poweroff)(struct device *dev ) ;
234 int (*restore)(struct device *dev ) ;
235 int (*suspend_late)(struct device *dev ) ;
236 int (*resume_early)(struct device *dev ) ;
237 int (*freeze_late)(struct device *dev ) ;
238 int (*thaw_early)(struct device *dev ) ;
239 int (*poweroff_late)(struct device *dev ) ;
240 int (*restore_early)(struct device *dev ) ;
241 int (*suspend_noirq)(struct device *dev ) ;
242 int (*resume_noirq)(struct device *dev ) ;
243 int (*freeze_noirq)(struct device *dev ) ;
244 int (*thaw_noirq)(struct device *dev ) ;
245 int (*poweroff_noirq)(struct device *dev ) ;
246 int (*restore_noirq)(struct device *dev ) ;
247 int (*runtime_suspend)(struct device *dev ) ;
248 int (*runtime_resume)(struct device *dev ) ;
249 int (*runtime_idle)(struct device *dev ) ;
250};
251#line 458
252enum rpm_status {
253 RPM_ACTIVE = 0,
254 RPM_RESUMING = 1,
255 RPM_SUSPENDED = 2,
256 RPM_SUSPENDING = 3
257} ;
258#line 480
259enum rpm_request {
260 RPM_REQ_NONE = 0,
261 RPM_REQ_IDLE = 1,
262 RPM_REQ_SUSPEND = 2,
263 RPM_REQ_AUTOSUSPEND = 3,
264 RPM_REQ_RESUME = 4
265} ;
266#line 488
267struct wakeup_source;
268#line 488
269struct wakeup_source;
270#line 495 "include/linux/pm.h"
271struct pm_subsys_data {
272 spinlock_t lock ;
273 unsigned int refcount ;
274};
275#line 506
276struct dev_pm_qos_request;
277#line 506
278struct pm_qos_constraints;
279#line 506 "include/linux/pm.h"
280struct dev_pm_info {
281 pm_message_t power_state ;
282 unsigned int can_wakeup : 1 ;
283 unsigned int async_suspend : 1 ;
284 bool is_prepared : 1 ;
285 bool is_suspended : 1 ;
286 bool ignore_children : 1 ;
287 spinlock_t lock ;
288 struct list_head entry ;
289 struct completion completion ;
290 struct wakeup_source *wakeup ;
291 bool wakeup_path : 1 ;
292 struct timer_list suspend_timer ;
293 unsigned long timer_expires ;
294 struct work_struct work ;
295 wait_queue_head_t wait_queue ;
296 atomic_t usage_count ;
297 atomic_t child_count ;
298 unsigned int disable_depth : 3 ;
299 unsigned int idle_notification : 1 ;
300 unsigned int request_pending : 1 ;
301 unsigned int deferred_resume : 1 ;
302 unsigned int run_wake : 1 ;
303 unsigned int runtime_auto : 1 ;
304 unsigned int no_callbacks : 1 ;
305 unsigned int irq_safe : 1 ;
306 unsigned int use_autosuspend : 1 ;
307 unsigned int timer_autosuspends : 1 ;
308 enum rpm_request request ;
309 enum rpm_status runtime_status ;
310 int runtime_error ;
311 int autosuspend_delay ;
312 unsigned long last_busy ;
313 unsigned long active_jiffies ;
314 unsigned long suspended_jiffies ;
315 unsigned long accounting_timestamp ;
316 ktime_t suspend_time ;
317 s64 max_time_suspended_ns ;
318 struct dev_pm_qos_request *pq_req ;
319 struct pm_subsys_data *subsys_data ;
320 struct pm_qos_constraints *constraints ;
321};
322#line 564 "include/linux/pm.h"
323struct dev_pm_domain {
324 struct dev_pm_ops ops ;
325};
326#line 8 "include/linux/vmalloc.h"
327struct vm_area_struct;
328#line 8
329struct vm_area_struct;
330#line 10 "include/linux/gfp.h"
331struct vm_area_struct;
332#line 29 "include/linux/sysctl.h"
333struct completion;
334#line 49 "include/linux/kmod.h"
335struct file;
336#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
337struct task_struct;
338#line 18 "include/linux/elf.h"
339typedef __u64 Elf64_Addr;
340#line 19 "include/linux/elf.h"
341typedef __u16 Elf64_Half;
342#line 23 "include/linux/elf.h"
343typedef __u32 Elf64_Word;
344#line 24 "include/linux/elf.h"
345typedef __u64 Elf64_Xword;
346#line 194 "include/linux/elf.h"
347struct elf64_sym {
348 Elf64_Word st_name ;
349 unsigned char st_info ;
350 unsigned char st_other ;
351 Elf64_Half st_shndx ;
352 Elf64_Addr st_value ;
353 Elf64_Xword st_size ;
354};
355#line 194 "include/linux/elf.h"
356typedef struct elf64_sym Elf64_Sym;
357#line 438
358struct file;
359#line 20 "include/linux/kobject_ns.h"
360struct sock;
361#line 20
362struct sock;
363#line 21
364struct kobject;
365#line 21
366struct kobject;
367#line 27
368enum kobj_ns_type {
369 KOBJ_NS_TYPE_NONE = 0,
370 KOBJ_NS_TYPE_NET = 1,
371 KOBJ_NS_TYPES = 2
372} ;
373#line 40 "include/linux/kobject_ns.h"
374struct kobj_ns_type_operations {
375 enum kobj_ns_type type ;
376 void *(*grab_current_ns)(void) ;
377 void const *(*netlink_ns)(struct sock *sk ) ;
378 void const *(*initial_ns)(void) ;
379 void (*drop_ns)(void * ) ;
380};
381#line 22 "include/linux/sysfs.h"
382struct kobject;
383#line 23
384struct module;
385#line 24
386enum kobj_ns_type;
387#line 26 "include/linux/sysfs.h"
388struct attribute {
389 char const *name ;
390 umode_t mode ;
391};
392#line 56 "include/linux/sysfs.h"
393struct attribute_group {
394 char const *name ;
395 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
396 struct attribute **attrs ;
397};
398#line 85
399struct file;
400#line 86
401struct vm_area_struct;
402#line 88 "include/linux/sysfs.h"
403struct bin_attribute {
404 struct attribute attr ;
405 size_t size ;
406 void *private ;
407 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
408 loff_t , size_t ) ;
409 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
410 loff_t , size_t ) ;
411 int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
412};
413#line 112 "include/linux/sysfs.h"
414struct sysfs_ops {
415 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
416 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
417 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
418};
419#line 118
420struct sysfs_dirent;
421#line 118
422struct sysfs_dirent;
423#line 22 "include/linux/kref.h"
424struct kref {
425 atomic_t refcount ;
426};
427#line 60 "include/linux/kobject.h"
428struct kset;
429#line 60
430struct kobj_type;
431#line 60 "include/linux/kobject.h"
432struct kobject {
433 char const *name ;
434 struct list_head entry ;
435 struct kobject *parent ;
436 struct kset *kset ;
437 struct kobj_type *ktype ;
438 struct sysfs_dirent *sd ;
439 struct kref kref ;
440 unsigned int state_initialized : 1 ;
441 unsigned int state_in_sysfs : 1 ;
442 unsigned int state_add_uevent_sent : 1 ;
443 unsigned int state_remove_uevent_sent : 1 ;
444 unsigned int uevent_suppress : 1 ;
445};
446#line 108 "include/linux/kobject.h"
447struct kobj_type {
448 void (*release)(struct kobject *kobj ) ;
449 struct sysfs_ops const *sysfs_ops ;
450 struct attribute **default_attrs ;
451 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
452 void const *(*namespace)(struct kobject *kobj ) ;
453};
454#line 116 "include/linux/kobject.h"
455struct kobj_uevent_env {
456 char *envp[32] ;
457 int envp_idx ;
458 char buf[2048] ;
459 int buflen ;
460};
461#line 123 "include/linux/kobject.h"
462struct kset_uevent_ops {
463 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
464 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
465 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
466};
467#line 140
468struct sock;
469#line 159 "include/linux/kobject.h"
470struct kset {
471 struct list_head list ;
472 spinlock_t list_lock ;
473 struct kobject kobj ;
474 struct kset_uevent_ops const *uevent_ops ;
475};
476#line 39 "include/linux/moduleparam.h"
477struct kernel_param;
478#line 39
479struct kernel_param;
480#line 41 "include/linux/moduleparam.h"
481struct kernel_param_ops {
482 int (*set)(char const *val , struct kernel_param const *kp ) ;
483 int (*get)(char *buffer , struct kernel_param const *kp ) ;
484 void (*free)(void *arg ) ;
485};
486#line 50
487struct kparam_string;
488#line 50
489struct kparam_array;
490#line 50 "include/linux/moduleparam.h"
491union __anonunion____missing_field_name_199 {
492 void *arg ;
493 struct kparam_string const *str ;
494 struct kparam_array const *arr ;
495};
496#line 50 "include/linux/moduleparam.h"
497struct kernel_param {
498 char const *name ;
499 struct kernel_param_ops const *ops ;
500 u16 perm ;
501 s16 level ;
502 union __anonunion____missing_field_name_199 __annonCompField32 ;
503};
504#line 63 "include/linux/moduleparam.h"
505struct kparam_string {
506 unsigned int maxlen ;
507 char *string ;
508};
509#line 69 "include/linux/moduleparam.h"
510struct kparam_array {
511 unsigned int max ;
512 unsigned int elemsize ;
513 unsigned int *num ;
514 struct kernel_param_ops const *ops ;
515 void *elem ;
516};
517#line 445
518struct module;
519#line 80 "include/linux/jump_label.h"
520struct module;
521#line 143 "include/linux/jump_label.h"
522struct static_key {
523 atomic_t enabled ;
524};
525#line 22 "include/linux/tracepoint.h"
526struct module;
527#line 23
528struct tracepoint;
529#line 23
530struct tracepoint;
531#line 25 "include/linux/tracepoint.h"
532struct tracepoint_func {
533 void *func ;
534 void *data ;
535};
536#line 30 "include/linux/tracepoint.h"
537struct tracepoint {
538 char const *name ;
539 struct static_key key ;
540 void (*regfunc)(void) ;
541 void (*unregfunc)(void) ;
542 struct tracepoint_func *funcs ;
543};
544#line 19 "include/linux/export.h"
545struct kernel_symbol {
546 unsigned long value ;
547 char const *name ;
548};
549#line 8 "include/asm-generic/module.h"
550struct mod_arch_specific {
551
552};
553#line 35 "include/linux/module.h"
554struct module;
555#line 37
556struct module_param_attrs;
557#line 37 "include/linux/module.h"
558struct module_kobject {
559 struct kobject kobj ;
560 struct module *mod ;
561 struct kobject *drivers_dir ;
562 struct module_param_attrs *mp ;
563};
564#line 44 "include/linux/module.h"
565struct module_attribute {
566 struct attribute attr ;
567 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
568 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
569 size_t count ) ;
570 void (*setup)(struct module * , char const * ) ;
571 int (*test)(struct module * ) ;
572 void (*free)(struct module * ) ;
573};
574#line 71
575struct exception_table_entry;
576#line 71
577struct exception_table_entry;
578#line 199
579enum module_state {
580 MODULE_STATE_LIVE = 0,
581 MODULE_STATE_COMING = 1,
582 MODULE_STATE_GOING = 2
583} ;
584#line 215 "include/linux/module.h"
585struct module_ref {
586 unsigned long incs ;
587 unsigned long decs ;
588} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
589#line 220
590struct module_sect_attrs;
591#line 220
592struct module_notes_attrs;
593#line 220
594struct ftrace_event_call;
595#line 220 "include/linux/module.h"
596struct module {
597 enum module_state state ;
598 struct list_head list ;
599 char name[64UL - sizeof(unsigned long )] ;
600 struct module_kobject mkobj ;
601 struct module_attribute *modinfo_attrs ;
602 char const *version ;
603 char const *srcversion ;
604 struct kobject *holders_dir ;
605 struct kernel_symbol const *syms ;
606 unsigned long const *crcs ;
607 unsigned int num_syms ;
608 struct kernel_param *kp ;
609 unsigned int num_kp ;
610 unsigned int num_gpl_syms ;
611 struct kernel_symbol const *gpl_syms ;
612 unsigned long const *gpl_crcs ;
613 struct kernel_symbol const *unused_syms ;
614 unsigned long const *unused_crcs ;
615 unsigned int num_unused_syms ;
616 unsigned int num_unused_gpl_syms ;
617 struct kernel_symbol const *unused_gpl_syms ;
618 unsigned long const *unused_gpl_crcs ;
619 struct kernel_symbol const *gpl_future_syms ;
620 unsigned long const *gpl_future_crcs ;
621 unsigned int num_gpl_future_syms ;
622 unsigned int num_exentries ;
623 struct exception_table_entry *extable ;
624 int (*init)(void) ;
625 void *module_init ;
626 void *module_core ;
627 unsigned int init_size ;
628 unsigned int core_size ;
629 unsigned int init_text_size ;
630 unsigned int core_text_size ;
631 unsigned int init_ro_size ;
632 unsigned int core_ro_size ;
633 struct mod_arch_specific arch ;
634 unsigned int taints ;
635 unsigned int num_bugs ;
636 struct list_head bug_list ;
637 struct bug_entry *bug_table ;
638 Elf64_Sym *symtab ;
639 Elf64_Sym *core_symtab ;
640 unsigned int num_symtab ;
641 unsigned int core_num_syms ;
642 char *strtab ;
643 char *core_strtab ;
644 struct module_sect_attrs *sect_attrs ;
645 struct module_notes_attrs *notes_attrs ;
646 char *args ;
647 void *percpu ;
648 unsigned int percpu_size ;
649 unsigned int num_tracepoints ;
650 struct tracepoint * const *tracepoints_ptrs ;
651 unsigned int num_trace_bprintk_fmt ;
652 char const **trace_bprintk_fmt_start ;
653 struct ftrace_event_call **trace_events ;
654 unsigned int num_trace_events ;
655 struct list_head source_list ;
656 struct list_head target_list ;
657 struct task_struct *waiter ;
658 void (*exit)(void) ;
659 struct module_ref *refptr ;
660 ctor_fn_t *ctors ;
661 unsigned int num_ctors ;
662};
663#line 19 "include/linux/klist.h"
664struct klist_node;
665#line 19
666struct klist_node;
667#line 39 "include/linux/klist.h"
668struct klist_node {
669 void *n_klist ;
670 struct list_head n_node ;
671 struct kref n_ref ;
672};
673#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
674struct dma_map_ops;
675#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
676struct dev_archdata {
677 void *acpi_handle ;
678 struct dma_map_ops *dma_ops ;
679 void *iommu ;
680};
681#line 28 "include/linux/device.h"
682struct device;
683#line 29
684struct device_private;
685#line 29
686struct device_private;
687#line 30
688struct device_driver;
689#line 30
690struct device_driver;
691#line 31
692struct driver_private;
693#line 31
694struct driver_private;
695#line 32
696struct module;
697#line 33
698struct class;
699#line 33
700struct class;
701#line 34
702struct subsys_private;
703#line 34
704struct subsys_private;
705#line 35
706struct bus_type;
707#line 35
708struct bus_type;
709#line 36
710struct device_node;
711#line 36
712struct device_node;
713#line 37
714struct iommu_ops;
715#line 37
716struct iommu_ops;
717#line 39 "include/linux/device.h"
718struct bus_attribute {
719 struct attribute attr ;
720 ssize_t (*show)(struct bus_type *bus , char *buf ) ;
721 ssize_t (*store)(struct bus_type *bus , char const *buf , size_t count ) ;
722};
723#line 89
724struct device_attribute;
725#line 89
726struct driver_attribute;
727#line 89 "include/linux/device.h"
728struct bus_type {
729 char const *name ;
730 char const *dev_name ;
731 struct device *dev_root ;
732 struct bus_attribute *bus_attrs ;
733 struct device_attribute *dev_attrs ;
734 struct driver_attribute *drv_attrs ;
735 int (*match)(struct device *dev , struct device_driver *drv ) ;
736 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
737 int (*probe)(struct device *dev ) ;
738 int (*remove)(struct device *dev ) ;
739 void (*shutdown)(struct device *dev ) ;
740 int (*suspend)(struct device *dev , pm_message_t state ) ;
741 int (*resume)(struct device *dev ) ;
742 struct dev_pm_ops const *pm ;
743 struct iommu_ops *iommu_ops ;
744 struct subsys_private *p ;
745};
746#line 127
747struct device_type;
748#line 214
749struct of_device_id;
750#line 214 "include/linux/device.h"
751struct device_driver {
752 char const *name ;
753 struct bus_type *bus ;
754 struct module *owner ;
755 char const *mod_name ;
756 bool suppress_bind_attrs ;
757 struct of_device_id const *of_match_table ;
758 int (*probe)(struct device *dev ) ;
759 int (*remove)(struct device *dev ) ;
760 void (*shutdown)(struct device *dev ) ;
761 int (*suspend)(struct device *dev , pm_message_t state ) ;
762 int (*resume)(struct device *dev ) ;
763 struct attribute_group const **groups ;
764 struct dev_pm_ops const *pm ;
765 struct driver_private *p ;
766};
767#line 249 "include/linux/device.h"
768struct driver_attribute {
769 struct attribute attr ;
770 ssize_t (*show)(struct device_driver *driver , char *buf ) ;
771 ssize_t (*store)(struct device_driver *driver , char const *buf , size_t count ) ;
772};
773#line 330
774struct class_attribute;
775#line 330 "include/linux/device.h"
776struct class {
777 char const *name ;
778 struct module *owner ;
779 struct class_attribute *class_attrs ;
780 struct device_attribute *dev_attrs ;
781 struct bin_attribute *dev_bin_attrs ;
782 struct kobject *dev_kobj ;
783 int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
784 char *(*devnode)(struct device *dev , umode_t *mode ) ;
785 void (*class_release)(struct class *class ) ;
786 void (*dev_release)(struct device *dev ) ;
787 int (*suspend)(struct device *dev , pm_message_t state ) ;
788 int (*resume)(struct device *dev ) ;
789 struct kobj_ns_type_operations const *ns_type ;
790 void const *(*namespace)(struct device *dev ) ;
791 struct dev_pm_ops const *pm ;
792 struct subsys_private *p ;
793};
794#line 397 "include/linux/device.h"
795struct class_attribute {
796 struct attribute attr ;
797 ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
798 ssize_t (*store)(struct class *class , struct class_attribute *attr , char const *buf ,
799 size_t count ) ;
800 void const *(*namespace)(struct class *class , struct class_attribute const *attr ) ;
801};
802#line 465 "include/linux/device.h"
803struct device_type {
804 char const *name ;
805 struct attribute_group const **groups ;
806 int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
807 char *(*devnode)(struct device *dev , umode_t *mode ) ;
808 void (*release)(struct device *dev ) ;
809 struct dev_pm_ops const *pm ;
810};
811#line 476 "include/linux/device.h"
812struct device_attribute {
813 struct attribute attr ;
814 ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
815 ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const *buf ,
816 size_t count ) ;
817};
818#line 559 "include/linux/device.h"
819struct device_dma_parameters {
820 unsigned int max_segment_size ;
821 unsigned long segment_boundary_mask ;
822};
823#line 627
824struct dma_coherent_mem;
825#line 627 "include/linux/device.h"
826struct device {
827 struct device *parent ;
828 struct device_private *p ;
829 struct kobject kobj ;
830 char const *init_name ;
831 struct device_type const *type ;
832 struct mutex mutex ;
833 struct bus_type *bus ;
834 struct device_driver *driver ;
835 void *platform_data ;
836 struct dev_pm_info power ;
837 struct dev_pm_domain *pm_domain ;
838 int numa_node ;
839 u64 *dma_mask ;
840 u64 coherent_dma_mask ;
841 struct device_dma_parameters *dma_parms ;
842 struct list_head dma_pools ;
843 struct dma_coherent_mem *dma_mem ;
844 struct dev_archdata archdata ;
845 struct device_node *of_node ;
846 dev_t devt ;
847 u32 id ;
848 spinlock_t devres_lock ;
849 struct list_head devres_head ;
850 struct klist_node knode_class ;
851 struct class *class ;
852 struct attribute_group const **groups ;
853 void (*release)(struct device *dev ) ;
854};
855#line 43 "include/linux/pm_wakeup.h"
856struct wakeup_source {
857 char const *name ;
858 struct list_head entry ;
859 spinlock_t lock ;
860 struct timer_list timer ;
861 unsigned long timer_expires ;
862 ktime_t total_time ;
863 ktime_t max_time ;
864 ktime_t last_time ;
865 unsigned long event_count ;
866 unsigned long active_count ;
867 unsigned long relax_count ;
868 unsigned long hit_count ;
869 unsigned int active : 1 ;
870};
871#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
872struct w1_reg_num {
873 __u64 family : 8 ;
874 __u64 id : 48 ;
875 __u64 crc : 8 ;
876};
877#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
878struct w1_slave;
879#line 46
880struct w1_slave;
881#line 48 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
882struct w1_family_ops {
883 int (*add_slave)(struct w1_slave * ) ;
884 void (*remove_slave)(struct w1_slave * ) ;
885};
886#line 54 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
887struct w1_family {
888 struct list_head family_entry ;
889 u8 fid ;
890 struct w1_family_ops *fops ;
891 atomic_t refcnt ;
892};
893#line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
894struct w1_master;
895#line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
896struct w1_slave {
897 struct module *owner ;
898 unsigned char name[32] ;
899 struct list_head w1_slave_entry ;
900 struct w1_reg_num reg_num ;
901 atomic_t refcnt ;
902 u8 rom[9] ;
903 u32 flags ;
904 int ttl ;
905 struct w1_master *master ;
906 struct w1_family *family ;
907 void *family_data ;
908 struct device dev ;
909 struct completion released ;
910};
911#line 90 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
912struct w1_bus_master {
913 void *data ;
914 u8 (*read_bit)(void * ) ;
915 void (*write_bit)(void * , u8 ) ;
916 u8 (*touch_bit)(void * , u8 ) ;
917 u8 (*read_byte)(void * ) ;
918 void (*write_byte)(void * , u8 ) ;
919 u8 (*read_block)(void * , u8 * , int ) ;
920 void (*write_block)(void * , u8 const * , int ) ;
921 u8 (*triplet)(void * , u8 ) ;
922 u8 (*reset_bus)(void * ) ;
923 u8 (*set_pullup)(void * , int ) ;
924 void (*search)(void * , struct w1_master * , u8 , void (*)(struct w1_master * ,
925 u64 ) ) ;
926};
927#line 158 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
928struct w1_master {
929 struct list_head w1_master_entry ;
930 struct module *owner ;
931 unsigned char name[32] ;
932 struct list_head slist ;
933 int max_slave_count ;
934 int slave_count ;
935 unsigned long attempts ;
936 int slave_ttl ;
937 int initialized ;
938 u32 id ;
939 int search_count ;
940 atomic_t refcnt ;
941 void *priv ;
942 int priv_size ;
943 int enable_pullup ;
944 int pullup_duration ;
945 struct task_struct *thread ;
946 struct mutex mutex ;
947 struct device_driver *driver ;
948 struct device dev ;
949 struct w1_bus_master *bus_master ;
950 u32 seq ;
951};
952#line 1 "<compiler builtins>"
953long __builtin_expect(long val , long res ) ;
954#line 49 "include/linux/dynamic_debug.h"
955extern int ( __dynamic_dev_dbg)(struct _ddebug *descriptor ,
956 struct device const *dev ,
957 char const *fmt , ...) ;
958#line 152 "include/linux/mutex.h"
959void mutex_lock(struct mutex *lock ) ;
960#line 153
961int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
962#line 154
963int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
964#line 168
965int mutex_trylock(struct mutex *lock ) ;
966#line 169
967void mutex_unlock(struct mutex *lock ) ;
968#line 170
969int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
970#line 140 "include/linux/sysfs.h"
971extern int __attribute__((__warn_unused_result__)) sysfs_create_bin_file(struct kobject *kobj ,
972 struct bin_attribute const *attr ) ;
973#line 142
974extern void sysfs_remove_bin_file(struct kobject *kobj , struct bin_attribute const *attr ) ;
975#line 67 "include/linux/module.h"
976int init_module(void) ;
977#line 68
978void cleanup_module(void) ;
979#line 69 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
980extern void w1_unregister_family(struct w1_family * ) ;
981#line 70
982extern int w1_register_family(struct w1_family * ) ;
983#line 211 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
984extern void w1_write_8(struct w1_master * , u8 ) ;
985#line 212
986extern u8 w1_read_8(struct w1_master * ) ;
987#line 215
988extern void w1_write_block(struct w1_master * , u8 const * , int ) ;
989#line 218
990extern int w1_reset_select_slave(struct w1_slave *sl ) ;
991#line 219
992extern int w1_reset_resume_command(struct w1_master * ) ;
993#line 222
994__inline static struct w1_slave *dev_to_w1_slave(struct device *dev ) __attribute__((__no_instrument_function__)) ;
995#line 222 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
996__inline static struct w1_slave *dev_to_w1_slave(struct device *dev )
997{ struct device const *__mptr ;
998 struct w1_slave *__cil_tmp3 ;
999 unsigned long __cil_tmp4 ;
1000 unsigned long __cil_tmp5 ;
1001 struct device *__cil_tmp6 ;
1002 unsigned int __cil_tmp7 ;
1003 char *__cil_tmp8 ;
1004 char *__cil_tmp9 ;
1005
1006 {
1007#line 224
1008 __mptr = (struct device const *)dev;
1009 {
1010#line 224
1011 __cil_tmp3 = (struct w1_slave *)0;
1012#line 224
1013 __cil_tmp4 = (unsigned long )__cil_tmp3;
1014#line 224
1015 __cil_tmp5 = __cil_tmp4 + 112;
1016#line 224
1017 __cil_tmp6 = (struct device *)__cil_tmp5;
1018#line 224
1019 __cil_tmp7 = (unsigned int )__cil_tmp6;
1020#line 224
1021 __cil_tmp8 = (char *)__mptr;
1022#line 224
1023 __cil_tmp9 = __cil_tmp8 - __cil_tmp7;
1024#line 224
1025 return ((struct w1_slave *)__cil_tmp9);
1026 }
1027}
1028}
1029#line 227
1030__inline static struct w1_slave *kobj_to_w1_slave(struct kobject *kobj ) __attribute__((__no_instrument_function__)) ;
1031#line 227 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
1032__inline static struct w1_slave *kobj_to_w1_slave(struct kobject *kobj )
1033{ struct kobject const *__mptr ;
1034 struct w1_slave *tmp ;
1035 struct device *__cil_tmp4 ;
1036 unsigned long __cil_tmp5 ;
1037 unsigned long __cil_tmp6 ;
1038 struct kobject *__cil_tmp7 ;
1039 unsigned int __cil_tmp8 ;
1040 char *__cil_tmp9 ;
1041 char *__cil_tmp10 ;
1042 struct device *__cil_tmp11 ;
1043
1044 {
1045 {
1046#line 229
1047 __mptr = (struct kobject const *)kobj;
1048#line 229
1049 __cil_tmp4 = (struct device *)0;
1050#line 229
1051 __cil_tmp5 = (unsigned long )__cil_tmp4;
1052#line 229
1053 __cil_tmp6 = __cil_tmp5 + 16;
1054#line 229
1055 __cil_tmp7 = (struct kobject *)__cil_tmp6;
1056#line 229
1057 __cil_tmp8 = (unsigned int )__cil_tmp7;
1058#line 229
1059 __cil_tmp9 = (char *)__mptr;
1060#line 229
1061 __cil_tmp10 = __cil_tmp9 - __cil_tmp8;
1062#line 229
1063 __cil_tmp11 = (struct device *)__cil_tmp10;
1064#line 229
1065 tmp = dev_to_w1_slave(__cil_tmp11);
1066 }
1067#line 229
1068 return (tmp);
1069}
1070}
1071#line 23 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1072static char const __mod_license23[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
1073__aligned__(1))) =
1074#line 23 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1075 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
1076 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
1077 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
1078#line 24 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1079static char const __mod_author24[55] __attribute__((__used__, __unused__, __section__(".modinfo"),
1080__aligned__(1))) =
1081#line 24
1082 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
1083 (char const )'o', (char const )'r', (char const )'=', (char const )'J',
1084 (char const )'e', (char const )'a', (char const )'n', (char const )'-',
1085 (char const )'F', (char const )'r', (char const )'a', (char const )'n',
1086 (char const )'c', (char const )'o', (char const )'i', (char const )'s',
1087 (char const )' ', (char const )'D', (char const )'a', (char const )'g',
1088 (char const )'e', (char const )'n', (char const )'a', (char const )'i',
1089 (char const )'s', (char const )' ', (char const )'<', (char const )'d',
1090 (char const )'a', (char const )'g', (char const )'e', (char const )'n',
1091 (char const )'a', (char const )'i', (char const )'s', (char const )'j',
1092 (char const )'@', (char const )'s', (char const )'o', (char const )'n',
1093 (char const )'a', (char const )'t', (char const )'e', (char const )'s',
1094 (char const )'t', (char const )'.', (char const )'c', (char const )'o',
1095 (char const )'m', (char const )'>', (char const )'\000'};
1096#line 25 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1097static char const __mod_description25[52] __attribute__((__used__, __unused__,
1098__section__(".modinfo"), __aligned__(1))) =
1099#line 25
1100 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
1101 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
1102 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
1103 (char const )'w', (char const )'1', (char const )' ', (char const )'f',
1104 (char const )'a', (char const )'m', (char const )'i', (char const )'l',
1105 (char const )'y', (char const )' ', (char const )'2', (char const )'9',
1106 (char const )' ', (char const )'d', (char const )'r', (char const )'i',
1107 (char const )'v', (char const )'e', (char const )'r', (char const )' ',
1108 (char const )'f', (char const )'o', (char const )'r', (char const )' ',
1109 (char const )'D', (char const )'S', (char const )'2', (char const )'4',
1110 (char const )'0', (char const )'8', (char const )' ', (char const )'8',
1111 (char const )' ', (char const )'P', (char const )'i', (char const )'n',
1112 (char const )' ', (char const )'I', (char const )'O', (char const )'\000'};
1113#line 49
1114static int _read_reg(struct w1_slave *sl , u8 address , unsigned char *buf ) ;
1115#line 49 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1116static struct _ddebug __attribute__((__aligned__(8))) descriptor __attribute__((__used__,
1117__section__("__verbose"))) = {"w1_ds2408", "_read_reg", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
1118 "Reading with slave: %p, reg addr: %0#4x, buff addr: %p", 51U, 0U};
1119#line 57
1120static int _read_reg(struct w1_slave *sl , u8 address , unsigned char *buf ) ;
1121#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1122static struct _ddebug __attribute__((__aligned__(8))) descriptor___0 __attribute__((__used__,
1123__section__("__verbose"))) = {"w1_ds2408", "_read_reg", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
1124 "mutex locked", 57U, 0U};
1125#line 71
1126static int _read_reg(struct w1_slave *sl , u8 address , unsigned char *buf ) ;
1127#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1128static struct _ddebug __attribute__((__aligned__(8))) descriptor___1 __attribute__((__used__,
1129__section__("__verbose"))) = {"w1_ds2408", "_read_reg", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
1130 "mutex unlocked", 71U, 0U};
1131#line 46 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1132static int _read_reg(struct w1_slave *sl , u8 address , unsigned char *buf )
1133{ u8 wrbuf[3] ;
1134 long tmp ;
1135 long tmp___0 ;
1136 int tmp___1 ;
1137 long tmp___2 ;
1138 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp9 ;
1139 unsigned int __cil_tmp10 ;
1140 unsigned int __cil_tmp11 ;
1141 int __cil_tmp12 ;
1142 int __cil_tmp13 ;
1143 long __cil_tmp14 ;
1144 unsigned long __cil_tmp15 ;
1145 unsigned long __cil_tmp16 ;
1146 struct device *__cil_tmp17 ;
1147 struct device const *__cil_tmp18 ;
1148 unsigned int __cil_tmp19 ;
1149 unsigned long __cil_tmp20 ;
1150 unsigned long __cil_tmp21 ;
1151 struct w1_master *__cil_tmp22 ;
1152 unsigned long __cil_tmp23 ;
1153 unsigned long __cil_tmp24 ;
1154 struct mutex *__cil_tmp25 ;
1155 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp26 ;
1156 unsigned int __cil_tmp27 ;
1157 unsigned int __cil_tmp28 ;
1158 int __cil_tmp29 ;
1159 int __cil_tmp30 ;
1160 long __cil_tmp31 ;
1161 unsigned long __cil_tmp32 ;
1162 unsigned long __cil_tmp33 ;
1163 struct device *__cil_tmp34 ;
1164 struct device const *__cil_tmp35 ;
1165 unsigned long __cil_tmp36 ;
1166 unsigned long __cil_tmp37 ;
1167 struct w1_master *__cil_tmp38 ;
1168 unsigned long __cil_tmp39 ;
1169 unsigned long __cil_tmp40 ;
1170 struct mutex *__cil_tmp41 ;
1171 unsigned long __cil_tmp42 ;
1172 unsigned long __cil_tmp43 ;
1173 unsigned long __cil_tmp44 ;
1174 unsigned long __cil_tmp45 ;
1175 unsigned long __cil_tmp46 ;
1176 unsigned long __cil_tmp47 ;
1177 unsigned long __cil_tmp48 ;
1178 unsigned long __cil_tmp49 ;
1179 struct w1_master *__cil_tmp50 ;
1180 unsigned long __cil_tmp51 ;
1181 unsigned long __cil_tmp52 ;
1182 u8 *__cil_tmp53 ;
1183 u8 const *__cil_tmp54 ;
1184 unsigned long __cil_tmp55 ;
1185 unsigned long __cil_tmp56 ;
1186 struct w1_master *__cil_tmp57 ;
1187 unsigned long __cil_tmp58 ;
1188 unsigned long __cil_tmp59 ;
1189 struct w1_master *__cil_tmp60 ;
1190 unsigned long __cil_tmp61 ;
1191 unsigned long __cil_tmp62 ;
1192 struct mutex *__cil_tmp63 ;
1193 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp64 ;
1194 unsigned int __cil_tmp65 ;
1195 unsigned int __cil_tmp66 ;
1196 int __cil_tmp67 ;
1197 int __cil_tmp68 ;
1198 long __cil_tmp69 ;
1199 unsigned long __cil_tmp70 ;
1200 unsigned long __cil_tmp71 ;
1201 struct device *__cil_tmp72 ;
1202 struct device const *__cil_tmp73 ;
1203
1204 {
1205 {
1206#line 49
1207 while (1) {
1208 while_continue: ;
1209 {
1210#line 49
1211 while (1) {
1212 while_continue___0: ;
1213 {
1214#line 49
1215 __cil_tmp9 = & descriptor;
1216#line 49
1217 __cil_tmp10 = __cil_tmp9->flags;
1218#line 49
1219 __cil_tmp11 = __cil_tmp10 & 1U;
1220#line 49
1221 __cil_tmp12 = ! __cil_tmp11;
1222#line 49
1223 __cil_tmp13 = ! __cil_tmp12;
1224#line 49
1225 __cil_tmp14 = (long )__cil_tmp13;
1226#line 49
1227 tmp = __builtin_expect(__cil_tmp14, 0L);
1228 }
1229#line 49
1230 if (tmp) {
1231 {
1232#line 49
1233 __cil_tmp15 = (unsigned long )sl;
1234#line 49
1235 __cil_tmp16 = __cil_tmp15 + 112;
1236#line 49
1237 __cil_tmp17 = (struct device *)__cil_tmp16;
1238#line 49
1239 __cil_tmp18 = (struct device const *)__cil_tmp17;
1240#line 49
1241 __cil_tmp19 = (unsigned int )address;
1242#line 49
1243 __dynamic_dev_dbg(& descriptor, __cil_tmp18, "Reading with slave: %p, reg addr: %0#4x, buff addr: %p",
1244 sl, __cil_tmp19, buf);
1245 }
1246 } else {
1247
1248 }
1249#line 49
1250 goto while_break___0;
1251 }
1252 while_break___0: ;
1253 }
1254#line 49
1255 goto while_break;
1256 }
1257 while_break: ;
1258 }
1259#line 53
1260 if (! buf) {
1261#line 54
1262 return (-22);
1263 } else {
1264
1265 }
1266 {
1267#line 56
1268 __cil_tmp20 = (unsigned long )sl;
1269#line 56
1270 __cil_tmp21 = __cil_tmp20 + 88;
1271#line 56
1272 __cil_tmp22 = *((struct w1_master **)__cil_tmp21);
1273#line 56
1274 __cil_tmp23 = (unsigned long )__cil_tmp22;
1275#line 56
1276 __cil_tmp24 = __cil_tmp23 + 144;
1277#line 56
1278 __cil_tmp25 = (struct mutex *)__cil_tmp24;
1279#line 56
1280 mutex_lock(__cil_tmp25);
1281 }
1282 {
1283#line 57
1284 while (1) {
1285 while_continue___1: ;
1286 {
1287#line 57
1288 while (1) {
1289 while_continue___2: ;
1290 {
1291#line 57
1292 __cil_tmp26 = & descriptor___0;
1293#line 57
1294 __cil_tmp27 = __cil_tmp26->flags;
1295#line 57
1296 __cil_tmp28 = __cil_tmp27 & 1U;
1297#line 57
1298 __cil_tmp29 = ! __cil_tmp28;
1299#line 57
1300 __cil_tmp30 = ! __cil_tmp29;
1301#line 57
1302 __cil_tmp31 = (long )__cil_tmp30;
1303#line 57
1304 tmp___0 = __builtin_expect(__cil_tmp31, 0L);
1305 }
1306#line 57
1307 if (tmp___0) {
1308 {
1309#line 57
1310 __cil_tmp32 = (unsigned long )sl;
1311#line 57
1312 __cil_tmp33 = __cil_tmp32 + 112;
1313#line 57
1314 __cil_tmp34 = (struct device *)__cil_tmp33;
1315#line 57
1316 __cil_tmp35 = (struct device const *)__cil_tmp34;
1317#line 57
1318 __dynamic_dev_dbg(& descriptor___0, __cil_tmp35, "mutex locked");
1319 }
1320 } else {
1321
1322 }
1323#line 57
1324 goto while_break___2;
1325 }
1326 while_break___2: ;
1327 }
1328#line 57
1329 goto while_break___1;
1330 }
1331 while_break___1: ;
1332 }
1333 {
1334#line 59
1335 tmp___1 = w1_reset_select_slave(sl);
1336 }
1337#line 59
1338 if (tmp___1) {
1339 {
1340#line 60
1341 __cil_tmp36 = (unsigned long )sl;
1342#line 60
1343 __cil_tmp37 = __cil_tmp36 + 88;
1344#line 60
1345 __cil_tmp38 = *((struct w1_master **)__cil_tmp37);
1346#line 60
1347 __cil_tmp39 = (unsigned long )__cil_tmp38;
1348#line 60
1349 __cil_tmp40 = __cil_tmp39 + 144;
1350#line 60
1351 __cil_tmp41 = (struct mutex *)__cil_tmp40;
1352#line 60
1353 mutex_unlock(__cil_tmp41);
1354 }
1355#line 61
1356 return (-5);
1357 } else {
1358
1359 }
1360 {
1361#line 64
1362 __cil_tmp42 = 0 * 1UL;
1363#line 64
1364 __cil_tmp43 = (unsigned long )(wrbuf) + __cil_tmp42;
1365#line 64
1366 *((u8 *)__cil_tmp43) = (u8 )240;
1367#line 65
1368 __cil_tmp44 = 1 * 1UL;
1369#line 65
1370 __cil_tmp45 = (unsigned long )(wrbuf) + __cil_tmp44;
1371#line 65
1372 *((u8 *)__cil_tmp45) = address;
1373#line 66
1374 __cil_tmp46 = 2 * 1UL;
1375#line 66
1376 __cil_tmp47 = (unsigned long )(wrbuf) + __cil_tmp46;
1377#line 66
1378 *((u8 *)__cil_tmp47) = (u8 )0;
1379#line 67
1380 __cil_tmp48 = (unsigned long )sl;
1381#line 67
1382 __cil_tmp49 = __cil_tmp48 + 88;
1383#line 67
1384 __cil_tmp50 = *((struct w1_master **)__cil_tmp49);
1385#line 67
1386 __cil_tmp51 = 0 * 1UL;
1387#line 67
1388 __cil_tmp52 = (unsigned long )(wrbuf) + __cil_tmp51;
1389#line 67
1390 __cil_tmp53 = (u8 *)__cil_tmp52;
1391#line 67
1392 __cil_tmp54 = (u8 const *)__cil_tmp53;
1393#line 67
1394 w1_write_block(__cil_tmp50, __cil_tmp54, 3);
1395#line 68
1396 __cil_tmp55 = (unsigned long )sl;
1397#line 68
1398 __cil_tmp56 = __cil_tmp55 + 88;
1399#line 68
1400 __cil_tmp57 = *((struct w1_master **)__cil_tmp56);
1401#line 68
1402 *buf = w1_read_8(__cil_tmp57);
1403#line 70
1404 __cil_tmp58 = (unsigned long )sl;
1405#line 70
1406 __cil_tmp59 = __cil_tmp58 + 88;
1407#line 70
1408 __cil_tmp60 = *((struct w1_master **)__cil_tmp59);
1409#line 70
1410 __cil_tmp61 = (unsigned long )__cil_tmp60;
1411#line 70
1412 __cil_tmp62 = __cil_tmp61 + 144;
1413#line 70
1414 __cil_tmp63 = (struct mutex *)__cil_tmp62;
1415#line 70
1416 mutex_unlock(__cil_tmp63);
1417 }
1418 {
1419#line 71
1420 while (1) {
1421 while_continue___3: ;
1422 {
1423#line 71
1424 while (1) {
1425 while_continue___4: ;
1426 {
1427#line 71
1428 __cil_tmp64 = & descriptor___1;
1429#line 71
1430 __cil_tmp65 = __cil_tmp64->flags;
1431#line 71
1432 __cil_tmp66 = __cil_tmp65 & 1U;
1433#line 71
1434 __cil_tmp67 = ! __cil_tmp66;
1435#line 71
1436 __cil_tmp68 = ! __cil_tmp67;
1437#line 71
1438 __cil_tmp69 = (long )__cil_tmp68;
1439#line 71
1440 tmp___2 = __builtin_expect(__cil_tmp69, 0L);
1441 }
1442#line 71
1443 if (tmp___2) {
1444 {
1445#line 71
1446 __cil_tmp70 = (unsigned long )sl;
1447#line 71
1448 __cil_tmp71 = __cil_tmp70 + 112;
1449#line 71
1450 __cil_tmp72 = (struct device *)__cil_tmp71;
1451#line 71
1452 __cil_tmp73 = (struct device const *)__cil_tmp72;
1453#line 71
1454 __dynamic_dev_dbg(& descriptor___1, __cil_tmp73, "mutex unlocked");
1455 }
1456 } else {
1457
1458 }
1459#line 71
1460 goto while_break___4;
1461 }
1462 while_break___4: ;
1463 }
1464#line 71
1465 goto while_break___3;
1466 }
1467 while_break___3: ;
1468 }
1469#line 72
1470 return (1);
1471}
1472}
1473#line 80
1474static ssize_t w1_f29_read_state(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1475 char *buf , loff_t off , size_t count ) ;
1476#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1477static struct _ddebug __attribute__((__aligned__(8))) descriptor___2 __attribute__((__used__,
1478__section__("__verbose"))) = {"w1_ds2408", "w1_f29_read_state", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
1479 "Reading %s kobj: %p, off: %0#10x, count: %zu, buff addr: %p", 82U, 0U};
1480#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1481static ssize_t w1_f29_read_state(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1482 char *buf , loff_t off , size_t count )
1483{ struct w1_slave *tmp ;
1484 long tmp___0 ;
1485 struct w1_slave *tmp___1 ;
1486 int tmp___2 ;
1487 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp11 ;
1488 unsigned int __cil_tmp12 ;
1489 unsigned int __cil_tmp13 ;
1490 int __cil_tmp14 ;
1491 int __cil_tmp15 ;
1492 long __cil_tmp16 ;
1493 unsigned long __cil_tmp17 ;
1494 unsigned long __cil_tmp18 ;
1495 struct device *__cil_tmp19 ;
1496 struct device const *__cil_tmp20 ;
1497 char const *__cil_tmp21 ;
1498 unsigned int __cil_tmp22 ;
1499 u8 __cil_tmp23 ;
1500 unsigned char *__cil_tmp24 ;
1501
1502 {
1503 {
1504#line 80
1505 while (1) {
1506 while_continue: ;
1507 {
1508#line 80
1509 while (1) {
1510 while_continue___0: ;
1511 {
1512#line 80
1513 __cil_tmp11 = & descriptor___2;
1514#line 80
1515 __cil_tmp12 = __cil_tmp11->flags;
1516#line 80
1517 __cil_tmp13 = __cil_tmp12 & 1U;
1518#line 80
1519 __cil_tmp14 = ! __cil_tmp13;
1520#line 80
1521 __cil_tmp15 = ! __cil_tmp14;
1522#line 80
1523 __cil_tmp16 = (long )__cil_tmp15;
1524#line 80
1525 tmp___0 = __builtin_expect(__cil_tmp16, 0L);
1526 }
1527#line 80
1528 if (tmp___0) {
1529 {
1530#line 80
1531 tmp = kobj_to_w1_slave(kobj);
1532#line 80
1533 __cil_tmp17 = (unsigned long )tmp;
1534#line 80
1535 __cil_tmp18 = __cil_tmp17 + 112;
1536#line 80
1537 __cil_tmp19 = (struct device *)__cil_tmp18;
1538#line 80
1539 __cil_tmp20 = (struct device const *)__cil_tmp19;
1540#line 80
1541 __cil_tmp21 = *((char const **)bin_attr);
1542#line 80
1543 __cil_tmp22 = (unsigned int )off;
1544#line 80
1545 __dynamic_dev_dbg(& descriptor___2, __cil_tmp20, "Reading %s kobj: %p, off: %0#10x, count: %zu, buff addr: %p",
1546 __cil_tmp21, kobj, __cil_tmp22, count, buf);
1547 }
1548 } else {
1549
1550 }
1551#line 80
1552 goto while_break___0;
1553 }
1554 while_break___0: ;
1555 }
1556#line 80
1557 goto while_break;
1558 }
1559 while_break: ;
1560 }
1561#line 83
1562 if (count != 1UL) {
1563#line 84
1564 return ((ssize_t )-14);
1565 } else
1566#line 83
1567 if (off != 0LL) {
1568#line 84
1569 return ((ssize_t )-14);
1570 } else {
1571
1572 }
1573 {
1574#line 85
1575 tmp___1 = kobj_to_w1_slave(kobj);
1576#line 85
1577 __cil_tmp23 = (u8 )136;
1578#line 85
1579 __cil_tmp24 = (unsigned char *)buf;
1580#line 85
1581 tmp___2 = _read_reg(tmp___1, __cil_tmp23, __cil_tmp24);
1582 }
1583#line 85
1584 return ((ssize_t )tmp___2);
1585}
1586}
1587#line 93
1588static ssize_t w1_f29_read_output(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1589 char *buf , loff_t off , size_t count ) ;
1590#line 93 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1591static struct _ddebug __attribute__((__aligned__(8))) descriptor___3 __attribute__((__used__,
1592__section__("__verbose"))) = {"w1_ds2408", "w1_f29_read_output", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
1593 "Reading %s kobj: %p, off: %0#10x, count: %zu, buff addr: %p", 95U, 0U};
1594#line 88 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1595static ssize_t w1_f29_read_output(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1596 char *buf , loff_t off , size_t count )
1597{ struct w1_slave *tmp ;
1598 long tmp___0 ;
1599 struct w1_slave *tmp___1 ;
1600 int tmp___2 ;
1601 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp11 ;
1602 unsigned int __cil_tmp12 ;
1603 unsigned int __cil_tmp13 ;
1604 int __cil_tmp14 ;
1605 int __cil_tmp15 ;
1606 long __cil_tmp16 ;
1607 unsigned long __cil_tmp17 ;
1608 unsigned long __cil_tmp18 ;
1609 struct device *__cil_tmp19 ;
1610 struct device const *__cil_tmp20 ;
1611 char const *__cil_tmp21 ;
1612 unsigned int __cil_tmp22 ;
1613 u8 __cil_tmp23 ;
1614 unsigned char *__cil_tmp24 ;
1615
1616 {
1617 {
1618#line 93
1619 while (1) {
1620 while_continue: ;
1621 {
1622#line 93
1623 while (1) {
1624 while_continue___0: ;
1625 {
1626#line 93
1627 __cil_tmp11 = & descriptor___3;
1628#line 93
1629 __cil_tmp12 = __cil_tmp11->flags;
1630#line 93
1631 __cil_tmp13 = __cil_tmp12 & 1U;
1632#line 93
1633 __cil_tmp14 = ! __cil_tmp13;
1634#line 93
1635 __cil_tmp15 = ! __cil_tmp14;
1636#line 93
1637 __cil_tmp16 = (long )__cil_tmp15;
1638#line 93
1639 tmp___0 = __builtin_expect(__cil_tmp16, 0L);
1640 }
1641#line 93
1642 if (tmp___0) {
1643 {
1644#line 93
1645 tmp = kobj_to_w1_slave(kobj);
1646#line 93
1647 __cil_tmp17 = (unsigned long )tmp;
1648#line 93
1649 __cil_tmp18 = __cil_tmp17 + 112;
1650#line 93
1651 __cil_tmp19 = (struct device *)__cil_tmp18;
1652#line 93
1653 __cil_tmp20 = (struct device const *)__cil_tmp19;
1654#line 93
1655 __cil_tmp21 = *((char const **)bin_attr);
1656#line 93
1657 __cil_tmp22 = (unsigned int )off;
1658#line 93
1659 __dynamic_dev_dbg(& descriptor___3, __cil_tmp20, "Reading %s kobj: %p, off: %0#10x, count: %zu, buff addr: %p",
1660 __cil_tmp21, kobj, __cil_tmp22, count, buf);
1661 }
1662 } else {
1663
1664 }
1665#line 93
1666 goto while_break___0;
1667 }
1668 while_break___0: ;
1669 }
1670#line 93
1671 goto while_break;
1672 }
1673 while_break: ;
1674 }
1675#line 96
1676 if (count != 1UL) {
1677#line 97
1678 return ((ssize_t )-14);
1679 } else
1680#line 96
1681 if (off != 0LL) {
1682#line 97
1683 return ((ssize_t )-14);
1684 } else {
1685
1686 }
1687 {
1688#line 98
1689 tmp___1 = kobj_to_w1_slave(kobj);
1690#line 98
1691 __cil_tmp23 = (u8 )137;
1692#line 98
1693 __cil_tmp24 = (unsigned char *)buf;
1694#line 98
1695 tmp___2 = _read_reg(tmp___1, __cil_tmp23, __cil_tmp24);
1696 }
1697#line 98
1698 return ((ssize_t )tmp___2);
1699}
1700}
1701#line 107
1702static ssize_t w1_f29_read_activity(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1703 char *buf , loff_t off , size_t count ) ;
1704#line 107 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1705static struct _ddebug __attribute__((__aligned__(8))) descriptor___4 __attribute__((__used__,
1706__section__("__verbose"))) = {"w1_ds2408", "w1_f29_read_activity", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
1707 "Reading %s kobj: %p, off: %0#10x, count: %zu, buff addr: %p", 109U, 0U};
1708#line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1709static ssize_t w1_f29_read_activity(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1710 char *buf , loff_t off , size_t count )
1711{ struct w1_slave *tmp ;
1712 long tmp___0 ;
1713 struct w1_slave *tmp___1 ;
1714 int tmp___2 ;
1715 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp11 ;
1716 unsigned int __cil_tmp12 ;
1717 unsigned int __cil_tmp13 ;
1718 int __cil_tmp14 ;
1719 int __cil_tmp15 ;
1720 long __cil_tmp16 ;
1721 unsigned long __cil_tmp17 ;
1722 unsigned long __cil_tmp18 ;
1723 struct device *__cil_tmp19 ;
1724 struct device const *__cil_tmp20 ;
1725 char const *__cil_tmp21 ;
1726 unsigned int __cil_tmp22 ;
1727 u8 __cil_tmp23 ;
1728 unsigned char *__cil_tmp24 ;
1729
1730 {
1731 {
1732#line 107
1733 while (1) {
1734 while_continue: ;
1735 {
1736#line 107
1737 while (1) {
1738 while_continue___0: ;
1739 {
1740#line 107
1741 __cil_tmp11 = & descriptor___4;
1742#line 107
1743 __cil_tmp12 = __cil_tmp11->flags;
1744#line 107
1745 __cil_tmp13 = __cil_tmp12 & 1U;
1746#line 107
1747 __cil_tmp14 = ! __cil_tmp13;
1748#line 107
1749 __cil_tmp15 = ! __cil_tmp14;
1750#line 107
1751 __cil_tmp16 = (long )__cil_tmp15;
1752#line 107
1753 tmp___0 = __builtin_expect(__cil_tmp16, 0L);
1754 }
1755#line 107
1756 if (tmp___0) {
1757 {
1758#line 107
1759 tmp = kobj_to_w1_slave(kobj);
1760#line 107
1761 __cil_tmp17 = (unsigned long )tmp;
1762#line 107
1763 __cil_tmp18 = __cil_tmp17 + 112;
1764#line 107
1765 __cil_tmp19 = (struct device *)__cil_tmp18;
1766#line 107
1767 __cil_tmp20 = (struct device const *)__cil_tmp19;
1768#line 107
1769 __cil_tmp21 = *((char const **)bin_attr);
1770#line 107
1771 __cil_tmp22 = (unsigned int )off;
1772#line 107
1773 __dynamic_dev_dbg(& descriptor___4, __cil_tmp20, "Reading %s kobj: %p, off: %0#10x, count: %zu, buff addr: %p",
1774 __cil_tmp21, kobj, __cil_tmp22, count, buf);
1775 }
1776 } else {
1777
1778 }
1779#line 107
1780 goto while_break___0;
1781 }
1782 while_break___0: ;
1783 }
1784#line 107
1785 goto while_break;
1786 }
1787 while_break: ;
1788 }
1789#line 110
1790 if (count != 1UL) {
1791#line 111
1792 return ((ssize_t )-14);
1793 } else
1794#line 110
1795 if (off != 0LL) {
1796#line 111
1797 return ((ssize_t )-14);
1798 } else {
1799
1800 }
1801 {
1802#line 112
1803 tmp___1 = kobj_to_w1_slave(kobj);
1804#line 112
1805 __cil_tmp23 = (u8 )138;
1806#line 112
1807 __cil_tmp24 = (unsigned char *)buf;
1808#line 112
1809 tmp___2 = _read_reg(tmp___1, __cil_tmp23, __cil_tmp24);
1810 }
1811#line 112
1812 return ((ssize_t )tmp___2);
1813}
1814}
1815#line 121
1816static ssize_t w1_f29_read_cond_search_mask(struct file *filp , struct kobject *kobj ,
1817 struct bin_attribute *bin_attr , char *buf ,
1818 loff_t off , size_t count ) ;
1819#line 121 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1820static struct _ddebug __attribute__((__aligned__(8))) descriptor___5 __attribute__((__used__,
1821__section__("__verbose"))) = {"w1_ds2408", "w1_f29_read_cond_search_mask", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
1822 "Reading %s kobj: %p, off: %0#10x, count: %zu, buff addr: %p", 123U, 0U};
1823#line 116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1824static ssize_t w1_f29_read_cond_search_mask(struct file *filp , struct kobject *kobj ,
1825 struct bin_attribute *bin_attr , char *buf ,
1826 loff_t off , size_t count )
1827{ struct w1_slave *tmp ;
1828 long tmp___0 ;
1829 struct w1_slave *tmp___1 ;
1830 int tmp___2 ;
1831 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp11 ;
1832 unsigned int __cil_tmp12 ;
1833 unsigned int __cil_tmp13 ;
1834 int __cil_tmp14 ;
1835 int __cil_tmp15 ;
1836 long __cil_tmp16 ;
1837 unsigned long __cil_tmp17 ;
1838 unsigned long __cil_tmp18 ;
1839 struct device *__cil_tmp19 ;
1840 struct device const *__cil_tmp20 ;
1841 char const *__cil_tmp21 ;
1842 unsigned int __cil_tmp22 ;
1843 u8 __cil_tmp23 ;
1844 unsigned char *__cil_tmp24 ;
1845
1846 {
1847 {
1848#line 121
1849 while (1) {
1850 while_continue: ;
1851 {
1852#line 121
1853 while (1) {
1854 while_continue___0: ;
1855 {
1856#line 121
1857 __cil_tmp11 = & descriptor___5;
1858#line 121
1859 __cil_tmp12 = __cil_tmp11->flags;
1860#line 121
1861 __cil_tmp13 = __cil_tmp12 & 1U;
1862#line 121
1863 __cil_tmp14 = ! __cil_tmp13;
1864#line 121
1865 __cil_tmp15 = ! __cil_tmp14;
1866#line 121
1867 __cil_tmp16 = (long )__cil_tmp15;
1868#line 121
1869 tmp___0 = __builtin_expect(__cil_tmp16, 0L);
1870 }
1871#line 121
1872 if (tmp___0) {
1873 {
1874#line 121
1875 tmp = kobj_to_w1_slave(kobj);
1876#line 121
1877 __cil_tmp17 = (unsigned long )tmp;
1878#line 121
1879 __cil_tmp18 = __cil_tmp17 + 112;
1880#line 121
1881 __cil_tmp19 = (struct device *)__cil_tmp18;
1882#line 121
1883 __cil_tmp20 = (struct device const *)__cil_tmp19;
1884#line 121
1885 __cil_tmp21 = *((char const **)bin_attr);
1886#line 121
1887 __cil_tmp22 = (unsigned int )off;
1888#line 121
1889 __dynamic_dev_dbg(& descriptor___5, __cil_tmp20, "Reading %s kobj: %p, off: %0#10x, count: %zu, buff addr: %p",
1890 __cil_tmp21, kobj, __cil_tmp22, count, buf);
1891 }
1892 } else {
1893
1894 }
1895#line 121
1896 goto while_break___0;
1897 }
1898 while_break___0: ;
1899 }
1900#line 121
1901 goto while_break;
1902 }
1903 while_break: ;
1904 }
1905#line 124
1906 if (count != 1UL) {
1907#line 125
1908 return ((ssize_t )-14);
1909 } else
1910#line 124
1911 if (off != 0LL) {
1912#line 125
1913 return ((ssize_t )-14);
1914 } else {
1915
1916 }
1917 {
1918#line 126
1919 tmp___1 = kobj_to_w1_slave(kobj);
1920#line 126
1921 __cil_tmp23 = (u8 )139;
1922#line 126
1923 __cil_tmp24 = (unsigned char *)buf;
1924#line 126
1925 tmp___2 = _read_reg(tmp___1, __cil_tmp23, __cil_tmp24);
1926 }
1927#line 126
1928 return ((ssize_t )tmp___2);
1929}
1930}
1931#line 130 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1932static ssize_t w1_f29_read_cond_search_polarity(struct file *filp , struct kobject *kobj ,
1933 struct bin_attribute *bin_attr , char *buf ,
1934 loff_t off , size_t count )
1935{ struct w1_slave *tmp ;
1936 int tmp___0 ;
1937 u8 __cil_tmp9 ;
1938 unsigned char *__cil_tmp10 ;
1939
1940 {
1941#line 135
1942 if (count != 1UL) {
1943#line 136
1944 return ((ssize_t )-14);
1945 } else
1946#line 135
1947 if (off != 0LL) {
1948#line 136
1949 return ((ssize_t )-14);
1950 } else {
1951
1952 }
1953 {
1954#line 137
1955 tmp = kobj_to_w1_slave(kobj);
1956#line 137
1957 __cil_tmp9 = (u8 )140;
1958#line 137
1959 __cil_tmp10 = (unsigned char *)buf;
1960#line 137
1961 tmp___0 = _read_reg(tmp, __cil_tmp9, __cil_tmp10);
1962 }
1963#line 137
1964 return ((ssize_t )tmp___0);
1965}
1966}
1967#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
1968static ssize_t w1_f29_read_status_control(struct file *filp , struct kobject *kobj ,
1969 struct bin_attribute *bin_attr , char *buf ,
1970 loff_t off , size_t count )
1971{ struct w1_slave *tmp ;
1972 int tmp___0 ;
1973 u8 __cil_tmp9 ;
1974 unsigned char *__cil_tmp10 ;
1975
1976 {
1977#line 146
1978 if (count != 1UL) {
1979#line 147
1980 return ((ssize_t )-14);
1981 } else
1982#line 146
1983 if (off != 0LL) {
1984#line 147
1985 return ((ssize_t )-14);
1986 } else {
1987
1988 }
1989 {
1990#line 148
1991 tmp = kobj_to_w1_slave(kobj);
1992#line 148
1993 __cil_tmp9 = (u8 )141;
1994#line 148
1995 __cil_tmp10 = (unsigned char *)buf;
1996#line 148
1997 tmp___0 = _read_reg(tmp, __cil_tmp9, __cil_tmp10);
1998 }
1999#line 148
2000 return ((ssize_t )tmp___0);
2001}
2002}
2003#line 168
2004static ssize_t w1_f29_write_output(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
2005 char *buf , loff_t off , size_t count ) ;
2006#line 168 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
2007static struct _ddebug __attribute__((__aligned__(8))) descriptor___6 __attribute__((__used__,
2008__section__("__verbose"))) = {"w1_ds2408", "w1_f29_write_output", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
2009 "locking mutex for write_output", 168U, 0U};
2010#line 170
2011static ssize_t w1_f29_write_output(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
2012 char *buf , loff_t off , size_t count ) ;
2013#line 170 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
2014static struct _ddebug __attribute__((__aligned__(8))) descriptor___7 __attribute__((__used__,
2015__section__("__verbose"))) = {"w1_ds2408", "w1_f29_write_output", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
2016 "mutex locked", 170U, 0U};
2017#line 205
2018static ssize_t w1_f29_write_output(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
2019 char *buf , loff_t off , size_t count ) ;
2020#line 205 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
2021static struct _ddebug __attribute__((__aligned__(8))) descriptor___8 __attribute__((__used__,
2022__section__("__verbose"))) = {"w1_ds2408", "w1_f29_write_output", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
2023 "mutex unlocked, retries:%d", 206U, 0U};
2024#line 212
2025static ssize_t w1_f29_write_output(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
2026 char *buf , loff_t off , size_t count ) ;
2027#line 212 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
2028static struct _ddebug __attribute__((__aligned__(8))) descriptor___9 __attribute__((__used__,
2029__section__("__verbose"))) = {"w1_ds2408", "w1_f29_write_output", "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c",
2030 "mutex unlocked in error, retries:%d", 212U, 0U};
2031#line 155 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
2032static ssize_t w1_f29_write_output(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
2033 char *buf , loff_t off , size_t count )
2034{ struct w1_slave *sl ;
2035 struct w1_slave *tmp ;
2036 u8 w1_buf[3] ;
2037 u8 readBack ;
2038 unsigned int retries ;
2039 long tmp___0 ;
2040 long tmp___1 ;
2041 int tmp___2 ;
2042 int tmp___3 ;
2043 long tmp___4 ;
2044 u8 tmp___5 ;
2045 unsigned int tmp___6 ;
2046 long tmp___7 ;
2047 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp20 ;
2048 unsigned int __cil_tmp21 ;
2049 unsigned int __cil_tmp22 ;
2050 int __cil_tmp23 ;
2051 int __cil_tmp24 ;
2052 long __cil_tmp25 ;
2053 unsigned long __cil_tmp26 ;
2054 unsigned long __cil_tmp27 ;
2055 struct device *__cil_tmp28 ;
2056 struct device const *__cil_tmp29 ;
2057 unsigned long __cil_tmp30 ;
2058 unsigned long __cil_tmp31 ;
2059 struct w1_master *__cil_tmp32 ;
2060 unsigned long __cil_tmp33 ;
2061 unsigned long __cil_tmp34 ;
2062 struct mutex *__cil_tmp35 ;
2063 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp36 ;
2064 unsigned int __cil_tmp37 ;
2065 unsigned int __cil_tmp38 ;
2066 int __cil_tmp39 ;
2067 int __cil_tmp40 ;
2068 long __cil_tmp41 ;
2069 unsigned long __cil_tmp42 ;
2070 unsigned long __cil_tmp43 ;
2071 struct device *__cil_tmp44 ;
2072 struct device const *__cil_tmp45 ;
2073 unsigned long __cil_tmp46 ;
2074 unsigned long __cil_tmp47 ;
2075 unsigned long __cil_tmp48 ;
2076 unsigned long __cil_tmp49 ;
2077 char __cil_tmp50 ;
2078 unsigned long __cil_tmp51 ;
2079 unsigned long __cil_tmp52 ;
2080 char __cil_tmp53 ;
2081 int __cil_tmp54 ;
2082 int __cil_tmp55 ;
2083 unsigned long __cil_tmp56 ;
2084 unsigned long __cil_tmp57 ;
2085 struct w1_master *__cil_tmp58 ;
2086 unsigned long __cil_tmp59 ;
2087 unsigned long __cil_tmp60 ;
2088 u8 *__cil_tmp61 ;
2089 u8 const *__cil_tmp62 ;
2090 unsigned long __cil_tmp63 ;
2091 unsigned long __cil_tmp64 ;
2092 struct w1_master *__cil_tmp65 ;
2093 unsigned long __cil_tmp66 ;
2094 unsigned long __cil_tmp67 ;
2095 struct w1_master *__cil_tmp68 ;
2096 int __cil_tmp69 ;
2097 unsigned long __cil_tmp70 ;
2098 unsigned long __cil_tmp71 ;
2099 unsigned long __cil_tmp72 ;
2100 unsigned long __cil_tmp73 ;
2101 unsigned long __cil_tmp74 ;
2102 unsigned long __cil_tmp75 ;
2103 unsigned long __cil_tmp76 ;
2104 unsigned long __cil_tmp77 ;
2105 struct w1_master *__cil_tmp78 ;
2106 unsigned long __cil_tmp79 ;
2107 unsigned long __cil_tmp80 ;
2108 u8 *__cil_tmp81 ;
2109 u8 const *__cil_tmp82 ;
2110 unsigned long __cil_tmp83 ;
2111 unsigned long __cil_tmp84 ;
2112 struct w1_master *__cil_tmp85 ;
2113 char __cil_tmp86 ;
2114 int __cil_tmp87 ;
2115 int __cil_tmp88 ;
2116 unsigned long __cil_tmp89 ;
2117 unsigned long __cil_tmp90 ;
2118 struct w1_master *__cil_tmp91 ;
2119 unsigned long __cil_tmp92 ;
2120 unsigned long __cil_tmp93 ;
2121 struct mutex *__cil_tmp94 ;
2122 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp95 ;
2123 unsigned int __cil_tmp96 ;
2124 unsigned int __cil_tmp97 ;
2125 int __cil_tmp98 ;
2126 int __cil_tmp99 ;
2127 long __cil_tmp100 ;
2128 unsigned long __cil_tmp101 ;
2129 unsigned long __cil_tmp102 ;
2130 struct device *__cil_tmp103 ;
2131 struct device const *__cil_tmp104 ;
2132 unsigned long __cil_tmp105 ;
2133 unsigned long __cil_tmp106 ;
2134 struct w1_master *__cil_tmp107 ;
2135 unsigned long __cil_tmp108 ;
2136 unsigned long __cil_tmp109 ;
2137 struct mutex *__cil_tmp110 ;
2138 struct _ddebug __attribute__((__aligned__(8))) *__cil_tmp111 ;
2139 unsigned int __cil_tmp112 ;
2140 unsigned int __cil_tmp113 ;
2141 int __cil_tmp114 ;
2142 int __cil_tmp115 ;
2143 long __cil_tmp116 ;
2144 unsigned long __cil_tmp117 ;
2145 unsigned long __cil_tmp118 ;
2146 struct device *__cil_tmp119 ;
2147 struct device const *__cil_tmp120 ;
2148
2149 {
2150 {
2151#line 160
2152 tmp = kobj_to_w1_slave(kobj);
2153#line 160
2154 sl = tmp;
2155#line 163
2156 retries = 3U;
2157 }
2158#line 165
2159 if (count != 1UL) {
2160#line 166
2161 return ((ssize_t )-14);
2162 } else
2163#line 165
2164 if (off != 0LL) {
2165#line 166
2166 return ((ssize_t )-14);
2167 } else {
2168
2169 }
2170 {
2171#line 168
2172 while (1) {
2173 while_continue: ;
2174 {
2175#line 168
2176 while (1) {
2177 while_continue___0: ;
2178 {
2179#line 168
2180 __cil_tmp20 = & descriptor___6;
2181#line 168
2182 __cil_tmp21 = __cil_tmp20->flags;
2183#line 168
2184 __cil_tmp22 = __cil_tmp21 & 1U;
2185#line 168
2186 __cil_tmp23 = ! __cil_tmp22;
2187#line 168
2188 __cil_tmp24 = ! __cil_tmp23;
2189#line 168
2190 __cil_tmp25 = (long )__cil_tmp24;
2191#line 168
2192 tmp___0 = __builtin_expect(__cil_tmp25, 0L);
2193 }
2194#line 168
2195 if (tmp___0) {
2196 {
2197#line 168
2198 __cil_tmp26 = (unsigned long )sl;
2199#line 168
2200 __cil_tmp27 = __cil_tmp26 + 112;
2201#line 168
2202 __cil_tmp28 = (struct device *)__cil_tmp27;
2203#line 168
2204 __cil_tmp29 = (struct device const *)__cil_tmp28;
2205#line 168
2206 __dynamic_dev_dbg(& descriptor___6, __cil_tmp29, "locking mutex for write_output");
2207 }
2208 } else {
2209
2210 }
2211#line 168
2212 goto while_break___0;
2213 }
2214 while_break___0: ;
2215 }
2216#line 168
2217 goto while_break;
2218 }
2219 while_break: ;
2220 }
2221 {
2222#line 169
2223 __cil_tmp30 = (unsigned long )sl;
2224#line 169
2225 __cil_tmp31 = __cil_tmp30 + 88;
2226#line 169
2227 __cil_tmp32 = *((struct w1_master **)__cil_tmp31);
2228#line 169
2229 __cil_tmp33 = (unsigned long )__cil_tmp32;
2230#line 169
2231 __cil_tmp34 = __cil_tmp33 + 144;
2232#line 169
2233 __cil_tmp35 = (struct mutex *)__cil_tmp34;
2234#line 169
2235 mutex_lock(__cil_tmp35);
2236 }
2237 {
2238#line 170
2239 while (1) {
2240 while_continue___1: ;
2241 {
2242#line 170
2243 while (1) {
2244 while_continue___2: ;
2245 {
2246#line 170
2247 __cil_tmp36 = & descriptor___7;
2248#line 170
2249 __cil_tmp37 = __cil_tmp36->flags;
2250#line 170
2251 __cil_tmp38 = __cil_tmp37 & 1U;
2252#line 170
2253 __cil_tmp39 = ! __cil_tmp38;
2254#line 170
2255 __cil_tmp40 = ! __cil_tmp39;
2256#line 170
2257 __cil_tmp41 = (long )__cil_tmp40;
2258#line 170
2259 tmp___1 = __builtin_expect(__cil_tmp41, 0L);
2260 }
2261#line 170
2262 if (tmp___1) {
2263 {
2264#line 170
2265 __cil_tmp42 = (unsigned long )sl;
2266#line 170
2267 __cil_tmp43 = __cil_tmp42 + 112;
2268#line 170
2269 __cil_tmp44 = (struct device *)__cil_tmp43;
2270#line 170
2271 __cil_tmp45 = (struct device const *)__cil_tmp44;
2272#line 170
2273 __dynamic_dev_dbg(& descriptor___7, __cil_tmp45, "mutex locked");
2274 }
2275 } else {
2276
2277 }
2278#line 170
2279 goto while_break___2;
2280 }
2281 while_break___2: ;
2282 }
2283#line 170
2284 goto while_break___1;
2285 }
2286 while_break___1: ;
2287 }
2288 {
2289#line 172
2290 tmp___2 = w1_reset_select_slave(sl);
2291 }
2292#line 172
2293 if (tmp___2) {
2294#line 173
2295 goto error;
2296 } else {
2297
2298 }
2299 {
2300#line 175
2301 while (1) {
2302 while_continue___3: ;
2303#line 175
2304 tmp___6 = retries;
2305#line 175
2306 retries = retries - 1U;
2307#line 175
2308 if (tmp___6) {
2309
2310 } else {
2311#line 175
2312 goto while_break___3;
2313 }
2314 {
2315#line 176
2316 __cil_tmp46 = 0 * 1UL;
2317#line 176
2318 __cil_tmp47 = (unsigned long )(w1_buf) + __cil_tmp46;
2319#line 176
2320 *((u8 *)__cil_tmp47) = (u8 )90;
2321#line 177
2322 __cil_tmp48 = 1 * 1UL;
2323#line 177
2324 __cil_tmp49 = (unsigned long )(w1_buf) + __cil_tmp48;
2325#line 177
2326 __cil_tmp50 = *buf;
2327#line 177
2328 *((u8 *)__cil_tmp49) = (u8 )__cil_tmp50;
2329#line 178
2330 __cil_tmp51 = 2 * 1UL;
2331#line 178
2332 __cil_tmp52 = (unsigned long )(w1_buf) + __cil_tmp51;
2333#line 178
2334 __cil_tmp53 = *buf;
2335#line 178
2336 __cil_tmp54 = (int )__cil_tmp53;
2337#line 178
2338 __cil_tmp55 = ~ __cil_tmp54;
2339#line 178
2340 *((u8 *)__cil_tmp52) = (u8 )__cil_tmp55;
2341#line 179
2342 __cil_tmp56 = (unsigned long )sl;
2343#line 179
2344 __cil_tmp57 = __cil_tmp56 + 88;
2345#line 179
2346 __cil_tmp58 = *((struct w1_master **)__cil_tmp57);
2347#line 179
2348 __cil_tmp59 = 0 * 1UL;
2349#line 179
2350 __cil_tmp60 = (unsigned long )(w1_buf) + __cil_tmp59;
2351#line 179
2352 __cil_tmp61 = (u8 *)__cil_tmp60;
2353#line 179
2354 __cil_tmp62 = (u8 const *)__cil_tmp61;
2355#line 179
2356 w1_write_block(__cil_tmp58, __cil_tmp62, 3);
2357#line 181
2358 __cil_tmp63 = (unsigned long )sl;
2359#line 181
2360 __cil_tmp64 = __cil_tmp63 + 88;
2361#line 181
2362 __cil_tmp65 = *((struct w1_master **)__cil_tmp64);
2363#line 181
2364 readBack = w1_read_8(__cil_tmp65);
2365#line 187
2366 __cil_tmp66 = (unsigned long )sl;
2367#line 187
2368 __cil_tmp67 = __cil_tmp66 + 88;
2369#line 187
2370 __cil_tmp68 = *((struct w1_master **)__cil_tmp67);
2371#line 187
2372 tmp___3 = w1_reset_resume_command(__cil_tmp68);
2373 }
2374#line 187
2375 if (tmp___3) {
2376#line 188
2377 goto error;
2378 } else {
2379
2380 }
2381 {
2382#line 190
2383 __cil_tmp69 = (int )readBack;
2384#line 190
2385 if (__cil_tmp69 != 170) {
2386#line 192
2387 goto while_continue___3;
2388 } else {
2389
2390 }
2391 }
2392 {
2393#line 197
2394 __cil_tmp70 = 0 * 1UL;
2395#line 197
2396 __cil_tmp71 = (unsigned long )(w1_buf) + __cil_tmp70;
2397#line 197
2398 *((u8 *)__cil_tmp71) = (u8 )240;
2399#line 198
2400 __cil_tmp72 = 1 * 1UL;
2401#line 198
2402 __cil_tmp73 = (unsigned long )(w1_buf) + __cil_tmp72;
2403#line 198
2404 *((u8 *)__cil_tmp73) = (u8 )137;
2405#line 199
2406 __cil_tmp74 = 2 * 1UL;
2407#line 199
2408 __cil_tmp75 = (unsigned long )(w1_buf) + __cil_tmp74;
2409#line 199
2410 *((u8 *)__cil_tmp75) = (u8 )0;
2411#line 200
2412 __cil_tmp76 = (unsigned long )sl;
2413#line 200
2414 __cil_tmp77 = __cil_tmp76 + 88;
2415#line 200
2416 __cil_tmp78 = *((struct w1_master **)__cil_tmp77);
2417#line 200
2418 __cil_tmp79 = 0 * 1UL;
2419#line 200
2420 __cil_tmp80 = (unsigned long )(w1_buf) + __cil_tmp79;
2421#line 200
2422 __cil_tmp81 = (u8 *)__cil_tmp80;
2423#line 200
2424 __cil_tmp82 = (u8 const *)__cil_tmp81;
2425#line 200
2426 w1_write_block(__cil_tmp78, __cil_tmp82, 3);
2427#line 202
2428 __cil_tmp83 = (unsigned long )sl;
2429#line 202
2430 __cil_tmp84 = __cil_tmp83 + 88;
2431#line 202
2432 __cil_tmp85 = *((struct w1_master **)__cil_tmp84);
2433#line 202
2434 tmp___5 = w1_read_8(__cil_tmp85);
2435 }
2436 {
2437#line 202
2438 __cil_tmp86 = *buf;
2439#line 202
2440 __cil_tmp87 = (int )__cil_tmp86;
2441#line 202
2442 __cil_tmp88 = (int )tmp___5;
2443#line 202
2444 if (__cil_tmp88 == __cil_tmp87) {
2445 {
2446#line 204
2447 __cil_tmp89 = (unsigned long )sl;
2448#line 204
2449 __cil_tmp90 = __cil_tmp89 + 88;
2450#line 204
2451 __cil_tmp91 = *((struct w1_master **)__cil_tmp90);
2452#line 204
2453 __cil_tmp92 = (unsigned long )__cil_tmp91;
2454#line 204
2455 __cil_tmp93 = __cil_tmp92 + 144;
2456#line 204
2457 __cil_tmp94 = (struct mutex *)__cil_tmp93;
2458#line 204
2459 mutex_unlock(__cil_tmp94);
2460 }
2461 {
2462#line 205
2463 while (1) {
2464 while_continue___4: ;
2465 {
2466#line 205
2467 while (1) {
2468 while_continue___5: ;
2469 {
2470#line 205
2471 __cil_tmp95 = & descriptor___8;
2472#line 205
2473 __cil_tmp96 = __cil_tmp95->flags;
2474#line 205
2475 __cil_tmp97 = __cil_tmp96 & 1U;
2476#line 205
2477 __cil_tmp98 = ! __cil_tmp97;
2478#line 205
2479 __cil_tmp99 = ! __cil_tmp98;
2480#line 205
2481 __cil_tmp100 = (long )__cil_tmp99;
2482#line 205
2483 tmp___4 = __builtin_expect(__cil_tmp100, 0L);
2484 }
2485#line 205
2486 if (tmp___4) {
2487 {
2488#line 205
2489 __cil_tmp101 = (unsigned long )sl;
2490#line 205
2491 __cil_tmp102 = __cil_tmp101 + 112;
2492#line 205
2493 __cil_tmp103 = (struct device *)__cil_tmp102;
2494#line 205
2495 __cil_tmp104 = (struct device const *)__cil_tmp103;
2496#line 205
2497 __dynamic_dev_dbg(& descriptor___8, __cil_tmp104, "mutex unlocked, retries:%d",
2498 retries);
2499 }
2500 } else {
2501
2502 }
2503#line 205
2504 goto while_break___5;
2505 }
2506 while_break___5: ;
2507 }
2508#line 205
2509 goto while_break___4;
2510 }
2511 while_break___4: ;
2512 }
2513#line 207
2514 return ((ssize_t )1);
2515 } else {
2516
2517 }
2518 }
2519 }
2520 while_break___3: ;
2521 }
2522 error:
2523 {
2524#line 211
2525 __cil_tmp105 = (unsigned long )sl;
2526#line 211
2527 __cil_tmp106 = __cil_tmp105 + 88;
2528#line 211
2529 __cil_tmp107 = *((struct w1_master **)__cil_tmp106);
2530#line 211
2531 __cil_tmp108 = (unsigned long )__cil_tmp107;
2532#line 211
2533 __cil_tmp109 = __cil_tmp108 + 144;
2534#line 211
2535 __cil_tmp110 = (struct mutex *)__cil_tmp109;
2536#line 211
2537 mutex_unlock(__cil_tmp110);
2538 }
2539 {
2540#line 212
2541 while (1) {
2542 while_continue___6: ;
2543 {
2544#line 212
2545 while (1) {
2546 while_continue___7: ;
2547 {
2548#line 212
2549 __cil_tmp111 = & descriptor___9;
2550#line 212
2551 __cil_tmp112 = __cil_tmp111->flags;
2552#line 212
2553 __cil_tmp113 = __cil_tmp112 & 1U;
2554#line 212
2555 __cil_tmp114 = ! __cil_tmp113;
2556#line 212
2557 __cil_tmp115 = ! __cil_tmp114;
2558#line 212
2559 __cil_tmp116 = (long )__cil_tmp115;
2560#line 212
2561 tmp___7 = __builtin_expect(__cil_tmp116, 0L);
2562 }
2563#line 212
2564 if (tmp___7) {
2565 {
2566#line 212
2567 __cil_tmp117 = (unsigned long )sl;
2568#line 212
2569 __cil_tmp118 = __cil_tmp117 + 112;
2570#line 212
2571 __cil_tmp119 = (struct device *)__cil_tmp118;
2572#line 212
2573 __cil_tmp120 = (struct device const *)__cil_tmp119;
2574#line 212
2575 __dynamic_dev_dbg(& descriptor___9, __cil_tmp120, "mutex unlocked in error, retries:%d",
2576 retries);
2577 }
2578 } else {
2579
2580 }
2581#line 212
2582 goto while_break___7;
2583 }
2584 while_break___7: ;
2585 }
2586#line 212
2587 goto while_break___6;
2588 }
2589 while_break___6: ;
2590 }
2591#line 214
2592 return ((ssize_t )-5);
2593}
2594}
2595#line 221 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
2596static ssize_t w1_f29_write_activity(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
2597 char *buf , loff_t off , size_t count )
2598{ struct w1_slave *sl ;
2599 struct w1_slave *tmp ;
2600 unsigned int retries ;
2601 int tmp___0 ;
2602 u8 tmp___1 ;
2603 int tmp___2 ;
2604 unsigned int tmp___3 ;
2605 unsigned long __cil_tmp14 ;
2606 unsigned long __cil_tmp15 ;
2607 struct w1_master *__cil_tmp16 ;
2608 unsigned long __cil_tmp17 ;
2609 unsigned long __cil_tmp18 ;
2610 struct mutex *__cil_tmp19 ;
2611 unsigned long __cil_tmp20 ;
2612 unsigned long __cil_tmp21 ;
2613 struct w1_master *__cil_tmp22 ;
2614 u8 __cil_tmp23 ;
2615 unsigned long __cil_tmp24 ;
2616 unsigned long __cil_tmp25 ;
2617 struct w1_master *__cil_tmp26 ;
2618 int __cil_tmp27 ;
2619 unsigned long __cil_tmp28 ;
2620 unsigned long __cil_tmp29 ;
2621 struct w1_master *__cil_tmp30 ;
2622 unsigned long __cil_tmp31 ;
2623 unsigned long __cil_tmp32 ;
2624 struct mutex *__cil_tmp33 ;
2625 unsigned long __cil_tmp34 ;
2626 unsigned long __cil_tmp35 ;
2627 struct w1_master *__cil_tmp36 ;
2628 unsigned long __cil_tmp37 ;
2629 unsigned long __cil_tmp38 ;
2630 struct w1_master *__cil_tmp39 ;
2631 unsigned long __cil_tmp40 ;
2632 unsigned long __cil_tmp41 ;
2633 struct mutex *__cil_tmp42 ;
2634
2635 {
2636 {
2637#line 226
2638 tmp = kobj_to_w1_slave(kobj);
2639#line 226
2640 sl = tmp;
2641#line 227
2642 retries = 3U;
2643 }
2644#line 229
2645 if (count != 1UL) {
2646#line 230
2647 return ((ssize_t )-14);
2648 } else
2649#line 229
2650 if (off != 0LL) {
2651#line 230
2652 return ((ssize_t )-14);
2653 } else {
2654
2655 }
2656 {
2657#line 232
2658 __cil_tmp14 = (unsigned long )sl;
2659#line 232
2660 __cil_tmp15 = __cil_tmp14 + 88;
2661#line 232
2662 __cil_tmp16 = *((struct w1_master **)__cil_tmp15);
2663#line 232
2664 __cil_tmp17 = (unsigned long )__cil_tmp16;
2665#line 232
2666 __cil_tmp18 = __cil_tmp17 + 144;
2667#line 232
2668 __cil_tmp19 = (struct mutex *)__cil_tmp18;
2669#line 232
2670 mutex_lock(__cil_tmp19);
2671#line 234
2672 tmp___0 = w1_reset_select_slave(sl);
2673 }
2674#line 234
2675 if (tmp___0) {
2676#line 235
2677 goto error;
2678 } else {
2679
2680 }
2681 {
2682#line 237
2683 while (1) {
2684 while_continue: ;
2685#line 237
2686 tmp___3 = retries;
2687#line 237
2688 retries = retries - 1U;
2689#line 237
2690 if (tmp___3) {
2691
2692 } else {
2693#line 237
2694 goto while_break;
2695 }
2696 {
2697#line 238
2698 __cil_tmp20 = (unsigned long )sl;
2699#line 238
2700 __cil_tmp21 = __cil_tmp20 + 88;
2701#line 238
2702 __cil_tmp22 = *((struct w1_master **)__cil_tmp21);
2703#line 238
2704 __cil_tmp23 = (u8 )195;
2705#line 238
2706 w1_write_8(__cil_tmp22, __cil_tmp23);
2707#line 239
2708 __cil_tmp24 = (unsigned long )sl;
2709#line 239
2710 __cil_tmp25 = __cil_tmp24 + 88;
2711#line 239
2712 __cil_tmp26 = *((struct w1_master **)__cil_tmp25);
2713#line 239
2714 tmp___1 = w1_read_8(__cil_tmp26);
2715 }
2716 {
2717#line 239
2718 __cil_tmp27 = (int )tmp___1;
2719#line 239
2720 if (__cil_tmp27 == 170) {
2721 {
2722#line 240
2723 __cil_tmp28 = (unsigned long )sl;
2724#line 240
2725 __cil_tmp29 = __cil_tmp28 + 88;
2726#line 240
2727 __cil_tmp30 = *((struct w1_master **)__cil_tmp29);
2728#line 240
2729 __cil_tmp31 = (unsigned long )__cil_tmp30;
2730#line 240
2731 __cil_tmp32 = __cil_tmp31 + 144;
2732#line 240
2733 __cil_tmp33 = (struct mutex *)__cil_tmp32;
2734#line 240
2735 mutex_unlock(__cil_tmp33);
2736 }
2737#line 241
2738 return ((ssize_t )1);
2739 } else {
2740
2741 }
2742 }
2743 {
2744#line 243
2745 __cil_tmp34 = (unsigned long )sl;
2746#line 243
2747 __cil_tmp35 = __cil_tmp34 + 88;
2748#line 243
2749 __cil_tmp36 = *((struct w1_master **)__cil_tmp35);
2750#line 243
2751 tmp___2 = w1_reset_resume_command(__cil_tmp36);
2752 }
2753#line 243
2754 if (tmp___2) {
2755#line 244
2756 goto error;
2757 } else {
2758
2759 }
2760 }
2761 while_break: ;
2762 }
2763 error:
2764 {
2765#line 248
2766 __cil_tmp37 = (unsigned long )sl;
2767#line 248
2768 __cil_tmp38 = __cil_tmp37 + 88;
2769#line 248
2770 __cil_tmp39 = *((struct w1_master **)__cil_tmp38);
2771#line 248
2772 __cil_tmp40 = (unsigned long )__cil_tmp39;
2773#line 248
2774 __cil_tmp41 = __cil_tmp40 + 144;
2775#line 248
2776 __cil_tmp42 = (struct mutex *)__cil_tmp41;
2777#line 248
2778 mutex_unlock(__cil_tmp42);
2779 }
2780#line 249
2781 return ((ssize_t )-5);
2782}
2783}
2784#line 252 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
2785static ssize_t w1_f29_write_status_control(struct file *filp , struct kobject *kobj ,
2786 struct bin_attribute *bin_attr , char *buf ,
2787 loff_t off , size_t count )
2788{ struct w1_slave *sl ;
2789 struct w1_slave *tmp ;
2790 u8 w1_buf[4] ;
2791 unsigned int retries ;
2792 int tmp___0 ;
2793 int tmp___1 ;
2794 u8 tmp___2 ;
2795 unsigned int tmp___3 ;
2796 unsigned long __cil_tmp15 ;
2797 unsigned long __cil_tmp16 ;
2798 struct w1_master *__cil_tmp17 ;
2799 unsigned long __cil_tmp18 ;
2800 unsigned long __cil_tmp19 ;
2801 struct mutex *__cil_tmp20 ;
2802 unsigned long __cil_tmp21 ;
2803 unsigned long __cil_tmp22 ;
2804 unsigned long __cil_tmp23 ;
2805 unsigned long __cil_tmp24 ;
2806 unsigned long __cil_tmp25 ;
2807 unsigned long __cil_tmp26 ;
2808 unsigned long __cil_tmp27 ;
2809 unsigned long __cil_tmp28 ;
2810 char __cil_tmp29 ;
2811 unsigned long __cil_tmp30 ;
2812 unsigned long __cil_tmp31 ;
2813 struct w1_master *__cil_tmp32 ;
2814 unsigned long __cil_tmp33 ;
2815 unsigned long __cil_tmp34 ;
2816 u8 *__cil_tmp35 ;
2817 u8 const *__cil_tmp36 ;
2818 unsigned long __cil_tmp37 ;
2819 unsigned long __cil_tmp38 ;
2820 struct w1_master *__cil_tmp39 ;
2821 unsigned long __cil_tmp40 ;
2822 unsigned long __cil_tmp41 ;
2823 unsigned long __cil_tmp42 ;
2824 unsigned long __cil_tmp43 ;
2825 unsigned long __cil_tmp44 ;
2826 unsigned long __cil_tmp45 ;
2827 unsigned long __cil_tmp46 ;
2828 unsigned long __cil_tmp47 ;
2829 struct w1_master *__cil_tmp48 ;
2830 unsigned long __cil_tmp49 ;
2831 unsigned long __cil_tmp50 ;
2832 u8 *__cil_tmp51 ;
2833 u8 const *__cil_tmp52 ;
2834 unsigned long __cil_tmp53 ;
2835 unsigned long __cil_tmp54 ;
2836 struct w1_master *__cil_tmp55 ;
2837 char __cil_tmp56 ;
2838 int __cil_tmp57 ;
2839 int __cil_tmp58 ;
2840 unsigned long __cil_tmp59 ;
2841 unsigned long __cil_tmp60 ;
2842 struct w1_master *__cil_tmp61 ;
2843 unsigned long __cil_tmp62 ;
2844 unsigned long __cil_tmp63 ;
2845 struct mutex *__cil_tmp64 ;
2846 unsigned long __cil_tmp65 ;
2847 unsigned long __cil_tmp66 ;
2848 struct w1_master *__cil_tmp67 ;
2849 unsigned long __cil_tmp68 ;
2850 unsigned long __cil_tmp69 ;
2851 struct mutex *__cil_tmp70 ;
2852
2853 {
2854 {
2855#line 260
2856 tmp = kobj_to_w1_slave(kobj);
2857#line 260
2858 sl = tmp;
2859#line 262
2860 retries = 3U;
2861 }
2862#line 264
2863 if (count != 1UL) {
2864#line 265
2865 return ((ssize_t )-14);
2866 } else
2867#line 264
2868 if (off != 0LL) {
2869#line 265
2870 return ((ssize_t )-14);
2871 } else {
2872
2873 }
2874 {
2875#line 267
2876 __cil_tmp15 = (unsigned long )sl;
2877#line 267
2878 __cil_tmp16 = __cil_tmp15 + 88;
2879#line 267
2880 __cil_tmp17 = *((struct w1_master **)__cil_tmp16);
2881#line 267
2882 __cil_tmp18 = (unsigned long )__cil_tmp17;
2883#line 267
2884 __cil_tmp19 = __cil_tmp18 + 144;
2885#line 267
2886 __cil_tmp20 = (struct mutex *)__cil_tmp19;
2887#line 267
2888 mutex_lock(__cil_tmp20);
2889#line 269
2890 tmp___0 = w1_reset_select_slave(sl);
2891 }
2892#line 269
2893 if (tmp___0) {
2894#line 270
2895 goto error;
2896 } else {
2897
2898 }
2899 {
2900#line 272
2901 while (1) {
2902 while_continue: ;
2903#line 272
2904 tmp___3 = retries;
2905#line 272
2906 retries = retries - 1U;
2907#line 272
2908 if (tmp___3) {
2909
2910 } else {
2911#line 272
2912 goto while_break;
2913 }
2914 {
2915#line 273
2916 __cil_tmp21 = 0 * 1UL;
2917#line 273
2918 __cil_tmp22 = (unsigned long )(w1_buf) + __cil_tmp21;
2919#line 273
2920 *((u8 *)__cil_tmp22) = (u8 )204;
2921#line 274
2922 __cil_tmp23 = 1 * 1UL;
2923#line 274
2924 __cil_tmp24 = (unsigned long )(w1_buf) + __cil_tmp23;
2925#line 274
2926 *((u8 *)__cil_tmp24) = (u8 )141;
2927#line 275
2928 __cil_tmp25 = 2 * 1UL;
2929#line 275
2930 __cil_tmp26 = (unsigned long )(w1_buf) + __cil_tmp25;
2931#line 275
2932 *((u8 *)__cil_tmp26) = (u8 )0;
2933#line 276
2934 __cil_tmp27 = 3 * 1UL;
2935#line 276
2936 __cil_tmp28 = (unsigned long )(w1_buf) + __cil_tmp27;
2937#line 276
2938 __cil_tmp29 = *buf;
2939#line 276
2940 *((u8 *)__cil_tmp28) = (u8 )__cil_tmp29;
2941#line 278
2942 __cil_tmp30 = (unsigned long )sl;
2943#line 278
2944 __cil_tmp31 = __cil_tmp30 + 88;
2945#line 278
2946 __cil_tmp32 = *((struct w1_master **)__cil_tmp31);
2947#line 278
2948 __cil_tmp33 = 0 * 1UL;
2949#line 278
2950 __cil_tmp34 = (unsigned long )(w1_buf) + __cil_tmp33;
2951#line 278
2952 __cil_tmp35 = (u8 *)__cil_tmp34;
2953#line 278
2954 __cil_tmp36 = (u8 const *)__cil_tmp35;
2955#line 278
2956 w1_write_block(__cil_tmp32, __cil_tmp36, 4);
2957#line 279
2958 __cil_tmp37 = (unsigned long )sl;
2959#line 279
2960 __cil_tmp38 = __cil_tmp37 + 88;
2961#line 279
2962 __cil_tmp39 = *((struct w1_master **)__cil_tmp38);
2963#line 279
2964 tmp___1 = w1_reset_resume_command(__cil_tmp39);
2965 }
2966#line 279
2967 if (tmp___1) {
2968#line 280
2969 goto error;
2970 } else {
2971
2972 }
2973 {
2974#line 282
2975 __cil_tmp40 = 0 * 1UL;
2976#line 282
2977 __cil_tmp41 = (unsigned long )(w1_buf) + __cil_tmp40;
2978#line 282
2979 *((u8 *)__cil_tmp41) = (u8 )240;
2980#line 283
2981 __cil_tmp42 = 1 * 1UL;
2982#line 283
2983 __cil_tmp43 = (unsigned long )(w1_buf) + __cil_tmp42;
2984#line 283
2985 *((u8 *)__cil_tmp43) = (u8 )141;
2986#line 284
2987 __cil_tmp44 = 2 * 1UL;
2988#line 284
2989 __cil_tmp45 = (unsigned long )(w1_buf) + __cil_tmp44;
2990#line 284
2991 *((u8 *)__cil_tmp45) = (u8 )0;
2992#line 286
2993 __cil_tmp46 = (unsigned long )sl;
2994#line 286
2995 __cil_tmp47 = __cil_tmp46 + 88;
2996#line 286
2997 __cil_tmp48 = *((struct w1_master **)__cil_tmp47);
2998#line 286
2999 __cil_tmp49 = 0 * 1UL;
3000#line 286
3001 __cil_tmp50 = (unsigned long )(w1_buf) + __cil_tmp49;
3002#line 286
3003 __cil_tmp51 = (u8 *)__cil_tmp50;
3004#line 286
3005 __cil_tmp52 = (u8 const *)__cil_tmp51;
3006#line 286
3007 w1_write_block(__cil_tmp48, __cil_tmp52, 3);
3008#line 287
3009 __cil_tmp53 = (unsigned long )sl;
3010#line 287
3011 __cil_tmp54 = __cil_tmp53 + 88;
3012#line 287
3013 __cil_tmp55 = *((struct w1_master **)__cil_tmp54);
3014#line 287
3015 tmp___2 = w1_read_8(__cil_tmp55);
3016 }
3017 {
3018#line 287
3019 __cil_tmp56 = *buf;
3020#line 287
3021 __cil_tmp57 = (int )__cil_tmp56;
3022#line 287
3023 __cil_tmp58 = (int )tmp___2;
3024#line 287
3025 if (__cil_tmp58 == __cil_tmp57) {
3026 {
3027#line 289
3028 __cil_tmp59 = (unsigned long )sl;
3029#line 289
3030 __cil_tmp60 = __cil_tmp59 + 88;
3031#line 289
3032 __cil_tmp61 = *((struct w1_master **)__cil_tmp60);
3033#line 289
3034 __cil_tmp62 = (unsigned long )__cil_tmp61;
3035#line 289
3036 __cil_tmp63 = __cil_tmp62 + 144;
3037#line 289
3038 __cil_tmp64 = (struct mutex *)__cil_tmp63;
3039#line 289
3040 mutex_unlock(__cil_tmp64);
3041 }
3042#line 290
3043 return ((ssize_t )1);
3044 } else {
3045
3046 }
3047 }
3048 }
3049 while_break: ;
3050 }
3051 error:
3052 {
3053#line 294
3054 __cil_tmp65 = (unsigned long )sl;
3055#line 294
3056 __cil_tmp66 = __cil_tmp65 + 88;
3057#line 294
3058 __cil_tmp67 = *((struct w1_master **)__cil_tmp66);
3059#line 294
3060 __cil_tmp68 = (unsigned long )__cil_tmp67;
3061#line 294
3062 __cil_tmp69 = __cil_tmp68 + 144;
3063#line 294
3064 __cil_tmp70 = (struct mutex *)__cil_tmp69;
3065#line 294
3066 mutex_unlock(__cil_tmp70);
3067 }
3068#line 296
3069 return ((ssize_t )-5);
3070}
3071}
3072#line 302 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3073static struct bin_attribute w1_f29_sysfs_bin_files[6] = { {{"state", (umode_t )292}, (size_t )1, (void *)0, & w1_f29_read_state, (ssize_t (*)(struct file * ,
3074 struct kobject * ,
3075 struct bin_attribute * ,
3076 char * ,
3077 loff_t ,
3078 size_t ))0,
3079 (int (*)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ))0},
3080 {{"output",
3081 (umode_t )436}, (size_t )1, (void *)0, & w1_f29_read_output, & w1_f29_write_output,
3082 (int (*)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ))0},
3083 {{"activity",
3084 (umode_t )292}, (size_t )1, (void *)0, & w1_f29_read_activity, & w1_f29_write_activity,
3085 (int (*)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ))0},
3086 {{"cond_search_mask",
3087 (umode_t )292}, (size_t )1, (void *)0, & w1_f29_read_cond_search_mask, (ssize_t (*)(struct file * ,
3088 struct kobject * ,
3089 struct bin_attribute * ,
3090 char * ,
3091 loff_t ,
3092 size_t ))0,
3093 (int (*)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ))0},
3094 {{"cond_search_polarity",
3095 (umode_t )292}, (size_t )1, (void *)0, & w1_f29_read_cond_search_polarity,
3096 (ssize_t (*)(struct file * , struct kobject * , struct bin_attribute * , char * ,
3097 loff_t , size_t ))0, (int (*)(struct file * , struct kobject * ,
3098 struct bin_attribute *attr , struct vm_area_struct *vma ))0},
3099 {{"status_control",
3100 (umode_t )436}, (size_t )1, (void *)0, & w1_f29_read_status_control, & w1_f29_write_status_control,
3101 (int (*)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ))0}};
3102#line 358 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3103static int w1_f29_add_slave(struct w1_slave *sl )
3104{ int err ;
3105 int i ;
3106 unsigned long __cil_tmp4 ;
3107 unsigned long __cil_tmp5 ;
3108 unsigned long __cil_tmp6 ;
3109 struct kobject *__cil_tmp7 ;
3110 unsigned long __cil_tmp8 ;
3111 unsigned long __cil_tmp9 ;
3112 struct bin_attribute *__cil_tmp10 ;
3113 struct bin_attribute const *__cil_tmp11 ;
3114 unsigned long __cil_tmp12 ;
3115 unsigned long __cil_tmp13 ;
3116 unsigned long __cil_tmp14 ;
3117 struct kobject *__cil_tmp15 ;
3118 unsigned long __cil_tmp16 ;
3119 unsigned long __cil_tmp17 ;
3120 struct bin_attribute *__cil_tmp18 ;
3121 struct bin_attribute const *__cil_tmp19 ;
3122
3123 {
3124#line 360
3125 err = 0;
3126#line 363
3127 i = 0;
3128 {
3129#line 363
3130 while (1) {
3131 while_continue: ;
3132#line 363
3133 if (i < 6) {
3134#line 363
3135 if (! err) {
3136
3137 } else {
3138#line 363
3139 goto while_break;
3140 }
3141 } else {
3142#line 363
3143 goto while_break;
3144 }
3145 {
3146#line 364
3147 __cil_tmp4 = 112 + 16;
3148#line 364
3149 __cil_tmp5 = (unsigned long )sl;
3150#line 364
3151 __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
3152#line 364
3153 __cil_tmp7 = (struct kobject *)__cil_tmp6;
3154#line 364
3155 __cil_tmp8 = i * 56UL;
3156#line 364
3157 __cil_tmp9 = (unsigned long )(w1_f29_sysfs_bin_files) + __cil_tmp8;
3158#line 364
3159 __cil_tmp10 = (struct bin_attribute *)__cil_tmp9;
3160#line 364
3161 __cil_tmp11 = (struct bin_attribute const *)__cil_tmp10;
3162#line 364
3163 err = (int )sysfs_create_bin_file(__cil_tmp7, __cil_tmp11);
3164#line 363
3165 i = i + 1;
3166 }
3167 }
3168 while_break: ;
3169 }
3170#line 367
3171 if (err) {
3172 {
3173#line 368
3174 while (1) {
3175 while_continue___0: ;
3176#line 368
3177 i = i - 1;
3178#line 368
3179 if (i >= 0) {
3180
3181 } else {
3182#line 368
3183 goto while_break___0;
3184 }
3185 {
3186#line 369
3187 __cil_tmp12 = 112 + 16;
3188#line 369
3189 __cil_tmp13 = (unsigned long )sl;
3190#line 369
3191 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
3192#line 369
3193 __cil_tmp15 = (struct kobject *)__cil_tmp14;
3194#line 369
3195 __cil_tmp16 = i * 56UL;
3196#line 369
3197 __cil_tmp17 = (unsigned long )(w1_f29_sysfs_bin_files) + __cil_tmp16;
3198#line 369
3199 __cil_tmp18 = (struct bin_attribute *)__cil_tmp17;
3200#line 369
3201 __cil_tmp19 = (struct bin_attribute const *)__cil_tmp18;
3202#line 369
3203 sysfs_remove_bin_file(__cil_tmp15, __cil_tmp19);
3204 }
3205 }
3206 while_break___0: ;
3207 }
3208 } else {
3209
3210 }
3211#line 371
3212 return (err);
3213}
3214}
3215#line 374 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3216static void w1_f29_remove_slave(struct w1_slave *sl )
3217{ int i ;
3218 unsigned long __cil_tmp3 ;
3219 unsigned long __cil_tmp4 ;
3220 unsigned long __cil_tmp5 ;
3221 struct kobject *__cil_tmp6 ;
3222 unsigned long __cil_tmp7 ;
3223 unsigned long __cil_tmp8 ;
3224 struct bin_attribute *__cil_tmp9 ;
3225 struct bin_attribute const *__cil_tmp10 ;
3226
3227 {
3228#line 377
3229 i = 5;
3230 {
3231#line 377
3232 while (1) {
3233 while_continue: ;
3234#line 377
3235 if (i >= 0) {
3236
3237 } else {
3238#line 377
3239 goto while_break;
3240 }
3241 {
3242#line 378
3243 __cil_tmp3 = 112 + 16;
3244#line 378
3245 __cil_tmp4 = (unsigned long )sl;
3246#line 378
3247 __cil_tmp5 = __cil_tmp4 + __cil_tmp3;
3248#line 378
3249 __cil_tmp6 = (struct kobject *)__cil_tmp5;
3250#line 378
3251 __cil_tmp7 = i * 56UL;
3252#line 378
3253 __cil_tmp8 = (unsigned long )(w1_f29_sysfs_bin_files) + __cil_tmp7;
3254#line 378
3255 __cil_tmp9 = (struct bin_attribute *)__cil_tmp8;
3256#line 378
3257 __cil_tmp10 = (struct bin_attribute const *)__cil_tmp9;
3258#line 378
3259 sysfs_remove_bin_file(__cil_tmp6, __cil_tmp10);
3260#line 377
3261 i = i - 1;
3262 }
3263 }
3264 while_break: ;
3265 }
3266#line 380
3267 return;
3268}
3269}
3270#line 382 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3271static struct w1_family_ops w1_f29_fops = {& w1_f29_add_slave, & w1_f29_remove_slave};
3272#line 387 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3273static struct w1_family w1_family_29 = {{(struct list_head *)0, (struct list_head *)0}, (u8 )41, & w1_f29_fops, {0}};
3274#line 392
3275static int w1_f29_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
3276#line 392 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3277static int w1_f29_init(void)
3278{ int tmp ;
3279
3280 {
3281 {
3282#line 394
3283 tmp = w1_register_family(& w1_family_29);
3284 }
3285#line 394
3286 return (tmp);
3287}
3288}
3289#line 397
3290static void w1_f29_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
3291#line 397 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3292static void w1_f29_exit(void)
3293{
3294
3295 {
3296 {
3297#line 399
3298 w1_unregister_family(& w1_family_29);
3299 }
3300#line 400
3301 return;
3302}
3303}
3304#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3305int init_module(void)
3306{ int tmp ;
3307
3308 {
3309 {
3310#line 402
3311 tmp = w1_f29_init();
3312 }
3313#line 402
3314 return (tmp);
3315}
3316}
3317#line 403 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3318void cleanup_module(void)
3319{
3320
3321 {
3322 {
3323#line 403
3324 w1_f29_exit();
3325 }
3326#line 403
3327 return;
3328}
3329}
3330#line 421
3331void ldv_check_final_state(void) ;
3332#line 427
3333extern void ldv_initialize(void) ;
3334#line 430
3335extern int __VERIFIER_nondet_int(void) ;
3336#line 433 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3337int LDV_IN_INTERRUPT ;
3338#line 436 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3339void main(void)
3340{ struct w1_slave *var_group1 ;
3341 int tmp ;
3342 int tmp___0 ;
3343 int tmp___1 ;
3344
3345 {
3346 {
3347#line 486
3348 LDV_IN_INTERRUPT = 1;
3349#line 495
3350 ldv_initialize();
3351#line 516
3352 tmp = w1_f29_init();
3353 }
3354#line 516
3355 if (tmp) {
3356#line 517
3357 goto ldv_final;
3358 } else {
3359
3360 }
3361 {
3362#line 521
3363 while (1) {
3364 while_continue: ;
3365 {
3366#line 521
3367 tmp___1 = __VERIFIER_nondet_int();
3368 }
3369#line 521
3370 if (tmp___1) {
3371
3372 } else {
3373#line 521
3374 goto while_break;
3375 }
3376 {
3377#line 524
3378 tmp___0 = __VERIFIER_nondet_int();
3379 }
3380#line 526
3381 if (tmp___0 == 0) {
3382#line 526
3383 goto case_0;
3384 } else
3385#line 557
3386 if (tmp___0 == 1) {
3387#line 557
3388 goto case_1;
3389 } else {
3390 {
3391#line 588
3392 goto switch_default;
3393#line 524
3394 if (0) {
3395 case_0:
3396 {
3397#line 549
3398 w1_f29_add_slave(var_group1);
3399 }
3400#line 556
3401 goto switch_break;
3402 case_1:
3403 {
3404#line 580
3405 w1_f29_remove_slave(var_group1);
3406 }
3407#line 587
3408 goto switch_break;
3409 switch_default:
3410#line 588
3411 goto switch_break;
3412 } else {
3413 switch_break: ;
3414 }
3415 }
3416 }
3417 }
3418 while_break: ;
3419 }
3420 {
3421#line 615
3422 w1_f29_exit();
3423 }
3424 ldv_final:
3425 {
3426#line 618
3427 ldv_check_final_state();
3428 }
3429#line 621
3430 return;
3431}
3432}
3433#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
3434void ldv_blast_assert(void)
3435{
3436
3437 {
3438 ERROR:
3439#line 6
3440 goto ERROR;
3441}
3442}
3443#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
3444extern int __VERIFIER_nondet_int(void) ;
3445#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3446int ldv_mutex = 1;
3447#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3448int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
3449{ int nondetermined ;
3450
3451 {
3452#line 29
3453 if (ldv_mutex == 1) {
3454
3455 } else {
3456 {
3457#line 29
3458 ldv_blast_assert();
3459 }
3460 }
3461 {
3462#line 32
3463 nondetermined = __VERIFIER_nondet_int();
3464 }
3465#line 35
3466 if (nondetermined) {
3467#line 38
3468 ldv_mutex = 2;
3469#line 40
3470 return (0);
3471 } else {
3472#line 45
3473 return (-4);
3474 }
3475}
3476}
3477#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3478int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
3479{ int nondetermined ;
3480
3481 {
3482#line 57
3483 if (ldv_mutex == 1) {
3484
3485 } else {
3486 {
3487#line 57
3488 ldv_blast_assert();
3489 }
3490 }
3491 {
3492#line 60
3493 nondetermined = __VERIFIER_nondet_int();
3494 }
3495#line 63
3496 if (nondetermined) {
3497#line 66
3498 ldv_mutex = 2;
3499#line 68
3500 return (0);
3501 } else {
3502#line 73
3503 return (-4);
3504 }
3505}
3506}
3507#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3508int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
3509{ int atomic_value_after_dec ;
3510
3511 {
3512#line 83
3513 if (ldv_mutex == 1) {
3514
3515 } else {
3516 {
3517#line 83
3518 ldv_blast_assert();
3519 }
3520 }
3521 {
3522#line 86
3523 atomic_value_after_dec = __VERIFIER_nondet_int();
3524 }
3525#line 89
3526 if (atomic_value_after_dec == 0) {
3527#line 92
3528 ldv_mutex = 2;
3529#line 94
3530 return (1);
3531 } else {
3532
3533 }
3534#line 98
3535 return (0);
3536}
3537}
3538#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3539void mutex_lock(struct mutex *lock )
3540{
3541
3542 {
3543#line 108
3544 if (ldv_mutex == 1) {
3545
3546 } else {
3547 {
3548#line 108
3549 ldv_blast_assert();
3550 }
3551 }
3552#line 110
3553 ldv_mutex = 2;
3554#line 111
3555 return;
3556}
3557}
3558#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3559int mutex_trylock(struct mutex *lock )
3560{ int nondetermined ;
3561
3562 {
3563#line 121
3564 if (ldv_mutex == 1) {
3565
3566 } else {
3567 {
3568#line 121
3569 ldv_blast_assert();
3570 }
3571 }
3572 {
3573#line 124
3574 nondetermined = __VERIFIER_nondet_int();
3575 }
3576#line 127
3577 if (nondetermined) {
3578#line 130
3579 ldv_mutex = 2;
3580#line 132
3581 return (1);
3582 } else {
3583#line 137
3584 return (0);
3585 }
3586}
3587}
3588#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3589void mutex_unlock(struct mutex *lock )
3590{
3591
3592 {
3593#line 147
3594 if (ldv_mutex == 2) {
3595
3596 } else {
3597 {
3598#line 147
3599 ldv_blast_assert();
3600 }
3601 }
3602#line 149
3603 ldv_mutex = 1;
3604#line 150
3605 return;
3606}
3607}
3608#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
3609void ldv_check_final_state(void)
3610{
3611
3612 {
3613#line 156
3614 if (ldv_mutex == 1) {
3615
3616 } else {
3617 {
3618#line 156
3619 ldv_blast_assert();
3620 }
3621 }
3622#line 157
3623 return;
3624}
3625}
3626#line 630 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/12354/dscv_tempdir/dscv/ri/32_1/drivers/w1/slaves/w1_ds2408.c.common.c"
3627long s__builtin_expect(long val , long res )
3628{
3629
3630 {
3631#line 631
3632 return (val);
3633}
3634}