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/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.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 28 "include/linux/crc16.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 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
1002struct w1_f23_data {
1003 u8 memory[512U] ;
1004 u32 validcrc ;
1005};
1006#line 1 "<compiler builtins>"
1007
1008#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
1009void ldv_spin_lock(void) ;
1010#line 3
1011void ldv_spin_unlock(void) ;
1012#line 4
1013int ldv_spin_trylock(void) ;
1014#line 60 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
1015extern int memcmp(void const * , void const * , size_t ) ;
1016#line 134 "include/linux/mutex.h"
1017extern void mutex_lock_nested(struct mutex * , unsigned int ) ;
1018#line 169
1019extern void mutex_unlock(struct mutex * ) ;
1020#line 140 "include/linux/sysfs.h"
1021extern int sysfs_create_bin_file(struct kobject * , struct bin_attribute const * ) ;
1022#line 142
1023extern void sysfs_remove_bin_file(struct kobject * , struct bin_attribute const * ) ;
1024#line 161 "include/linux/slab.h"
1025extern void kfree(void const * ) ;
1026#line 220 "include/linux/slub_def.h"
1027extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
1028#line 223
1029void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1030#line 353 "include/linux/slab.h"
1031__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1032#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
1033extern void *__VERIFIER_nondet_pointer(void) ;
1034#line 11
1035void ldv_check_alloc_flags(gfp_t flags ) ;
1036#line 12
1037void ldv_check_alloc_nonatomic(void) ;
1038#line 14
1039struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1040#line 892 "include/linux/device.h"
1041extern int dev_err(struct device const * , char const * , ...) ;
1042#line 46 "include/linux/delay.h"
1043extern void msleep(unsigned int ) ;
1044#line 22 "include/linux/crc16.h"
1045extern u16 crc16(u16 , u8 const * , size_t ) ;
1046#line 69 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1_family.h"
1047extern void w1_unregister_family(struct w1_family * ) ;
1048#line 70
1049extern int w1_register_family(struct w1_family * ) ;
1050#line 211 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
1051extern void w1_write_8(struct w1_master * , u8 ) ;
1052#line 213
1053extern int w1_reset_bus(struct w1_master * ) ;
1054#line 215
1055extern void w1_write_block(struct w1_master * , u8 const * , int ) ;
1056#line 217
1057extern u8 w1_read_block(struct w1_master * , u8 * , int ) ;
1058#line 218
1059extern int w1_reset_select_slave(struct w1_slave * ) ;
1060#line 222 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
1061__inline static struct w1_slave *dev_to_w1_slave(struct device *dev )
1062{ struct device const *__mptr ;
1063 struct w1_slave *__cil_tmp3 ;
1064
1065 {
1066#line 224
1067 __mptr = (struct device const *)dev;
1068 {
1069#line 224
1070 __cil_tmp3 = (struct w1_slave *)__mptr;
1071#line 224
1072 return (__cil_tmp3 + 0xffffffffffffff90UL);
1073 }
1074}
1075}
1076#line 227 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/w1/slaves/../w1.h"
1077__inline static struct w1_slave *kobj_to_w1_slave(struct kobject *kobj )
1078{ struct kobject const *__mptr ;
1079 struct w1_slave *tmp ;
1080 struct device *__cil_tmp4 ;
1081 struct device *__cil_tmp5 ;
1082
1083 {
1084 {
1085#line 229
1086 __mptr = (struct kobject const *)kobj;
1087#line 229
1088 __cil_tmp4 = (struct device *)__mptr;
1089#line 229
1090 __cil_tmp5 = __cil_tmp4 + 0xfffffffffffffff0UL;
1091#line 229
1092 tmp = dev_to_w1_slave(__cil_tmp5);
1093 }
1094#line 229
1095 return (tmp);
1096}
1097}
1098#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
1099__inline static size_t w1_f23_fix_count(loff_t off , size_t count , size_t size )
1100{ unsigned long long __cil_tmp4 ;
1101 unsigned long long __cil_tmp5 ;
1102 unsigned long long __cil_tmp6 ;
1103 unsigned long long __cil_tmp7 ;
1104 unsigned long long __cil_tmp8 ;
1105 unsigned long long __cil_tmp9 ;
1106 unsigned long long __cil_tmp10 ;
1107 unsigned long long __cil_tmp11 ;
1108 unsigned long long __cil_tmp12 ;
1109
1110 {
1111 {
1112#line 72
1113 __cil_tmp4 = (unsigned long long )size;
1114#line 72
1115 __cil_tmp5 = (unsigned long long )off;
1116#line 72
1117 if (__cil_tmp5 > __cil_tmp4) {
1118#line 73
1119 return (0UL);
1120 } else {
1121
1122 }
1123 }
1124 {
1125#line 75
1126 __cil_tmp6 = (unsigned long long )size;
1127#line 75
1128 __cil_tmp7 = (unsigned long long )count;
1129#line 75
1130 __cil_tmp8 = (unsigned long long )off;
1131#line 75
1132 __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
1133#line 75
1134 if (__cil_tmp9 > __cil_tmp6) {
1135 {
1136#line 76
1137 __cil_tmp10 = (unsigned long long )off;
1138#line 76
1139 __cil_tmp11 = (unsigned long long )size;
1140#line 76
1141 __cil_tmp12 = __cil_tmp11 - __cil_tmp10;
1142#line 76
1143 return ((size_t )__cil_tmp12);
1144 }
1145 } else {
1146
1147 }
1148 }
1149#line 78
1150 return (count);
1151}
1152}
1153#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
1154static int w1_f23_refresh_block(struct w1_slave *sl , struct w1_f23_data *data , int block )
1155{ u8 wrbuf[3U] ;
1156 int off ;
1157 int tmp ;
1158 u16 tmp___0 ;
1159 int __cil_tmp8 ;
1160 u32 __cil_tmp9 ;
1161 unsigned long __cil_tmp10 ;
1162 unsigned long __cil_tmp11 ;
1163 u32 __cil_tmp12 ;
1164 unsigned int __cil_tmp13 ;
1165 unsigned long __cil_tmp14 ;
1166 unsigned long __cil_tmp15 ;
1167 unsigned long __cil_tmp16 ;
1168 unsigned long __cil_tmp17 ;
1169 unsigned long __cil_tmp18 ;
1170 unsigned long __cil_tmp19 ;
1171 unsigned long __cil_tmp20 ;
1172 unsigned long __cil_tmp21 ;
1173 int __cil_tmp22 ;
1174 unsigned long __cil_tmp23 ;
1175 unsigned long __cil_tmp24 ;
1176 struct w1_master *__cil_tmp25 ;
1177 u8 const *__cil_tmp26 ;
1178 unsigned long __cil_tmp27 ;
1179 unsigned long __cil_tmp28 ;
1180 struct w1_master *__cil_tmp29 ;
1181 unsigned long __cil_tmp30 ;
1182 u8 (*__cil_tmp31)[512U] ;
1183 u8 *__cil_tmp32 ;
1184 u8 *__cil_tmp33 ;
1185 u16 __cil_tmp34 ;
1186 unsigned long __cil_tmp35 ;
1187 u8 (*__cil_tmp36)[512U] ;
1188 u8 const *__cil_tmp37 ;
1189 u8 const *__cil_tmp38 ;
1190 unsigned int __cil_tmp39 ;
1191 unsigned long __cil_tmp40 ;
1192 unsigned long __cil_tmp41 ;
1193 int __cil_tmp42 ;
1194 u32 __cil_tmp43 ;
1195 unsigned long __cil_tmp44 ;
1196 unsigned long __cil_tmp45 ;
1197 u32 __cil_tmp46 ;
1198
1199 {
1200#line 86
1201 off = block * 32;
1202 {
1203#line 88
1204 __cil_tmp8 = 1 << block;
1205#line 88
1206 __cil_tmp9 = (u32 )__cil_tmp8;
1207#line 88
1208 __cil_tmp10 = (unsigned long )data;
1209#line 88
1210 __cil_tmp11 = __cil_tmp10 + 512;
1211#line 88
1212 __cil_tmp12 = *((u32 *)__cil_tmp11);
1213#line 88
1214 __cil_tmp13 = __cil_tmp12 & __cil_tmp9;
1215#line 88
1216 if (__cil_tmp13 != 0U) {
1217#line 89
1218 return (0);
1219 } else {
1220
1221 }
1222 }
1223 {
1224#line 91
1225 tmp = w1_reset_select_slave(sl);
1226 }
1227#line 91
1228 if (tmp != 0) {
1229#line 92
1230 __cil_tmp14 = (unsigned long )data;
1231#line 92
1232 __cil_tmp15 = __cil_tmp14 + 512;
1233#line 92
1234 *((u32 *)__cil_tmp15) = 0U;
1235#line 93
1236 return (-5);
1237 } else {
1238
1239 }
1240 {
1241#line 96
1242 __cil_tmp16 = 0 * 1UL;
1243#line 96
1244 __cil_tmp17 = (unsigned long )(wrbuf) + __cil_tmp16;
1245#line 96
1246 *((u8 *)__cil_tmp17) = (u8 )240U;
1247#line 97
1248 __cil_tmp18 = 1 * 1UL;
1249#line 97
1250 __cil_tmp19 = (unsigned long )(wrbuf) + __cil_tmp18;
1251#line 97
1252 *((u8 *)__cil_tmp19) = (u8 )off;
1253#line 98
1254 __cil_tmp20 = 2 * 1UL;
1255#line 98
1256 __cil_tmp21 = (unsigned long )(wrbuf) + __cil_tmp20;
1257#line 98
1258 __cil_tmp22 = off >> 8;
1259#line 98
1260 *((u8 *)__cil_tmp21) = (u8 )__cil_tmp22;
1261#line 99
1262 __cil_tmp23 = (unsigned long )sl;
1263#line 99
1264 __cil_tmp24 = __cil_tmp23 + 88;
1265#line 99
1266 __cil_tmp25 = *((struct w1_master **)__cil_tmp24);
1267#line 99
1268 __cil_tmp26 = (u8 const *)(& wrbuf);
1269#line 99
1270 w1_write_block(__cil_tmp25, __cil_tmp26, 3);
1271#line 100
1272 __cil_tmp27 = (unsigned long )sl;
1273#line 100
1274 __cil_tmp28 = __cil_tmp27 + 88;
1275#line 100
1276 __cil_tmp29 = *((struct w1_master **)__cil_tmp28);
1277#line 100
1278 __cil_tmp30 = (unsigned long )off;
1279#line 100
1280 __cil_tmp31 = (u8 (*)[512U])data;
1281#line 100
1282 __cil_tmp32 = (u8 *)__cil_tmp31;
1283#line 100
1284 __cil_tmp33 = __cil_tmp32 + __cil_tmp30;
1285#line 100
1286 w1_read_block(__cil_tmp29, __cil_tmp33, 32);
1287#line 103
1288 __cil_tmp34 = (u16 )0;
1289#line 103
1290 __cil_tmp35 = (unsigned long )off;
1291#line 103
1292 __cil_tmp36 = (u8 (*)[512U])data;
1293#line 103
1294 __cil_tmp37 = (u8 const *)__cil_tmp36;
1295#line 103
1296 __cil_tmp38 = __cil_tmp37 + __cil_tmp35;
1297#line 103
1298 tmp___0 = crc16(__cil_tmp34, __cil_tmp38, 32UL);
1299 }
1300 {
1301#line 103
1302 __cil_tmp39 = (unsigned int )tmp___0;
1303#line 103
1304 if (__cil_tmp39 == 45057U) {
1305#line 104
1306 __cil_tmp40 = (unsigned long )data;
1307#line 104
1308 __cil_tmp41 = __cil_tmp40 + 512;
1309#line 104
1310 __cil_tmp42 = 1 << block;
1311#line 104
1312 __cil_tmp43 = (u32 )__cil_tmp42;
1313#line 104
1314 __cil_tmp44 = (unsigned long )data;
1315#line 104
1316 __cil_tmp45 = __cil_tmp44 + 512;
1317#line 104
1318 __cil_tmp46 = *((u32 *)__cil_tmp45);
1319#line 104
1320 *((u32 *)__cil_tmp41) = __cil_tmp46 | __cil_tmp43;
1321 } else {
1322
1323 }
1324 }
1325#line 106
1326 return (0);
1327}
1328}
1329#line 110 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
1330static ssize_t w1_f23_read_bin(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1331 char *buf , loff_t off , size_t count )
1332{ struct w1_slave *sl ;
1333 struct w1_slave *tmp ;
1334 struct w1_f23_data *data ;
1335 int i ;
1336 int min_page ;
1337 int max_page ;
1338 int tmp___0 ;
1339 size_t __len ;
1340 void *__ret ;
1341 unsigned long __cil_tmp16 ;
1342 unsigned long __cil_tmp17 ;
1343 void *__cil_tmp18 ;
1344 unsigned long __cil_tmp19 ;
1345 unsigned long __cil_tmp20 ;
1346 struct w1_master *__cil_tmp21 ;
1347 unsigned long __cil_tmp22 ;
1348 unsigned long __cil_tmp23 ;
1349 struct mutex *__cil_tmp24 ;
1350 loff_t __cil_tmp25 ;
1351 unsigned long long __cil_tmp26 ;
1352 unsigned long long __cil_tmp27 ;
1353 unsigned long long __cil_tmp28 ;
1354 unsigned long long __cil_tmp29 ;
1355 unsigned long long __cil_tmp30 ;
1356 void *__cil_tmp31 ;
1357 unsigned long __cil_tmp32 ;
1358 u8 (*__cil_tmp33)[512U] ;
1359 void const *__cil_tmp34 ;
1360 void const *__cil_tmp35 ;
1361 unsigned long __cil_tmp36 ;
1362 unsigned long __cil_tmp37 ;
1363 struct w1_master *__cil_tmp38 ;
1364 unsigned long __cil_tmp39 ;
1365 unsigned long __cil_tmp40 ;
1366 struct mutex *__cil_tmp41 ;
1367
1368 {
1369 {
1370#line 114
1371 tmp = kobj_to_w1_slave(kobj);
1372#line 114
1373 sl = tmp;
1374#line 116
1375 __cil_tmp16 = (unsigned long )sl;
1376#line 116
1377 __cil_tmp17 = __cil_tmp16 + 104;
1378#line 116
1379 __cil_tmp18 = *((void **)__cil_tmp17);
1380#line 116
1381 data = (struct w1_f23_data *)__cil_tmp18;
1382#line 122
1383 count = w1_f23_fix_count(off, count, 512UL);
1384 }
1385#line 122
1386 if (count == 0UL) {
1387#line 123
1388 return (0L);
1389 } else {
1390
1391 }
1392 {
1393#line 125
1394 __cil_tmp19 = (unsigned long )sl;
1395#line 125
1396 __cil_tmp20 = __cil_tmp19 + 88;
1397#line 125
1398 __cil_tmp21 = *((struct w1_master **)__cil_tmp20);
1399#line 125
1400 __cil_tmp22 = (unsigned long )__cil_tmp21;
1401#line 125
1402 __cil_tmp23 = __cil_tmp22 + 144;
1403#line 125
1404 __cil_tmp24 = (struct mutex *)__cil_tmp23;
1405#line 125
1406 mutex_lock_nested(__cil_tmp24, 0U);
1407#line 129
1408 __cil_tmp25 = off >> 5;
1409#line 129
1410 min_page = (int )__cil_tmp25;
1411#line 130
1412 __cil_tmp26 = (unsigned long long )count;
1413#line 130
1414 __cil_tmp27 = (unsigned long long )off;
1415#line 130
1416 __cil_tmp28 = __cil_tmp27 + __cil_tmp26;
1417#line 130
1418 __cil_tmp29 = __cil_tmp28 - 1ULL;
1419#line 130
1420 __cil_tmp30 = __cil_tmp29 >> 5;
1421#line 130
1422 max_page = (int )__cil_tmp30;
1423#line 131
1424 i = min_page;
1425 }
1426#line 131
1427 goto ldv_15172;
1428 ldv_15171:
1429 {
1430#line 132
1431 tmp___0 = w1_f23_refresh_block(sl, data, i);
1432 }
1433#line 132
1434 if (tmp___0 != 0) {
1435#line 133
1436 count = 0xfffffffffffffffbUL;
1437#line 134
1438 goto out_up;
1439 } else {
1440
1441 }
1442#line 131
1443 i = i + 1;
1444 ldv_15172: ;
1445#line 131
1446 if (i <= max_page) {
1447#line 132
1448 goto ldv_15171;
1449 } else {
1450#line 134
1451 goto ldv_15173;
1452 }
1453 ldv_15173:
1454 {
1455#line 137
1456 __len = count;
1457#line 137
1458 __cil_tmp31 = (void *)buf;
1459#line 137
1460 __cil_tmp32 = (unsigned long )off;
1461#line 137
1462 __cil_tmp33 = (u8 (*)[512U])data;
1463#line 137
1464 __cil_tmp34 = (void const *)__cil_tmp33;
1465#line 137
1466 __cil_tmp35 = __cil_tmp34 + __cil_tmp32;
1467#line 137
1468 __ret = __builtin_memcpy(__cil_tmp31, __cil_tmp35, __len);
1469 }
1470 out_up:
1471 {
1472#line 156
1473 __cil_tmp36 = (unsigned long )sl;
1474#line 156
1475 __cil_tmp37 = __cil_tmp36 + 88;
1476#line 156
1477 __cil_tmp38 = *((struct w1_master **)__cil_tmp37);
1478#line 156
1479 __cil_tmp39 = (unsigned long )__cil_tmp38;
1480#line 156
1481 __cil_tmp40 = __cil_tmp39 + 144;
1482#line 156
1483 __cil_tmp41 = (struct mutex *)__cil_tmp40;
1484#line 156
1485 mutex_unlock(__cil_tmp41);
1486 }
1487#line 158
1488 return ((ssize_t )count);
1489}
1490}
1491#line 173 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
1492static int w1_f23_write(struct w1_slave *sl , int addr , int len , u8 const *data )
1493{ struct w1_f23_data *f23 ;
1494 u8 wrbuf[4U] ;
1495 u8 rdbuf[35U] ;
1496 u8 es ;
1497 int tmp ;
1498 int tmp___0 ;
1499 int tmp___1 ;
1500 int tmp___2 ;
1501 unsigned long __cil_tmp13 ;
1502 unsigned long __cil_tmp14 ;
1503 void *__cil_tmp15 ;
1504 unsigned char __cil_tmp16 ;
1505 int __cil_tmp17 ;
1506 unsigned char __cil_tmp18 ;
1507 int __cil_tmp19 ;
1508 int __cil_tmp20 ;
1509 unsigned int __cil_tmp21 ;
1510 unsigned int __cil_tmp22 ;
1511 u8 __cil_tmp23 ;
1512 unsigned int __cil_tmp24 ;
1513 unsigned int __cil_tmp25 ;
1514 unsigned long __cil_tmp26 ;
1515 unsigned long __cil_tmp27 ;
1516 unsigned long __cil_tmp28 ;
1517 unsigned long __cil_tmp29 ;
1518 unsigned long __cil_tmp30 ;
1519 unsigned long __cil_tmp31 ;
1520 int __cil_tmp32 ;
1521 unsigned long __cil_tmp33 ;
1522 unsigned long __cil_tmp34 ;
1523 struct w1_master *__cil_tmp35 ;
1524 u8 const *__cil_tmp36 ;
1525 unsigned long __cil_tmp37 ;
1526 unsigned long __cil_tmp38 ;
1527 struct w1_master *__cil_tmp39 ;
1528 unsigned long __cil_tmp40 ;
1529 unsigned long __cil_tmp41 ;
1530 struct w1_master *__cil_tmp42 ;
1531 u8 __cil_tmp43 ;
1532 unsigned long __cil_tmp44 ;
1533 unsigned long __cil_tmp45 ;
1534 struct w1_master *__cil_tmp46 ;
1535 u8 *__cil_tmp47 ;
1536 int __cil_tmp48 ;
1537 unsigned long __cil_tmp49 ;
1538 unsigned long __cil_tmp50 ;
1539 u8 __cil_tmp51 ;
1540 int __cil_tmp52 ;
1541 unsigned long __cil_tmp53 ;
1542 unsigned long __cil_tmp54 ;
1543 u8 __cil_tmp55 ;
1544 int __cil_tmp56 ;
1545 unsigned long __cil_tmp57 ;
1546 unsigned long __cil_tmp58 ;
1547 u8 __cil_tmp59 ;
1548 int __cil_tmp60 ;
1549 unsigned long __cil_tmp61 ;
1550 unsigned long __cil_tmp62 ;
1551 u8 __cil_tmp63 ;
1552 int __cil_tmp64 ;
1553 int __cil_tmp65 ;
1554 unsigned long __cil_tmp66 ;
1555 unsigned long __cil_tmp67 ;
1556 u8 __cil_tmp68 ;
1557 int __cil_tmp69 ;
1558 void const *__cil_tmp70 ;
1559 void const *__cil_tmp71 ;
1560 void const *__cil_tmp72 ;
1561 size_t __cil_tmp73 ;
1562 unsigned long __cil_tmp74 ;
1563 unsigned long __cil_tmp75 ;
1564 unsigned long __cil_tmp76 ;
1565 unsigned long __cil_tmp77 ;
1566 unsigned long __cil_tmp78 ;
1567 unsigned long __cil_tmp79 ;
1568 struct w1_master *__cil_tmp80 ;
1569 u8 const *__cil_tmp81 ;
1570 unsigned long __cil_tmp82 ;
1571 unsigned long __cil_tmp83 ;
1572 struct w1_master *__cil_tmp84 ;
1573 unsigned long __cil_tmp85 ;
1574 unsigned long __cil_tmp86 ;
1575 int __cil_tmp87 ;
1576 int __cil_tmp88 ;
1577 int __cil_tmp89 ;
1578 u32 __cil_tmp90 ;
1579 unsigned long __cil_tmp91 ;
1580 unsigned long __cil_tmp92 ;
1581 u32 __cil_tmp93 ;
1582
1583 {
1584 {
1585#line 176
1586 __cil_tmp13 = (unsigned long )sl;
1587#line 176
1588 __cil_tmp14 = __cil_tmp13 + 104;
1589#line 176
1590 __cil_tmp15 = *((void **)__cil_tmp14);
1591#line 176
1592 f23 = (struct w1_f23_data *)__cil_tmp15;
1593#line 180
1594 __cil_tmp16 = (unsigned char )len;
1595#line 180
1596 __cil_tmp17 = (int )__cil_tmp16;
1597#line 180
1598 __cil_tmp18 = (unsigned char )addr;
1599#line 180
1600 __cil_tmp19 = (int )__cil_tmp18;
1601#line 180
1602 __cil_tmp20 = __cil_tmp19 + __cil_tmp17;
1603#line 180
1604 __cil_tmp21 = (unsigned int )__cil_tmp20;
1605#line 180
1606 __cil_tmp22 = __cil_tmp21 + 255U;
1607#line 180
1608 __cil_tmp23 = (u8 )__cil_tmp22;
1609#line 180
1610 __cil_tmp24 = (unsigned int )__cil_tmp23;
1611#line 180
1612 __cil_tmp25 = __cil_tmp24 & 31U;
1613#line 180
1614 es = (u8 )__cil_tmp25;
1615#line 183
1616 tmp = w1_reset_select_slave(sl);
1617 }
1618#line 183
1619 if (tmp != 0) {
1620#line 184
1621 return (-1);
1622 } else {
1623
1624 }
1625 {
1626#line 186
1627 __cil_tmp26 = 0 * 1UL;
1628#line 186
1629 __cil_tmp27 = (unsigned long )(wrbuf) + __cil_tmp26;
1630#line 186
1631 *((u8 *)__cil_tmp27) = (u8 )15U;
1632#line 187
1633 __cil_tmp28 = 1 * 1UL;
1634#line 187
1635 __cil_tmp29 = (unsigned long )(wrbuf) + __cil_tmp28;
1636#line 187
1637 *((u8 *)__cil_tmp29) = (u8 )addr;
1638#line 188
1639 __cil_tmp30 = 2 * 1UL;
1640#line 188
1641 __cil_tmp31 = (unsigned long )(wrbuf) + __cil_tmp30;
1642#line 188
1643 __cil_tmp32 = addr >> 8;
1644#line 188
1645 *((u8 *)__cil_tmp31) = (u8 )__cil_tmp32;
1646#line 190
1647 __cil_tmp33 = (unsigned long )sl;
1648#line 190
1649 __cil_tmp34 = __cil_tmp33 + 88;
1650#line 190
1651 __cil_tmp35 = *((struct w1_master **)__cil_tmp34);
1652#line 190
1653 __cil_tmp36 = (u8 const *)(& wrbuf);
1654#line 190
1655 w1_write_block(__cil_tmp35, __cil_tmp36, 3);
1656#line 191
1657 __cil_tmp37 = (unsigned long )sl;
1658#line 191
1659 __cil_tmp38 = __cil_tmp37 + 88;
1660#line 191
1661 __cil_tmp39 = *((struct w1_master **)__cil_tmp38);
1662#line 191
1663 w1_write_block(__cil_tmp39, data, len);
1664#line 194
1665 tmp___0 = w1_reset_select_slave(sl);
1666 }
1667#line 194
1668 if (tmp___0 != 0) {
1669#line 195
1670 return (-1);
1671 } else {
1672
1673 }
1674 {
1675#line 197
1676 __cil_tmp40 = (unsigned long )sl;
1677#line 197
1678 __cil_tmp41 = __cil_tmp40 + 88;
1679#line 197
1680 __cil_tmp42 = *((struct w1_master **)__cil_tmp41);
1681#line 197
1682 __cil_tmp43 = (u8 )170;
1683#line 197
1684 w1_write_8(__cil_tmp42, __cil_tmp43);
1685#line 198
1686 __cil_tmp44 = (unsigned long )sl;
1687#line 198
1688 __cil_tmp45 = __cil_tmp44 + 88;
1689#line 198
1690 __cil_tmp46 = *((struct w1_master **)__cil_tmp45);
1691#line 198
1692 __cil_tmp47 = (u8 *)(& rdbuf);
1693#line 198
1694 __cil_tmp48 = len + 3;
1695#line 198
1696 w1_read_block(__cil_tmp46, __cil_tmp47, __cil_tmp48);
1697 }
1698 {
1699#line 201
1700 __cil_tmp49 = 1 * 1UL;
1701#line 201
1702 __cil_tmp50 = (unsigned long )(wrbuf) + __cil_tmp49;
1703#line 201
1704 __cil_tmp51 = *((u8 *)__cil_tmp50);
1705#line 201
1706 __cil_tmp52 = (int )__cil_tmp51;
1707#line 201
1708 __cil_tmp53 = 0 * 1UL;
1709#line 201
1710 __cil_tmp54 = (unsigned long )(rdbuf) + __cil_tmp53;
1711#line 201
1712 __cil_tmp55 = *((u8 *)__cil_tmp54);
1713#line 201
1714 __cil_tmp56 = (int )__cil_tmp55;
1715#line 201
1716 if (__cil_tmp56 != __cil_tmp52) {
1717#line 203
1718 return (-1);
1719 } else {
1720 {
1721#line 201
1722 __cil_tmp57 = 2 * 1UL;
1723#line 201
1724 __cil_tmp58 = (unsigned long )(wrbuf) + __cil_tmp57;
1725#line 201
1726 __cil_tmp59 = *((u8 *)__cil_tmp58);
1727#line 201
1728 __cil_tmp60 = (int )__cil_tmp59;
1729#line 201
1730 __cil_tmp61 = 1 * 1UL;
1731#line 201
1732 __cil_tmp62 = (unsigned long )(rdbuf) + __cil_tmp61;
1733#line 201
1734 __cil_tmp63 = *((u8 *)__cil_tmp62);
1735#line 201
1736 __cil_tmp64 = (int )__cil_tmp63;
1737#line 201
1738 if (__cil_tmp64 != __cil_tmp60) {
1739#line 203
1740 return (-1);
1741 } else {
1742 {
1743#line 201
1744 __cil_tmp65 = (int )es;
1745#line 201
1746 __cil_tmp66 = 2 * 1UL;
1747#line 201
1748 __cil_tmp67 = (unsigned long )(rdbuf) + __cil_tmp66;
1749#line 201
1750 __cil_tmp68 = *((u8 *)__cil_tmp67);
1751#line 201
1752 __cil_tmp69 = (int )__cil_tmp68;
1753#line 201
1754 if (__cil_tmp69 != __cil_tmp65) {
1755#line 203
1756 return (-1);
1757 } else {
1758 {
1759#line 201
1760 __cil_tmp70 = (void const *)data;
1761#line 201
1762 __cil_tmp71 = (void const *)(& rdbuf);
1763#line 201
1764 __cil_tmp72 = __cil_tmp71 + 3U;
1765#line 201
1766 __cil_tmp73 = (size_t )len;
1767#line 201
1768 tmp___1 = memcmp(__cil_tmp70, __cil_tmp72, __cil_tmp73);
1769 }
1770#line 201
1771 if (tmp___1 != 0) {
1772#line 203
1773 return (-1);
1774 } else {
1775
1776 }
1777 }
1778 }
1779 }
1780 }
1781 }
1782 }
1783 {
1784#line 206
1785 tmp___2 = w1_reset_select_slave(sl);
1786 }
1787#line 206
1788 if (tmp___2 != 0) {
1789#line 207
1790 return (-1);
1791 } else {
1792
1793 }
1794 {
1795#line 209
1796 __cil_tmp74 = 0 * 1UL;
1797#line 209
1798 __cil_tmp75 = (unsigned long )(wrbuf) + __cil_tmp74;
1799#line 209
1800 *((u8 *)__cil_tmp75) = (u8 )85U;
1801#line 210
1802 __cil_tmp76 = 3 * 1UL;
1803#line 210
1804 __cil_tmp77 = (unsigned long )(wrbuf) + __cil_tmp76;
1805#line 210
1806 *((u8 *)__cil_tmp77) = es;
1807#line 211
1808 __cil_tmp78 = (unsigned long )sl;
1809#line 211
1810 __cil_tmp79 = __cil_tmp78 + 88;
1811#line 211
1812 __cil_tmp80 = *((struct w1_master **)__cil_tmp79);
1813#line 211
1814 __cil_tmp81 = (u8 const *)(& wrbuf);
1815#line 211
1816 w1_write_block(__cil_tmp80, __cil_tmp81, 4);
1817#line 214
1818 msleep(5U);
1819#line 217
1820 __cil_tmp82 = (unsigned long )sl;
1821#line 217
1822 __cil_tmp83 = __cil_tmp82 + 88;
1823#line 217
1824 __cil_tmp84 = *((struct w1_master **)__cil_tmp83);
1825#line 217
1826 w1_reset_bus(__cil_tmp84);
1827#line 219
1828 __cil_tmp85 = (unsigned long )f23;
1829#line 219
1830 __cil_tmp86 = __cil_tmp85 + 512;
1831#line 219
1832 __cil_tmp87 = addr >> 5;
1833#line 219
1834 __cil_tmp88 = 1 << __cil_tmp87;
1835#line 219
1836 __cil_tmp89 = ~ __cil_tmp88;
1837#line 219
1838 __cil_tmp90 = (u32 )__cil_tmp89;
1839#line 219
1840 __cil_tmp91 = (unsigned long )f23;
1841#line 219
1842 __cil_tmp92 = __cil_tmp91 + 512;
1843#line 219
1844 __cil_tmp93 = *((u32 *)__cil_tmp92);
1845#line 219
1846 *((u32 *)__cil_tmp86) = __cil_tmp93 & __cil_tmp90;
1847 }
1848#line 221
1849 return (0);
1850}
1851}
1852#line 224 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
1853static ssize_t w1_f23_write_bin(struct file *filp , struct kobject *kobj , struct bin_attribute *bin_attr ,
1854 char *buf , loff_t off , size_t count )
1855{ struct w1_slave *sl ;
1856 struct w1_slave *tmp ;
1857 int addr ;
1858 int len ;
1859 int idx ;
1860 u16 tmp___0 ;
1861 int tmp___1 ;
1862 long long __cil_tmp14 ;
1863 unsigned long __cil_tmp15 ;
1864 unsigned long __cil_tmp16 ;
1865 struct device *__cil_tmp17 ;
1866 struct device const *__cil_tmp18 ;
1867 int __cil_tmp19 ;
1868 unsigned long __cil_tmp20 ;
1869 unsigned long __cil_tmp21 ;
1870 unsigned long __cil_tmp22 ;
1871 struct device *__cil_tmp23 ;
1872 struct device const *__cil_tmp24 ;
1873 int __cil_tmp25 ;
1874 u16 __cil_tmp26 ;
1875 unsigned long __cil_tmp27 ;
1876 u8 const *__cil_tmp28 ;
1877 u8 const *__cil_tmp29 ;
1878 unsigned int __cil_tmp30 ;
1879 unsigned long __cil_tmp31 ;
1880 unsigned long __cil_tmp32 ;
1881 struct device *__cil_tmp33 ;
1882 struct device const *__cil_tmp34 ;
1883 int __cil_tmp35 ;
1884 size_t __cil_tmp36 ;
1885 unsigned long __cil_tmp37 ;
1886 unsigned long __cil_tmp38 ;
1887 struct w1_master *__cil_tmp39 ;
1888 unsigned long __cil_tmp40 ;
1889 unsigned long __cil_tmp41 ;
1890 struct mutex *__cil_tmp42 ;
1891 unsigned int __cil_tmp43 ;
1892 unsigned int __cil_tmp44 ;
1893 unsigned int __cil_tmp45 ;
1894 int __cil_tmp46 ;
1895 size_t __cil_tmp47 ;
1896 size_t __cil_tmp48 ;
1897 size_t __cil_tmp49 ;
1898 unsigned int __cil_tmp50 ;
1899 unsigned int __cil_tmp51 ;
1900 unsigned int __cil_tmp52 ;
1901 unsigned long __cil_tmp53 ;
1902 u8 const *__cil_tmp54 ;
1903 u8 const *__cil_tmp55 ;
1904 size_t __cil_tmp56 ;
1905 unsigned long __cil_tmp57 ;
1906 unsigned long __cil_tmp58 ;
1907 struct w1_master *__cil_tmp59 ;
1908 unsigned long __cil_tmp60 ;
1909 unsigned long __cil_tmp61 ;
1910 struct mutex *__cil_tmp62 ;
1911
1912 {
1913 {
1914#line 228
1915 tmp = kobj_to_w1_slave(kobj);
1916#line 228
1917 sl = tmp;
1918#line 231
1919 count = w1_f23_fix_count(off, count, 512UL);
1920 }
1921#line 231
1922 if (count == 0UL) {
1923#line 232
1924 return (0L);
1925 } else {
1926
1927 }
1928 {
1929#line 236
1930 __cil_tmp14 = off & 31LL;
1931#line 236
1932 if (__cil_tmp14 != 0LL) {
1933 {
1934#line 237
1935 __cil_tmp15 = (unsigned long )sl;
1936#line 237
1937 __cil_tmp16 = __cil_tmp15 + 112;
1938#line 237
1939 __cil_tmp17 = (struct device *)__cil_tmp16;
1940#line 237
1941 __cil_tmp18 = (struct device const *)__cil_tmp17;
1942#line 237
1943 __cil_tmp19 = (int )off;
1944#line 237
1945 dev_err(__cil_tmp18, "invalid offset/count off=%d cnt=%zd\n", __cil_tmp19, count);
1946 }
1947#line 239
1948 return (-22L);
1949 } else {
1950 {
1951#line 236
1952 __cil_tmp20 = count & 31UL;
1953#line 236
1954 if (__cil_tmp20 != 0UL) {
1955 {
1956#line 237
1957 __cil_tmp21 = (unsigned long )sl;
1958#line 237
1959 __cil_tmp22 = __cil_tmp21 + 112;
1960#line 237
1961 __cil_tmp23 = (struct device *)__cil_tmp22;
1962#line 237
1963 __cil_tmp24 = (struct device const *)__cil_tmp23;
1964#line 237
1965 __cil_tmp25 = (int )off;
1966#line 237
1967 dev_err(__cil_tmp24, "invalid offset/count off=%d cnt=%zd\n", __cil_tmp25, count);
1968 }
1969#line 239
1970 return (-22L);
1971 } else {
1972
1973 }
1974 }
1975 }
1976 }
1977#line 243
1978 idx = 0;
1979#line 243
1980 goto ldv_15200;
1981 ldv_15199:
1982 {
1983#line 244
1984 __cil_tmp26 = (u16 )0;
1985#line 244
1986 __cil_tmp27 = (unsigned long )idx;
1987#line 244
1988 __cil_tmp28 = (u8 const *)buf;
1989#line 244
1990 __cil_tmp29 = __cil_tmp28 + __cil_tmp27;
1991#line 244
1992 tmp___0 = crc16(__cil_tmp26, __cil_tmp29, 32UL);
1993 }
1994 {
1995#line 244
1996 __cil_tmp30 = (unsigned int )tmp___0;
1997#line 244
1998 if (__cil_tmp30 != 45057U) {
1999 {
2000#line 245
2001 __cil_tmp31 = (unsigned long )sl;
2002#line 245
2003 __cil_tmp32 = __cil_tmp31 + 112;
2004#line 245
2005 __cil_tmp33 = (struct device *)__cil_tmp32;
2006#line 245
2007 __cil_tmp34 = (struct device const *)__cil_tmp33;
2008#line 245
2009 __cil_tmp35 = (int )off;
2010#line 245
2011 dev_err(__cil_tmp34, "bad CRC at offset %d\n", __cil_tmp35);
2012 }
2013#line 246
2014 return (-22L);
2015 } else {
2016
2017 }
2018 }
2019#line 243
2020 idx = idx + 32;
2021 ldv_15200: ;
2022 {
2023#line 243
2024 __cil_tmp36 = (size_t )idx;
2025#line 243
2026 if (__cil_tmp36 < count) {
2027#line 244
2028 goto ldv_15199;
2029 } else {
2030#line 246
2031 goto ldv_15201;
2032 }
2033 }
2034 ldv_15201:
2035 {
2036#line 251
2037 __cil_tmp37 = (unsigned long )sl;
2038#line 251
2039 __cil_tmp38 = __cil_tmp37 + 88;
2040#line 251
2041 __cil_tmp39 = *((struct w1_master **)__cil_tmp38);
2042#line 251
2043 __cil_tmp40 = (unsigned long )__cil_tmp39;
2044#line 251
2045 __cil_tmp41 = __cil_tmp40 + 144;
2046#line 251
2047 __cil_tmp42 = (struct mutex *)__cil_tmp41;
2048#line 251
2049 mutex_lock_nested(__cil_tmp42, 0U);
2050#line 254
2051 idx = 0;
2052 }
2053#line 255
2054 goto ldv_15204;
2055 ldv_15203:
2056#line 256
2057 __cil_tmp43 = (unsigned int )idx;
2058#line 256
2059 __cil_tmp44 = (unsigned int )off;
2060#line 256
2061 __cil_tmp45 = __cil_tmp44 + __cil_tmp43;
2062#line 256
2063 addr = (int )__cil_tmp45;
2064#line 257
2065 __cil_tmp46 = addr & 31;
2066#line 257
2067 len = 32 - __cil_tmp46;
2068 {
2069#line 258
2070 __cil_tmp47 = (size_t )idx;
2071#line 258
2072 __cil_tmp48 = count - __cil_tmp47;
2073#line 258
2074 __cil_tmp49 = (size_t )len;
2075#line 258
2076 if (__cil_tmp49 > __cil_tmp48) {
2077#line 259
2078 __cil_tmp50 = (unsigned int )idx;
2079#line 259
2080 __cil_tmp51 = (unsigned int )count;
2081#line 259
2082 __cil_tmp52 = __cil_tmp51 - __cil_tmp50;
2083#line 259
2084 len = (int )__cil_tmp52;
2085 } else {
2086
2087 }
2088 }
2089 {
2090#line 261
2091 __cil_tmp53 = (unsigned long )idx;
2092#line 261
2093 __cil_tmp54 = (u8 const *)buf;
2094#line 261
2095 __cil_tmp55 = __cil_tmp54 + __cil_tmp53;
2096#line 261
2097 tmp___1 = w1_f23_write(sl, addr, len, __cil_tmp55);
2098 }
2099#line 261
2100 if (tmp___1 < 0) {
2101#line 262
2102 count = 0xfffffffffffffffbUL;
2103#line 263
2104 goto out_up;
2105 } else {
2106
2107 }
2108#line 265
2109 idx = idx + len;
2110 ldv_15204: ;
2111 {
2112#line 255
2113 __cil_tmp56 = (size_t )idx;
2114#line 255
2115 if (__cil_tmp56 < count) {
2116#line 256
2117 goto ldv_15203;
2118 } else {
2119#line 258
2120 goto ldv_15205;
2121 }
2122 }
2123 ldv_15205: ;
2124 out_up:
2125 {
2126#line 269
2127 __cil_tmp57 = (unsigned long )sl;
2128#line 269
2129 __cil_tmp58 = __cil_tmp57 + 88;
2130#line 269
2131 __cil_tmp59 = *((struct w1_master **)__cil_tmp58);
2132#line 269
2133 __cil_tmp60 = (unsigned long )__cil_tmp59;
2134#line 269
2135 __cil_tmp61 = __cil_tmp60 + 144;
2136#line 269
2137 __cil_tmp62 = (struct mutex *)__cil_tmp61;
2138#line 269
2139 mutex_unlock(__cil_tmp62);
2140 }
2141#line 271
2142 return ((ssize_t )count);
2143}
2144}
2145#line 274 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2146static struct bin_attribute w1_f23_bin_attr = {{"eeprom", (umode_t )420U, (struct lock_class_key *)0, {{{(char)0}, {(char)0},
2147 {(char)0}, {(char)0},
2148 {(char)0}, {(char)0},
2149 {(char)0}, {(char)0}}}},
2150 512UL, (void *)0, & w1_f23_read_bin, & w1_f23_write_bin, (int (*)(struct file * ,
2151 struct kobject * ,
2152 struct bin_attribute * ,
2153 struct vm_area_struct * ))0};
2154#line 284 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2155static int w1_f23_add_slave(struct w1_slave *sl )
2156{ int err ;
2157 struct w1_f23_data *data ;
2158 void *tmp ;
2159 struct w1_f23_data *__cil_tmp5 ;
2160 unsigned long __cil_tmp6 ;
2161 unsigned long __cil_tmp7 ;
2162 unsigned long __cil_tmp8 ;
2163 unsigned long __cil_tmp9 ;
2164 unsigned long __cil_tmp10 ;
2165 unsigned long __cil_tmp11 ;
2166 unsigned long __cil_tmp12 ;
2167 struct kobject *__cil_tmp13 ;
2168 struct bin_attribute const *__cil_tmp14 ;
2169 void const *__cil_tmp15 ;
2170
2171 {
2172 {
2173#line 290
2174 tmp = kzalloc(516UL, 208U);
2175#line 290
2176 data = (struct w1_f23_data *)tmp;
2177 }
2178 {
2179#line 291
2180 __cil_tmp5 = (struct w1_f23_data *)0;
2181#line 291
2182 __cil_tmp6 = (unsigned long )__cil_tmp5;
2183#line 291
2184 __cil_tmp7 = (unsigned long )data;
2185#line 291
2186 if (__cil_tmp7 == __cil_tmp6) {
2187#line 292
2188 return (-12);
2189 } else {
2190
2191 }
2192 }
2193 {
2194#line 293
2195 __cil_tmp8 = (unsigned long )sl;
2196#line 293
2197 __cil_tmp9 = __cil_tmp8 + 104;
2198#line 293
2199 *((void **)__cil_tmp9) = (void *)data;
2200#line 297
2201 __cil_tmp10 = 112 + 16;
2202#line 297
2203 __cil_tmp11 = (unsigned long )sl;
2204#line 297
2205 __cil_tmp12 = __cil_tmp11 + __cil_tmp10;
2206#line 297
2207 __cil_tmp13 = (struct kobject *)__cil_tmp12;
2208#line 297
2209 __cil_tmp14 = (struct bin_attribute const *)(& w1_f23_bin_attr);
2210#line 297
2211 err = sysfs_create_bin_file(__cil_tmp13, __cil_tmp14);
2212 }
2213#line 300
2214 if (err != 0) {
2215 {
2216#line 301
2217 __cil_tmp15 = (void const *)data;
2218#line 301
2219 kfree(__cil_tmp15);
2220 }
2221 } else {
2222
2223 }
2224#line 304
2225 return (err);
2226}
2227}
2228#line 307 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2229static void w1_f23_remove_slave(struct w1_slave *sl )
2230{ unsigned long __cil_tmp2 ;
2231 unsigned long __cil_tmp3 ;
2232 void *__cil_tmp4 ;
2233 void const *__cil_tmp5 ;
2234 unsigned long __cil_tmp6 ;
2235 unsigned long __cil_tmp7 ;
2236 unsigned long __cil_tmp8 ;
2237 unsigned long __cil_tmp9 ;
2238 unsigned long __cil_tmp10 ;
2239 struct kobject *__cil_tmp11 ;
2240 struct bin_attribute const *__cil_tmp12 ;
2241
2242 {
2243 {
2244#line 310
2245 __cil_tmp2 = (unsigned long )sl;
2246#line 310
2247 __cil_tmp3 = __cil_tmp2 + 104;
2248#line 310
2249 __cil_tmp4 = *((void **)__cil_tmp3);
2250#line 310
2251 __cil_tmp5 = (void const *)__cil_tmp4;
2252#line 310
2253 kfree(__cil_tmp5);
2254#line 311
2255 __cil_tmp6 = (unsigned long )sl;
2256#line 311
2257 __cil_tmp7 = __cil_tmp6 + 104;
2258#line 311
2259 *((void **)__cil_tmp7) = (void *)0;
2260#line 313
2261 __cil_tmp8 = 112 + 16;
2262#line 313
2263 __cil_tmp9 = (unsigned long )sl;
2264#line 313
2265 __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
2266#line 313
2267 __cil_tmp11 = (struct kobject *)__cil_tmp10;
2268#line 313
2269 __cil_tmp12 = (struct bin_attribute const *)(& w1_f23_bin_attr);
2270#line 313
2271 sysfs_remove_bin_file(__cil_tmp11, __cil_tmp12);
2272 }
2273#line 314
2274 return;
2275}
2276}
2277#line 316 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2278static struct w1_family_ops w1_f23_fops = {& w1_f23_add_slave, & w1_f23_remove_slave};
2279#line 321 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2280static struct w1_family w1_family_23 = {{(struct list_head *)0, (struct list_head *)0}, (u8 )35U, & w1_f23_fops, {0}};
2281#line 326 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2282static int w1_f23_init(void)
2283{ int tmp ;
2284
2285 {
2286 {
2287#line 328
2288 tmp = w1_register_family(& w1_family_23);
2289 }
2290#line 328
2291 return (tmp);
2292}
2293}
2294#line 331 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2295static void w1_f23_fini(void)
2296{
2297
2298 {
2299 {
2300#line 333
2301 w1_unregister_family(& w1_family_23);
2302 }
2303#line 334
2304 return;
2305}
2306}
2307#line 355
2308extern void ldv_check_final_state(void) ;
2309#line 361
2310extern void ldv_initialize(void) ;
2311#line 364
2312extern int __VERIFIER_nondet_int(void) ;
2313#line 367 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2314int LDV_IN_INTERRUPT ;
2315#line 370 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2316void main(void)
2317{ struct file *var_group1 ;
2318 struct kobject *var_group2 ;
2319 struct bin_attribute *var_w1_f23_read_bin_2_p2 ;
2320 char *var_w1_f23_read_bin_2_p3 ;
2321 loff_t var_w1_f23_read_bin_2_p4 ;
2322 size_t var_w1_f23_read_bin_2_p5 ;
2323 struct bin_attribute *var_w1_f23_write_bin_4_p2 ;
2324 char *var_w1_f23_write_bin_4_p3 ;
2325 loff_t var_w1_f23_write_bin_4_p4 ;
2326 size_t var_w1_f23_write_bin_4_p5 ;
2327 struct w1_slave *var_group3 ;
2328 int tmp ;
2329 int tmp___0 ;
2330 int tmp___1 ;
2331
2332 {
2333 {
2334#line 548
2335 LDV_IN_INTERRUPT = 1;
2336#line 557
2337 ldv_initialize();
2338#line 598
2339 tmp = w1_f23_init();
2340 }
2341#line 598
2342 if (tmp != 0) {
2343#line 599
2344 goto ldv_final;
2345 } else {
2346
2347 }
2348#line 605
2349 goto ldv_15264;
2350 ldv_15263:
2351 {
2352#line 608
2353 tmp___0 = __VERIFIER_nondet_int();
2354 }
2355#line 610
2356 if (tmp___0 == 0) {
2357#line 610
2358 goto case_0;
2359 } else
2360#line 657
2361 if (tmp___0 == 1) {
2362#line 657
2363 goto case_1;
2364 } else
2365#line 708
2366 if (tmp___0 == 2) {
2367#line 708
2368 goto case_2;
2369 } else
2370#line 757
2371 if (tmp___0 == 3) {
2372#line 757
2373 goto case_3;
2374 } else {
2375 {
2376#line 806
2377 goto switch_default;
2378#line 608
2379 if (0) {
2380 case_0:
2381 {
2382#line 635
2383 w1_f23_read_bin(var_group1, var_group2, var_w1_f23_read_bin_2_p2, var_w1_f23_read_bin_2_p3,
2384 var_w1_f23_read_bin_2_p4, var_w1_f23_read_bin_2_p5);
2385 }
2386#line 656
2387 goto ldv_15258;
2388 case_1:
2389 {
2390#line 692
2391 w1_f23_write_bin(var_group1, var_group2, var_w1_f23_write_bin_4_p2, var_w1_f23_write_bin_4_p3,
2392 var_w1_f23_write_bin_4_p4, var_w1_f23_write_bin_4_p5);
2393 }
2394#line 707
2395 goto ldv_15258;
2396 case_2:
2397 {
2398#line 745
2399 w1_f23_add_slave(var_group3);
2400 }
2401#line 756
2402 goto ldv_15258;
2403 case_3:
2404 {
2405#line 798
2406 w1_f23_remove_slave(var_group3);
2407 }
2408#line 805
2409 goto ldv_15258;
2410 switch_default: ;
2411#line 806
2412 goto ldv_15258;
2413 } else {
2414 switch_break: ;
2415 }
2416 }
2417 }
2418 ldv_15258: ;
2419 ldv_15264:
2420 {
2421#line 605
2422 tmp___1 = __VERIFIER_nondet_int();
2423 }
2424#line 605
2425 if (tmp___1 != 0) {
2426#line 606
2427 goto ldv_15263;
2428 } else {
2429#line 608
2430 goto ldv_15265;
2431 }
2432 ldv_15265: ;
2433 {
2434#line 853
2435 w1_f23_fini();
2436 }
2437 ldv_final:
2438 {
2439#line 856
2440 ldv_check_final_state();
2441 }
2442#line 859
2443 return;
2444}
2445}
2446#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2447void ldv_blast_assert(void)
2448{
2449
2450 {
2451 ERROR: ;
2452#line 6
2453 goto ERROR;
2454}
2455}
2456#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2457extern int __VERIFIER_nondet_int(void) ;
2458#line 880 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2459int ldv_spin = 0;
2460#line 884 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2461void ldv_check_alloc_flags(gfp_t flags )
2462{
2463
2464 {
2465#line 887
2466 if (ldv_spin != 0) {
2467#line 887
2468 if (flags != 32U) {
2469 {
2470#line 887
2471 ldv_blast_assert();
2472 }
2473 } else {
2474
2475 }
2476 } else {
2477
2478 }
2479#line 890
2480 return;
2481}
2482}
2483#line 890
2484extern struct page *ldv_some_page(void) ;
2485#line 893 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2486struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
2487{ struct page *tmp ;
2488
2489 {
2490#line 896
2491 if (ldv_spin != 0) {
2492#line 896
2493 if (flags != 32U) {
2494 {
2495#line 896
2496 ldv_blast_assert();
2497 }
2498 } else {
2499
2500 }
2501 } else {
2502
2503 }
2504 {
2505#line 898
2506 tmp = ldv_some_page();
2507 }
2508#line 898
2509 return (tmp);
2510}
2511}
2512#line 902 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2513void ldv_check_alloc_nonatomic(void)
2514{
2515
2516 {
2517#line 905
2518 if (ldv_spin != 0) {
2519 {
2520#line 905
2521 ldv_blast_assert();
2522 }
2523 } else {
2524
2525 }
2526#line 908
2527 return;
2528}
2529}
2530#line 909 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2531void ldv_spin_lock(void)
2532{
2533
2534 {
2535#line 912
2536 ldv_spin = 1;
2537#line 913
2538 return;
2539}
2540}
2541#line 916 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2542void ldv_spin_unlock(void)
2543{
2544
2545 {
2546#line 919
2547 ldv_spin = 0;
2548#line 920
2549 return;
2550}
2551}
2552#line 923 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2553int ldv_spin_trylock(void)
2554{ int is_lock ;
2555
2556 {
2557 {
2558#line 928
2559 is_lock = __VERIFIER_nondet_int();
2560 }
2561#line 930
2562 if (is_lock != 0) {
2563#line 933
2564 return (0);
2565 } else {
2566#line 938
2567 ldv_spin = 1;
2568#line 940
2569 return (1);
2570 }
2571}
2572}
2573#line 1107 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2574void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
2575{
2576
2577 {
2578 {
2579#line 1113
2580 ldv_check_alloc_flags(ldv_func_arg2);
2581#line 1115
2582 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2583 }
2584#line 1116
2585 return ((void *)0);
2586}
2587}
2588#line 1118 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4911/dscv_tempdir/dscv/ri/43_1a/drivers/w1/slaves/w1_ds2433.c.p"
2589__inline static void *kzalloc(size_t size , gfp_t flags )
2590{ void *tmp ;
2591
2592 {
2593 {
2594#line 1124
2595 ldv_check_alloc_flags(flags);
2596#line 1125
2597 tmp = __VERIFIER_nondet_pointer();
2598 }
2599#line 1125
2600 return (tmp);
2601}
2602}