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