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