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