1
2
3
4#line 19 "include/asm-generic/int-ll64.h"
5typedef signed char __s8;
6#line 22 "include/asm-generic/int-ll64.h"
7typedef short __s16;
8#line 23 "include/asm-generic/int-ll64.h"
9typedef unsigned short __u16;
10#line 25 "include/asm-generic/int-ll64.h"
11typedef int __s32;
12#line 26 "include/asm-generic/int-ll64.h"
13typedef unsigned int __u32;
14#line 30 "include/asm-generic/int-ll64.h"
15typedef unsigned long long __u64;
16#line 43 "include/asm-generic/int-ll64.h"
17typedef unsigned char u8;
18#line 45 "include/asm-generic/int-ll64.h"
19typedef short s16;
20#line 46 "include/asm-generic/int-ll64.h"
21typedef unsigned short u16;
22#line 48 "include/asm-generic/int-ll64.h"
23typedef int s32;
24#line 49 "include/asm-generic/int-ll64.h"
25typedef unsigned int u32;
26#line 51 "include/asm-generic/int-ll64.h"
27typedef long long s64;
28#line 52 "include/asm-generic/int-ll64.h"
29typedef unsigned long long u64;
30#line 14 "include/asm-generic/posix_types.h"
31typedef long __kernel_long_t;
32#line 15 "include/asm-generic/posix_types.h"
33typedef unsigned long __kernel_ulong_t;
34#line 52 "include/asm-generic/posix_types.h"
35typedef unsigned int __kernel_uid32_t;
36#line 53 "include/asm-generic/posix_types.h"
37typedef unsigned int __kernel_gid32_t;
38#line 75 "include/asm-generic/posix_types.h"
39typedef __kernel_ulong_t __kernel_size_t;
40#line 76 "include/asm-generic/posix_types.h"
41typedef __kernel_long_t __kernel_ssize_t;
42#line 91 "include/asm-generic/posix_types.h"
43typedef long long __kernel_loff_t;
44#line 92 "include/asm-generic/posix_types.h"
45typedef __kernel_long_t __kernel_time_t;
46#line 95 "include/asm-generic/posix_types.h"
47typedef int __kernel_clockid_t;
48#line 21 "include/linux/types.h"
49typedef __u32 __kernel_dev_t;
50#line 24 "include/linux/types.h"
51typedef __kernel_dev_t dev_t;
52#line 27 "include/linux/types.h"
53typedef unsigned short umode_t;
54#line 35 "include/linux/types.h"
55typedef __kernel_clockid_t clockid_t;
56#line 38 "include/linux/types.h"
57typedef _Bool bool;
58#line 40 "include/linux/types.h"
59typedef __kernel_uid32_t uid_t;
60#line 41 "include/linux/types.h"
61typedef __kernel_gid32_t gid_t;
62#line 54 "include/linux/types.h"
63typedef __kernel_loff_t loff_t;
64#line 63 "include/linux/types.h"
65typedef __kernel_size_t size_t;
66#line 68 "include/linux/types.h"
67typedef __kernel_ssize_t ssize_t;
68#line 78 "include/linux/types.h"
69typedef __kernel_time_t time_t;
70#line 142 "include/linux/types.h"
71typedef unsigned long sector_t;
72#line 143 "include/linux/types.h"
73typedef unsigned long blkcnt_t;
74#line 202 "include/linux/types.h"
75typedef unsigned int gfp_t;
76#line 203 "include/linux/types.h"
77typedef unsigned int fmode_t;
78#line 206 "include/linux/types.h"
79typedef u64 phys_addr_t;
80#line 211 "include/linux/types.h"
81typedef phys_addr_t resource_size_t;
82#line 221 "include/linux/types.h"
83struct __anonstruct_atomic_t_6 {
84 int counter ;
85};
86#line 221 "include/linux/types.h"
87typedef struct __anonstruct_atomic_t_6 atomic_t;
88#line 226 "include/linux/types.h"
89struct __anonstruct_atomic64_t_7 {
90 long counter ;
91};
92#line 226 "include/linux/types.h"
93typedef struct __anonstruct_atomic64_t_7 atomic64_t;
94#line 227 "include/linux/types.h"
95struct list_head {
96 struct list_head *next ;
97 struct list_head *prev ;
98};
99#line 232
100struct hlist_node;
101#line 232 "include/linux/types.h"
102struct hlist_head {
103 struct hlist_node *first ;
104};
105#line 236 "include/linux/types.h"
106struct hlist_node {
107 struct hlist_node *next ;
108 struct hlist_node **pprev ;
109};
110#line 247 "include/linux/types.h"
111struct rcu_head {
112 struct rcu_head *next ;
113 void (*func)(struct rcu_head * ) ;
114};
115#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
116struct module;
117#line 55
118struct module;
119#line 146 "include/linux/init.h"
120typedef void (*ctor_fn_t)(void);
121#line 305 "include/linux/printk.h"
122struct _ddebug {
123 char const *modname ;
124 char const *function ;
125 char const *filename ;
126 char const *format ;
127 unsigned int lineno : 18 ;
128 unsigned char flags ;
129};
130#line 46 "include/linux/dynamic_debug.h"
131struct device;
132#line 46
133struct device;
134#line 57
135struct completion;
136#line 57
137struct completion;
138#line 348 "include/linux/kernel.h"
139struct pid;
140#line 348
141struct pid;
142#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
143struct timespec;
144#line 112
145struct timespec;
146#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
147struct page;
148#line 58
149struct page;
150#line 26 "include/asm-generic/getorder.h"
151struct task_struct;
152#line 26
153struct task_struct;
154#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
155struct file;
156#line 290
157struct file;
158#line 305
159struct seq_file;
160#line 305
161struct seq_file;
162#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
163struct arch_spinlock;
164#line 327
165struct arch_spinlock;
166#line 306 "include/linux/bitmap.h"
167struct bug_entry {
168 int bug_addr_disp ;
169 int file_disp ;
170 unsigned short line ;
171 unsigned short flags ;
172};
173#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
174struct static_key;
175#line 234
176struct static_key;
177#line 153 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
178struct seq_operations;
179#line 433
180struct kmem_cache;
181#line 23 "include/asm-generic/atomic-long.h"
182typedef atomic64_t atomic_long_t;
183#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
184typedef u16 __ticket_t;
185#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
186typedef u32 __ticketpair_t;
187#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
188struct __raw_tickets {
189 __ticket_t head ;
190 __ticket_t tail ;
191};
192#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
193union __anonunion_ldv_5907_29 {
194 __ticketpair_t head_tail ;
195 struct __raw_tickets tickets ;
196};
197#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
198struct arch_spinlock {
199 union __anonunion_ldv_5907_29 ldv_5907 ;
200};
201#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
202typedef struct arch_spinlock arch_spinlock_t;
203#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
204struct __anonstruct_ldv_5914_31 {
205 u32 read ;
206 s32 write ;
207};
208#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
209union __anonunion_arch_rwlock_t_30 {
210 s64 lock ;
211 struct __anonstruct_ldv_5914_31 ldv_5914 ;
212};
213#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
214typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
215#line 34
216struct lockdep_map;
217#line 34
218struct lockdep_map;
219#line 55 "include/linux/debug_locks.h"
220struct stack_trace {
221 unsigned int nr_entries ;
222 unsigned int max_entries ;
223 unsigned long *entries ;
224 int skip ;
225};
226#line 26 "include/linux/stacktrace.h"
227struct lockdep_subclass_key {
228 char __one_byte ;
229};
230#line 53 "include/linux/lockdep.h"
231struct lock_class_key {
232 struct lockdep_subclass_key subkeys[8U] ;
233};
234#line 59 "include/linux/lockdep.h"
235struct lock_class {
236 struct list_head hash_entry ;
237 struct list_head lock_entry ;
238 struct lockdep_subclass_key *key ;
239 unsigned int subclass ;
240 unsigned int dep_gen_id ;
241 unsigned long usage_mask ;
242 struct stack_trace usage_traces[13U] ;
243 struct list_head locks_after ;
244 struct list_head locks_before ;
245 unsigned int version ;
246 unsigned long ops ;
247 char const *name ;
248 int name_version ;
249 unsigned long contention_point[4U] ;
250 unsigned long contending_point[4U] ;
251};
252#line 144 "include/linux/lockdep.h"
253struct lockdep_map {
254 struct lock_class_key *key ;
255 struct lock_class *class_cache[2U] ;
256 char const *name ;
257 int cpu ;
258 unsigned long ip ;
259};
260#line 556 "include/linux/lockdep.h"
261struct raw_spinlock {
262 arch_spinlock_t raw_lock ;
263 unsigned int magic ;
264 unsigned int owner_cpu ;
265 void *owner ;
266 struct lockdep_map dep_map ;
267};
268#line 32 "include/linux/spinlock_types.h"
269typedef struct raw_spinlock raw_spinlock_t;
270#line 33 "include/linux/spinlock_types.h"
271struct __anonstruct_ldv_6122_33 {
272 u8 __padding[24U] ;
273 struct lockdep_map dep_map ;
274};
275#line 33 "include/linux/spinlock_types.h"
276union __anonunion_ldv_6123_32 {
277 struct raw_spinlock rlock ;
278 struct __anonstruct_ldv_6122_33 ldv_6122 ;
279};
280#line 33 "include/linux/spinlock_types.h"
281struct spinlock {
282 union __anonunion_ldv_6123_32 ldv_6123 ;
283};
284#line 76 "include/linux/spinlock_types.h"
285typedef struct spinlock spinlock_t;
286#line 23 "include/linux/rwlock_types.h"
287struct __anonstruct_rwlock_t_34 {
288 arch_rwlock_t raw_lock ;
289 unsigned int magic ;
290 unsigned int owner_cpu ;
291 void *owner ;
292 struct lockdep_map dep_map ;
293};
294#line 23 "include/linux/rwlock_types.h"
295typedef struct __anonstruct_rwlock_t_34 rwlock_t;
296#line 110 "include/linux/seqlock.h"
297struct seqcount {
298 unsigned int sequence ;
299};
300#line 121 "include/linux/seqlock.h"
301typedef struct seqcount seqcount_t;
302#line 254 "include/linux/seqlock.h"
303struct timespec {
304 __kernel_time_t tv_sec ;
305 long tv_nsec ;
306};
307#line 286 "include/linux/time.h"
308struct kstat {
309 u64 ino ;
310 dev_t dev ;
311 umode_t mode ;
312 unsigned int nlink ;
313 uid_t uid ;
314 gid_t gid ;
315 dev_t rdev ;
316 loff_t size ;
317 struct timespec atime ;
318 struct timespec mtime ;
319 struct timespec ctime ;
320 unsigned long blksize ;
321 unsigned long long blocks ;
322};
323#line 48 "include/linux/wait.h"
324struct __wait_queue_head {
325 spinlock_t lock ;
326 struct list_head task_list ;
327};
328#line 53 "include/linux/wait.h"
329typedef struct __wait_queue_head wait_queue_head_t;
330#line 670 "include/linux/mmzone.h"
331struct mutex {
332 atomic_t count ;
333 spinlock_t wait_lock ;
334 struct list_head wait_list ;
335 struct task_struct *owner ;
336 char const *name ;
337 void *magic ;
338 struct lockdep_map dep_map ;
339};
340#line 171 "include/linux/mutex.h"
341struct rw_semaphore;
342#line 171
343struct rw_semaphore;
344#line 172 "include/linux/mutex.h"
345struct rw_semaphore {
346 long count ;
347 raw_spinlock_t wait_lock ;
348 struct list_head wait_list ;
349 struct lockdep_map dep_map ;
350};
351#line 128 "include/linux/rwsem.h"
352struct completion {
353 unsigned int done ;
354 wait_queue_head_t wait ;
355};
356#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
357struct resource {
358 resource_size_t start ;
359 resource_size_t end ;
360 char const *name ;
361 unsigned long flags ;
362 struct resource *parent ;
363 struct resource *sibling ;
364 struct resource *child ;
365};
366#line 312 "include/linux/jiffies.h"
367union ktime {
368 s64 tv64 ;
369};
370#line 59 "include/linux/ktime.h"
371typedef union ktime ktime_t;
372#line 341
373struct tvec_base;
374#line 341
375struct tvec_base;
376#line 342 "include/linux/ktime.h"
377struct timer_list {
378 struct list_head entry ;
379 unsigned long expires ;
380 struct tvec_base *base ;
381 void (*function)(unsigned long ) ;
382 unsigned long data ;
383 int slack ;
384 int start_pid ;
385 void *start_site ;
386 char start_comm[16U] ;
387 struct lockdep_map lockdep_map ;
388};
389#line 289 "include/linux/timer.h"
390struct hrtimer;
391#line 289
392struct hrtimer;
393#line 290
394enum hrtimer_restart;
395#line 302
396struct work_struct;
397#line 302
398struct work_struct;
399#line 45 "include/linux/workqueue.h"
400struct work_struct {
401 atomic_long_t data ;
402 struct list_head entry ;
403 void (*func)(struct work_struct * ) ;
404 struct lockdep_map lockdep_map ;
405};
406#line 46 "include/linux/pm.h"
407struct pm_message {
408 int event ;
409};
410#line 52 "include/linux/pm.h"
411typedef struct pm_message pm_message_t;
412#line 53 "include/linux/pm.h"
413struct dev_pm_ops {
414 int (*prepare)(struct device * ) ;
415 void (*complete)(struct device * ) ;
416 int (*suspend)(struct device * ) ;
417 int (*resume)(struct device * ) ;
418 int (*freeze)(struct device * ) ;
419 int (*thaw)(struct device * ) ;
420 int (*poweroff)(struct device * ) ;
421 int (*restore)(struct device * ) ;
422 int (*suspend_late)(struct device * ) ;
423 int (*resume_early)(struct device * ) ;
424 int (*freeze_late)(struct device * ) ;
425 int (*thaw_early)(struct device * ) ;
426 int (*poweroff_late)(struct device * ) ;
427 int (*restore_early)(struct device * ) ;
428 int (*suspend_noirq)(struct device * ) ;
429 int (*resume_noirq)(struct device * ) ;
430 int (*freeze_noirq)(struct device * ) ;
431 int (*thaw_noirq)(struct device * ) ;
432 int (*poweroff_noirq)(struct device * ) ;
433 int (*restore_noirq)(struct device * ) ;
434 int (*runtime_suspend)(struct device * ) ;
435 int (*runtime_resume)(struct device * ) ;
436 int (*runtime_idle)(struct device * ) ;
437};
438#line 289
439enum rpm_status {
440 RPM_ACTIVE = 0,
441 RPM_RESUMING = 1,
442 RPM_SUSPENDED = 2,
443 RPM_SUSPENDING = 3
444} ;
445#line 296
446enum rpm_request {
447 RPM_REQ_NONE = 0,
448 RPM_REQ_IDLE = 1,
449 RPM_REQ_SUSPEND = 2,
450 RPM_REQ_AUTOSUSPEND = 3,
451 RPM_REQ_RESUME = 4
452} ;
453#line 304
454struct wakeup_source;
455#line 304
456struct wakeup_source;
457#line 494 "include/linux/pm.h"
458struct pm_subsys_data {
459 spinlock_t lock ;
460 unsigned int refcount ;
461};
462#line 499
463struct dev_pm_qos_request;
464#line 499
465struct pm_qos_constraints;
466#line 499 "include/linux/pm.h"
467struct dev_pm_info {
468 pm_message_t power_state ;
469 unsigned char can_wakeup : 1 ;
470 unsigned char async_suspend : 1 ;
471 bool is_prepared ;
472 bool is_suspended ;
473 bool ignore_children ;
474 spinlock_t lock ;
475 struct list_head entry ;
476 struct completion completion ;
477 struct wakeup_source *wakeup ;
478 bool wakeup_path ;
479 struct timer_list suspend_timer ;
480 unsigned long timer_expires ;
481 struct work_struct work ;
482 wait_queue_head_t wait_queue ;
483 atomic_t usage_count ;
484 atomic_t child_count ;
485 unsigned char disable_depth : 3 ;
486 unsigned char idle_notification : 1 ;
487 unsigned char request_pending : 1 ;
488 unsigned char deferred_resume : 1 ;
489 unsigned char run_wake : 1 ;
490 unsigned char runtime_auto : 1 ;
491 unsigned char no_callbacks : 1 ;
492 unsigned char irq_safe : 1 ;
493 unsigned char use_autosuspend : 1 ;
494 unsigned char timer_autosuspends : 1 ;
495 enum rpm_request request ;
496 enum rpm_status runtime_status ;
497 int runtime_error ;
498 int autosuspend_delay ;
499 unsigned long last_busy ;
500 unsigned long active_jiffies ;
501 unsigned long suspended_jiffies ;
502 unsigned long accounting_timestamp ;
503 ktime_t suspend_time ;
504 s64 max_time_suspended_ns ;
505 struct dev_pm_qos_request *pq_req ;
506 struct pm_subsys_data *subsys_data ;
507 struct pm_qos_constraints *constraints ;
508};
509#line 558 "include/linux/pm.h"
510struct dev_pm_domain {
511 struct dev_pm_ops ops ;
512};
513#line 18 "include/asm-generic/pci_iomap.h"
514struct vm_area_struct;
515#line 18
516struct vm_area_struct;
517#line 835 "include/linux/sysctl.h"
518struct rb_node {
519 unsigned long rb_parent_color ;
520 struct rb_node *rb_right ;
521 struct rb_node *rb_left ;
522};
523#line 108 "include/linux/rbtree.h"
524struct rb_root {
525 struct rb_node *rb_node ;
526};
527#line 37 "include/linux/kmod.h"
528struct cred;
529#line 37
530struct cred;
531#line 18 "include/linux/elf.h"
532typedef __u64 Elf64_Addr;
533#line 19 "include/linux/elf.h"
534typedef __u16 Elf64_Half;
535#line 23 "include/linux/elf.h"
536typedef __u32 Elf64_Word;
537#line 24 "include/linux/elf.h"
538typedef __u64 Elf64_Xword;
539#line 193 "include/linux/elf.h"
540struct elf64_sym {
541 Elf64_Word st_name ;
542 unsigned char st_info ;
543 unsigned char st_other ;
544 Elf64_Half st_shndx ;
545 Elf64_Addr st_value ;
546 Elf64_Xword st_size ;
547};
548#line 201 "include/linux/elf.h"
549typedef struct elf64_sym Elf64_Sym;
550#line 445
551struct sock;
552#line 445
553struct sock;
554#line 446
555struct kobject;
556#line 446
557struct kobject;
558#line 447
559enum kobj_ns_type {
560 KOBJ_NS_TYPE_NONE = 0,
561 KOBJ_NS_TYPE_NET = 1,
562 KOBJ_NS_TYPES = 2
563} ;
564#line 453 "include/linux/elf.h"
565struct kobj_ns_type_operations {
566 enum kobj_ns_type type ;
567 void *(*grab_current_ns)(void) ;
568 void const *(*netlink_ns)(struct sock * ) ;
569 void const *(*initial_ns)(void) ;
570 void (*drop_ns)(void * ) ;
571};
572#line 57 "include/linux/kobject_ns.h"
573struct attribute {
574 char const *name ;
575 umode_t mode ;
576 struct lock_class_key *key ;
577 struct lock_class_key skey ;
578};
579#line 33 "include/linux/sysfs.h"
580struct attribute_group {
581 char const *name ;
582 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
583 struct attribute **attrs ;
584};
585#line 62 "include/linux/sysfs.h"
586struct bin_attribute {
587 struct attribute attr ;
588 size_t size ;
589 void *private ;
590 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
591 loff_t , size_t ) ;
592 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
593 loff_t , size_t ) ;
594 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
595};
596#line 98 "include/linux/sysfs.h"
597struct sysfs_ops {
598 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
599 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
600 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
601};
602#line 117
603struct sysfs_dirent;
604#line 117
605struct sysfs_dirent;
606#line 182 "include/linux/sysfs.h"
607struct kref {
608 atomic_t refcount ;
609};
610#line 49 "include/linux/kobject.h"
611struct kset;
612#line 49
613struct kobj_type;
614#line 49 "include/linux/kobject.h"
615struct kobject {
616 char const *name ;
617 struct list_head entry ;
618 struct kobject *parent ;
619 struct kset *kset ;
620 struct kobj_type *ktype ;
621 struct sysfs_dirent *sd ;
622 struct kref kref ;
623 unsigned char state_initialized : 1 ;
624 unsigned char state_in_sysfs : 1 ;
625 unsigned char state_add_uevent_sent : 1 ;
626 unsigned char state_remove_uevent_sent : 1 ;
627 unsigned char uevent_suppress : 1 ;
628};
629#line 107 "include/linux/kobject.h"
630struct kobj_type {
631 void (*release)(struct kobject * ) ;
632 struct sysfs_ops const *sysfs_ops ;
633 struct attribute **default_attrs ;
634 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
635 void const *(*namespace)(struct kobject * ) ;
636};
637#line 115 "include/linux/kobject.h"
638struct kobj_uevent_env {
639 char *envp[32U] ;
640 int envp_idx ;
641 char buf[2048U] ;
642 int buflen ;
643};
644#line 122 "include/linux/kobject.h"
645struct kset_uevent_ops {
646 int (* const filter)(struct kset * , struct kobject * ) ;
647 char const *(* const name)(struct kset * , struct kobject * ) ;
648 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
649};
650#line 139 "include/linux/kobject.h"
651struct kset {
652 struct list_head list ;
653 spinlock_t list_lock ;
654 struct kobject kobj ;
655 struct kset_uevent_ops const *uevent_ops ;
656};
657#line 215
658struct kernel_param;
659#line 215
660struct kernel_param;
661#line 216 "include/linux/kobject.h"
662struct kernel_param_ops {
663 int (*set)(char const * , struct kernel_param const * ) ;
664 int (*get)(char * , struct kernel_param const * ) ;
665 void (*free)(void * ) ;
666};
667#line 49 "include/linux/moduleparam.h"
668struct kparam_string;
669#line 49
670struct kparam_array;
671#line 49 "include/linux/moduleparam.h"
672union __anonunion_ldv_13363_134 {
673 void *arg ;
674 struct kparam_string const *str ;
675 struct kparam_array const *arr ;
676};
677#line 49 "include/linux/moduleparam.h"
678struct kernel_param {
679 char const *name ;
680 struct kernel_param_ops const *ops ;
681 u16 perm ;
682 s16 level ;
683 union __anonunion_ldv_13363_134 ldv_13363 ;
684};
685#line 61 "include/linux/moduleparam.h"
686struct kparam_string {
687 unsigned int maxlen ;
688 char *string ;
689};
690#line 67 "include/linux/moduleparam.h"
691struct kparam_array {
692 unsigned int max ;
693 unsigned int elemsize ;
694 unsigned int *num ;
695 struct kernel_param_ops const *ops ;
696 void *elem ;
697};
698#line 458 "include/linux/moduleparam.h"
699struct static_key {
700 atomic_t enabled ;
701};
702#line 225 "include/linux/jump_label.h"
703struct tracepoint;
704#line 225
705struct tracepoint;
706#line 226 "include/linux/jump_label.h"
707struct tracepoint_func {
708 void *func ;
709 void *data ;
710};
711#line 29 "include/linux/tracepoint.h"
712struct tracepoint {
713 char const *name ;
714 struct static_key key ;
715 void (*regfunc)(void) ;
716 void (*unregfunc)(void) ;
717 struct tracepoint_func *funcs ;
718};
719#line 86 "include/linux/tracepoint.h"
720struct kernel_symbol {
721 unsigned long value ;
722 char const *name ;
723};
724#line 27 "include/linux/export.h"
725struct mod_arch_specific {
726
727};
728#line 34 "include/linux/module.h"
729struct module_param_attrs;
730#line 34 "include/linux/module.h"
731struct module_kobject {
732 struct kobject kobj ;
733 struct module *mod ;
734 struct kobject *drivers_dir ;
735 struct module_param_attrs *mp ;
736};
737#line 43 "include/linux/module.h"
738struct module_attribute {
739 struct attribute attr ;
740 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
741 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
742 size_t ) ;
743 void (*setup)(struct module * , char const * ) ;
744 int (*test)(struct module * ) ;
745 void (*free)(struct module * ) ;
746};
747#line 69
748struct exception_table_entry;
749#line 69
750struct exception_table_entry;
751#line 198
752enum module_state {
753 MODULE_STATE_LIVE = 0,
754 MODULE_STATE_COMING = 1,
755 MODULE_STATE_GOING = 2
756} ;
757#line 204 "include/linux/module.h"
758struct module_ref {
759 unsigned long incs ;
760 unsigned long decs ;
761};
762#line 219
763struct module_sect_attrs;
764#line 219
765struct module_notes_attrs;
766#line 219
767struct ftrace_event_call;
768#line 219 "include/linux/module.h"
769struct module {
770 enum module_state state ;
771 struct list_head list ;
772 char name[56U] ;
773 struct module_kobject mkobj ;
774 struct module_attribute *modinfo_attrs ;
775 char const *version ;
776 char const *srcversion ;
777 struct kobject *holders_dir ;
778 struct kernel_symbol const *syms ;
779 unsigned long const *crcs ;
780 unsigned int num_syms ;
781 struct kernel_param *kp ;
782 unsigned int num_kp ;
783 unsigned int num_gpl_syms ;
784 struct kernel_symbol const *gpl_syms ;
785 unsigned long const *gpl_crcs ;
786 struct kernel_symbol const *unused_syms ;
787 unsigned long const *unused_crcs ;
788 unsigned int num_unused_syms ;
789 unsigned int num_unused_gpl_syms ;
790 struct kernel_symbol const *unused_gpl_syms ;
791 unsigned long const *unused_gpl_crcs ;
792 struct kernel_symbol const *gpl_future_syms ;
793 unsigned long const *gpl_future_crcs ;
794 unsigned int num_gpl_future_syms ;
795 unsigned int num_exentries ;
796 struct exception_table_entry *extable ;
797 int (*init)(void) ;
798 void *module_init ;
799 void *module_core ;
800 unsigned int init_size ;
801 unsigned int core_size ;
802 unsigned int init_text_size ;
803 unsigned int core_text_size ;
804 unsigned int init_ro_size ;
805 unsigned int core_ro_size ;
806 struct mod_arch_specific arch ;
807 unsigned int taints ;
808 unsigned int num_bugs ;
809 struct list_head bug_list ;
810 struct bug_entry *bug_table ;
811 Elf64_Sym *symtab ;
812 Elf64_Sym *core_symtab ;
813 unsigned int num_symtab ;
814 unsigned int core_num_syms ;
815 char *strtab ;
816 char *core_strtab ;
817 struct module_sect_attrs *sect_attrs ;
818 struct module_notes_attrs *notes_attrs ;
819 char *args ;
820 void *percpu ;
821 unsigned int percpu_size ;
822 unsigned int num_tracepoints ;
823 struct tracepoint * const *tracepoints_ptrs ;
824 unsigned int num_trace_bprintk_fmt ;
825 char const **trace_bprintk_fmt_start ;
826 struct ftrace_event_call **trace_events ;
827 unsigned int num_trace_events ;
828 struct list_head source_list ;
829 struct list_head target_list ;
830 struct task_struct *waiter ;
831 void (*exit)(void) ;
832 struct module_ref *refptr ;
833 ctor_fn_t (**ctors)(void) ;
834 unsigned int num_ctors ;
835};
836#line 88 "include/linux/kmemleak.h"
837struct kmem_cache_cpu {
838 void **freelist ;
839 unsigned long tid ;
840 struct page *page ;
841 struct page *partial ;
842 int node ;
843 unsigned int stat[26U] ;
844};
845#line 55 "include/linux/slub_def.h"
846struct kmem_cache_node {
847 spinlock_t list_lock ;
848 unsigned long nr_partial ;
849 struct list_head partial ;
850 atomic_long_t nr_slabs ;
851 atomic_long_t total_objects ;
852 struct list_head full ;
853};
854#line 66 "include/linux/slub_def.h"
855struct kmem_cache_order_objects {
856 unsigned long x ;
857};
858#line 76 "include/linux/slub_def.h"
859struct kmem_cache {
860 struct kmem_cache_cpu *cpu_slab ;
861 unsigned long flags ;
862 unsigned long min_partial ;
863 int size ;
864 int objsize ;
865 int offset ;
866 int cpu_partial ;
867 struct kmem_cache_order_objects oo ;
868 struct kmem_cache_order_objects max ;
869 struct kmem_cache_order_objects min ;
870 gfp_t allocflags ;
871 int refcount ;
872 void (*ctor)(void * ) ;
873 int inuse ;
874 int align ;
875 int reserved ;
876 char const *name ;
877 struct list_head list ;
878 struct kobject kobj ;
879 int remote_node_defrag_ratio ;
880 struct kmem_cache_node *node[1024U] ;
881};
882#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
883struct rtc_time {
884 int tm_sec ;
885 int tm_min ;
886 int tm_hour ;
887 int tm_mday ;
888 int tm_mon ;
889 int tm_year ;
890 int tm_wday ;
891 int tm_yday ;
892 int tm_isdst ;
893};
894#line 31 "include/linux/rtc.h"
895struct rtc_wkalrm {
896 unsigned char enabled ;
897 unsigned char pending ;
898 struct rtc_time time ;
899};
900#line 64
901enum irqreturn {
902 IRQ_NONE = 0,
903 IRQ_HANDLED = 1,
904 IRQ_WAKE_THREAD = 2
905} ;
906#line 16 "include/linux/irqreturn.h"
907typedef enum irqreturn irqreturn_t;
908#line 41 "include/asm-generic/sections.h"
909struct exception_table_entry {
910 unsigned long insn ;
911 unsigned long fixup ;
912};
913#line 189 "include/linux/hardirq.h"
914struct timerqueue_node {
915 struct rb_node node ;
916 ktime_t expires ;
917};
918#line 12 "include/linux/timerqueue.h"
919struct timerqueue_head {
920 struct rb_root head ;
921 struct timerqueue_node *next ;
922};
923#line 50
924struct hrtimer_clock_base;
925#line 50
926struct hrtimer_clock_base;
927#line 51
928struct hrtimer_cpu_base;
929#line 51
930struct hrtimer_cpu_base;
931#line 60
932enum hrtimer_restart {
933 HRTIMER_NORESTART = 0,
934 HRTIMER_RESTART = 1
935} ;
936#line 65 "include/linux/timerqueue.h"
937struct hrtimer {
938 struct timerqueue_node node ;
939 ktime_t _softexpires ;
940 enum hrtimer_restart (*function)(struct hrtimer * ) ;
941 struct hrtimer_clock_base *base ;
942 unsigned long state ;
943 int start_pid ;
944 void *start_site ;
945 char start_comm[16U] ;
946};
947#line 132 "include/linux/hrtimer.h"
948struct hrtimer_clock_base {
949 struct hrtimer_cpu_base *cpu_base ;
950 int index ;
951 clockid_t clockid ;
952 struct timerqueue_head active ;
953 ktime_t resolution ;
954 ktime_t (*get_time)(void) ;
955 ktime_t softirq_time ;
956 ktime_t offset ;
957};
958#line 162 "include/linux/hrtimer.h"
959struct hrtimer_cpu_base {
960 raw_spinlock_t lock ;
961 unsigned long active_bases ;
962 ktime_t expires_next ;
963 int hres_active ;
964 int hang_detected ;
965 unsigned long nr_events ;
966 unsigned long nr_retries ;
967 unsigned long nr_hangs ;
968 ktime_t max_hang_time ;
969 struct hrtimer_clock_base clock_base[3U] ;
970};
971#line 115 "include/linux/rtc.h"
972struct klist_node;
973#line 115
974struct klist_node;
975#line 37 "include/linux/klist.h"
976struct klist_node {
977 void *n_klist ;
978 struct list_head n_node ;
979 struct kref n_ref ;
980};
981#line 67
982struct dma_map_ops;
983#line 67 "include/linux/klist.h"
984struct dev_archdata {
985 void *acpi_handle ;
986 struct dma_map_ops *dma_ops ;
987 void *iommu ;
988};
989#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
990struct pdev_archdata {
991
992};
993#line 17
994struct device_private;
995#line 17
996struct device_private;
997#line 18
998struct device_driver;
999#line 18
1000struct device_driver;
1001#line 19
1002struct driver_private;
1003#line 19
1004struct driver_private;
1005#line 20
1006struct class;
1007#line 20
1008struct class;
1009#line 21
1010struct subsys_private;
1011#line 21
1012struct subsys_private;
1013#line 22
1014struct bus_type;
1015#line 22
1016struct bus_type;
1017#line 23
1018struct device_node;
1019#line 23
1020struct device_node;
1021#line 24
1022struct iommu_ops;
1023#line 24
1024struct iommu_ops;
1025#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1026struct bus_attribute {
1027 struct attribute attr ;
1028 ssize_t (*show)(struct bus_type * , char * ) ;
1029 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
1030};
1031#line 51 "include/linux/device.h"
1032struct device_attribute;
1033#line 51
1034struct driver_attribute;
1035#line 51 "include/linux/device.h"
1036struct bus_type {
1037 char const *name ;
1038 char const *dev_name ;
1039 struct device *dev_root ;
1040 struct bus_attribute *bus_attrs ;
1041 struct device_attribute *dev_attrs ;
1042 struct driver_attribute *drv_attrs ;
1043 int (*match)(struct device * , struct device_driver * ) ;
1044 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1045 int (*probe)(struct device * ) ;
1046 int (*remove)(struct device * ) ;
1047 void (*shutdown)(struct device * ) ;
1048 int (*suspend)(struct device * , pm_message_t ) ;
1049 int (*resume)(struct device * ) ;
1050 struct dev_pm_ops const *pm ;
1051 struct iommu_ops *iommu_ops ;
1052 struct subsys_private *p ;
1053};
1054#line 125
1055struct device_type;
1056#line 182
1057struct of_device_id;
1058#line 182 "include/linux/device.h"
1059struct device_driver {
1060 char const *name ;
1061 struct bus_type *bus ;
1062 struct module *owner ;
1063 char const *mod_name ;
1064 bool suppress_bind_attrs ;
1065 struct of_device_id const *of_match_table ;
1066 int (*probe)(struct device * ) ;
1067 int (*remove)(struct device * ) ;
1068 void (*shutdown)(struct device * ) ;
1069 int (*suspend)(struct device * , pm_message_t ) ;
1070 int (*resume)(struct device * ) ;
1071 struct attribute_group const **groups ;
1072 struct dev_pm_ops const *pm ;
1073 struct driver_private *p ;
1074};
1075#line 245 "include/linux/device.h"
1076struct driver_attribute {
1077 struct attribute attr ;
1078 ssize_t (*show)(struct device_driver * , char * ) ;
1079 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
1080};
1081#line 299
1082struct class_attribute;
1083#line 299 "include/linux/device.h"
1084struct class {
1085 char const *name ;
1086 struct module *owner ;
1087 struct class_attribute *class_attrs ;
1088 struct device_attribute *dev_attrs ;
1089 struct bin_attribute *dev_bin_attrs ;
1090 struct kobject *dev_kobj ;
1091 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
1092 char *(*devnode)(struct device * , umode_t * ) ;
1093 void (*class_release)(struct class * ) ;
1094 void (*dev_release)(struct device * ) ;
1095 int (*suspend)(struct device * , pm_message_t ) ;
1096 int (*resume)(struct device * ) ;
1097 struct kobj_ns_type_operations const *ns_type ;
1098 void const *(*namespace)(struct device * ) ;
1099 struct dev_pm_ops const *pm ;
1100 struct subsys_private *p ;
1101};
1102#line 394 "include/linux/device.h"
1103struct class_attribute {
1104 struct attribute attr ;
1105 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
1106 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
1107 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
1108};
1109#line 447 "include/linux/device.h"
1110struct device_type {
1111 char const *name ;
1112 struct attribute_group const **groups ;
1113 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1114 char *(*devnode)(struct device * , umode_t * ) ;
1115 void (*release)(struct device * ) ;
1116 struct dev_pm_ops const *pm ;
1117};
1118#line 474 "include/linux/device.h"
1119struct device_attribute {
1120 struct attribute attr ;
1121 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
1122 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
1123 size_t ) ;
1124};
1125#line 557 "include/linux/device.h"
1126struct device_dma_parameters {
1127 unsigned int max_segment_size ;
1128 unsigned long segment_boundary_mask ;
1129};
1130#line 567
1131struct dma_coherent_mem;
1132#line 567 "include/linux/device.h"
1133struct device {
1134 struct device *parent ;
1135 struct device_private *p ;
1136 struct kobject kobj ;
1137 char const *init_name ;
1138 struct device_type const *type ;
1139 struct mutex mutex ;
1140 struct bus_type *bus ;
1141 struct device_driver *driver ;
1142 void *platform_data ;
1143 struct dev_pm_info power ;
1144 struct dev_pm_domain *pm_domain ;
1145 int numa_node ;
1146 u64 *dma_mask ;
1147 u64 coherent_dma_mask ;
1148 struct device_dma_parameters *dma_parms ;
1149 struct list_head dma_pools ;
1150 struct dma_coherent_mem *dma_mem ;
1151 struct dev_archdata archdata ;
1152 struct device_node *of_node ;
1153 dev_t devt ;
1154 u32 id ;
1155 spinlock_t devres_lock ;
1156 struct list_head devres_head ;
1157 struct klist_node knode_class ;
1158 struct class *class ;
1159 struct attribute_group const **groups ;
1160 void (*release)(struct device * ) ;
1161};
1162#line 681 "include/linux/device.h"
1163struct wakeup_source {
1164 char const *name ;
1165 struct list_head entry ;
1166 spinlock_t lock ;
1167 struct timer_list timer ;
1168 unsigned long timer_expires ;
1169 ktime_t total_time ;
1170 ktime_t max_time ;
1171 ktime_t last_time ;
1172 unsigned long event_count ;
1173 unsigned long active_count ;
1174 unsigned long relax_count ;
1175 unsigned long hit_count ;
1176 unsigned char active : 1 ;
1177};
1178#line 991
1179struct path;
1180#line 991
1181struct path;
1182#line 992
1183struct inode;
1184#line 992
1185struct inode;
1186#line 993
1187struct dentry;
1188#line 993
1189struct dentry;
1190#line 994 "include/linux/device.h"
1191struct seq_file {
1192 char *buf ;
1193 size_t size ;
1194 size_t from ;
1195 size_t count ;
1196 loff_t index ;
1197 loff_t read_pos ;
1198 u64 version ;
1199 struct mutex lock ;
1200 struct seq_operations const *op ;
1201 int poll_event ;
1202 void *private ;
1203};
1204#line 30 "include/linux/seq_file.h"
1205struct seq_operations {
1206 void *(*start)(struct seq_file * , loff_t * ) ;
1207 void (*stop)(struct seq_file * , void * ) ;
1208 void *(*next)(struct seq_file * , void * , loff_t * ) ;
1209 int (*show)(struct seq_file * , void * ) ;
1210};
1211#line 89 "include/linux/kdev_t.h"
1212struct file_operations;
1213#line 89
1214struct file_operations;
1215#line 90 "include/linux/kdev_t.h"
1216struct cdev {
1217 struct kobject kobj ;
1218 struct module *owner ;
1219 struct file_operations const *ops ;
1220 struct list_head list ;
1221 dev_t dev ;
1222 unsigned int count ;
1223};
1224#line 33 "include/linux/cdev.h"
1225struct backing_dev_info;
1226#line 41 "include/asm-generic/poll.h"
1227struct block_device;
1228#line 41
1229struct block_device;
1230#line 93 "include/linux/bit_spinlock.h"
1231struct hlist_bl_node;
1232#line 93 "include/linux/bit_spinlock.h"
1233struct hlist_bl_head {
1234 struct hlist_bl_node *first ;
1235};
1236#line 36 "include/linux/list_bl.h"
1237struct hlist_bl_node {
1238 struct hlist_bl_node *next ;
1239 struct hlist_bl_node **pprev ;
1240};
1241#line 114 "include/linux/rculist_bl.h"
1242struct nameidata;
1243#line 114
1244struct nameidata;
1245#line 115
1246struct vfsmount;
1247#line 115
1248struct vfsmount;
1249#line 116 "include/linux/rculist_bl.h"
1250struct qstr {
1251 unsigned int hash ;
1252 unsigned int len ;
1253 unsigned char const *name ;
1254};
1255#line 72 "include/linux/dcache.h"
1256struct dentry_operations;
1257#line 72
1258struct super_block;
1259#line 72 "include/linux/dcache.h"
1260union __anonunion_d_u_136 {
1261 struct list_head d_child ;
1262 struct rcu_head d_rcu ;
1263};
1264#line 72 "include/linux/dcache.h"
1265struct dentry {
1266 unsigned int d_flags ;
1267 seqcount_t d_seq ;
1268 struct hlist_bl_node d_hash ;
1269 struct dentry *d_parent ;
1270 struct qstr d_name ;
1271 struct inode *d_inode ;
1272 unsigned char d_iname[32U] ;
1273 unsigned int d_count ;
1274 spinlock_t d_lock ;
1275 struct dentry_operations const *d_op ;
1276 struct super_block *d_sb ;
1277 unsigned long d_time ;
1278 void *d_fsdata ;
1279 struct list_head d_lru ;
1280 union __anonunion_d_u_136 d_u ;
1281 struct list_head d_subdirs ;
1282 struct list_head d_alias ;
1283};
1284#line 123 "include/linux/dcache.h"
1285struct dentry_operations {
1286 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1287 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
1288 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
1289 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
1290 int (*d_delete)(struct dentry const * ) ;
1291 void (*d_release)(struct dentry * ) ;
1292 void (*d_prune)(struct dentry * ) ;
1293 void (*d_iput)(struct dentry * , struct inode * ) ;
1294 char *(*d_dname)(struct dentry * , char * , int ) ;
1295 struct vfsmount *(*d_automount)(struct path * ) ;
1296 int (*d_manage)(struct dentry * , bool ) ;
1297};
1298#line 402 "include/linux/dcache.h"
1299struct path {
1300 struct vfsmount *mnt ;
1301 struct dentry *dentry ;
1302};
1303#line 58 "include/linux/radix-tree.h"
1304struct radix_tree_node;
1305#line 58 "include/linux/radix-tree.h"
1306struct radix_tree_root {
1307 unsigned int height ;
1308 gfp_t gfp_mask ;
1309 struct radix_tree_node *rnode ;
1310};
1311#line 377
1312struct prio_tree_node;
1313#line 19 "include/linux/prio_tree.h"
1314struct prio_tree_node {
1315 struct prio_tree_node *left ;
1316 struct prio_tree_node *right ;
1317 struct prio_tree_node *parent ;
1318 unsigned long start ;
1319 unsigned long last ;
1320};
1321#line 27 "include/linux/prio_tree.h"
1322struct prio_tree_root {
1323 struct prio_tree_node *prio_tree_node ;
1324 unsigned short index_bits ;
1325 unsigned short raw ;
1326};
1327#line 111
1328enum pid_type {
1329 PIDTYPE_PID = 0,
1330 PIDTYPE_PGID = 1,
1331 PIDTYPE_SID = 2,
1332 PIDTYPE_MAX = 3
1333} ;
1334#line 118
1335struct pid_namespace;
1336#line 118 "include/linux/prio_tree.h"
1337struct upid {
1338 int nr ;
1339 struct pid_namespace *ns ;
1340 struct hlist_node pid_chain ;
1341};
1342#line 56 "include/linux/pid.h"
1343struct pid {
1344 atomic_t count ;
1345 unsigned int level ;
1346 struct hlist_head tasks[3U] ;
1347 struct rcu_head rcu ;
1348 struct upid numbers[1U] ;
1349};
1350#line 45 "include/linux/semaphore.h"
1351struct fiemap_extent {
1352 __u64 fe_logical ;
1353 __u64 fe_physical ;
1354 __u64 fe_length ;
1355 __u64 fe_reserved64[2U] ;
1356 __u32 fe_flags ;
1357 __u32 fe_reserved[3U] ;
1358};
1359#line 38 "include/linux/fiemap.h"
1360struct shrink_control {
1361 gfp_t gfp_mask ;
1362 unsigned long nr_to_scan ;
1363};
1364#line 14 "include/linux/shrinker.h"
1365struct shrinker {
1366 int (*shrink)(struct shrinker * , struct shrink_control * ) ;
1367 int seeks ;
1368 long batch ;
1369 struct list_head list ;
1370 atomic_long_t nr_in_batch ;
1371};
1372#line 43
1373enum migrate_mode {
1374 MIGRATE_ASYNC = 0,
1375 MIGRATE_SYNC_LIGHT = 1,
1376 MIGRATE_SYNC = 2
1377} ;
1378#line 49
1379struct export_operations;
1380#line 49
1381struct export_operations;
1382#line 51
1383struct iovec;
1384#line 51
1385struct iovec;
1386#line 52
1387struct kiocb;
1388#line 52
1389struct kiocb;
1390#line 53
1391struct pipe_inode_info;
1392#line 53
1393struct pipe_inode_info;
1394#line 54
1395struct poll_table_struct;
1396#line 54
1397struct poll_table_struct;
1398#line 55
1399struct kstatfs;
1400#line 55
1401struct kstatfs;
1402#line 435 "include/linux/fs.h"
1403struct iattr {
1404 unsigned int ia_valid ;
1405 umode_t ia_mode ;
1406 uid_t ia_uid ;
1407 gid_t ia_gid ;
1408 loff_t ia_size ;
1409 struct timespec ia_atime ;
1410 struct timespec ia_mtime ;
1411 struct timespec ia_ctime ;
1412 struct file *ia_file ;
1413};
1414#line 119 "include/linux/quota.h"
1415struct if_dqinfo {
1416 __u64 dqi_bgrace ;
1417 __u64 dqi_igrace ;
1418 __u32 dqi_flags ;
1419 __u32 dqi_valid ;
1420};
1421#line 176 "include/linux/percpu_counter.h"
1422struct fs_disk_quota {
1423 __s8 d_version ;
1424 __s8 d_flags ;
1425 __u16 d_fieldmask ;
1426 __u32 d_id ;
1427 __u64 d_blk_hardlimit ;
1428 __u64 d_blk_softlimit ;
1429 __u64 d_ino_hardlimit ;
1430 __u64 d_ino_softlimit ;
1431 __u64 d_bcount ;
1432 __u64 d_icount ;
1433 __s32 d_itimer ;
1434 __s32 d_btimer ;
1435 __u16 d_iwarns ;
1436 __u16 d_bwarns ;
1437 __s32 d_padding2 ;
1438 __u64 d_rtb_hardlimit ;
1439 __u64 d_rtb_softlimit ;
1440 __u64 d_rtbcount ;
1441 __s32 d_rtbtimer ;
1442 __u16 d_rtbwarns ;
1443 __s16 d_padding3 ;
1444 char d_padding4[8U] ;
1445};
1446#line 75 "include/linux/dqblk_xfs.h"
1447struct fs_qfilestat {
1448 __u64 qfs_ino ;
1449 __u64 qfs_nblks ;
1450 __u32 qfs_nextents ;
1451};
1452#line 150 "include/linux/dqblk_xfs.h"
1453typedef struct fs_qfilestat fs_qfilestat_t;
1454#line 151 "include/linux/dqblk_xfs.h"
1455struct fs_quota_stat {
1456 __s8 qs_version ;
1457 __u16 qs_flags ;
1458 __s8 qs_pad ;
1459 fs_qfilestat_t qs_uquota ;
1460 fs_qfilestat_t qs_gquota ;
1461 __u32 qs_incoredqs ;
1462 __s32 qs_btimelimit ;
1463 __s32 qs_itimelimit ;
1464 __s32 qs_rtbtimelimit ;
1465 __u16 qs_bwarnlimit ;
1466 __u16 qs_iwarnlimit ;
1467};
1468#line 165
1469struct dquot;
1470#line 165
1471struct dquot;
1472#line 185 "include/linux/quota.h"
1473typedef __kernel_uid32_t qid_t;
1474#line 186 "include/linux/quota.h"
1475typedef long long qsize_t;
1476#line 189 "include/linux/quota.h"
1477struct mem_dqblk {
1478 qsize_t dqb_bhardlimit ;
1479 qsize_t dqb_bsoftlimit ;
1480 qsize_t dqb_curspace ;
1481 qsize_t dqb_rsvspace ;
1482 qsize_t dqb_ihardlimit ;
1483 qsize_t dqb_isoftlimit ;
1484 qsize_t dqb_curinodes ;
1485 time_t dqb_btime ;
1486 time_t dqb_itime ;
1487};
1488#line 211
1489struct quota_format_type;
1490#line 211
1491struct quota_format_type;
1492#line 212 "include/linux/quota.h"
1493struct mem_dqinfo {
1494 struct quota_format_type *dqi_format ;
1495 int dqi_fmt_id ;
1496 struct list_head dqi_dirty_list ;
1497 unsigned long dqi_flags ;
1498 unsigned int dqi_bgrace ;
1499 unsigned int dqi_igrace ;
1500 qsize_t dqi_maxblimit ;
1501 qsize_t dqi_maxilimit ;
1502 void *dqi_priv ;
1503};
1504#line 275 "include/linux/quota.h"
1505struct dquot {
1506 struct hlist_node dq_hash ;
1507 struct list_head dq_inuse ;
1508 struct list_head dq_free ;
1509 struct list_head dq_dirty ;
1510 struct mutex dq_lock ;
1511 atomic_t dq_count ;
1512 wait_queue_head_t dq_wait_unused ;
1513 struct super_block *dq_sb ;
1514 unsigned int dq_id ;
1515 loff_t dq_off ;
1516 unsigned long dq_flags ;
1517 short dq_type ;
1518 struct mem_dqblk dq_dqb ;
1519};
1520#line 303 "include/linux/quota.h"
1521struct quota_format_ops {
1522 int (*check_quota_file)(struct super_block * , int ) ;
1523 int (*read_file_info)(struct super_block * , int ) ;
1524 int (*write_file_info)(struct super_block * , int ) ;
1525 int (*free_file_info)(struct super_block * , int ) ;
1526 int (*read_dqblk)(struct dquot * ) ;
1527 int (*commit_dqblk)(struct dquot * ) ;
1528 int (*release_dqblk)(struct dquot * ) ;
1529};
1530#line 314 "include/linux/quota.h"
1531struct dquot_operations {
1532 int (*write_dquot)(struct dquot * ) ;
1533 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
1534 void (*destroy_dquot)(struct dquot * ) ;
1535 int (*acquire_dquot)(struct dquot * ) ;
1536 int (*release_dquot)(struct dquot * ) ;
1537 int (*mark_dirty)(struct dquot * ) ;
1538 int (*write_info)(struct super_block * , int ) ;
1539 qsize_t *(*get_reserved_space)(struct inode * ) ;
1540};
1541#line 328 "include/linux/quota.h"
1542struct quotactl_ops {
1543 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
1544 int (*quota_on_meta)(struct super_block * , int , int ) ;
1545 int (*quota_off)(struct super_block * , int ) ;
1546 int (*quota_sync)(struct super_block * , int , int ) ;
1547 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
1548 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
1549 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1550 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1551 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1552 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
1553};
1554#line 344 "include/linux/quota.h"
1555struct quota_format_type {
1556 int qf_fmt_id ;
1557 struct quota_format_ops const *qf_ops ;
1558 struct module *qf_owner ;
1559 struct quota_format_type *qf_next ;
1560};
1561#line 390 "include/linux/quota.h"
1562struct quota_info {
1563 unsigned int flags ;
1564 struct mutex dqio_mutex ;
1565 struct mutex dqonoff_mutex ;
1566 struct rw_semaphore dqptr_sem ;
1567 struct inode *files[2U] ;
1568 struct mem_dqinfo info[2U] ;
1569 struct quota_format_ops const *ops[2U] ;
1570};
1571#line 421
1572struct address_space;
1573#line 421
1574struct address_space;
1575#line 422
1576struct writeback_control;
1577#line 422
1578struct writeback_control;
1579#line 585 "include/linux/fs.h"
1580union __anonunion_arg_139 {
1581 char *buf ;
1582 void *data ;
1583};
1584#line 585 "include/linux/fs.h"
1585struct __anonstruct_read_descriptor_t_138 {
1586 size_t written ;
1587 size_t count ;
1588 union __anonunion_arg_139 arg ;
1589 int error ;
1590};
1591#line 585 "include/linux/fs.h"
1592typedef struct __anonstruct_read_descriptor_t_138 read_descriptor_t;
1593#line 588 "include/linux/fs.h"
1594struct address_space_operations {
1595 int (*writepage)(struct page * , struct writeback_control * ) ;
1596 int (*readpage)(struct file * , struct page * ) ;
1597 int (*writepages)(struct address_space * , struct writeback_control * ) ;
1598 int (*set_page_dirty)(struct page * ) ;
1599 int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1600 unsigned int ) ;
1601 int (*write_begin)(struct file * , struct address_space * , loff_t , unsigned int ,
1602 unsigned int , struct page ** , void ** ) ;
1603 int (*write_end)(struct file * , struct address_space * , loff_t , unsigned int ,
1604 unsigned int , struct page * , void * ) ;
1605 sector_t (*bmap)(struct address_space * , sector_t ) ;
1606 void (*invalidatepage)(struct page * , unsigned long ) ;
1607 int (*releasepage)(struct page * , gfp_t ) ;
1608 void (*freepage)(struct page * ) ;
1609 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const * , loff_t ,
1610 unsigned long ) ;
1611 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
1612 int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode ) ;
1613 int (*launder_page)(struct page * ) ;
1614 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
1615 int (*error_remove_page)(struct address_space * , struct page * ) ;
1616};
1617#line 642 "include/linux/fs.h"
1618struct address_space {
1619 struct inode *host ;
1620 struct radix_tree_root page_tree ;
1621 spinlock_t tree_lock ;
1622 unsigned int i_mmap_writable ;
1623 struct prio_tree_root i_mmap ;
1624 struct list_head i_mmap_nonlinear ;
1625 struct mutex i_mmap_mutex ;
1626 unsigned long nrpages ;
1627 unsigned long writeback_index ;
1628 struct address_space_operations const *a_ops ;
1629 unsigned long flags ;
1630 struct backing_dev_info *backing_dev_info ;
1631 spinlock_t private_lock ;
1632 struct list_head private_list ;
1633 struct address_space *assoc_mapping ;
1634};
1635#line 664
1636struct request_queue;
1637#line 664
1638struct request_queue;
1639#line 665
1640struct hd_struct;
1641#line 665
1642struct gendisk;
1643#line 665 "include/linux/fs.h"
1644struct block_device {
1645 dev_t bd_dev ;
1646 int bd_openers ;
1647 struct inode *bd_inode ;
1648 struct super_block *bd_super ;
1649 struct mutex bd_mutex ;
1650 struct list_head bd_inodes ;
1651 void *bd_claiming ;
1652 void *bd_holder ;
1653 int bd_holders ;
1654 bool bd_write_holder ;
1655 struct list_head bd_holder_disks ;
1656 struct block_device *bd_contains ;
1657 unsigned int bd_block_size ;
1658 struct hd_struct *bd_part ;
1659 unsigned int bd_part_count ;
1660 int bd_invalidated ;
1661 struct gendisk *bd_disk ;
1662 struct request_queue *bd_queue ;
1663 struct list_head bd_list ;
1664 unsigned long bd_private ;
1665 int bd_fsfreeze_count ;
1666 struct mutex bd_fsfreeze_mutex ;
1667};
1668#line 737
1669struct posix_acl;
1670#line 737
1671struct posix_acl;
1672#line 738
1673struct inode_operations;
1674#line 738 "include/linux/fs.h"
1675union __anonunion_ldv_18339_140 {
1676 unsigned int const i_nlink ;
1677 unsigned int __i_nlink ;
1678};
1679#line 738 "include/linux/fs.h"
1680union __anonunion_ldv_18358_141 {
1681 struct list_head i_dentry ;
1682 struct rcu_head i_rcu ;
1683};
1684#line 738
1685struct file_lock;
1686#line 738 "include/linux/fs.h"
1687union __anonunion_ldv_18374_142 {
1688 struct pipe_inode_info *i_pipe ;
1689 struct block_device *i_bdev ;
1690 struct cdev *i_cdev ;
1691};
1692#line 738 "include/linux/fs.h"
1693struct inode {
1694 umode_t i_mode ;
1695 unsigned short i_opflags ;
1696 uid_t i_uid ;
1697 gid_t i_gid ;
1698 unsigned int i_flags ;
1699 struct posix_acl *i_acl ;
1700 struct posix_acl *i_default_acl ;
1701 struct inode_operations const *i_op ;
1702 struct super_block *i_sb ;
1703 struct address_space *i_mapping ;
1704 void *i_security ;
1705 unsigned long i_ino ;
1706 union __anonunion_ldv_18339_140 ldv_18339 ;
1707 dev_t i_rdev ;
1708 struct timespec i_atime ;
1709 struct timespec i_mtime ;
1710 struct timespec i_ctime ;
1711 spinlock_t i_lock ;
1712 unsigned short i_bytes ;
1713 blkcnt_t i_blocks ;
1714 loff_t i_size ;
1715 unsigned long i_state ;
1716 struct mutex i_mutex ;
1717 unsigned long dirtied_when ;
1718 struct hlist_node i_hash ;
1719 struct list_head i_wb_list ;
1720 struct list_head i_lru ;
1721 struct list_head i_sb_list ;
1722 union __anonunion_ldv_18358_141 ldv_18358 ;
1723 atomic_t i_count ;
1724 unsigned int i_blkbits ;
1725 u64 i_version ;
1726 atomic_t i_dio_count ;
1727 atomic_t i_writecount ;
1728 struct file_operations const *i_fop ;
1729 struct file_lock *i_flock ;
1730 struct address_space i_data ;
1731 struct dquot *i_dquot[2U] ;
1732 struct list_head i_devices ;
1733 union __anonunion_ldv_18374_142 ldv_18374 ;
1734 __u32 i_generation ;
1735 __u32 i_fsnotify_mask ;
1736 struct hlist_head i_fsnotify_marks ;
1737 atomic_t i_readcount ;
1738 void *i_private ;
1739};
1740#line 941 "include/linux/fs.h"
1741struct fown_struct {
1742 rwlock_t lock ;
1743 struct pid *pid ;
1744 enum pid_type pid_type ;
1745 uid_t uid ;
1746 uid_t euid ;
1747 int signum ;
1748};
1749#line 949 "include/linux/fs.h"
1750struct file_ra_state {
1751 unsigned long start ;
1752 unsigned int size ;
1753 unsigned int async_size ;
1754 unsigned int ra_pages ;
1755 unsigned int mmap_miss ;
1756 loff_t prev_pos ;
1757};
1758#line 972 "include/linux/fs.h"
1759union __anonunion_f_u_143 {
1760 struct list_head fu_list ;
1761 struct rcu_head fu_rcuhead ;
1762};
1763#line 972 "include/linux/fs.h"
1764struct file {
1765 union __anonunion_f_u_143 f_u ;
1766 struct path f_path ;
1767 struct file_operations const *f_op ;
1768 spinlock_t f_lock ;
1769 int f_sb_list_cpu ;
1770 atomic_long_t f_count ;
1771 unsigned int f_flags ;
1772 fmode_t f_mode ;
1773 loff_t f_pos ;
1774 struct fown_struct f_owner ;
1775 struct cred const *f_cred ;
1776 struct file_ra_state f_ra ;
1777 u64 f_version ;
1778 void *f_security ;
1779 void *private_data ;
1780 struct list_head f_ep_links ;
1781 struct list_head f_tfile_llink ;
1782 struct address_space *f_mapping ;
1783 unsigned long f_mnt_write_state ;
1784};
1785#line 1111
1786struct files_struct;
1787#line 1111 "include/linux/fs.h"
1788typedef struct files_struct *fl_owner_t;
1789#line 1112 "include/linux/fs.h"
1790struct file_lock_operations {
1791 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1792 void (*fl_release_private)(struct file_lock * ) ;
1793};
1794#line 1117 "include/linux/fs.h"
1795struct lock_manager_operations {
1796 int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1797 void (*lm_notify)(struct file_lock * ) ;
1798 int (*lm_grant)(struct file_lock * , struct file_lock * , int ) ;
1799 void (*lm_release_private)(struct file_lock * ) ;
1800 void (*lm_break)(struct file_lock * ) ;
1801 int (*lm_change)(struct file_lock ** , int ) ;
1802};
1803#line 1134
1804struct nlm_lockowner;
1805#line 1134
1806struct nlm_lockowner;
1807#line 1135 "include/linux/fs.h"
1808struct nfs_lock_info {
1809 u32 state ;
1810 struct nlm_lockowner *owner ;
1811 struct list_head list ;
1812};
1813#line 14 "include/linux/nfs_fs_i.h"
1814struct nfs4_lock_state;
1815#line 14
1816struct nfs4_lock_state;
1817#line 15 "include/linux/nfs_fs_i.h"
1818struct nfs4_lock_info {
1819 struct nfs4_lock_state *owner ;
1820};
1821#line 19
1822struct fasync_struct;
1823#line 19 "include/linux/nfs_fs_i.h"
1824struct __anonstruct_afs_145 {
1825 struct list_head link ;
1826 int state ;
1827};
1828#line 19 "include/linux/nfs_fs_i.h"
1829union __anonunion_fl_u_144 {
1830 struct nfs_lock_info nfs_fl ;
1831 struct nfs4_lock_info nfs4_fl ;
1832 struct __anonstruct_afs_145 afs ;
1833};
1834#line 19 "include/linux/nfs_fs_i.h"
1835struct file_lock {
1836 struct file_lock *fl_next ;
1837 struct list_head fl_link ;
1838 struct list_head fl_block ;
1839 fl_owner_t fl_owner ;
1840 unsigned int fl_flags ;
1841 unsigned char fl_type ;
1842 unsigned int fl_pid ;
1843 struct pid *fl_nspid ;
1844 wait_queue_head_t fl_wait ;
1845 struct file *fl_file ;
1846 loff_t fl_start ;
1847 loff_t fl_end ;
1848 struct fasync_struct *fl_fasync ;
1849 unsigned long fl_break_time ;
1850 unsigned long fl_downgrade_time ;
1851 struct file_lock_operations const *fl_ops ;
1852 struct lock_manager_operations const *fl_lmops ;
1853 union __anonunion_fl_u_144 fl_u ;
1854};
1855#line 1221 "include/linux/fs.h"
1856struct fasync_struct {
1857 spinlock_t fa_lock ;
1858 int magic ;
1859 int fa_fd ;
1860 struct fasync_struct *fa_next ;
1861 struct file *fa_file ;
1862 struct rcu_head fa_rcu ;
1863};
1864#line 1417
1865struct file_system_type;
1866#line 1417
1867struct super_operations;
1868#line 1417
1869struct xattr_handler;
1870#line 1417
1871struct mtd_info;
1872#line 1417 "include/linux/fs.h"
1873struct super_block {
1874 struct list_head s_list ;
1875 dev_t s_dev ;
1876 unsigned char s_dirt ;
1877 unsigned char s_blocksize_bits ;
1878 unsigned long s_blocksize ;
1879 loff_t s_maxbytes ;
1880 struct file_system_type *s_type ;
1881 struct super_operations const *s_op ;
1882 struct dquot_operations const *dq_op ;
1883 struct quotactl_ops const *s_qcop ;
1884 struct export_operations const *s_export_op ;
1885 unsigned long s_flags ;
1886 unsigned long s_magic ;
1887 struct dentry *s_root ;
1888 struct rw_semaphore s_umount ;
1889 struct mutex s_lock ;
1890 int s_count ;
1891 atomic_t s_active ;
1892 void *s_security ;
1893 struct xattr_handler const **s_xattr ;
1894 struct list_head s_inodes ;
1895 struct hlist_bl_head s_anon ;
1896 struct list_head *s_files ;
1897 struct list_head s_mounts ;
1898 struct list_head s_dentry_lru ;
1899 int s_nr_dentry_unused ;
1900 spinlock_t s_inode_lru_lock ;
1901 struct list_head s_inode_lru ;
1902 int s_nr_inodes_unused ;
1903 struct block_device *s_bdev ;
1904 struct backing_dev_info *s_bdi ;
1905 struct mtd_info *s_mtd ;
1906 struct hlist_node s_instances ;
1907 struct quota_info s_dquot ;
1908 int s_frozen ;
1909 wait_queue_head_t s_wait_unfrozen ;
1910 char s_id[32U] ;
1911 u8 s_uuid[16U] ;
1912 void *s_fs_info ;
1913 unsigned int s_max_links ;
1914 fmode_t s_mode ;
1915 u32 s_time_gran ;
1916 struct mutex s_vfs_rename_mutex ;
1917 char *s_subtype ;
1918 char *s_options ;
1919 struct dentry_operations const *s_d_op ;
1920 int cleancache_poolid ;
1921 struct shrinker s_shrink ;
1922 atomic_long_t s_remove_count ;
1923 int s_readonly_remount ;
1924};
1925#line 1563 "include/linux/fs.h"
1926struct fiemap_extent_info {
1927 unsigned int fi_flags ;
1928 unsigned int fi_extents_mapped ;
1929 unsigned int fi_extents_max ;
1930 struct fiemap_extent *fi_extents_start ;
1931};
1932#line 1602 "include/linux/fs.h"
1933struct file_operations {
1934 struct module *owner ;
1935 loff_t (*llseek)(struct file * , loff_t , int ) ;
1936 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
1937 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
1938 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
1939 loff_t ) ;
1940 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
1941 loff_t ) ;
1942 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
1943 loff_t , u64 , unsigned int ) ) ;
1944 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1945 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
1946 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
1947 int (*mmap)(struct file * , struct vm_area_struct * ) ;
1948 int (*open)(struct inode * , struct file * ) ;
1949 int (*flush)(struct file * , fl_owner_t ) ;
1950 int (*release)(struct inode * , struct file * ) ;
1951 int (*fsync)(struct file * , loff_t , loff_t , int ) ;
1952 int (*aio_fsync)(struct kiocb * , int ) ;
1953 int (*fasync)(int , struct file * , int ) ;
1954 int (*lock)(struct file * , int , struct file_lock * ) ;
1955 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
1956 int ) ;
1957 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
1958 unsigned long , unsigned long ) ;
1959 int (*check_flags)(int ) ;
1960 int (*flock)(struct file * , int , struct file_lock * ) ;
1961 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
1962 unsigned int ) ;
1963 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
1964 unsigned int ) ;
1965 int (*setlease)(struct file * , long , struct file_lock ** ) ;
1966 long (*fallocate)(struct file * , int , loff_t , loff_t ) ;
1967};
1968#line 1637 "include/linux/fs.h"
1969struct inode_operations {
1970 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1971 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1972 int (*permission)(struct inode * , int ) ;
1973 struct posix_acl *(*get_acl)(struct inode * , int ) ;
1974 int (*readlink)(struct dentry * , char * , int ) ;
1975 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1976 int (*create)(struct inode * , struct dentry * , umode_t , struct nameidata * ) ;
1977 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1978 int (*unlink)(struct inode * , struct dentry * ) ;
1979 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
1980 int (*mkdir)(struct inode * , struct dentry * , umode_t ) ;
1981 int (*rmdir)(struct inode * , struct dentry * ) ;
1982 int (*mknod)(struct inode * , struct dentry * , umode_t , dev_t ) ;
1983 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1984 void (*truncate)(struct inode * ) ;
1985 int (*setattr)(struct dentry * , struct iattr * ) ;
1986 int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
1987 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
1988 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
1989 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
1990 int (*removexattr)(struct dentry * , char const * ) ;
1991 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
1992 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 , u64 ) ;
1993};
1994#line 1682 "include/linux/fs.h"
1995struct super_operations {
1996 struct inode *(*alloc_inode)(struct super_block * ) ;
1997 void (*destroy_inode)(struct inode * ) ;
1998 void (*dirty_inode)(struct inode * , int ) ;
1999 int (*write_inode)(struct inode * , struct writeback_control * ) ;
2000 int (*drop_inode)(struct inode * ) ;
2001 void (*evict_inode)(struct inode * ) ;
2002 void (*put_super)(struct super_block * ) ;
2003 void (*write_super)(struct super_block * ) ;
2004 int (*sync_fs)(struct super_block * , int ) ;
2005 int (*freeze_fs)(struct super_block * ) ;
2006 int (*unfreeze_fs)(struct super_block * ) ;
2007 int (*statfs)(struct dentry * , struct kstatfs * ) ;
2008 int (*remount_fs)(struct super_block * , int * , char * ) ;
2009 void (*umount_begin)(struct super_block * ) ;
2010 int (*show_options)(struct seq_file * , struct dentry * ) ;
2011 int (*show_devname)(struct seq_file * , struct dentry * ) ;
2012 int (*show_path)(struct seq_file * , struct dentry * ) ;
2013 int (*show_stats)(struct seq_file * , struct dentry * ) ;
2014 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
2015 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
2016 loff_t ) ;
2017 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
2018 int (*nr_cached_objects)(struct super_block * ) ;
2019 void (*free_cached_objects)(struct super_block * , int ) ;
2020};
2021#line 1834 "include/linux/fs.h"
2022struct file_system_type {
2023 char const *name ;
2024 int fs_flags ;
2025 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
2026 void (*kill_sb)(struct super_block * ) ;
2027 struct module *owner ;
2028 struct file_system_type *next ;
2029 struct hlist_head fs_supers ;
2030 struct lock_class_key s_lock_key ;
2031 struct lock_class_key s_umount_key ;
2032 struct lock_class_key s_vfs_rename_key ;
2033 struct lock_class_key i_lock_key ;
2034 struct lock_class_key i_mutex_key ;
2035 struct lock_class_key i_mutex_dir_key ;
2036};
2037#line 34 "include/linux/poll.h"
2038struct poll_table_struct {
2039 void (*_qproc)(struct file * , wait_queue_head_t * , struct poll_table_struct * ) ;
2040 unsigned long _key ;
2041};
2042#line 126 "include/linux/rtc.h"
2043struct rtc_class_ops {
2044 int (*open)(struct device * ) ;
2045 void (*release)(struct device * ) ;
2046 int (*ioctl)(struct device * , unsigned int , unsigned long ) ;
2047 int (*read_time)(struct device * , struct rtc_time * ) ;
2048 int (*set_time)(struct device * , struct rtc_time * ) ;
2049 int (*read_alarm)(struct device * , struct rtc_wkalrm * ) ;
2050 int (*set_alarm)(struct device * , struct rtc_wkalrm * ) ;
2051 int (*proc)(struct device * , struct seq_file * ) ;
2052 int (*set_mmss)(struct device * , unsigned long ) ;
2053 int (*read_callback)(struct device * , int ) ;
2054 int (*alarm_irq_enable)(struct device * , unsigned int ) ;
2055};
2056#line 156 "include/linux/rtc.h"
2057struct rtc_task {
2058 void (*func)(void * ) ;
2059 void *private_data ;
2060};
2061#line 162 "include/linux/rtc.h"
2062struct rtc_timer {
2063 struct rtc_task task ;
2064 struct timerqueue_node node ;
2065 ktime_t period ;
2066 int enabled ;
2067};
2068#line 170 "include/linux/rtc.h"
2069struct rtc_device {
2070 struct device dev ;
2071 struct module *owner ;
2072 int id ;
2073 char name[20U] ;
2074 struct rtc_class_ops const *ops ;
2075 struct mutex ops_lock ;
2076 struct cdev char_dev ;
2077 unsigned long flags ;
2078 unsigned long irq_data ;
2079 spinlock_t irq_lock ;
2080 wait_queue_head_t irq_queue ;
2081 struct fasync_struct *async_queue ;
2082 struct rtc_task *irq_task ;
2083 spinlock_t irq_task_lock ;
2084 int irq_freq ;
2085 int max_user_freq ;
2086 struct timerqueue_head timerqueue ;
2087 struct rtc_timer aie_timer ;
2088 struct rtc_timer uie_rtctimer ;
2089 struct hrtimer pie_timer ;
2090 int pie_enabled ;
2091 struct work_struct irqwork ;
2092 int uie_unsupported ;
2093 struct work_struct uie_task ;
2094 struct timer_list uie_timer ;
2095 unsigned int oldsecs ;
2096 unsigned char uie_irq_active : 1 ;
2097 unsigned char stop_uie_polling : 1 ;
2098 unsigned char uie_task_active : 1 ;
2099 unsigned char uie_timer_active : 1 ;
2100};
2101#line 10 "include/linux/bcd.h"
2102struct regmap;
2103#line 10
2104struct regmap;
2105#line 231 "include/linux/regmap.h"
2106struct wm831x;
2107#line 231
2108struct wm831x;
2109#line 232
2110enum wm831x_auxadc;
2111#line 232
2112enum wm831x_auxadc;
2113#line 359 "include/linux/mfd/wm831x/core.h"
2114struct wm831x {
2115 struct mutex io_lock ;
2116 struct device *dev ;
2117 struct regmap *regmap ;
2118 int irq ;
2119 struct mutex irq_lock ;
2120 int irq_base ;
2121 int irq_masks_cur[5U] ;
2122 int irq_masks_cache[5U] ;
2123 bool soft_shutdown ;
2124 unsigned char has_gpio_ena : 1 ;
2125 unsigned char has_cs_sts : 1 ;
2126 unsigned char charger_irq_wake : 1 ;
2127 int num_gpio ;
2128 int gpio_update[16U] ;
2129 bool gpio_level[16U] ;
2130 struct mutex auxadc_lock ;
2131 struct list_head auxadc_pending ;
2132 u16 auxadc_active ;
2133 int (*auxadc_read)(struct wm831x * , enum wm831x_auxadc ) ;
2134 struct mutex key_lock ;
2135 unsigned char locked : 1 ;
2136};
2137#line 12 "include/linux/mod_devicetable.h"
2138typedef unsigned long kernel_ulong_t;
2139#line 215 "include/linux/mod_devicetable.h"
2140struct of_device_id {
2141 char name[32U] ;
2142 char type[32U] ;
2143 char compatible[128U] ;
2144 void *data ;
2145};
2146#line 492 "include/linux/mod_devicetable.h"
2147struct platform_device_id {
2148 char name[20U] ;
2149 kernel_ulong_t driver_data ;
2150};
2151#line 584
2152struct mfd_cell;
2153#line 584
2154struct mfd_cell;
2155#line 585 "include/linux/mod_devicetable.h"
2156struct platform_device {
2157 char const *name ;
2158 int id ;
2159 struct device dev ;
2160 u32 num_resources ;
2161 struct resource *resource ;
2162 struct platform_device_id const *id_entry ;
2163 struct mfd_cell *mfd_cell ;
2164 struct pdev_archdata archdata ;
2165};
2166#line 272 "include/linux/platform_device.h"
2167struct wm831x_rtc {
2168 struct wm831x *wm831x ;
2169 struct rtc_device *rtc ;
2170 unsigned char alarm_enabled : 1 ;
2171};
2172#line 1 "<compiler builtins>"
2173long __builtin_expect(long , long ) ;
2174#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
2175void ldv_spin_lock(void) ;
2176#line 3
2177void ldv_spin_unlock(void) ;
2178#line 4
2179int ldv_spin_trylock(void) ;
2180#line 50 "include/linux/dynamic_debug.h"
2181extern int __dynamic_dev_dbg(struct _ddebug * , struct device const * , char const *
2182 , ...) ;
2183#line 60 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
2184extern int memcmp(void const * , void const * , size_t ) ;
2185#line 27 "include/linux/err.h"
2186__inline static long PTR_ERR(void const *ptr )
2187{
2188
2189 {
2190#line 29
2191 return ((long )ptr);
2192}
2193}
2194#line 32 "include/linux/err.h"
2195__inline static long IS_ERR(void const *ptr )
2196{ long tmp ;
2197 unsigned long __cil_tmp3 ;
2198 int __cil_tmp4 ;
2199 long __cil_tmp5 ;
2200
2201 {
2202 {
2203#line 34
2204 __cil_tmp3 = (unsigned long )ptr;
2205#line 34
2206 __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;
2207#line 34
2208 __cil_tmp5 = (long )__cil_tmp4;
2209#line 34
2210 tmp = __builtin_expect(__cil_tmp5, 0L);
2211 }
2212#line 34
2213 return (tmp);
2214}
2215}
2216#line 26 "include/linux/export.h"
2217extern struct module __this_module ;
2218#line 220 "include/linux/slub_def.h"
2219extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
2220#line 223
2221void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
2222#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
2223void ldv_check_alloc_flags(gfp_t flags ) ;
2224#line 12
2225void ldv_check_alloc_nonatomic(void) ;
2226#line 14
2227struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
2228#line 127 "include/linux/interrupt.h"
2229extern int request_threaded_irq(unsigned int , irqreturn_t (*)(int , void * ) ,
2230 irqreturn_t (*)(int , void * ) , unsigned long ,
2231 char const * , void * ) ;
2232#line 110 "include/linux/rtc.h"
2233extern int rtc_valid_tm(struct rtc_time * ) ;
2234#line 111
2235extern int rtc_tm_to_time(struct rtc_time * , unsigned long * ) ;
2236#line 112
2237extern void rtc_time_to_tm(unsigned long , struct rtc_time * ) ;
2238#line 553 "include/linux/device.h"
2239extern void *devm_kzalloc(struct device * , size_t , gfp_t ) ;
2240#line 70 "include/linux/pm_wakeup.h"
2241__inline static bool device_may_wakeup(struct device *dev )
2242{ int tmp ;
2243 unsigned char *__cil_tmp3 ;
2244 unsigned char *__cil_tmp4 ;
2245 unsigned char __cil_tmp5 ;
2246 unsigned int __cil_tmp6 ;
2247 struct wakeup_source *__cil_tmp7 ;
2248 unsigned long __cil_tmp8 ;
2249 unsigned long __cil_tmp9 ;
2250 unsigned long __cil_tmp10 ;
2251 unsigned long __cil_tmp11 ;
2252 struct wakeup_source *__cil_tmp12 ;
2253 unsigned long __cil_tmp13 ;
2254
2255 {
2256 {
2257#line 72
2258 __cil_tmp3 = (unsigned char *)dev;
2259#line 72
2260 __cil_tmp4 = __cil_tmp3 + 292UL;
2261#line 72
2262 __cil_tmp5 = *__cil_tmp4;
2263#line 72
2264 __cil_tmp6 = (unsigned int )__cil_tmp5;
2265#line 72
2266 if (__cil_tmp6 != 0U) {
2267 {
2268#line 72
2269 __cil_tmp7 = (struct wakeup_source *)0;
2270#line 72
2271 __cil_tmp8 = (unsigned long )__cil_tmp7;
2272#line 72
2273 __cil_tmp9 = 288 + 192;
2274#line 72
2275 __cil_tmp10 = (unsigned long )dev;
2276#line 72
2277 __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
2278#line 72
2279 __cil_tmp12 = *((struct wakeup_source **)__cil_tmp11);
2280#line 72
2281 __cil_tmp13 = (unsigned long )__cil_tmp12;
2282#line 72
2283 if (__cil_tmp13 != __cil_tmp8) {
2284#line 72
2285 tmp = 1;
2286 } else {
2287#line 72
2288 tmp = 0;
2289 }
2290 }
2291 } else {
2292#line 72
2293 tmp = 0;
2294 }
2295 }
2296#line 72
2297 return ((bool )tmp);
2298}
2299}
2300#line 87
2301extern int device_init_wakeup(struct device * , bool ) ;
2302#line 792 "include/linux/device.h"
2303extern void *dev_get_drvdata(struct device const * ) ;
2304#line 793
2305extern int dev_set_drvdata(struct device * , void * ) ;
2306#line 892
2307extern int dev_err(struct device const * , char const * , ...) ;
2308#line 221 "include/linux/rtc.h"
2309extern struct rtc_device *rtc_device_register(char const * , struct device * , struct rtc_class_ops const * ,
2310 struct module * ) ;
2311#line 237
2312extern void rtc_update_irq(struct rtc_device * , unsigned long , unsigned long ) ;
2313#line 402 "include/linux/mfd/wm831x/core.h"
2314extern int wm831x_reg_read(struct wm831x * , unsigned short ) ;
2315#line 403
2316extern int wm831x_reg_write(struct wm831x * , unsigned short , unsigned short ) ;
2317#line 407
2318extern int wm831x_set_bits(struct wm831x * , unsigned short , unsigned short , unsigned short ) ;
2319#line 409
2320extern int wm831x_bulk_read(struct wm831x * , unsigned short , int , u16 * ) ;
2321#line 46 "include/linux/delay.h"
2322extern void msleep(unsigned int ) ;
2323#line 49 "include/linux/platform_device.h"
2324extern int platform_get_irq_byname(struct platform_device * , char const * ) ;
2325#line 188 "include/linux/platform_device.h"
2326__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
2327{ unsigned long __cil_tmp3 ;
2328 unsigned long __cil_tmp4 ;
2329 struct device *__cil_tmp5 ;
2330
2331 {
2332 {
2333#line 190
2334 __cil_tmp3 = (unsigned long )pdev;
2335#line 190
2336 __cil_tmp4 = __cil_tmp3 + 16;
2337#line 190
2338 __cil_tmp5 = (struct device *)__cil_tmp4;
2339#line 190
2340 dev_set_drvdata(__cil_tmp5, data);
2341 }
2342#line 191
2343 return;
2344}
2345}
2346#line 117 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
2347static int wm831x_rtc_readtime(struct device *dev , struct rtc_time *tm )
2348{ struct wm831x_rtc *wm831x_rtc ;
2349 void *tmp ;
2350 struct wm831x *wm831x ;
2351 u16 time1[2U] ;
2352 u16 time2[2U] ;
2353 int ret ;
2354 int count ;
2355 struct _ddebug descriptor ;
2356 long tmp___0 ;
2357 u32 time ;
2358 int tmp___1 ;
2359 int tmp___2 ;
2360 struct device const *__cil_tmp15 ;
2361 struct device const *__cil_tmp16 ;
2362 int __cil_tmp17 ;
2363 struct _ddebug *__cil_tmp18 ;
2364 unsigned long __cil_tmp19 ;
2365 unsigned long __cil_tmp20 ;
2366 unsigned long __cil_tmp21 ;
2367 unsigned long __cil_tmp22 ;
2368 unsigned long __cil_tmp23 ;
2369 unsigned long __cil_tmp24 ;
2370 unsigned char __cil_tmp25 ;
2371 long __cil_tmp26 ;
2372 long __cil_tmp27 ;
2373 struct device const *__cil_tmp28 ;
2374 u16 *__cil_tmp29 ;
2375 u16 *__cil_tmp30 ;
2376 void const *__cil_tmp31 ;
2377 void const *__cil_tmp32 ;
2378 unsigned long __cil_tmp33 ;
2379 unsigned long __cil_tmp34 ;
2380 u16 __cil_tmp35 ;
2381 int __cil_tmp36 ;
2382 unsigned long __cil_tmp37 ;
2383 unsigned long __cil_tmp38 ;
2384 u16 __cil_tmp39 ;
2385 int __cil_tmp40 ;
2386 int __cil_tmp41 ;
2387 int __cil_tmp42 ;
2388 unsigned long __cil_tmp43 ;
2389 struct device const *__cil_tmp44 ;
2390
2391 {
2392 {
2393#line 119
2394 __cil_tmp15 = (struct device const *)dev;
2395#line 119
2396 tmp = dev_get_drvdata(__cil_tmp15);
2397#line 119
2398 wm831x_rtc = (struct wm831x_rtc *)tmp;
2399#line 120
2400 wm831x = *((struct wm831x **)wm831x_rtc);
2401#line 123
2402 count = 0;
2403#line 126
2404 ret = wm831x_reg_read(wm831x, (unsigned short)16421);
2405 }
2406#line 127
2407 if (ret < 0) {
2408 {
2409#line 128
2410 __cil_tmp16 = (struct device const *)dev;
2411#line 128
2412 dev_err(__cil_tmp16, "Failed to read RTC control: %d\n", ret);
2413 }
2414#line 129
2415 return (ret);
2416 } else {
2417
2418 }
2419 {
2420#line 131
2421 __cil_tmp17 = ret & 32768;
2422#line 131
2423 if (__cil_tmp17 == 0) {
2424 {
2425#line 132
2426 __cil_tmp18 = & descriptor;
2427#line 132
2428 *((char const **)__cil_tmp18) = "rtc_wm831x";
2429#line 132
2430 __cil_tmp19 = (unsigned long )(& descriptor) + 8;
2431#line 132
2432 *((char const **)__cil_tmp19) = "wm831x_rtc_readtime";
2433#line 132
2434 __cil_tmp20 = (unsigned long )(& descriptor) + 16;
2435#line 132
2436 *((char const **)__cil_tmp20) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p";
2437#line 132
2438 __cil_tmp21 = (unsigned long )(& descriptor) + 24;
2439#line 132
2440 *((char const **)__cil_tmp21) = "RTC not yet configured\n";
2441#line 132
2442 __cil_tmp22 = (unsigned long )(& descriptor) + 32;
2443#line 132
2444 *((unsigned int *)__cil_tmp22) = 132U;
2445#line 132
2446 __cil_tmp23 = (unsigned long )(& descriptor) + 35;
2447#line 132
2448 *((unsigned char *)__cil_tmp23) = (unsigned char)1;
2449#line 132
2450 __cil_tmp24 = (unsigned long )(& descriptor) + 35;
2451#line 132
2452 __cil_tmp25 = *((unsigned char *)__cil_tmp24);
2453#line 132
2454 __cil_tmp26 = (long )__cil_tmp25;
2455#line 132
2456 __cil_tmp27 = __cil_tmp26 & 1L;
2457#line 132
2458 tmp___0 = __builtin_expect(__cil_tmp27, 0L);
2459 }
2460#line 132
2461 if (tmp___0 != 0L) {
2462 {
2463#line 132
2464 __cil_tmp28 = (struct device const *)dev;
2465#line 132
2466 __dynamic_dev_dbg(& descriptor, __cil_tmp28, "RTC not yet configured\n");
2467 }
2468 } else {
2469
2470 }
2471#line 133
2472 return (-22);
2473 } else {
2474
2475 }
2476 }
2477 ldv_21167:
2478 {
2479#line 140
2480 __cil_tmp29 = (u16 *)(& time1);
2481#line 140
2482 ret = wm831x_bulk_read(wm831x, (unsigned short)16417, 2, __cil_tmp29);
2483 }
2484#line 142
2485 if (ret != 0) {
2486#line 143
2487 goto ldv_21165;
2488 } else {
2489
2490 }
2491 {
2492#line 145
2493 __cil_tmp30 = (u16 *)(& time2);
2494#line 145
2495 ret = wm831x_bulk_read(wm831x, (unsigned short)16417, 2, __cil_tmp30);
2496 }
2497#line 147
2498 if (ret != 0) {
2499#line 148
2500 goto ldv_21165;
2501 } else {
2502
2503 }
2504 {
2505#line 150
2506 __cil_tmp31 = (void const *)(& time1);
2507#line 150
2508 __cil_tmp32 = (void const *)(& time2);
2509#line 150
2510 tmp___2 = memcmp(__cil_tmp31, __cil_tmp32, 4UL);
2511 }
2512#line 150
2513 if (tmp___2 == 0) {
2514 {
2515#line 151
2516 __cil_tmp33 = 1 * 2UL;
2517#line 151
2518 __cil_tmp34 = (unsigned long )(time1) + __cil_tmp33;
2519#line 151
2520 __cil_tmp35 = *((u16 *)__cil_tmp34);
2521#line 151
2522 __cil_tmp36 = (int )__cil_tmp35;
2523#line 151
2524 __cil_tmp37 = 0 * 2UL;
2525#line 151
2526 __cil_tmp38 = (unsigned long )(time1) + __cil_tmp37;
2527#line 151
2528 __cil_tmp39 = *((u16 *)__cil_tmp38);
2529#line 151
2530 __cil_tmp40 = (int )__cil_tmp39;
2531#line 151
2532 __cil_tmp41 = __cil_tmp40 << 16;
2533#line 151
2534 __cil_tmp42 = __cil_tmp41 | __cil_tmp36;
2535#line 151
2536 time = (u32 )__cil_tmp42;
2537#line 153
2538 __cil_tmp43 = (unsigned long )time;
2539#line 153
2540 rtc_time_to_tm(__cil_tmp43, tm);
2541#line 154
2542 tmp___1 = rtc_valid_tm(tm);
2543 }
2544#line 154
2545 return (tmp___1);
2546 } else {
2547
2548 }
2549 ldv_21165:
2550#line 157
2551 count = count + 1;
2552#line 157
2553 if (count <= 4) {
2554#line 158
2555 goto ldv_21167;
2556 } else {
2557#line 160
2558 goto ldv_21168;
2559 }
2560 ldv_21168:
2561 {
2562#line 159
2563 __cil_tmp44 = (struct device const *)dev;
2564#line 159
2565 dev_err(__cil_tmp44, "Timed out reading current time\n");
2566 }
2567#line 161
2568 return (-5);
2569}
2570}
2571#line 167 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
2572static int wm831x_rtc_set_mmss(struct device *dev , unsigned long time )
2573{ struct wm831x_rtc *wm831x_rtc ;
2574 void *tmp ;
2575 struct wm831x *wm831x ;
2576 struct rtc_time new_tm ;
2577 unsigned long new_time ;
2578 int ret ;
2579 int count ;
2580 struct device const *__cil_tmp10 ;
2581 unsigned long __cil_tmp11 ;
2582 unsigned short __cil_tmp12 ;
2583 int __cil_tmp13 ;
2584 unsigned short __cil_tmp14 ;
2585 struct device const *__cil_tmp15 ;
2586 unsigned short __cil_tmp16 ;
2587 int __cil_tmp17 ;
2588 unsigned short __cil_tmp18 ;
2589 struct device const *__cil_tmp19 ;
2590 int __cil_tmp20 ;
2591 int __cil_tmp21 ;
2592 struct device const *__cil_tmp22 ;
2593 struct device const *__cil_tmp23 ;
2594 unsigned long *__cil_tmp24 ;
2595 unsigned long __cil_tmp25 ;
2596 unsigned long __cil_tmp26 ;
2597 struct device const *__cil_tmp27 ;
2598
2599 {
2600 {
2601#line 169
2602 __cil_tmp10 = (struct device const *)dev;
2603#line 169
2604 tmp = dev_get_drvdata(__cil_tmp10);
2605#line 169
2606 wm831x_rtc = (struct wm831x_rtc *)tmp;
2607#line 170
2608 wm831x = *((struct wm831x **)wm831x_rtc);
2609#line 174
2610 count = 0;
2611#line 176
2612 __cil_tmp11 = time >> 16;
2613#line 176
2614 __cil_tmp12 = (unsigned short )__cil_tmp11;
2615#line 176
2616 __cil_tmp13 = (int )__cil_tmp12;
2617#line 176
2618 __cil_tmp14 = (unsigned short )__cil_tmp13;
2619#line 176
2620 ret = wm831x_reg_write(wm831x, (unsigned short)16417, __cil_tmp14);
2621 }
2622#line 178
2623 if (ret < 0) {
2624 {
2625#line 179
2626 __cil_tmp15 = (struct device const *)dev;
2627#line 179
2628 dev_err(__cil_tmp15, "Failed to write TIME_1: %d\n", ret);
2629 }
2630#line 180
2631 return (ret);
2632 } else {
2633
2634 }
2635 {
2636#line 183
2637 __cil_tmp16 = (unsigned short )time;
2638#line 183
2639 __cil_tmp17 = (int )__cil_tmp16;
2640#line 183
2641 __cil_tmp18 = (unsigned short )__cil_tmp17;
2642#line 183
2643 ret = wm831x_reg_write(wm831x, (unsigned short)16418, __cil_tmp18);
2644 }
2645#line 184
2646 if (ret < 0) {
2647 {
2648#line 185
2649 __cil_tmp19 = (struct device const *)dev;
2650#line 185
2651 dev_err(__cil_tmp19, "Failed to write TIME_2: %d\n", ret);
2652 }
2653#line 186
2654 return (ret);
2655 } else {
2656
2657 }
2658 ldv_21179:
2659 {
2660#line 193
2661 msleep(1U);
2662#line 195
2663 ret = wm831x_reg_read(wm831x, (unsigned short)16421);
2664 }
2665#line 196
2666 if (ret < 0) {
2667#line 197
2668 ret = 16384;
2669 } else {
2670
2671 }
2672 {
2673#line 199
2674 __cil_tmp20 = ret & 16384;
2675#line 199
2676 if (__cil_tmp20 == 0) {
2677#line 199
2678 count = count + 1;
2679#line 199
2680 if (count <= 4) {
2681#line 200
2682 goto ldv_21179;
2683 } else {
2684#line 202
2685 goto ldv_21180;
2686 }
2687 } else {
2688#line 202
2689 goto ldv_21180;
2690 }
2691 }
2692 ldv_21180: ;
2693 {
2694#line 201
2695 __cil_tmp21 = ret & 16384;
2696#line 201
2697 if (__cil_tmp21 != 0) {
2698 {
2699#line 202
2700 __cil_tmp22 = (struct device const *)dev;
2701#line 202
2702 dev_err(__cil_tmp22, "Timed out writing RTC update\n");
2703 }
2704#line 203
2705 return (-5);
2706 } else {
2707
2708 }
2709 }
2710 {
2711#line 209
2712 ret = wm831x_rtc_readtime(dev, & new_tm);
2713 }
2714#line 210
2715 if (ret < 0) {
2716#line 211
2717 return (ret);
2718 } else {
2719
2720 }
2721 {
2722#line 213
2723 ret = rtc_tm_to_time(& new_tm, & new_time);
2724 }
2725#line 214
2726 if (ret < 0) {
2727 {
2728#line 215
2729 __cil_tmp23 = (struct device const *)dev;
2730#line 215
2731 dev_err(__cil_tmp23, "Failed to convert time: %d\n", ret);
2732 }
2733#line 216
2734 return (ret);
2735 } else {
2736
2737 }
2738 {
2739#line 220
2740 __cil_tmp24 = & new_time;
2741#line 220
2742 __cil_tmp25 = *__cil_tmp24;
2743#line 220
2744 __cil_tmp26 = __cil_tmp25 - time;
2745#line 220
2746 if (__cil_tmp26 > 1UL) {
2747 {
2748#line 221
2749 __cil_tmp27 = (struct device const *)dev;
2750#line 221
2751 dev_err(__cil_tmp27, "RTC update not permitted by hardware\n");
2752 }
2753#line 222
2754 return (-1);
2755 } else {
2756
2757 }
2758 }
2759#line 225
2760 return (0);
2761}
2762}
2763#line 231 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
2764static int wm831x_rtc_readalarm(struct device *dev , struct rtc_wkalrm *alrm )
2765{ struct wm831x_rtc *wm831x_rtc ;
2766 void *tmp ;
2767 int ret ;
2768 u16 data[2U] ;
2769 u32 time ;
2770 struct device const *__cil_tmp8 ;
2771 struct wm831x *__cil_tmp9 ;
2772 u16 *__cil_tmp10 ;
2773 struct device const *__cil_tmp11 ;
2774 unsigned long __cil_tmp12 ;
2775 unsigned long __cil_tmp13 ;
2776 u16 __cil_tmp14 ;
2777 int __cil_tmp15 ;
2778 unsigned long __cil_tmp16 ;
2779 unsigned long __cil_tmp17 ;
2780 u16 __cil_tmp18 ;
2781 int __cil_tmp19 ;
2782 int __cil_tmp20 ;
2783 int __cil_tmp21 ;
2784 unsigned long __cil_tmp22 ;
2785 unsigned long __cil_tmp23 ;
2786 unsigned long __cil_tmp24 ;
2787 struct rtc_time *__cil_tmp25 ;
2788 struct wm831x *__cil_tmp26 ;
2789 struct device const *__cil_tmp27 ;
2790 int __cil_tmp28 ;
2791
2792 {
2793 {
2794#line 233
2795 __cil_tmp8 = (struct device const *)dev;
2796#line 233
2797 tmp = dev_get_drvdata(__cil_tmp8);
2798#line 233
2799 wm831x_rtc = (struct wm831x_rtc *)tmp;
2800#line 238
2801 __cil_tmp9 = *((struct wm831x **)wm831x_rtc);
2802#line 238
2803 __cil_tmp10 = (u16 *)(& data);
2804#line 238
2805 ret = wm831x_bulk_read(__cil_tmp9, (unsigned short)16419, 2, __cil_tmp10);
2806 }
2807#line 240
2808 if (ret != 0) {
2809 {
2810#line 241
2811 __cil_tmp11 = (struct device const *)dev;
2812#line 241
2813 dev_err(__cil_tmp11, "Failed to read alarm time: %d\n", ret);
2814 }
2815#line 242
2816 return (ret);
2817 } else {
2818
2819 }
2820 {
2821#line 245
2822 __cil_tmp12 = 1 * 2UL;
2823#line 245
2824 __cil_tmp13 = (unsigned long )(data) + __cil_tmp12;
2825#line 245
2826 __cil_tmp14 = *((u16 *)__cil_tmp13);
2827#line 245
2828 __cil_tmp15 = (int )__cil_tmp14;
2829#line 245
2830 __cil_tmp16 = 0 * 2UL;
2831#line 245
2832 __cil_tmp17 = (unsigned long )(data) + __cil_tmp16;
2833#line 245
2834 __cil_tmp18 = *((u16 *)__cil_tmp17);
2835#line 245
2836 __cil_tmp19 = (int )__cil_tmp18;
2837#line 245
2838 __cil_tmp20 = __cil_tmp19 << 16;
2839#line 245
2840 __cil_tmp21 = __cil_tmp20 | __cil_tmp15;
2841#line 245
2842 time = (u32 )__cil_tmp21;
2843#line 247
2844 __cil_tmp22 = (unsigned long )time;
2845#line 247
2846 __cil_tmp23 = (unsigned long )alrm;
2847#line 247
2848 __cil_tmp24 = __cil_tmp23 + 4;
2849#line 247
2850 __cil_tmp25 = (struct rtc_time *)__cil_tmp24;
2851#line 247
2852 rtc_time_to_tm(__cil_tmp22, __cil_tmp25);
2853#line 249
2854 __cil_tmp26 = *((struct wm831x **)wm831x_rtc);
2855#line 249
2856 ret = wm831x_reg_read(__cil_tmp26, (unsigned short)16421);
2857 }
2858#line 250
2859 if (ret < 0) {
2860 {
2861#line 251
2862 __cil_tmp27 = (struct device const *)dev;
2863#line 251
2864 dev_err(__cil_tmp27, "Failed to read RTC control: %d\n", ret);
2865 }
2866#line 252
2867 return (ret);
2868 } else {
2869
2870 }
2871 {
2872#line 255
2873 __cil_tmp28 = ret & 1024;
2874#line 255
2875 if (__cil_tmp28 != 0) {
2876#line 256
2877 *((unsigned char *)alrm) = (unsigned char)1;
2878 } else {
2879#line 258
2880 *((unsigned char *)alrm) = (unsigned char)0;
2881 }
2882 }
2883#line 260
2884 return (0);
2885}
2886}
2887#line 263 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
2888static int wm831x_rtc_stop_alarm(struct wm831x_rtc *wm831x_rtc )
2889{ int tmp ;
2890 unsigned long __cil_tmp3 ;
2891 unsigned long __cil_tmp4 ;
2892 struct wm831x *__cil_tmp5 ;
2893
2894 {
2895 {
2896#line 265
2897 __cil_tmp3 = (unsigned long )wm831x_rtc;
2898#line 265
2899 __cil_tmp4 = __cil_tmp3 + 16;
2900#line 265
2901 *((unsigned char *)__cil_tmp4) = (unsigned char)0;
2902#line 267
2903 __cil_tmp5 = *((struct wm831x **)wm831x_rtc);
2904#line 267
2905 tmp = wm831x_set_bits(__cil_tmp5, (unsigned short)16421, (unsigned short)1024, (unsigned short)0);
2906 }
2907#line 267
2908 return (tmp);
2909}
2910}
2911#line 271 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
2912static int wm831x_rtc_start_alarm(struct wm831x_rtc *wm831x_rtc )
2913{ int tmp ;
2914 unsigned long __cil_tmp3 ;
2915 unsigned long __cil_tmp4 ;
2916 struct wm831x *__cil_tmp5 ;
2917
2918 {
2919 {
2920#line 273
2921 __cil_tmp3 = (unsigned long )wm831x_rtc;
2922#line 273
2923 __cil_tmp4 = __cil_tmp3 + 16;
2924#line 273
2925 *((unsigned char *)__cil_tmp4) = (unsigned char)1;
2926#line 275
2927 __cil_tmp5 = *((struct wm831x **)wm831x_rtc);
2928#line 275
2929 tmp = wm831x_set_bits(__cil_tmp5, (unsigned short)16421, (unsigned short)1024, (unsigned short)1024);
2930 }
2931#line 275
2932 return (tmp);
2933}
2934}
2935#line 279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
2936static int wm831x_rtc_setalarm(struct device *dev , struct rtc_wkalrm *alrm )
2937{ struct wm831x_rtc *wm831x_rtc ;
2938 void *tmp ;
2939 struct wm831x *wm831x ;
2940 int ret ;
2941 unsigned long time ;
2942 struct device const *__cil_tmp8 ;
2943 unsigned long __cil_tmp9 ;
2944 unsigned long __cil_tmp10 ;
2945 struct rtc_time *__cil_tmp11 ;
2946 struct device const *__cil_tmp12 ;
2947 struct device const *__cil_tmp13 ;
2948 unsigned long *__cil_tmp14 ;
2949 unsigned long __cil_tmp15 ;
2950 unsigned long __cil_tmp16 ;
2951 unsigned short __cil_tmp17 ;
2952 int __cil_tmp18 ;
2953 unsigned short __cil_tmp19 ;
2954 struct device const *__cil_tmp20 ;
2955 unsigned long *__cil_tmp21 ;
2956 unsigned long __cil_tmp22 ;
2957 unsigned short __cil_tmp23 ;
2958 int __cil_tmp24 ;
2959 unsigned short __cil_tmp25 ;
2960 struct device const *__cil_tmp26 ;
2961 unsigned char __cil_tmp27 ;
2962 unsigned int __cil_tmp28 ;
2963 struct device const *__cil_tmp29 ;
2964
2965 {
2966 {
2967#line 281
2968 __cil_tmp8 = (struct device const *)dev;
2969#line 281
2970 tmp = dev_get_drvdata(__cil_tmp8);
2971#line 281
2972 wm831x_rtc = (struct wm831x_rtc *)tmp;
2973#line 282
2974 wm831x = *((struct wm831x **)wm831x_rtc);
2975#line 286
2976 __cil_tmp9 = (unsigned long )alrm;
2977#line 286
2978 __cil_tmp10 = __cil_tmp9 + 4;
2979#line 286
2980 __cil_tmp11 = (struct rtc_time *)__cil_tmp10;
2981#line 286
2982 ret = rtc_tm_to_time(__cil_tmp11, & time);
2983 }
2984#line 287
2985 if (ret < 0) {
2986 {
2987#line 288
2988 __cil_tmp12 = (struct device const *)dev;
2989#line 288
2990 dev_err(__cil_tmp12, "Failed to convert time: %d\n", ret);
2991 }
2992#line 289
2993 return (ret);
2994 } else {
2995
2996 }
2997 {
2998#line 292
2999 ret = wm831x_rtc_stop_alarm(wm831x_rtc);
3000 }
3001#line 293
3002 if (ret < 0) {
3003 {
3004#line 294
3005 __cil_tmp13 = (struct device const *)dev;
3006#line 294
3007 dev_err(__cil_tmp13, "Failed to stop alarm: %d\n", ret);
3008 }
3009#line 295
3010 return (ret);
3011 } else {
3012
3013 }
3014 {
3015#line 298
3016 __cil_tmp14 = & time;
3017#line 298
3018 __cil_tmp15 = *__cil_tmp14;
3019#line 298
3020 __cil_tmp16 = __cil_tmp15 >> 16;
3021#line 298
3022 __cil_tmp17 = (unsigned short )__cil_tmp16;
3023#line 298
3024 __cil_tmp18 = (int )__cil_tmp17;
3025#line 298
3026 __cil_tmp19 = (unsigned short )__cil_tmp18;
3027#line 298
3028 ret = wm831x_reg_write(wm831x, (unsigned short)16419, __cil_tmp19);
3029 }
3030#line 300
3031 if (ret < 0) {
3032 {
3033#line 301
3034 __cil_tmp20 = (struct device const *)dev;
3035#line 301
3036 dev_err(__cil_tmp20, "Failed to write ALARM_1: %d\n", ret);
3037 }
3038#line 302
3039 return (ret);
3040 } else {
3041
3042 }
3043 {
3044#line 305
3045 __cil_tmp21 = & time;
3046#line 305
3047 __cil_tmp22 = *__cil_tmp21;
3048#line 305
3049 __cil_tmp23 = (unsigned short )__cil_tmp22;
3050#line 305
3051 __cil_tmp24 = (int )__cil_tmp23;
3052#line 305
3053 __cil_tmp25 = (unsigned short )__cil_tmp24;
3054#line 305
3055 ret = wm831x_reg_write(wm831x, (unsigned short)16420, __cil_tmp25);
3056 }
3057#line 306
3058 if (ret < 0) {
3059 {
3060#line 307
3061 __cil_tmp26 = (struct device const *)dev;
3062#line 307
3063 dev_err(__cil_tmp26, "Failed to write ALARM_2: %d\n", ret);
3064 }
3065#line 308
3066 return (ret);
3067 } else {
3068
3069 }
3070 {
3071#line 311
3072 __cil_tmp27 = *((unsigned char *)alrm);
3073#line 311
3074 __cil_tmp28 = (unsigned int )__cil_tmp27;
3075#line 311
3076 if (__cil_tmp28 != 0U) {
3077 {
3078#line 312
3079 ret = wm831x_rtc_start_alarm(wm831x_rtc);
3080 }
3081#line 313
3082 if (ret < 0) {
3083 {
3084#line 314
3085 __cil_tmp29 = (struct device const *)dev;
3086#line 314
3087 dev_err(__cil_tmp29, "Failed to start alarm: %d\n", ret);
3088 }
3089#line 315
3090 return (ret);
3091 } else {
3092
3093 }
3094 } else {
3095
3096 }
3097 }
3098#line 319
3099 return (0);
3100}
3101}
3102#line 322 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3103static int wm831x_rtc_alarm_irq_enable(struct device *dev , unsigned int enabled )
3104{ struct wm831x_rtc *wm831x_rtc ;
3105 void *tmp ;
3106 int tmp___0 ;
3107 int tmp___1 ;
3108 struct device const *__cil_tmp7 ;
3109
3110 {
3111 {
3112#line 325
3113 __cil_tmp7 = (struct device const *)dev;
3114#line 325
3115 tmp = dev_get_drvdata(__cil_tmp7);
3116#line 325
3117 wm831x_rtc = (struct wm831x_rtc *)tmp;
3118 }
3119#line 327
3120 if (enabled != 0U) {
3121 {
3122#line 328
3123 tmp___0 = wm831x_rtc_start_alarm(wm831x_rtc);
3124 }
3125#line 328
3126 return (tmp___0);
3127 } else {
3128 {
3129#line 330
3130 tmp___1 = wm831x_rtc_stop_alarm(wm831x_rtc);
3131 }
3132#line 330
3133 return (tmp___1);
3134 }
3135}
3136}
3137#line 333 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3138static irqreturn_t wm831x_alm_irq(int irq , void *data )
3139{ struct wm831x_rtc *wm831x_rtc ;
3140 unsigned long __cil_tmp4 ;
3141 unsigned long __cil_tmp5 ;
3142 struct rtc_device *__cil_tmp6 ;
3143
3144 {
3145 {
3146#line 335
3147 wm831x_rtc = (struct wm831x_rtc *)data;
3148#line 337
3149 __cil_tmp4 = (unsigned long )wm831x_rtc;
3150#line 337
3151 __cil_tmp5 = __cil_tmp4 + 8;
3152#line 337
3153 __cil_tmp6 = *((struct rtc_device **)__cil_tmp5);
3154#line 337
3155 rtc_update_irq(__cil_tmp6, 1UL, 160UL);
3156 }
3157#line 339
3158 return ((irqreturn_t )1);
3159}
3160}
3161#line 342 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3162static struct rtc_class_ops const wm831x_rtc_ops =
3163#line 342
3164 {(int (*)(struct device * ))0, (void (*)(struct device * ))0, (int (*)(struct device * ,
3165 unsigned int ,
3166 unsigned long ))0,
3167 & wm831x_rtc_readtime, (int (*)(struct device * , struct rtc_time * ))0, & wm831x_rtc_readalarm,
3168 & wm831x_rtc_setalarm, (int (*)(struct device * , struct seq_file * ))0, & wm831x_rtc_set_mmss,
3169 (int (*)(struct device * , int ))0, & wm831x_rtc_alarm_irq_enable};
3170#line 352 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3171static int wm831x_rtc_suspend(struct device *dev )
3172{ struct platform_device *pdev ;
3173 struct device const *__mptr ;
3174 struct wm831x_rtc *wm831x_rtc ;
3175 void *tmp ;
3176 int ret ;
3177 int enable ;
3178 bool tmp___0 ;
3179 struct platform_device *__cil_tmp9 ;
3180 unsigned long __cil_tmp10 ;
3181 unsigned long __cil_tmp11 ;
3182 struct device *__cil_tmp12 ;
3183 struct device const *__cil_tmp13 ;
3184 unsigned char *__cil_tmp14 ;
3185 unsigned char *__cil_tmp15 ;
3186 unsigned char __cil_tmp16 ;
3187 unsigned int __cil_tmp17 ;
3188 unsigned long __cil_tmp18 ;
3189 unsigned long __cil_tmp19 ;
3190 struct device *__cil_tmp20 ;
3191 struct wm831x *__cil_tmp21 ;
3192 unsigned short __cil_tmp22 ;
3193 int __cil_tmp23 ;
3194 unsigned short __cil_tmp24 ;
3195 unsigned long __cil_tmp25 ;
3196 unsigned long __cil_tmp26 ;
3197 struct device *__cil_tmp27 ;
3198 struct device const *__cil_tmp28 ;
3199
3200 {
3201 {
3202#line 354
3203 __mptr = (struct device const *)dev;
3204#line 354
3205 __cil_tmp9 = (struct platform_device *)__mptr;
3206#line 354
3207 pdev = __cil_tmp9 + 0xfffffffffffffff0UL;
3208#line 355
3209 __cil_tmp10 = (unsigned long )pdev;
3210#line 355
3211 __cil_tmp11 = __cil_tmp10 + 16;
3212#line 355
3213 __cil_tmp12 = (struct device *)__cil_tmp11;
3214#line 355
3215 __cil_tmp13 = (struct device const *)__cil_tmp12;
3216#line 355
3217 tmp = dev_get_drvdata(__cil_tmp13);
3218#line 355
3219 wm831x_rtc = (struct wm831x_rtc *)tmp;
3220 }
3221 {
3222#line 358
3223 __cil_tmp14 = (unsigned char *)wm831x_rtc;
3224#line 358
3225 __cil_tmp15 = __cil_tmp14 + 16UL;
3226#line 358
3227 __cil_tmp16 = *__cil_tmp15;
3228#line 358
3229 __cil_tmp17 = (unsigned int )__cil_tmp16;
3230#line 358
3231 if (__cil_tmp17 != 0U) {
3232 {
3233#line 358
3234 __cil_tmp18 = (unsigned long )pdev;
3235#line 358
3236 __cil_tmp19 = __cil_tmp18 + 16;
3237#line 358
3238 __cil_tmp20 = (struct device *)__cil_tmp19;
3239#line 358
3240 tmp___0 = device_may_wakeup(__cil_tmp20);
3241 }
3242#line 358
3243 if ((int )tmp___0) {
3244#line 359
3245 enable = 1024;
3246 } else {
3247#line 361
3248 enable = 0;
3249 }
3250 } else {
3251#line 361
3252 enable = 0;
3253 }
3254 }
3255 {
3256#line 363
3257 __cil_tmp21 = *((struct wm831x **)wm831x_rtc);
3258#line 363
3259 __cil_tmp22 = (unsigned short )enable;
3260#line 363
3261 __cil_tmp23 = (int )__cil_tmp22;
3262#line 363
3263 __cil_tmp24 = (unsigned short )__cil_tmp23;
3264#line 363
3265 ret = wm831x_set_bits(__cil_tmp21, (unsigned short)16421, (unsigned short)1024,
3266 __cil_tmp24);
3267 }
3268#line 365
3269 if (ret != 0) {
3270 {
3271#line 366
3272 __cil_tmp25 = (unsigned long )pdev;
3273#line 366
3274 __cil_tmp26 = __cil_tmp25 + 16;
3275#line 366
3276 __cil_tmp27 = (struct device *)__cil_tmp26;
3277#line 366
3278 __cil_tmp28 = (struct device const *)__cil_tmp27;
3279#line 366
3280 dev_err(__cil_tmp28, "Failed to update RTC alarm: %d\n", ret);
3281 }
3282 } else {
3283
3284 }
3285#line 368
3286 return (0);
3287}
3288}
3289#line 374 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3290static int wm831x_rtc_resume(struct device *dev )
3291{ struct platform_device *pdev ;
3292 struct device const *__mptr ;
3293 struct wm831x_rtc *wm831x_rtc ;
3294 void *tmp ;
3295 int ret ;
3296 struct platform_device *__cil_tmp7 ;
3297 unsigned long __cil_tmp8 ;
3298 unsigned long __cil_tmp9 ;
3299 struct device *__cil_tmp10 ;
3300 struct device const *__cil_tmp11 ;
3301 unsigned char *__cil_tmp12 ;
3302 unsigned char *__cil_tmp13 ;
3303 unsigned char __cil_tmp14 ;
3304 unsigned int __cil_tmp15 ;
3305 unsigned long __cil_tmp16 ;
3306 unsigned long __cil_tmp17 ;
3307 struct device *__cil_tmp18 ;
3308 struct device const *__cil_tmp19 ;
3309
3310 {
3311 {
3312#line 376
3313 __mptr = (struct device const *)dev;
3314#line 376
3315 __cil_tmp7 = (struct platform_device *)__mptr;
3316#line 376
3317 pdev = __cil_tmp7 + 0xfffffffffffffff0UL;
3318#line 377
3319 __cil_tmp8 = (unsigned long )pdev;
3320#line 377
3321 __cil_tmp9 = __cil_tmp8 + 16;
3322#line 377
3323 __cil_tmp10 = (struct device *)__cil_tmp9;
3324#line 377
3325 __cil_tmp11 = (struct device const *)__cil_tmp10;
3326#line 377
3327 tmp = dev_get_drvdata(__cil_tmp11);
3328#line 377
3329 wm831x_rtc = (struct wm831x_rtc *)tmp;
3330 }
3331 {
3332#line 380
3333 __cil_tmp12 = (unsigned char *)wm831x_rtc;
3334#line 380
3335 __cil_tmp13 = __cil_tmp12 + 16UL;
3336#line 380
3337 __cil_tmp14 = *__cil_tmp13;
3338#line 380
3339 __cil_tmp15 = (unsigned int )__cil_tmp14;
3340#line 380
3341 if (__cil_tmp15 != 0U) {
3342 {
3343#line 381
3344 ret = wm831x_rtc_start_alarm(wm831x_rtc);
3345 }
3346#line 382
3347 if (ret != 0) {
3348 {
3349#line 383
3350 __cil_tmp16 = (unsigned long )pdev;
3351#line 383
3352 __cil_tmp17 = __cil_tmp16 + 16;
3353#line 383
3354 __cil_tmp18 = (struct device *)__cil_tmp17;
3355#line 383
3356 __cil_tmp19 = (struct device const *)__cil_tmp18;
3357#line 383
3358 dev_err(__cil_tmp19, "Failed to restart RTC alarm: %d\n", ret);
3359 }
3360 } else {
3361
3362 }
3363 } else {
3364
3365 }
3366 }
3367#line 387
3368 return (0);
3369}
3370}
3371#line 391 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3372static int wm831x_rtc_freeze(struct device *dev )
3373{ struct platform_device *pdev ;
3374 struct device const *__mptr ;
3375 struct wm831x_rtc *wm831x_rtc ;
3376 void *tmp ;
3377 int ret ;
3378 struct platform_device *__cil_tmp7 ;
3379 unsigned long __cil_tmp8 ;
3380 unsigned long __cil_tmp9 ;
3381 struct device *__cil_tmp10 ;
3382 struct device const *__cil_tmp11 ;
3383 struct wm831x *__cil_tmp12 ;
3384 unsigned long __cil_tmp13 ;
3385 unsigned long __cil_tmp14 ;
3386 struct device *__cil_tmp15 ;
3387 struct device const *__cil_tmp16 ;
3388
3389 {
3390 {
3391#line 393
3392 __mptr = (struct device const *)dev;
3393#line 393
3394 __cil_tmp7 = (struct platform_device *)__mptr;
3395#line 393
3396 pdev = __cil_tmp7 + 0xfffffffffffffff0UL;
3397#line 394
3398 __cil_tmp8 = (unsigned long )pdev;
3399#line 394
3400 __cil_tmp9 = __cil_tmp8 + 16;
3401#line 394
3402 __cil_tmp10 = (struct device *)__cil_tmp9;
3403#line 394
3404 __cil_tmp11 = (struct device const *)__cil_tmp10;
3405#line 394
3406 tmp = dev_get_drvdata(__cil_tmp11);
3407#line 394
3408 wm831x_rtc = (struct wm831x_rtc *)tmp;
3409#line 397
3410 __cil_tmp12 = *((struct wm831x **)wm831x_rtc);
3411#line 397
3412 ret = wm831x_set_bits(__cil_tmp12, (unsigned short)16421, (unsigned short)1024,
3413 (unsigned short)0);
3414 }
3415#line 399
3416 if (ret != 0) {
3417 {
3418#line 400
3419 __cil_tmp13 = (unsigned long )pdev;
3420#line 400
3421 __cil_tmp14 = __cil_tmp13 + 16;
3422#line 400
3423 __cil_tmp15 = (struct device *)__cil_tmp14;
3424#line 400
3425 __cil_tmp16 = (struct device const *)__cil_tmp15;
3426#line 400
3427 dev_err(__cil_tmp16, "Failed to stop RTC alarm: %d\n", ret);
3428 }
3429 } else {
3430
3431 }
3432#line 402
3433 return (0);
3434}
3435}
3436#line 410 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3437static int wm831x_rtc_probe(struct platform_device *pdev )
3438{ struct wm831x *wm831x ;
3439 void *tmp ;
3440 struct wm831x_rtc *wm831x_rtc ;
3441 int alm_irq ;
3442 int tmp___0 ;
3443 int ret ;
3444 void *tmp___1 ;
3445 long tmp___2 ;
3446 long tmp___3 ;
3447 unsigned long __cil_tmp11 ;
3448 unsigned long __cil_tmp12 ;
3449 struct device *__cil_tmp13 ;
3450 struct device const *__cil_tmp14 ;
3451 unsigned long __cil_tmp15 ;
3452 unsigned long __cil_tmp16 ;
3453 struct device *__cil_tmp17 ;
3454 struct wm831x_rtc *__cil_tmp18 ;
3455 unsigned long __cil_tmp19 ;
3456 unsigned long __cil_tmp20 ;
3457 void *__cil_tmp21 ;
3458 unsigned long __cil_tmp22 ;
3459 unsigned long __cil_tmp23 ;
3460 struct device *__cil_tmp24 ;
3461 struct device const *__cil_tmp25 ;
3462 int __cil_tmp26 ;
3463 unsigned long __cil_tmp27 ;
3464 unsigned long __cil_tmp28 ;
3465 unsigned long __cil_tmp29 ;
3466 unsigned long __cil_tmp30 ;
3467 struct device *__cil_tmp31 ;
3468 bool __cil_tmp32 ;
3469 unsigned long __cil_tmp33 ;
3470 unsigned long __cil_tmp34 ;
3471 unsigned long __cil_tmp35 ;
3472 unsigned long __cil_tmp36 ;
3473 struct device *__cil_tmp37 ;
3474 unsigned long __cil_tmp38 ;
3475 unsigned long __cil_tmp39 ;
3476 struct rtc_device *__cil_tmp40 ;
3477 void const *__cil_tmp41 ;
3478 unsigned long __cil_tmp42 ;
3479 unsigned long __cil_tmp43 ;
3480 struct rtc_device *__cil_tmp44 ;
3481 void const *__cil_tmp45 ;
3482 unsigned int __cil_tmp46 ;
3483 irqreturn_t (*__cil_tmp47)(int , void * ) ;
3484 void *__cil_tmp48 ;
3485 unsigned long __cil_tmp49 ;
3486 unsigned long __cil_tmp50 ;
3487 struct device *__cil_tmp51 ;
3488 struct device const *__cil_tmp52 ;
3489
3490 {
3491 {
3492#line 412
3493 __cil_tmp11 = (unsigned long )pdev;
3494#line 412
3495 __cil_tmp12 = __cil_tmp11 + 16;
3496#line 412
3497 __cil_tmp13 = *((struct device **)__cil_tmp12);
3498#line 412
3499 __cil_tmp14 = (struct device const *)__cil_tmp13;
3500#line 412
3501 tmp = dev_get_drvdata(__cil_tmp14);
3502#line 412
3503 wm831x = (struct wm831x *)tmp;
3504#line 414
3505 tmp___0 = platform_get_irq_byname(pdev, "ALM");
3506#line 414
3507 alm_irq = tmp___0;
3508#line 415
3509 ret = 0;
3510#line 417
3511 __cil_tmp15 = (unsigned long )pdev;
3512#line 417
3513 __cil_tmp16 = __cil_tmp15 + 16;
3514#line 417
3515 __cil_tmp17 = (struct device *)__cil_tmp16;
3516#line 417
3517 tmp___1 = devm_kzalloc(__cil_tmp17, 24UL, 208U);
3518#line 417
3519 wm831x_rtc = (struct wm831x_rtc *)tmp___1;
3520 }
3521 {
3522#line 418
3523 __cil_tmp18 = (struct wm831x_rtc *)0;
3524#line 418
3525 __cil_tmp19 = (unsigned long )__cil_tmp18;
3526#line 418
3527 __cil_tmp20 = (unsigned long )wm831x_rtc;
3528#line 418
3529 if (__cil_tmp20 == __cil_tmp19) {
3530#line 419
3531 return (-12);
3532 } else {
3533
3534 }
3535 }
3536 {
3537#line 421
3538 __cil_tmp21 = (void *)wm831x_rtc;
3539#line 421
3540 platform_set_drvdata(pdev, __cil_tmp21);
3541#line 422
3542 *((struct wm831x **)wm831x_rtc) = wm831x;
3543#line 424
3544 ret = wm831x_reg_read(wm831x, (unsigned short)16421);
3545 }
3546#line 425
3547 if (ret < 0) {
3548 {
3549#line 426
3550 __cil_tmp22 = (unsigned long )pdev;
3551#line 426
3552 __cil_tmp23 = __cil_tmp22 + 16;
3553#line 426
3554 __cil_tmp24 = (struct device *)__cil_tmp23;
3555#line 426
3556 __cil_tmp25 = (struct device const *)__cil_tmp24;
3557#line 426
3558 dev_err(__cil_tmp25, "Failed to read RTC control: %d\n", ret);
3559 }
3560#line 427
3561 goto err;
3562 } else {
3563
3564 }
3565 {
3566#line 429
3567 __cil_tmp26 = ret & 1024;
3568#line 429
3569 if (__cil_tmp26 != 0) {
3570#line 430
3571 __cil_tmp27 = (unsigned long )wm831x_rtc;
3572#line 430
3573 __cil_tmp28 = __cil_tmp27 + 16;
3574#line 430
3575 *((unsigned char *)__cil_tmp28) = (unsigned char)1;
3576 } else {
3577
3578 }
3579 }
3580 {
3581#line 432
3582 __cil_tmp29 = (unsigned long )pdev;
3583#line 432
3584 __cil_tmp30 = __cil_tmp29 + 16;
3585#line 432
3586 __cil_tmp31 = (struct device *)__cil_tmp30;
3587#line 432
3588 __cil_tmp32 = (bool )1;
3589#line 432
3590 device_init_wakeup(__cil_tmp31, __cil_tmp32);
3591#line 434
3592 __cil_tmp33 = (unsigned long )wm831x_rtc;
3593#line 434
3594 __cil_tmp34 = __cil_tmp33 + 8;
3595#line 434
3596 __cil_tmp35 = (unsigned long )pdev;
3597#line 434
3598 __cil_tmp36 = __cil_tmp35 + 16;
3599#line 434
3600 __cil_tmp37 = (struct device *)__cil_tmp36;
3601#line 434
3602 *((struct rtc_device **)__cil_tmp34) = rtc_device_register("wm831x", __cil_tmp37,
3603 & wm831x_rtc_ops, & __this_module);
3604#line 436
3605 __cil_tmp38 = (unsigned long )wm831x_rtc;
3606#line 436
3607 __cil_tmp39 = __cil_tmp38 + 8;
3608#line 436
3609 __cil_tmp40 = *((struct rtc_device **)__cil_tmp39);
3610#line 436
3611 __cil_tmp41 = (void const *)__cil_tmp40;
3612#line 436
3613 tmp___3 = IS_ERR(__cil_tmp41);
3614 }
3615#line 436
3616 if (tmp___3 != 0L) {
3617 {
3618#line 437
3619 __cil_tmp42 = (unsigned long )wm831x_rtc;
3620#line 437
3621 __cil_tmp43 = __cil_tmp42 + 8;
3622#line 437
3623 __cil_tmp44 = *((struct rtc_device **)__cil_tmp43);
3624#line 437
3625 __cil_tmp45 = (void const *)__cil_tmp44;
3626#line 437
3627 tmp___2 = PTR_ERR(__cil_tmp45);
3628#line 437
3629 ret = (int )tmp___2;
3630 }
3631#line 438
3632 goto err;
3633 } else {
3634
3635 }
3636 {
3637#line 441
3638 __cil_tmp46 = (unsigned int )alm_irq;
3639#line 441
3640 __cil_tmp47 = (irqreturn_t (*)(int , void * ))0;
3641#line 441
3642 __cil_tmp48 = (void *)wm831x_rtc;
3643#line 441
3644 ret = request_threaded_irq(__cil_tmp46, __cil_tmp47, & wm831x_alm_irq, 1UL, "RTC alarm",
3645 __cil_tmp48);
3646 }
3647#line 444
3648 if (ret != 0) {
3649 {
3650#line 445
3651 __cil_tmp49 = (unsigned long )pdev;
3652#line 445
3653 __cil_tmp50 = __cil_tmp49 + 16;
3654#line 445
3655 __cil_tmp51 = (struct device *)__cil_tmp50;
3656#line 445
3657 __cil_tmp52 = (struct device const *)__cil_tmp51;
3658#line 445
3659 dev_err(__cil_tmp52, "Failed to request alarm IRQ %d: %d\n", alm_irq, ret);
3660 }
3661 } else {
3662
3663 }
3664#line 449
3665 return (0);
3666 err: ;
3667#line 452
3668 return (ret);
3669}
3670}
3671#line 509
3672extern void ldv_check_final_state(void) ;
3673#line 512
3674extern void ldv_check_return_value(int ) ;
3675#line 515
3676extern void ldv_initialize(void) ;
3677#line 518
3678extern int __VERIFIER_nondet_int(void) ;
3679#line 521 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3680int LDV_IN_INTERRUPT ;
3681#line 524 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3682void main(void)
3683{ struct device *var_group1 ;
3684 struct rtc_time *var_group2 ;
3685 unsigned long var_wm831x_rtc_set_mmss_1_p1 ;
3686 struct rtc_wkalrm *var_group3 ;
3687 unsigned int var_wm831x_rtc_alarm_irq_enable_6_p1 ;
3688 struct platform_device *var_group4 ;
3689 int res_wm831x_rtc_probe_11 ;
3690 int var_wm831x_alm_irq_7_p0 ;
3691 void *var_wm831x_alm_irq_7_p1 ;
3692 int ldv_s_wm831x_rtc_driver_platform_driver ;
3693 int tmp ;
3694 int tmp___0 ;
3695
3696 {
3697 {
3698#line 1034
3699 ldv_s_wm831x_rtc_driver_platform_driver = 0;
3700#line 1020
3701 LDV_IN_INTERRUPT = 1;
3702#line 1029
3703 ldv_initialize();
3704 }
3705#line 1039
3706 goto ldv_21310;
3707 ldv_21309:
3708 {
3709#line 1043
3710 tmp = __VERIFIER_nondet_int();
3711 }
3712#line 1045
3713 if (tmp == 0) {
3714#line 1045
3715 goto case_0;
3716 } else
3717#line 1105
3718 if (tmp == 1) {
3719#line 1105
3720 goto case_1;
3721 } else
3722#line 1165
3723 if (tmp == 2) {
3724#line 1165
3725 goto case_2;
3726 } else
3727#line 1225
3728 if (tmp == 3) {
3729#line 1225
3730 goto case_3;
3731 } else
3732#line 1285
3733 if (tmp == 4) {
3734#line 1285
3735 goto case_4;
3736 } else
3737#line 1345
3738 if (tmp == 5) {
3739#line 1345
3740 goto case_5;
3741 } else
3742#line 1405
3743 if (tmp == 6) {
3744#line 1405
3745 goto case_6;
3746 } else
3747#line 1465
3748 if (tmp == 7) {
3749#line 1465
3750 goto case_7;
3751 } else
3752#line 1525
3753 if (tmp == 8) {
3754#line 1525
3755 goto case_8;
3756 } else
3757#line 1586
3758 if (tmp == 9) {
3759#line 1586
3760 goto case_9;
3761 } else {
3762 {
3763#line 1646
3764 goto switch_default;
3765#line 1043
3766 if (0) {
3767 case_0:
3768 {
3769#line 1089
3770 wm831x_rtc_readtime(var_group1, var_group2);
3771 }
3772#line 1104
3773 goto ldv_21297;
3774 case_1:
3775 {
3776#line 1149
3777 wm831x_rtc_set_mmss(var_group1, var_wm831x_rtc_set_mmss_1_p1);
3778 }
3779#line 1164
3780 goto ldv_21297;
3781 case_2:
3782 {
3783#line 1209
3784 wm831x_rtc_readalarm(var_group1, var_group3);
3785 }
3786#line 1224
3787 goto ldv_21297;
3788 case_3:
3789 {
3790#line 1269
3791 wm831x_rtc_setalarm(var_group1, var_group3);
3792 }
3793#line 1284
3794 goto ldv_21297;
3795 case_4:
3796 {
3797#line 1329
3798 wm831x_rtc_alarm_irq_enable(var_group1, var_wm831x_rtc_alarm_irq_enable_6_p1);
3799 }
3800#line 1344
3801 goto ldv_21297;
3802 case_5:
3803 {
3804#line 1390
3805 wm831x_rtc_suspend(var_group1);
3806 }
3807#line 1404
3808 goto ldv_21297;
3809 case_6:
3810 {
3811#line 1450
3812 wm831x_rtc_resume(var_group1);
3813 }
3814#line 1464
3815 goto ldv_21297;
3816 case_7:
3817 {
3818#line 1510
3819 wm831x_rtc_freeze(var_group1);
3820 }
3821#line 1524
3822 goto ldv_21297;
3823 case_8: ;
3824#line 1528
3825 if (ldv_s_wm831x_rtc_driver_platform_driver == 0) {
3826 {
3827#line 1575
3828 res_wm831x_rtc_probe_11 = wm831x_rtc_probe(var_group4);
3829#line 1576
3830 ldv_check_return_value(res_wm831x_rtc_probe_11);
3831 }
3832#line 1577
3833 if (res_wm831x_rtc_probe_11 != 0) {
3834#line 1578
3835 goto ldv_module_exit;
3836 } else {
3837
3838 }
3839#line 1579
3840 ldv_s_wm831x_rtc_driver_platform_driver = 0;
3841 } else {
3842
3843 }
3844#line 1585
3845 goto ldv_21297;
3846 case_9:
3847 {
3848#line 1589
3849 LDV_IN_INTERRUPT = 2;
3850#line 1630
3851 wm831x_alm_irq(var_wm831x_alm_irq_7_p0, var_wm831x_alm_irq_7_p1);
3852#line 1639
3853 LDV_IN_INTERRUPT = 1;
3854 }
3855#line 1645
3856 goto ldv_21297;
3857 switch_default: ;
3858#line 1646
3859 goto ldv_21297;
3860 } else {
3861 switch_break: ;
3862 }
3863 }
3864 }
3865 ldv_21297: ;
3866 ldv_21310:
3867 {
3868#line 1039
3869 tmp___0 = __VERIFIER_nondet_int();
3870 }
3871#line 1039
3872 if (tmp___0 != 0) {
3873#line 1041
3874 goto ldv_21309;
3875 } else
3876#line 1039
3877 if (ldv_s_wm831x_rtc_driver_platform_driver != 0) {
3878#line 1041
3879 goto ldv_21309;
3880 } else {
3881#line 1043
3882 goto ldv_21311;
3883 }
3884 ldv_21311: ;
3885 ldv_module_exit: ;
3886 {
3887#line 1655
3888 ldv_check_final_state();
3889 }
3890#line 1658
3891 return;
3892}
3893}
3894#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3895void ldv_blast_assert(void)
3896{
3897
3898 {
3899 ERROR: ;
3900#line 6
3901 goto ERROR;
3902}
3903}
3904#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3905extern int __VERIFIER_nondet_int(void) ;
3906#line 1679 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3907int ldv_spin = 0;
3908#line 1683 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3909void ldv_check_alloc_flags(gfp_t flags )
3910{
3911
3912 {
3913#line 1686
3914 if (ldv_spin != 0) {
3915#line 1686
3916 if (flags != 32U) {
3917 {
3918#line 1686
3919 ldv_blast_assert();
3920 }
3921 } else {
3922
3923 }
3924 } else {
3925
3926 }
3927#line 1689
3928 return;
3929}
3930}
3931#line 1689
3932extern struct page *ldv_some_page(void) ;
3933#line 1692 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3934struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
3935{ struct page *tmp ;
3936
3937 {
3938#line 1695
3939 if (ldv_spin != 0) {
3940#line 1695
3941 if (flags != 32U) {
3942 {
3943#line 1695
3944 ldv_blast_assert();
3945 }
3946 } else {
3947
3948 }
3949 } else {
3950
3951 }
3952 {
3953#line 1697
3954 tmp = ldv_some_page();
3955 }
3956#line 1697
3957 return (tmp);
3958}
3959}
3960#line 1701 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3961void ldv_check_alloc_nonatomic(void)
3962{
3963
3964 {
3965#line 1704
3966 if (ldv_spin != 0) {
3967 {
3968#line 1704
3969 ldv_blast_assert();
3970 }
3971 } else {
3972
3973 }
3974#line 1707
3975 return;
3976}
3977}
3978#line 1708 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3979void ldv_spin_lock(void)
3980{
3981
3982 {
3983#line 1711
3984 ldv_spin = 1;
3985#line 1712
3986 return;
3987}
3988}
3989#line 1715 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
3990void ldv_spin_unlock(void)
3991{
3992
3993 {
3994#line 1718
3995 ldv_spin = 0;
3996#line 1719
3997 return;
3998}
3999}
4000#line 1722 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
4001int ldv_spin_trylock(void)
4002{ int is_lock ;
4003
4004 {
4005 {
4006#line 1727
4007 is_lock = __VERIFIER_nondet_int();
4008 }
4009#line 1729
4010 if (is_lock != 0) {
4011#line 1732
4012 return (0);
4013 } else {
4014#line 1737
4015 ldv_spin = 1;
4016#line 1739
4017 return (1);
4018 }
4019}
4020}
4021#line 1906 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2674/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-wm831x.c.p"
4022void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
4023{
4024
4025 {
4026 {
4027#line 1912
4028 ldv_check_alloc_flags(ldv_func_arg2);
4029#line 1914
4030 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
4031 }
4032#line 1915
4033 return ((void *)0);
4034}
4035}