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/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
883enum irqreturn {
884 IRQ_NONE = 0,
885 IRQ_HANDLED = 1,
886 IRQ_WAKE_THREAD = 2
887} ;
888#line 16 "include/linux/irqreturn.h"
889typedef enum irqreturn irqreturn_t;
890#line 41 "include/asm-generic/sections.h"
891struct exception_table_entry {
892 unsigned long insn ;
893 unsigned long fixup ;
894};
895#line 189 "include/linux/hardirq.h"
896struct timerqueue_node {
897 struct rb_node node ;
898 ktime_t expires ;
899};
900#line 12 "include/linux/timerqueue.h"
901struct timerqueue_head {
902 struct rb_root head ;
903 struct timerqueue_node *next ;
904};
905#line 50
906struct hrtimer_clock_base;
907#line 50
908struct hrtimer_clock_base;
909#line 51
910struct hrtimer_cpu_base;
911#line 51
912struct hrtimer_cpu_base;
913#line 60
914enum hrtimer_restart {
915 HRTIMER_NORESTART = 0,
916 HRTIMER_RESTART = 1
917} ;
918#line 65 "include/linux/timerqueue.h"
919struct hrtimer {
920 struct timerqueue_node node ;
921 ktime_t _softexpires ;
922 enum hrtimer_restart (*function)(struct hrtimer * ) ;
923 struct hrtimer_clock_base *base ;
924 unsigned long state ;
925 int start_pid ;
926 void *start_site ;
927 char start_comm[16U] ;
928};
929#line 132 "include/linux/hrtimer.h"
930struct hrtimer_clock_base {
931 struct hrtimer_cpu_base *cpu_base ;
932 int index ;
933 clockid_t clockid ;
934 struct timerqueue_head active ;
935 ktime_t resolution ;
936 ktime_t (*get_time)(void) ;
937 ktime_t softirq_time ;
938 ktime_t offset ;
939};
940#line 162 "include/linux/hrtimer.h"
941struct hrtimer_cpu_base {
942 raw_spinlock_t lock ;
943 unsigned long active_bases ;
944 ktime_t expires_next ;
945 int hres_active ;
946 int hang_detected ;
947 unsigned long nr_events ;
948 unsigned long nr_retries ;
949 unsigned long nr_hangs ;
950 ktime_t max_hang_time ;
951 struct hrtimer_clock_base clock_base[3U] ;
952};
953#line 702 "include/linux/interrupt.h"
954struct mc13xxx;
955#line 702
956struct mc13xxx;
957#line 42 "include/linux/mfd/mc13xxx.h"
958struct device_node;
959#line 185
960struct klist_node;
961#line 185
962struct klist_node;
963#line 37 "include/linux/klist.h"
964struct klist_node {
965 void *n_klist ;
966 struct list_head n_node ;
967 struct kref n_ref ;
968};
969#line 67
970struct dma_map_ops;
971#line 67 "include/linux/klist.h"
972struct dev_archdata {
973 void *acpi_handle ;
974 struct dma_map_ops *dma_ops ;
975 void *iommu ;
976};
977#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
978struct pdev_archdata {
979
980};
981#line 17
982struct device_private;
983#line 17
984struct device_private;
985#line 18
986struct device_driver;
987#line 18
988struct device_driver;
989#line 19
990struct driver_private;
991#line 19
992struct driver_private;
993#line 20
994struct class;
995#line 20
996struct class;
997#line 21
998struct subsys_private;
999#line 21
1000struct subsys_private;
1001#line 22
1002struct bus_type;
1003#line 22
1004struct bus_type;
1005#line 23
1006struct iommu_ops;
1007#line 23
1008struct iommu_ops;
1009#line 24 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
1010struct bus_attribute {
1011 struct attribute attr ;
1012 ssize_t (*show)(struct bus_type * , char * ) ;
1013 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
1014};
1015#line 51 "include/linux/device.h"
1016struct device_attribute;
1017#line 51
1018struct driver_attribute;
1019#line 51 "include/linux/device.h"
1020struct bus_type {
1021 char const *name ;
1022 char const *dev_name ;
1023 struct device *dev_root ;
1024 struct bus_attribute *bus_attrs ;
1025 struct device_attribute *dev_attrs ;
1026 struct driver_attribute *drv_attrs ;
1027 int (*match)(struct device * , struct device_driver * ) ;
1028 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1029 int (*probe)(struct device * ) ;
1030 int (*remove)(struct device * ) ;
1031 void (*shutdown)(struct device * ) ;
1032 int (*suspend)(struct device * , pm_message_t ) ;
1033 int (*resume)(struct device * ) ;
1034 struct dev_pm_ops const *pm ;
1035 struct iommu_ops *iommu_ops ;
1036 struct subsys_private *p ;
1037};
1038#line 125
1039struct device_type;
1040#line 182
1041struct of_device_id;
1042#line 182 "include/linux/device.h"
1043struct device_driver {
1044 char const *name ;
1045 struct bus_type *bus ;
1046 struct module *owner ;
1047 char const *mod_name ;
1048 bool suppress_bind_attrs ;
1049 struct of_device_id const *of_match_table ;
1050 int (*probe)(struct device * ) ;
1051 int (*remove)(struct device * ) ;
1052 void (*shutdown)(struct device * ) ;
1053 int (*suspend)(struct device * , pm_message_t ) ;
1054 int (*resume)(struct device * ) ;
1055 struct attribute_group const **groups ;
1056 struct dev_pm_ops const *pm ;
1057 struct driver_private *p ;
1058};
1059#line 245 "include/linux/device.h"
1060struct driver_attribute {
1061 struct attribute attr ;
1062 ssize_t (*show)(struct device_driver * , char * ) ;
1063 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
1064};
1065#line 299
1066struct class_attribute;
1067#line 299 "include/linux/device.h"
1068struct class {
1069 char const *name ;
1070 struct module *owner ;
1071 struct class_attribute *class_attrs ;
1072 struct device_attribute *dev_attrs ;
1073 struct bin_attribute *dev_bin_attrs ;
1074 struct kobject *dev_kobj ;
1075 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
1076 char *(*devnode)(struct device * , umode_t * ) ;
1077 void (*class_release)(struct class * ) ;
1078 void (*dev_release)(struct device * ) ;
1079 int (*suspend)(struct device * , pm_message_t ) ;
1080 int (*resume)(struct device * ) ;
1081 struct kobj_ns_type_operations const *ns_type ;
1082 void const *(*namespace)(struct device * ) ;
1083 struct dev_pm_ops const *pm ;
1084 struct subsys_private *p ;
1085};
1086#line 394 "include/linux/device.h"
1087struct class_attribute {
1088 struct attribute attr ;
1089 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
1090 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
1091 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
1092};
1093#line 447 "include/linux/device.h"
1094struct device_type {
1095 char const *name ;
1096 struct attribute_group const **groups ;
1097 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1098 char *(*devnode)(struct device * , umode_t * ) ;
1099 void (*release)(struct device * ) ;
1100 struct dev_pm_ops const *pm ;
1101};
1102#line 474 "include/linux/device.h"
1103struct device_attribute {
1104 struct attribute attr ;
1105 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
1106 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
1107 size_t ) ;
1108};
1109#line 557 "include/linux/device.h"
1110struct device_dma_parameters {
1111 unsigned int max_segment_size ;
1112 unsigned long segment_boundary_mask ;
1113};
1114#line 567
1115struct dma_coherent_mem;
1116#line 567 "include/linux/device.h"
1117struct device {
1118 struct device *parent ;
1119 struct device_private *p ;
1120 struct kobject kobj ;
1121 char const *init_name ;
1122 struct device_type const *type ;
1123 struct mutex mutex ;
1124 struct bus_type *bus ;
1125 struct device_driver *driver ;
1126 void *platform_data ;
1127 struct dev_pm_info power ;
1128 struct dev_pm_domain *pm_domain ;
1129 int numa_node ;
1130 u64 *dma_mask ;
1131 u64 coherent_dma_mask ;
1132 struct device_dma_parameters *dma_parms ;
1133 struct list_head dma_pools ;
1134 struct dma_coherent_mem *dma_mem ;
1135 struct dev_archdata archdata ;
1136 struct device_node *of_node ;
1137 dev_t devt ;
1138 u32 id ;
1139 spinlock_t devres_lock ;
1140 struct list_head devres_head ;
1141 struct klist_node knode_class ;
1142 struct class *class ;
1143 struct attribute_group const **groups ;
1144 void (*release)(struct device * ) ;
1145};
1146#line 681 "include/linux/device.h"
1147struct wakeup_source {
1148 char const *name ;
1149 struct list_head entry ;
1150 spinlock_t lock ;
1151 struct timer_list timer ;
1152 unsigned long timer_expires ;
1153 ktime_t total_time ;
1154 ktime_t max_time ;
1155 ktime_t last_time ;
1156 unsigned long event_count ;
1157 unsigned long active_count ;
1158 unsigned long relax_count ;
1159 unsigned long hit_count ;
1160 unsigned char active : 1 ;
1161};
1162#line 12 "include/linux/mod_devicetable.h"
1163typedef unsigned long kernel_ulong_t;
1164#line 215 "include/linux/mod_devicetable.h"
1165struct of_device_id {
1166 char name[32U] ;
1167 char type[32U] ;
1168 char compatible[128U] ;
1169 void *data ;
1170};
1171#line 492 "include/linux/mod_devicetable.h"
1172struct platform_device_id {
1173 char name[20U] ;
1174 kernel_ulong_t driver_data ;
1175};
1176#line 584
1177struct mfd_cell;
1178#line 584
1179struct mfd_cell;
1180#line 585 "include/linux/mod_devicetable.h"
1181struct platform_device {
1182 char const *name ;
1183 int id ;
1184 struct device dev ;
1185 u32 num_resources ;
1186 struct resource *resource ;
1187 struct platform_device_id const *id_entry ;
1188 struct mfd_cell *mfd_cell ;
1189 struct pdev_archdata archdata ;
1190};
1191#line 163 "include/linux/platform_device.h"
1192struct platform_driver {
1193 int (*probe)(struct platform_device * ) ;
1194 int (*remove)(struct platform_device * ) ;
1195 void (*shutdown)(struct platform_device * ) ;
1196 int (*suspend)(struct platform_device * , pm_message_t ) ;
1197 int (*resume)(struct platform_device * ) ;
1198 struct device_driver driver ;
1199 struct platform_device_id const *id_table ;
1200};
1201#line 272 "include/linux/platform_device.h"
1202struct rtc_time {
1203 int tm_sec ;
1204 int tm_min ;
1205 int tm_hour ;
1206 int tm_mday ;
1207 int tm_mon ;
1208 int tm_year ;
1209 int tm_wday ;
1210 int tm_yday ;
1211 int tm_isdst ;
1212};
1213#line 31 "include/linux/rtc.h"
1214struct rtc_wkalrm {
1215 unsigned char enabled ;
1216 unsigned char pending ;
1217 struct rtc_time time ;
1218};
1219#line 115
1220struct path;
1221#line 115
1222struct path;
1223#line 116
1224struct inode;
1225#line 116
1226struct inode;
1227#line 117
1228struct dentry;
1229#line 117
1230struct dentry;
1231#line 118 "include/linux/rtc.h"
1232struct seq_file {
1233 char *buf ;
1234 size_t size ;
1235 size_t from ;
1236 size_t count ;
1237 loff_t index ;
1238 loff_t read_pos ;
1239 u64 version ;
1240 struct mutex lock ;
1241 struct seq_operations const *op ;
1242 int poll_event ;
1243 void *private ;
1244};
1245#line 30 "include/linux/seq_file.h"
1246struct seq_operations {
1247 void *(*start)(struct seq_file * , loff_t * ) ;
1248 void (*stop)(struct seq_file * , void * ) ;
1249 void *(*next)(struct seq_file * , void * , loff_t * ) ;
1250 int (*show)(struct seq_file * , void * ) ;
1251};
1252#line 89 "include/linux/kdev_t.h"
1253struct file_operations;
1254#line 89
1255struct file_operations;
1256#line 90 "include/linux/kdev_t.h"
1257struct cdev {
1258 struct kobject kobj ;
1259 struct module *owner ;
1260 struct file_operations const *ops ;
1261 struct list_head list ;
1262 dev_t dev ;
1263 unsigned int count ;
1264};
1265#line 33 "include/linux/cdev.h"
1266struct backing_dev_info;
1267#line 41 "include/asm-generic/poll.h"
1268struct block_device;
1269#line 41
1270struct block_device;
1271#line 93 "include/linux/bit_spinlock.h"
1272struct hlist_bl_node;
1273#line 93 "include/linux/bit_spinlock.h"
1274struct hlist_bl_head {
1275 struct hlist_bl_node *first ;
1276};
1277#line 36 "include/linux/list_bl.h"
1278struct hlist_bl_node {
1279 struct hlist_bl_node *next ;
1280 struct hlist_bl_node **pprev ;
1281};
1282#line 114 "include/linux/rculist_bl.h"
1283struct nameidata;
1284#line 114
1285struct nameidata;
1286#line 115
1287struct vfsmount;
1288#line 115
1289struct vfsmount;
1290#line 116 "include/linux/rculist_bl.h"
1291struct qstr {
1292 unsigned int hash ;
1293 unsigned int len ;
1294 unsigned char const *name ;
1295};
1296#line 72 "include/linux/dcache.h"
1297struct dentry_operations;
1298#line 72
1299struct super_block;
1300#line 72 "include/linux/dcache.h"
1301union __anonunion_d_u_137 {
1302 struct list_head d_child ;
1303 struct rcu_head d_rcu ;
1304};
1305#line 72 "include/linux/dcache.h"
1306struct dentry {
1307 unsigned int d_flags ;
1308 seqcount_t d_seq ;
1309 struct hlist_bl_node d_hash ;
1310 struct dentry *d_parent ;
1311 struct qstr d_name ;
1312 struct inode *d_inode ;
1313 unsigned char d_iname[32U] ;
1314 unsigned int d_count ;
1315 spinlock_t d_lock ;
1316 struct dentry_operations const *d_op ;
1317 struct super_block *d_sb ;
1318 unsigned long d_time ;
1319 void *d_fsdata ;
1320 struct list_head d_lru ;
1321 union __anonunion_d_u_137 d_u ;
1322 struct list_head d_subdirs ;
1323 struct list_head d_alias ;
1324};
1325#line 123 "include/linux/dcache.h"
1326struct dentry_operations {
1327 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1328 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
1329 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
1330 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
1331 int (*d_delete)(struct dentry const * ) ;
1332 void (*d_release)(struct dentry * ) ;
1333 void (*d_prune)(struct dentry * ) ;
1334 void (*d_iput)(struct dentry * , struct inode * ) ;
1335 char *(*d_dname)(struct dentry * , char * , int ) ;
1336 struct vfsmount *(*d_automount)(struct path * ) ;
1337 int (*d_manage)(struct dentry * , bool ) ;
1338};
1339#line 402 "include/linux/dcache.h"
1340struct path {
1341 struct vfsmount *mnt ;
1342 struct dentry *dentry ;
1343};
1344#line 58 "include/linux/radix-tree.h"
1345struct radix_tree_node;
1346#line 58 "include/linux/radix-tree.h"
1347struct radix_tree_root {
1348 unsigned int height ;
1349 gfp_t gfp_mask ;
1350 struct radix_tree_node *rnode ;
1351};
1352#line 377
1353struct prio_tree_node;
1354#line 19 "include/linux/prio_tree.h"
1355struct prio_tree_node {
1356 struct prio_tree_node *left ;
1357 struct prio_tree_node *right ;
1358 struct prio_tree_node *parent ;
1359 unsigned long start ;
1360 unsigned long last ;
1361};
1362#line 27 "include/linux/prio_tree.h"
1363struct prio_tree_root {
1364 struct prio_tree_node *prio_tree_node ;
1365 unsigned short index_bits ;
1366 unsigned short raw ;
1367};
1368#line 111
1369enum pid_type {
1370 PIDTYPE_PID = 0,
1371 PIDTYPE_PGID = 1,
1372 PIDTYPE_SID = 2,
1373 PIDTYPE_MAX = 3
1374} ;
1375#line 118
1376struct pid_namespace;
1377#line 118 "include/linux/prio_tree.h"
1378struct upid {
1379 int nr ;
1380 struct pid_namespace *ns ;
1381 struct hlist_node pid_chain ;
1382};
1383#line 56 "include/linux/pid.h"
1384struct pid {
1385 atomic_t count ;
1386 unsigned int level ;
1387 struct hlist_head tasks[3U] ;
1388 struct rcu_head rcu ;
1389 struct upid numbers[1U] ;
1390};
1391#line 45 "include/linux/semaphore.h"
1392struct fiemap_extent {
1393 __u64 fe_logical ;
1394 __u64 fe_physical ;
1395 __u64 fe_length ;
1396 __u64 fe_reserved64[2U] ;
1397 __u32 fe_flags ;
1398 __u32 fe_reserved[3U] ;
1399};
1400#line 38 "include/linux/fiemap.h"
1401struct shrink_control {
1402 gfp_t gfp_mask ;
1403 unsigned long nr_to_scan ;
1404};
1405#line 14 "include/linux/shrinker.h"
1406struct shrinker {
1407 int (*shrink)(struct shrinker * , struct shrink_control * ) ;
1408 int seeks ;
1409 long batch ;
1410 struct list_head list ;
1411 atomic_long_t nr_in_batch ;
1412};
1413#line 43
1414enum migrate_mode {
1415 MIGRATE_ASYNC = 0,
1416 MIGRATE_SYNC_LIGHT = 1,
1417 MIGRATE_SYNC = 2
1418} ;
1419#line 49
1420struct export_operations;
1421#line 49
1422struct export_operations;
1423#line 51
1424struct iovec;
1425#line 51
1426struct iovec;
1427#line 52
1428struct kiocb;
1429#line 52
1430struct kiocb;
1431#line 53
1432struct pipe_inode_info;
1433#line 53
1434struct pipe_inode_info;
1435#line 54
1436struct poll_table_struct;
1437#line 54
1438struct poll_table_struct;
1439#line 55
1440struct kstatfs;
1441#line 55
1442struct kstatfs;
1443#line 435 "include/linux/fs.h"
1444struct iattr {
1445 unsigned int ia_valid ;
1446 umode_t ia_mode ;
1447 uid_t ia_uid ;
1448 gid_t ia_gid ;
1449 loff_t ia_size ;
1450 struct timespec ia_atime ;
1451 struct timespec ia_mtime ;
1452 struct timespec ia_ctime ;
1453 struct file *ia_file ;
1454};
1455#line 119 "include/linux/quota.h"
1456struct if_dqinfo {
1457 __u64 dqi_bgrace ;
1458 __u64 dqi_igrace ;
1459 __u32 dqi_flags ;
1460 __u32 dqi_valid ;
1461};
1462#line 176 "include/linux/percpu_counter.h"
1463struct fs_disk_quota {
1464 __s8 d_version ;
1465 __s8 d_flags ;
1466 __u16 d_fieldmask ;
1467 __u32 d_id ;
1468 __u64 d_blk_hardlimit ;
1469 __u64 d_blk_softlimit ;
1470 __u64 d_ino_hardlimit ;
1471 __u64 d_ino_softlimit ;
1472 __u64 d_bcount ;
1473 __u64 d_icount ;
1474 __s32 d_itimer ;
1475 __s32 d_btimer ;
1476 __u16 d_iwarns ;
1477 __u16 d_bwarns ;
1478 __s32 d_padding2 ;
1479 __u64 d_rtb_hardlimit ;
1480 __u64 d_rtb_softlimit ;
1481 __u64 d_rtbcount ;
1482 __s32 d_rtbtimer ;
1483 __u16 d_rtbwarns ;
1484 __s16 d_padding3 ;
1485 char d_padding4[8U] ;
1486};
1487#line 75 "include/linux/dqblk_xfs.h"
1488struct fs_qfilestat {
1489 __u64 qfs_ino ;
1490 __u64 qfs_nblks ;
1491 __u32 qfs_nextents ;
1492};
1493#line 150 "include/linux/dqblk_xfs.h"
1494typedef struct fs_qfilestat fs_qfilestat_t;
1495#line 151 "include/linux/dqblk_xfs.h"
1496struct fs_quota_stat {
1497 __s8 qs_version ;
1498 __u16 qs_flags ;
1499 __s8 qs_pad ;
1500 fs_qfilestat_t qs_uquota ;
1501 fs_qfilestat_t qs_gquota ;
1502 __u32 qs_incoredqs ;
1503 __s32 qs_btimelimit ;
1504 __s32 qs_itimelimit ;
1505 __s32 qs_rtbtimelimit ;
1506 __u16 qs_bwarnlimit ;
1507 __u16 qs_iwarnlimit ;
1508};
1509#line 165
1510struct dquot;
1511#line 165
1512struct dquot;
1513#line 185 "include/linux/quota.h"
1514typedef __kernel_uid32_t qid_t;
1515#line 186 "include/linux/quota.h"
1516typedef long long qsize_t;
1517#line 189 "include/linux/quota.h"
1518struct mem_dqblk {
1519 qsize_t dqb_bhardlimit ;
1520 qsize_t dqb_bsoftlimit ;
1521 qsize_t dqb_curspace ;
1522 qsize_t dqb_rsvspace ;
1523 qsize_t dqb_ihardlimit ;
1524 qsize_t dqb_isoftlimit ;
1525 qsize_t dqb_curinodes ;
1526 time_t dqb_btime ;
1527 time_t dqb_itime ;
1528};
1529#line 211
1530struct quota_format_type;
1531#line 211
1532struct quota_format_type;
1533#line 212 "include/linux/quota.h"
1534struct mem_dqinfo {
1535 struct quota_format_type *dqi_format ;
1536 int dqi_fmt_id ;
1537 struct list_head dqi_dirty_list ;
1538 unsigned long dqi_flags ;
1539 unsigned int dqi_bgrace ;
1540 unsigned int dqi_igrace ;
1541 qsize_t dqi_maxblimit ;
1542 qsize_t dqi_maxilimit ;
1543 void *dqi_priv ;
1544};
1545#line 275 "include/linux/quota.h"
1546struct dquot {
1547 struct hlist_node dq_hash ;
1548 struct list_head dq_inuse ;
1549 struct list_head dq_free ;
1550 struct list_head dq_dirty ;
1551 struct mutex dq_lock ;
1552 atomic_t dq_count ;
1553 wait_queue_head_t dq_wait_unused ;
1554 struct super_block *dq_sb ;
1555 unsigned int dq_id ;
1556 loff_t dq_off ;
1557 unsigned long dq_flags ;
1558 short dq_type ;
1559 struct mem_dqblk dq_dqb ;
1560};
1561#line 303 "include/linux/quota.h"
1562struct quota_format_ops {
1563 int (*check_quota_file)(struct super_block * , int ) ;
1564 int (*read_file_info)(struct super_block * , int ) ;
1565 int (*write_file_info)(struct super_block * , int ) ;
1566 int (*free_file_info)(struct super_block * , int ) ;
1567 int (*read_dqblk)(struct dquot * ) ;
1568 int (*commit_dqblk)(struct dquot * ) ;
1569 int (*release_dqblk)(struct dquot * ) ;
1570};
1571#line 314 "include/linux/quota.h"
1572struct dquot_operations {
1573 int (*write_dquot)(struct dquot * ) ;
1574 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
1575 void (*destroy_dquot)(struct dquot * ) ;
1576 int (*acquire_dquot)(struct dquot * ) ;
1577 int (*release_dquot)(struct dquot * ) ;
1578 int (*mark_dirty)(struct dquot * ) ;
1579 int (*write_info)(struct super_block * , int ) ;
1580 qsize_t *(*get_reserved_space)(struct inode * ) ;
1581};
1582#line 328 "include/linux/quota.h"
1583struct quotactl_ops {
1584 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
1585 int (*quota_on_meta)(struct super_block * , int , int ) ;
1586 int (*quota_off)(struct super_block * , int ) ;
1587 int (*quota_sync)(struct super_block * , int , int ) ;
1588 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
1589 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
1590 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1591 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1592 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1593 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
1594};
1595#line 344 "include/linux/quota.h"
1596struct quota_format_type {
1597 int qf_fmt_id ;
1598 struct quota_format_ops const *qf_ops ;
1599 struct module *qf_owner ;
1600 struct quota_format_type *qf_next ;
1601};
1602#line 390 "include/linux/quota.h"
1603struct quota_info {
1604 unsigned int flags ;
1605 struct mutex dqio_mutex ;
1606 struct mutex dqonoff_mutex ;
1607 struct rw_semaphore dqptr_sem ;
1608 struct inode *files[2U] ;
1609 struct mem_dqinfo info[2U] ;
1610 struct quota_format_ops const *ops[2U] ;
1611};
1612#line 421
1613struct address_space;
1614#line 421
1615struct address_space;
1616#line 422
1617struct writeback_control;
1618#line 422
1619struct writeback_control;
1620#line 585 "include/linux/fs.h"
1621union __anonunion_arg_140 {
1622 char *buf ;
1623 void *data ;
1624};
1625#line 585 "include/linux/fs.h"
1626struct __anonstruct_read_descriptor_t_139 {
1627 size_t written ;
1628 size_t count ;
1629 union __anonunion_arg_140 arg ;
1630 int error ;
1631};
1632#line 585 "include/linux/fs.h"
1633typedef struct __anonstruct_read_descriptor_t_139 read_descriptor_t;
1634#line 588 "include/linux/fs.h"
1635struct address_space_operations {
1636 int (*writepage)(struct page * , struct writeback_control * ) ;
1637 int (*readpage)(struct file * , struct page * ) ;
1638 int (*writepages)(struct address_space * , struct writeback_control * ) ;
1639 int (*set_page_dirty)(struct page * ) ;
1640 int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1641 unsigned int ) ;
1642 int (*write_begin)(struct file * , struct address_space * , loff_t , unsigned int ,
1643 unsigned int , struct page ** , void ** ) ;
1644 int (*write_end)(struct file * , struct address_space * , loff_t , unsigned int ,
1645 unsigned int , struct page * , void * ) ;
1646 sector_t (*bmap)(struct address_space * , sector_t ) ;
1647 void (*invalidatepage)(struct page * , unsigned long ) ;
1648 int (*releasepage)(struct page * , gfp_t ) ;
1649 void (*freepage)(struct page * ) ;
1650 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const * , loff_t ,
1651 unsigned long ) ;
1652 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
1653 int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode ) ;
1654 int (*launder_page)(struct page * ) ;
1655 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
1656 int (*error_remove_page)(struct address_space * , struct page * ) ;
1657};
1658#line 642 "include/linux/fs.h"
1659struct address_space {
1660 struct inode *host ;
1661 struct radix_tree_root page_tree ;
1662 spinlock_t tree_lock ;
1663 unsigned int i_mmap_writable ;
1664 struct prio_tree_root i_mmap ;
1665 struct list_head i_mmap_nonlinear ;
1666 struct mutex i_mmap_mutex ;
1667 unsigned long nrpages ;
1668 unsigned long writeback_index ;
1669 struct address_space_operations const *a_ops ;
1670 unsigned long flags ;
1671 struct backing_dev_info *backing_dev_info ;
1672 spinlock_t private_lock ;
1673 struct list_head private_list ;
1674 struct address_space *assoc_mapping ;
1675};
1676#line 664
1677struct request_queue;
1678#line 664
1679struct request_queue;
1680#line 665
1681struct hd_struct;
1682#line 665
1683struct gendisk;
1684#line 665 "include/linux/fs.h"
1685struct block_device {
1686 dev_t bd_dev ;
1687 int bd_openers ;
1688 struct inode *bd_inode ;
1689 struct super_block *bd_super ;
1690 struct mutex bd_mutex ;
1691 struct list_head bd_inodes ;
1692 void *bd_claiming ;
1693 void *bd_holder ;
1694 int bd_holders ;
1695 bool bd_write_holder ;
1696 struct list_head bd_holder_disks ;
1697 struct block_device *bd_contains ;
1698 unsigned int bd_block_size ;
1699 struct hd_struct *bd_part ;
1700 unsigned int bd_part_count ;
1701 int bd_invalidated ;
1702 struct gendisk *bd_disk ;
1703 struct request_queue *bd_queue ;
1704 struct list_head bd_list ;
1705 unsigned long bd_private ;
1706 int bd_fsfreeze_count ;
1707 struct mutex bd_fsfreeze_mutex ;
1708};
1709#line 737
1710struct posix_acl;
1711#line 737
1712struct posix_acl;
1713#line 738
1714struct inode_operations;
1715#line 738 "include/linux/fs.h"
1716union __anonunion_ldv_18792_141 {
1717 unsigned int const i_nlink ;
1718 unsigned int __i_nlink ;
1719};
1720#line 738 "include/linux/fs.h"
1721union __anonunion_ldv_18811_142 {
1722 struct list_head i_dentry ;
1723 struct rcu_head i_rcu ;
1724};
1725#line 738
1726struct file_lock;
1727#line 738 "include/linux/fs.h"
1728union __anonunion_ldv_18827_143 {
1729 struct pipe_inode_info *i_pipe ;
1730 struct block_device *i_bdev ;
1731 struct cdev *i_cdev ;
1732};
1733#line 738 "include/linux/fs.h"
1734struct inode {
1735 umode_t i_mode ;
1736 unsigned short i_opflags ;
1737 uid_t i_uid ;
1738 gid_t i_gid ;
1739 unsigned int i_flags ;
1740 struct posix_acl *i_acl ;
1741 struct posix_acl *i_default_acl ;
1742 struct inode_operations const *i_op ;
1743 struct super_block *i_sb ;
1744 struct address_space *i_mapping ;
1745 void *i_security ;
1746 unsigned long i_ino ;
1747 union __anonunion_ldv_18792_141 ldv_18792 ;
1748 dev_t i_rdev ;
1749 struct timespec i_atime ;
1750 struct timespec i_mtime ;
1751 struct timespec i_ctime ;
1752 spinlock_t i_lock ;
1753 unsigned short i_bytes ;
1754 blkcnt_t i_blocks ;
1755 loff_t i_size ;
1756 unsigned long i_state ;
1757 struct mutex i_mutex ;
1758 unsigned long dirtied_when ;
1759 struct hlist_node i_hash ;
1760 struct list_head i_wb_list ;
1761 struct list_head i_lru ;
1762 struct list_head i_sb_list ;
1763 union __anonunion_ldv_18811_142 ldv_18811 ;
1764 atomic_t i_count ;
1765 unsigned int i_blkbits ;
1766 u64 i_version ;
1767 atomic_t i_dio_count ;
1768 atomic_t i_writecount ;
1769 struct file_operations const *i_fop ;
1770 struct file_lock *i_flock ;
1771 struct address_space i_data ;
1772 struct dquot *i_dquot[2U] ;
1773 struct list_head i_devices ;
1774 union __anonunion_ldv_18827_143 ldv_18827 ;
1775 __u32 i_generation ;
1776 __u32 i_fsnotify_mask ;
1777 struct hlist_head i_fsnotify_marks ;
1778 atomic_t i_readcount ;
1779 void *i_private ;
1780};
1781#line 941 "include/linux/fs.h"
1782struct fown_struct {
1783 rwlock_t lock ;
1784 struct pid *pid ;
1785 enum pid_type pid_type ;
1786 uid_t uid ;
1787 uid_t euid ;
1788 int signum ;
1789};
1790#line 949 "include/linux/fs.h"
1791struct file_ra_state {
1792 unsigned long start ;
1793 unsigned int size ;
1794 unsigned int async_size ;
1795 unsigned int ra_pages ;
1796 unsigned int mmap_miss ;
1797 loff_t prev_pos ;
1798};
1799#line 972 "include/linux/fs.h"
1800union __anonunion_f_u_144 {
1801 struct list_head fu_list ;
1802 struct rcu_head fu_rcuhead ;
1803};
1804#line 972 "include/linux/fs.h"
1805struct file {
1806 union __anonunion_f_u_144 f_u ;
1807 struct path f_path ;
1808 struct file_operations const *f_op ;
1809 spinlock_t f_lock ;
1810 int f_sb_list_cpu ;
1811 atomic_long_t f_count ;
1812 unsigned int f_flags ;
1813 fmode_t f_mode ;
1814 loff_t f_pos ;
1815 struct fown_struct f_owner ;
1816 struct cred const *f_cred ;
1817 struct file_ra_state f_ra ;
1818 u64 f_version ;
1819 void *f_security ;
1820 void *private_data ;
1821 struct list_head f_ep_links ;
1822 struct list_head f_tfile_llink ;
1823 struct address_space *f_mapping ;
1824 unsigned long f_mnt_write_state ;
1825};
1826#line 1111
1827struct files_struct;
1828#line 1111 "include/linux/fs.h"
1829typedef struct files_struct *fl_owner_t;
1830#line 1112 "include/linux/fs.h"
1831struct file_lock_operations {
1832 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1833 void (*fl_release_private)(struct file_lock * ) ;
1834};
1835#line 1117 "include/linux/fs.h"
1836struct lock_manager_operations {
1837 int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1838 void (*lm_notify)(struct file_lock * ) ;
1839 int (*lm_grant)(struct file_lock * , struct file_lock * , int ) ;
1840 void (*lm_release_private)(struct file_lock * ) ;
1841 void (*lm_break)(struct file_lock * ) ;
1842 int (*lm_change)(struct file_lock ** , int ) ;
1843};
1844#line 1134
1845struct nlm_lockowner;
1846#line 1134
1847struct nlm_lockowner;
1848#line 1135 "include/linux/fs.h"
1849struct nfs_lock_info {
1850 u32 state ;
1851 struct nlm_lockowner *owner ;
1852 struct list_head list ;
1853};
1854#line 14 "include/linux/nfs_fs_i.h"
1855struct nfs4_lock_state;
1856#line 14
1857struct nfs4_lock_state;
1858#line 15 "include/linux/nfs_fs_i.h"
1859struct nfs4_lock_info {
1860 struct nfs4_lock_state *owner ;
1861};
1862#line 19
1863struct fasync_struct;
1864#line 19 "include/linux/nfs_fs_i.h"
1865struct __anonstruct_afs_146 {
1866 struct list_head link ;
1867 int state ;
1868};
1869#line 19 "include/linux/nfs_fs_i.h"
1870union __anonunion_fl_u_145 {
1871 struct nfs_lock_info nfs_fl ;
1872 struct nfs4_lock_info nfs4_fl ;
1873 struct __anonstruct_afs_146 afs ;
1874};
1875#line 19 "include/linux/nfs_fs_i.h"
1876struct file_lock {
1877 struct file_lock *fl_next ;
1878 struct list_head fl_link ;
1879 struct list_head fl_block ;
1880 fl_owner_t fl_owner ;
1881 unsigned int fl_flags ;
1882 unsigned char fl_type ;
1883 unsigned int fl_pid ;
1884 struct pid *fl_nspid ;
1885 wait_queue_head_t fl_wait ;
1886 struct file *fl_file ;
1887 loff_t fl_start ;
1888 loff_t fl_end ;
1889 struct fasync_struct *fl_fasync ;
1890 unsigned long fl_break_time ;
1891 unsigned long fl_downgrade_time ;
1892 struct file_lock_operations const *fl_ops ;
1893 struct lock_manager_operations const *fl_lmops ;
1894 union __anonunion_fl_u_145 fl_u ;
1895};
1896#line 1221 "include/linux/fs.h"
1897struct fasync_struct {
1898 spinlock_t fa_lock ;
1899 int magic ;
1900 int fa_fd ;
1901 struct fasync_struct *fa_next ;
1902 struct file *fa_file ;
1903 struct rcu_head fa_rcu ;
1904};
1905#line 1417
1906struct file_system_type;
1907#line 1417
1908struct super_operations;
1909#line 1417
1910struct xattr_handler;
1911#line 1417
1912struct mtd_info;
1913#line 1417 "include/linux/fs.h"
1914struct super_block {
1915 struct list_head s_list ;
1916 dev_t s_dev ;
1917 unsigned char s_dirt ;
1918 unsigned char s_blocksize_bits ;
1919 unsigned long s_blocksize ;
1920 loff_t s_maxbytes ;
1921 struct file_system_type *s_type ;
1922 struct super_operations const *s_op ;
1923 struct dquot_operations const *dq_op ;
1924 struct quotactl_ops const *s_qcop ;
1925 struct export_operations const *s_export_op ;
1926 unsigned long s_flags ;
1927 unsigned long s_magic ;
1928 struct dentry *s_root ;
1929 struct rw_semaphore s_umount ;
1930 struct mutex s_lock ;
1931 int s_count ;
1932 atomic_t s_active ;
1933 void *s_security ;
1934 struct xattr_handler const **s_xattr ;
1935 struct list_head s_inodes ;
1936 struct hlist_bl_head s_anon ;
1937 struct list_head *s_files ;
1938 struct list_head s_mounts ;
1939 struct list_head s_dentry_lru ;
1940 int s_nr_dentry_unused ;
1941 spinlock_t s_inode_lru_lock ;
1942 struct list_head s_inode_lru ;
1943 int s_nr_inodes_unused ;
1944 struct block_device *s_bdev ;
1945 struct backing_dev_info *s_bdi ;
1946 struct mtd_info *s_mtd ;
1947 struct hlist_node s_instances ;
1948 struct quota_info s_dquot ;
1949 int s_frozen ;
1950 wait_queue_head_t s_wait_unfrozen ;
1951 char s_id[32U] ;
1952 u8 s_uuid[16U] ;
1953 void *s_fs_info ;
1954 unsigned int s_max_links ;
1955 fmode_t s_mode ;
1956 u32 s_time_gran ;
1957 struct mutex s_vfs_rename_mutex ;
1958 char *s_subtype ;
1959 char *s_options ;
1960 struct dentry_operations const *s_d_op ;
1961 int cleancache_poolid ;
1962 struct shrinker s_shrink ;
1963 atomic_long_t s_remove_count ;
1964 int s_readonly_remount ;
1965};
1966#line 1563 "include/linux/fs.h"
1967struct fiemap_extent_info {
1968 unsigned int fi_flags ;
1969 unsigned int fi_extents_mapped ;
1970 unsigned int fi_extents_max ;
1971 struct fiemap_extent *fi_extents_start ;
1972};
1973#line 1602 "include/linux/fs.h"
1974struct file_operations {
1975 struct module *owner ;
1976 loff_t (*llseek)(struct file * , loff_t , int ) ;
1977 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
1978 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
1979 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
1980 loff_t ) ;
1981 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
1982 loff_t ) ;
1983 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
1984 loff_t , u64 , unsigned int ) ) ;
1985 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1986 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
1987 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
1988 int (*mmap)(struct file * , struct vm_area_struct * ) ;
1989 int (*open)(struct inode * , struct file * ) ;
1990 int (*flush)(struct file * , fl_owner_t ) ;
1991 int (*release)(struct inode * , struct file * ) ;
1992 int (*fsync)(struct file * , loff_t , loff_t , int ) ;
1993 int (*aio_fsync)(struct kiocb * , int ) ;
1994 int (*fasync)(int , struct file * , int ) ;
1995 int (*lock)(struct file * , int , struct file_lock * ) ;
1996 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
1997 int ) ;
1998 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
1999 unsigned long , unsigned long ) ;
2000 int (*check_flags)(int ) ;
2001 int (*flock)(struct file * , int , struct file_lock * ) ;
2002 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
2003 unsigned int ) ;
2004 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
2005 unsigned int ) ;
2006 int (*setlease)(struct file * , long , struct file_lock ** ) ;
2007 long (*fallocate)(struct file * , int , loff_t , loff_t ) ;
2008};
2009#line 1637 "include/linux/fs.h"
2010struct inode_operations {
2011 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
2012 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
2013 int (*permission)(struct inode * , int ) ;
2014 struct posix_acl *(*get_acl)(struct inode * , int ) ;
2015 int (*readlink)(struct dentry * , char * , int ) ;
2016 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
2017 int (*create)(struct inode * , struct dentry * , umode_t , struct nameidata * ) ;
2018 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
2019 int (*unlink)(struct inode * , struct dentry * ) ;
2020 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
2021 int (*mkdir)(struct inode * , struct dentry * , umode_t ) ;
2022 int (*rmdir)(struct inode * , struct dentry * ) ;
2023 int (*mknod)(struct inode * , struct dentry * , umode_t , dev_t ) ;
2024 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
2025 void (*truncate)(struct inode * ) ;
2026 int (*setattr)(struct dentry * , struct iattr * ) ;
2027 int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
2028 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
2029 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
2030 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
2031 int (*removexattr)(struct dentry * , char const * ) ;
2032 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
2033 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 , u64 ) ;
2034};
2035#line 1682 "include/linux/fs.h"
2036struct super_operations {
2037 struct inode *(*alloc_inode)(struct super_block * ) ;
2038 void (*destroy_inode)(struct inode * ) ;
2039 void (*dirty_inode)(struct inode * , int ) ;
2040 int (*write_inode)(struct inode * , struct writeback_control * ) ;
2041 int (*drop_inode)(struct inode * ) ;
2042 void (*evict_inode)(struct inode * ) ;
2043 void (*put_super)(struct super_block * ) ;
2044 void (*write_super)(struct super_block * ) ;
2045 int (*sync_fs)(struct super_block * , int ) ;
2046 int (*freeze_fs)(struct super_block * ) ;
2047 int (*unfreeze_fs)(struct super_block * ) ;
2048 int (*statfs)(struct dentry * , struct kstatfs * ) ;
2049 int (*remount_fs)(struct super_block * , int * , char * ) ;
2050 void (*umount_begin)(struct super_block * ) ;
2051 int (*show_options)(struct seq_file * , struct dentry * ) ;
2052 int (*show_devname)(struct seq_file * , struct dentry * ) ;
2053 int (*show_path)(struct seq_file * , struct dentry * ) ;
2054 int (*show_stats)(struct seq_file * , struct dentry * ) ;
2055 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
2056 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
2057 loff_t ) ;
2058 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
2059 int (*nr_cached_objects)(struct super_block * ) ;
2060 void (*free_cached_objects)(struct super_block * , int ) ;
2061};
2062#line 1834 "include/linux/fs.h"
2063struct file_system_type {
2064 char const *name ;
2065 int fs_flags ;
2066 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
2067 void (*kill_sb)(struct super_block * ) ;
2068 struct module *owner ;
2069 struct file_system_type *next ;
2070 struct hlist_head fs_supers ;
2071 struct lock_class_key s_lock_key ;
2072 struct lock_class_key s_umount_key ;
2073 struct lock_class_key s_vfs_rename_key ;
2074 struct lock_class_key i_lock_key ;
2075 struct lock_class_key i_mutex_key ;
2076 struct lock_class_key i_mutex_dir_key ;
2077};
2078#line 34 "include/linux/poll.h"
2079struct poll_table_struct {
2080 void (*_qproc)(struct file * , wait_queue_head_t * , struct poll_table_struct * ) ;
2081 unsigned long _key ;
2082};
2083#line 126 "include/linux/rtc.h"
2084struct rtc_class_ops {
2085 int (*open)(struct device * ) ;
2086 void (*release)(struct device * ) ;
2087 int (*ioctl)(struct device * , unsigned int , unsigned long ) ;
2088 int (*read_time)(struct device * , struct rtc_time * ) ;
2089 int (*set_time)(struct device * , struct rtc_time * ) ;
2090 int (*read_alarm)(struct device * , struct rtc_wkalrm * ) ;
2091 int (*set_alarm)(struct device * , struct rtc_wkalrm * ) ;
2092 int (*proc)(struct device * , struct seq_file * ) ;
2093 int (*set_mmss)(struct device * , unsigned long ) ;
2094 int (*read_callback)(struct device * , int ) ;
2095 int (*alarm_irq_enable)(struct device * , unsigned int ) ;
2096};
2097#line 156 "include/linux/rtc.h"
2098struct rtc_task {
2099 void (*func)(void * ) ;
2100 void *private_data ;
2101};
2102#line 162 "include/linux/rtc.h"
2103struct rtc_timer {
2104 struct rtc_task task ;
2105 struct timerqueue_node node ;
2106 ktime_t period ;
2107 int enabled ;
2108};
2109#line 170 "include/linux/rtc.h"
2110struct rtc_device {
2111 struct device dev ;
2112 struct module *owner ;
2113 int id ;
2114 char name[20U] ;
2115 struct rtc_class_ops const *ops ;
2116 struct mutex ops_lock ;
2117 struct cdev char_dev ;
2118 unsigned long flags ;
2119 unsigned long irq_data ;
2120 spinlock_t irq_lock ;
2121 wait_queue_head_t irq_queue ;
2122 struct fasync_struct *async_queue ;
2123 struct rtc_task *irq_task ;
2124 spinlock_t irq_task_lock ;
2125 int irq_freq ;
2126 int max_user_freq ;
2127 struct timerqueue_head timerqueue ;
2128 struct rtc_timer aie_timer ;
2129 struct rtc_timer uie_rtctimer ;
2130 struct hrtimer pie_timer ;
2131 int pie_enabled ;
2132 struct work_struct irqwork ;
2133 int uie_unsupported ;
2134 struct work_struct uie_task ;
2135 struct timer_list uie_timer ;
2136 unsigned int oldsecs ;
2137 unsigned char uie_irq_active : 1 ;
2138 unsigned char stop_uie_polling : 1 ;
2139 unsigned char uie_task_active : 1 ;
2140 unsigned char uie_timer_active : 1 ;
2141};
2142#line 278 "include/linux/rtc.h"
2143struct mc13xxx_rtc {
2144 struct rtc_device *rtc ;
2145 struct mc13xxx *mc13xxx ;
2146 int valid ;
2147};
2148#line 1 "<compiler builtins>"
2149long __builtin_expect(long , long ) ;
2150#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
2151void ldv_spin_lock(void) ;
2152#line 3
2153void ldv_spin_unlock(void) ;
2154#line 4
2155int ldv_spin_trylock(void) ;
2156#line 50 "include/linux/dynamic_debug.h"
2157extern int __dynamic_dev_dbg(struct _ddebug * , struct device const * , char const *
2158 , ...) ;
2159#line 27 "include/linux/err.h"
2160__inline static long PTR_ERR(void const *ptr )
2161{
2162
2163 {
2164#line 29
2165 return ((long )ptr);
2166}
2167}
2168#line 32 "include/linux/err.h"
2169__inline static long IS_ERR(void const *ptr )
2170{ long tmp ;
2171 unsigned long __cil_tmp3 ;
2172 int __cil_tmp4 ;
2173 long __cil_tmp5 ;
2174
2175 {
2176 {
2177#line 34
2178 __cil_tmp3 = (unsigned long )ptr;
2179#line 34
2180 __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;
2181#line 34
2182 __cil_tmp5 = (long )__cil_tmp4;
2183#line 34
2184 tmp = __builtin_expect(__cil_tmp5, 0L);
2185 }
2186#line 34
2187 return (tmp);
2188}
2189}
2190#line 26 "include/linux/export.h"
2191extern struct module __this_module ;
2192#line 161 "include/linux/slab.h"
2193extern void kfree(void const * ) ;
2194#line 220 "include/linux/slub_def.h"
2195extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
2196#line 223
2197void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
2198#line 353 "include/linux/slab.h"
2199__inline static void *kzalloc(size_t size , gfp_t flags ) ;
2200#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
2201extern void *__VERIFIER_nondet_pointer(void) ;
2202#line 11
2203void ldv_check_alloc_flags(gfp_t flags ) ;
2204#line 12
2205void ldv_check_alloc_nonatomic(void) ;
2206#line 14
2207struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
2208#line 16 "include/linux/mfd/mc13xxx.h"
2209extern void mc13xxx_lock(struct mc13xxx * ) ;
2210#line 17
2211extern void mc13xxx_unlock(struct mc13xxx * ) ;
2212#line 19
2213extern int mc13xxx_reg_read(struct mc13xxx * , unsigned int , u32 * ) ;
2214#line 20
2215extern int mc13xxx_reg_write(struct mc13xxx * , unsigned int , u32 ) ;
2216#line 26
2217extern int mc13xxx_irq_request(struct mc13xxx * , int , irqreturn_t (*)(int , void * ) ,
2218 char const * , void * ) ;
2219#line 28
2220extern int mc13xxx_irq_request_nounmask(struct mc13xxx * , int , irqreturn_t (*)(int ,
2221 void * ) ,
2222 char const * , void * ) ;
2223#line 30
2224extern int mc13xxx_irq_free(struct mc13xxx * , int , void * ) ;
2225#line 32
2226extern int mc13xxx_irq_mask(struct mc13xxx * , int ) ;
2227#line 33
2228extern int mc13xxx_irq_unmask(struct mc13xxx * , int ) ;
2229#line 34
2230extern int mc13xxx_irq_status(struct mc13xxx * , int , int * , int * ) ;
2231#line 36
2232extern int mc13xxx_irq_ack(struct mc13xxx * , int ) ;
2233#line 792 "include/linux/device.h"
2234extern void *dev_get_drvdata(struct device const * ) ;
2235#line 793
2236extern int dev_set_drvdata(struct device * , void * ) ;
2237#line 175 "include/linux/platform_device.h"
2238extern void platform_driver_unregister(struct platform_driver * ) ;
2239#line 180
2240extern int platform_driver_probe(struct platform_driver * , int (*)(struct platform_device * ) ) ;
2241#line 183 "include/linux/platform_device.h"
2242__inline static void *platform_get_drvdata(struct platform_device const *pdev )
2243{ void *tmp ;
2244 unsigned long __cil_tmp3 ;
2245 unsigned long __cil_tmp4 ;
2246 struct device const *__cil_tmp5 ;
2247
2248 {
2249 {
2250#line 185
2251 __cil_tmp3 = (unsigned long )pdev;
2252#line 185
2253 __cil_tmp4 = __cil_tmp3 + 16;
2254#line 185
2255 __cil_tmp5 = (struct device const *)__cil_tmp4;
2256#line 185
2257 tmp = dev_get_drvdata(__cil_tmp5);
2258 }
2259#line 185
2260 return (tmp);
2261}
2262}
2263#line 188 "include/linux/platform_device.h"
2264__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
2265{ unsigned long __cil_tmp3 ;
2266 unsigned long __cil_tmp4 ;
2267 struct device *__cil_tmp5 ;
2268
2269 {
2270 {
2271#line 190
2272 __cil_tmp3 = (unsigned long )pdev;
2273#line 190
2274 __cil_tmp4 = __cil_tmp3 + 16;
2275#line 190
2276 __cil_tmp5 = (struct device *)__cil_tmp4;
2277#line 190
2278 dev_set_drvdata(__cil_tmp5, data);
2279 }
2280#line 191
2281 return;
2282}
2283}
2284#line 110 "include/linux/rtc.h"
2285extern int rtc_valid_tm(struct rtc_time * ) ;
2286#line 111
2287extern int rtc_tm_to_time(struct rtc_time * , unsigned long * ) ;
2288#line 112
2289extern void rtc_time_to_tm(unsigned long , struct rtc_time * ) ;
2290#line 221
2291extern struct rtc_device *rtc_device_register(char const * , struct device * , struct rtc_class_ops const * ,
2292 struct module * ) ;
2293#line 225
2294extern void rtc_device_unregister(struct rtc_device * ) ;
2295#line 237
2296extern void rtc_update_irq(struct rtc_device * , unsigned long , unsigned long ) ;
2297#line 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
2298static int mc13xxx_rtc_irq_enable_unlocked(struct device *dev , unsigned int enabled ,
2299 int irq )
2300{ struct mc13xxx_rtc *priv ;
2301 void *tmp ;
2302 int (*func)(struct mc13xxx * , int ) ;
2303 int tmp___0 ;
2304 struct device const *__cil_tmp8 ;
2305 unsigned long __cil_tmp9 ;
2306 unsigned long __cil_tmp10 ;
2307 int __cil_tmp11 ;
2308 unsigned long __cil_tmp12 ;
2309 unsigned long __cil_tmp13 ;
2310 struct mc13xxx *__cil_tmp14 ;
2311
2312 {
2313 {
2314#line 50
2315 __cil_tmp8 = (struct device const *)dev;
2316#line 50
2317 tmp = dev_get_drvdata(__cil_tmp8);
2318#line 50
2319 priv = (struct mc13xxx_rtc *)tmp;
2320 }
2321 {
2322#line 53
2323 __cil_tmp9 = (unsigned long )priv;
2324#line 53
2325 __cil_tmp10 = __cil_tmp9 + 16;
2326#line 53
2327 __cil_tmp11 = *((int *)__cil_tmp10);
2328#line 53
2329 if (__cil_tmp11 == 0) {
2330#line 54
2331 return (-61);
2332 } else {
2333
2334 }
2335 }
2336#line 56
2337 if (enabled != 0U) {
2338#line 56
2339 func = & mc13xxx_irq_unmask;
2340 } else {
2341#line 56
2342 func = & mc13xxx_irq_mask;
2343 }
2344 {
2345#line 57
2346 __cil_tmp12 = (unsigned long )priv;
2347#line 57
2348 __cil_tmp13 = __cil_tmp12 + 8;
2349#line 57
2350 __cil_tmp14 = *((struct mc13xxx **)__cil_tmp13);
2351#line 57
2352 tmp___0 = (*func)(__cil_tmp14, irq);
2353 }
2354#line 57
2355 return (tmp___0);
2356}
2357}
2358#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
2359static int mc13xxx_rtc_irq_enable(struct device *dev , unsigned int enabled , int irq )
2360{ struct mc13xxx_rtc *priv ;
2361 void *tmp ;
2362 int ret ;
2363 struct device const *__cil_tmp7 ;
2364 unsigned long __cil_tmp8 ;
2365 unsigned long __cil_tmp9 ;
2366 struct mc13xxx *__cil_tmp10 ;
2367 unsigned long __cil_tmp11 ;
2368 unsigned long __cil_tmp12 ;
2369 struct mc13xxx *__cil_tmp13 ;
2370
2371 {
2372 {
2373#line 63
2374 __cil_tmp7 = (struct device const *)dev;
2375#line 63
2376 tmp = dev_get_drvdata(__cil_tmp7);
2377#line 63
2378 priv = (struct mc13xxx_rtc *)tmp;
2379#line 66
2380 __cil_tmp8 = (unsigned long )priv;
2381#line 66
2382 __cil_tmp9 = __cil_tmp8 + 8;
2383#line 66
2384 __cil_tmp10 = *((struct mc13xxx **)__cil_tmp9);
2385#line 66
2386 mc13xxx_lock(__cil_tmp10);
2387#line 68
2388 ret = mc13xxx_rtc_irq_enable_unlocked(dev, enabled, irq);
2389#line 70
2390 __cil_tmp11 = (unsigned long )priv;
2391#line 70
2392 __cil_tmp12 = __cil_tmp11 + 8;
2393#line 70
2394 __cil_tmp13 = *((struct mc13xxx **)__cil_tmp12);
2395#line 70
2396 mc13xxx_unlock(__cil_tmp13);
2397 }
2398#line 72
2399 return (ret);
2400}
2401}
2402#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
2403static int mc13xxx_rtc_read_time(struct device *dev , struct rtc_time *tm )
2404{ struct mc13xxx_rtc *priv ;
2405 void *tmp ;
2406 unsigned int seconds ;
2407 unsigned int days1 ;
2408 unsigned int days2 ;
2409 unsigned long s1970 ;
2410 int ret ;
2411 long tmp___0 ;
2412 long tmp___1 ;
2413 int tmp___2 ;
2414 struct device const *__cil_tmp13 ;
2415 unsigned long __cil_tmp14 ;
2416 unsigned long __cil_tmp15 ;
2417 struct mc13xxx *__cil_tmp16 ;
2418 unsigned long __cil_tmp17 ;
2419 unsigned long __cil_tmp18 ;
2420 int __cil_tmp19 ;
2421 unsigned long __cil_tmp20 ;
2422 unsigned long __cil_tmp21 ;
2423 struct mc13xxx *__cil_tmp22 ;
2424 int __cil_tmp23 ;
2425 long __cil_tmp24 ;
2426 unsigned long __cil_tmp25 ;
2427 unsigned long __cil_tmp26 ;
2428 struct mc13xxx *__cil_tmp27 ;
2429 int __cil_tmp28 ;
2430 long __cil_tmp29 ;
2431 unsigned long __cil_tmp30 ;
2432 unsigned long __cil_tmp31 ;
2433 struct mc13xxx *__cil_tmp32 ;
2434 unsigned long __cil_tmp33 ;
2435 unsigned long __cil_tmp34 ;
2436 struct mc13xxx *__cil_tmp35 ;
2437 unsigned int *__cil_tmp36 ;
2438 unsigned int __cil_tmp37 ;
2439 unsigned int *__cil_tmp38 ;
2440 unsigned int __cil_tmp39 ;
2441 unsigned int __cil_tmp40 ;
2442 unsigned int *__cil_tmp41 ;
2443 unsigned int __cil_tmp42 ;
2444 unsigned int *__cil_tmp43 ;
2445 unsigned int *__cil_tmp44 ;
2446 unsigned int *__cil_tmp45 ;
2447 unsigned int *__cil_tmp46 ;
2448 unsigned int *__cil_tmp47 ;
2449 unsigned int __cil_tmp48 ;
2450 unsigned int *__cil_tmp49 ;
2451 unsigned int __cil_tmp50 ;
2452 unsigned int *__cil_tmp51 ;
2453 unsigned int __cil_tmp52 ;
2454 unsigned int *__cil_tmp53 ;
2455 unsigned int __cil_tmp54 ;
2456 unsigned int __cil_tmp55 ;
2457 unsigned int __cil_tmp56 ;
2458
2459 {
2460 {
2461#line 77
2462 __cil_tmp13 = (struct device const *)dev;
2463#line 77
2464 tmp = dev_get_drvdata(__cil_tmp13);
2465#line 77
2466 priv = (struct mc13xxx_rtc *)tmp;
2467#line 82
2468 __cil_tmp14 = (unsigned long )priv;
2469#line 82
2470 __cil_tmp15 = __cil_tmp14 + 8;
2471#line 82
2472 __cil_tmp16 = *((struct mc13xxx **)__cil_tmp15);
2473#line 82
2474 mc13xxx_lock(__cil_tmp16);
2475 }
2476 {
2477#line 84
2478 __cil_tmp17 = (unsigned long )priv;
2479#line 84
2480 __cil_tmp18 = __cil_tmp17 + 16;
2481#line 84
2482 __cil_tmp19 = *((int *)__cil_tmp18);
2483#line 84
2484 if (__cil_tmp19 == 0) {
2485#line 85
2486 ret = -61;
2487#line 86
2488 goto out;
2489 } else {
2490
2491 }
2492 }
2493 {
2494#line 89
2495 __cil_tmp20 = (unsigned long )priv;
2496#line 89
2497 __cil_tmp21 = __cil_tmp20 + 8;
2498#line 89
2499 __cil_tmp22 = *((struct mc13xxx **)__cil_tmp21);
2500#line 89
2501 ret = mc13xxx_reg_read(__cil_tmp22, 22U, & days1);
2502#line 90
2503 __cil_tmp23 = ret != 0;
2504#line 90
2505 __cil_tmp24 = (long )__cil_tmp23;
2506#line 90
2507 tmp___0 = __builtin_expect(__cil_tmp24, 0L);
2508 }
2509#line 90
2510 if (tmp___0 != 0L) {
2511#line 91
2512 goto out;
2513 } else {
2514
2515 }
2516 {
2517#line 93
2518 __cil_tmp25 = (unsigned long )priv;
2519#line 93
2520 __cil_tmp26 = __cil_tmp25 + 8;
2521#line 93
2522 __cil_tmp27 = *((struct mc13xxx **)__cil_tmp26);
2523#line 93
2524 ret = mc13xxx_reg_read(__cil_tmp27, 20U, & seconds);
2525#line 94
2526 __cil_tmp28 = ret != 0;
2527#line 94
2528 __cil_tmp29 = (long )__cil_tmp28;
2529#line 94
2530 tmp___1 = __builtin_expect(__cil_tmp29, 0L);
2531 }
2532#line 94
2533 if (tmp___1 != 0L) {
2534#line 95
2535 goto out;
2536 } else {
2537
2538 }
2539 {
2540#line 97
2541 __cil_tmp30 = (unsigned long )priv;
2542#line 97
2543 __cil_tmp31 = __cil_tmp30 + 8;
2544#line 97
2545 __cil_tmp32 = *((struct mc13xxx **)__cil_tmp31);
2546#line 97
2547 ret = mc13xxx_reg_read(__cil_tmp32, 22U, & days2);
2548 }
2549 out:
2550 {
2551#line 99
2552 __cil_tmp33 = (unsigned long )priv;
2553#line 99
2554 __cil_tmp34 = __cil_tmp33 + 8;
2555#line 99
2556 __cil_tmp35 = *((struct mc13xxx **)__cil_tmp34);
2557#line 99
2558 mc13xxx_unlock(__cil_tmp35);
2559 }
2560#line 101
2561 if (ret != 0) {
2562#line 102
2563 return (ret);
2564 } else {
2565
2566 }
2567 {
2568#line 104
2569 __cil_tmp36 = & days2;
2570#line 104
2571 __cil_tmp37 = *__cil_tmp36;
2572#line 104
2573 __cil_tmp38 = & days1;
2574#line 104
2575 __cil_tmp39 = *__cil_tmp38;
2576#line 104
2577 __cil_tmp40 = __cil_tmp39 + 1U;
2578#line 104
2579 if (__cil_tmp40 == __cil_tmp37) {
2580 {
2581#line 105
2582 __cil_tmp41 = & seconds;
2583#line 105
2584 __cil_tmp42 = *__cil_tmp41;
2585#line 105
2586 if (__cil_tmp42 > 43199U) {
2587#line 106
2588 __cil_tmp43 = & days2;
2589#line 106
2590 __cil_tmp44 = & days1;
2591#line 106
2592 *__cil_tmp43 = *__cil_tmp44;
2593 } else {
2594#line 108
2595 __cil_tmp45 = & days1;
2596#line 108
2597 __cil_tmp46 = & days2;
2598#line 108
2599 *__cil_tmp45 = *__cil_tmp46;
2600 }
2601 }
2602 } else {
2603
2604 }
2605 }
2606 {
2607#line 111
2608 __cil_tmp47 = & days2;
2609#line 111
2610 __cil_tmp48 = *__cil_tmp47;
2611#line 111
2612 __cil_tmp49 = & days1;
2613#line 111
2614 __cil_tmp50 = *__cil_tmp49;
2615#line 111
2616 if (__cil_tmp50 != __cil_tmp48) {
2617#line 112
2618 return (-5);
2619 } else {
2620
2621 }
2622 }
2623 {
2624#line 114
2625 __cil_tmp51 = & seconds;
2626#line 114
2627 __cil_tmp52 = *__cil_tmp51;
2628#line 114
2629 __cil_tmp53 = & days1;
2630#line 114
2631 __cil_tmp54 = *__cil_tmp53;
2632#line 114
2633 __cil_tmp55 = __cil_tmp54 * 86400U;
2634#line 114
2635 __cil_tmp56 = __cil_tmp55 + __cil_tmp52;
2636#line 114
2637 s1970 = (unsigned long )__cil_tmp56;
2638#line 116
2639 rtc_time_to_tm(s1970, tm);
2640#line 118
2641 tmp___2 = rtc_valid_tm(tm);
2642 }
2643#line 118
2644 return (tmp___2);
2645}
2646}
2647#line 121 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
2648static int mc13xxx_rtc_set_mmss(struct device *dev , unsigned long secs )
2649{ struct mc13xxx_rtc *priv ;
2650 void *tmp ;
2651 unsigned int seconds ;
2652 unsigned int days ;
2653 unsigned int alarmseconds ;
2654 int ret ;
2655 long tmp___0 ;
2656 long tmp___1 ;
2657 long tmp___2 ;
2658 long tmp___3 ;
2659 long tmp___4 ;
2660 long tmp___5 ;
2661 long tmp___6 ;
2662 struct device const *__cil_tmp16 ;
2663 unsigned long __cil_tmp17 ;
2664 unsigned long __cil_tmp18 ;
2665 unsigned long __cil_tmp19 ;
2666 unsigned long __cil_tmp20 ;
2667 struct mc13xxx *__cil_tmp21 ;
2668 unsigned long __cil_tmp22 ;
2669 unsigned long __cil_tmp23 ;
2670 struct mc13xxx *__cil_tmp24 ;
2671 int __cil_tmp25 ;
2672 long __cil_tmp26 ;
2673 unsigned int *__cil_tmp27 ;
2674 unsigned int __cil_tmp28 ;
2675 unsigned long __cil_tmp29 ;
2676 unsigned long __cil_tmp30 ;
2677 struct mc13xxx *__cil_tmp31 ;
2678 int __cil_tmp32 ;
2679 long __cil_tmp33 ;
2680 unsigned long __cil_tmp34 ;
2681 unsigned long __cil_tmp35 ;
2682 struct mc13xxx *__cil_tmp36 ;
2683 int __cil_tmp37 ;
2684 long __cil_tmp38 ;
2685 unsigned long __cil_tmp39 ;
2686 unsigned long __cil_tmp40 ;
2687 struct mc13xxx *__cil_tmp41 ;
2688 int __cil_tmp42 ;
2689 long __cil_tmp43 ;
2690 unsigned long __cil_tmp44 ;
2691 unsigned long __cil_tmp45 ;
2692 struct mc13xxx *__cil_tmp46 ;
2693 int __cil_tmp47 ;
2694 long __cil_tmp48 ;
2695 unsigned int *__cil_tmp49 ;
2696 unsigned int __cil_tmp50 ;
2697 unsigned long __cil_tmp51 ;
2698 unsigned long __cil_tmp52 ;
2699 struct mc13xxx *__cil_tmp53 ;
2700 unsigned int *__cil_tmp54 ;
2701 unsigned int __cil_tmp55 ;
2702 int __cil_tmp56 ;
2703 long __cil_tmp57 ;
2704 unsigned long __cil_tmp58 ;
2705 unsigned long __cil_tmp59 ;
2706 struct mc13xxx *__cil_tmp60 ;
2707 int __cil_tmp61 ;
2708 long __cil_tmp62 ;
2709 unsigned long __cil_tmp63 ;
2710 unsigned long __cil_tmp64 ;
2711 struct mc13xxx *__cil_tmp65 ;
2712 unsigned long __cil_tmp66 ;
2713 unsigned long __cil_tmp67 ;
2714 unsigned long __cil_tmp68 ;
2715 unsigned long __cil_tmp69 ;
2716 struct mc13xxx *__cil_tmp70 ;
2717
2718 {
2719 {
2720#line 123
2721 __cil_tmp16 = (struct device const *)dev;
2722#line 123
2723 tmp = dev_get_drvdata(__cil_tmp16);
2724#line 123
2725 priv = (struct mc13xxx_rtc *)tmp;
2726#line 128
2727 __cil_tmp17 = secs % 86400UL;
2728#line 128
2729 seconds = (unsigned int )__cil_tmp17;
2730#line 129
2731 __cil_tmp18 = secs / 86400UL;
2732#line 129
2733 days = (unsigned int )__cil_tmp18;
2734#line 131
2735 __cil_tmp19 = (unsigned long )priv;
2736#line 131
2737 __cil_tmp20 = __cil_tmp19 + 8;
2738#line 131
2739 __cil_tmp21 = *((struct mc13xxx **)__cil_tmp20);
2740#line 131
2741 mc13xxx_lock(__cil_tmp21);
2742#line 137
2743 __cil_tmp22 = (unsigned long )priv;
2744#line 137
2745 __cil_tmp23 = __cil_tmp22 + 8;
2746#line 137
2747 __cil_tmp24 = *((struct mc13xxx **)__cil_tmp23);
2748#line 137
2749 ret = mc13xxx_reg_read(__cil_tmp24, 21U, & alarmseconds);
2750#line 138
2751 __cil_tmp25 = ret != 0;
2752#line 138
2753 __cil_tmp26 = (long )__cil_tmp25;
2754#line 138
2755 tmp___0 = __builtin_expect(__cil_tmp26, 0L);
2756 }
2757#line 138
2758 if (tmp___0 != 0L) {
2759#line 139
2760 goto out;
2761 } else {
2762
2763 }
2764 {
2765#line 141
2766 __cil_tmp27 = & alarmseconds;
2767#line 141
2768 __cil_tmp28 = *__cil_tmp27;
2769#line 141
2770 if (__cil_tmp28 <= 86399U) {
2771 {
2772#line 142
2773 __cil_tmp29 = (unsigned long )priv;
2774#line 142
2775 __cil_tmp30 = __cil_tmp29 + 8;
2776#line 142
2777 __cil_tmp31 = *((struct mc13xxx **)__cil_tmp30);
2778#line 142
2779 ret = mc13xxx_reg_write(__cil_tmp31, 21U, 131071U);
2780#line 144
2781 __cil_tmp32 = ret != 0;
2782#line 144
2783 __cil_tmp33 = (long )__cil_tmp32;
2784#line 144
2785 tmp___1 = __builtin_expect(__cil_tmp33, 0L);
2786 }
2787#line 144
2788 if (tmp___1 != 0L) {
2789#line 145
2790 goto out;
2791 } else {
2792
2793 }
2794 } else {
2795
2796 }
2797 }
2798 {
2799#line 152
2800 __cil_tmp34 = (unsigned long )priv;
2801#line 152
2802 __cil_tmp35 = __cil_tmp34 + 8;
2803#line 152
2804 __cil_tmp36 = *((struct mc13xxx **)__cil_tmp35);
2805#line 152
2806 ret = mc13xxx_reg_write(__cil_tmp36, 20U, 0U);
2807#line 153
2808 __cil_tmp37 = ret != 0;
2809#line 153
2810 __cil_tmp38 = (long )__cil_tmp37;
2811#line 153
2812 tmp___2 = __builtin_expect(__cil_tmp38, 0L);
2813 }
2814#line 153
2815 if (tmp___2 != 0L) {
2816#line 154
2817 goto out;
2818 } else {
2819
2820 }
2821 {
2822#line 156
2823 __cil_tmp39 = (unsigned long )priv;
2824#line 156
2825 __cil_tmp40 = __cil_tmp39 + 8;
2826#line 156
2827 __cil_tmp41 = *((struct mc13xxx **)__cil_tmp40);
2828#line 156
2829 ret = mc13xxx_reg_write(__cil_tmp41, 22U, days);
2830#line 157
2831 __cil_tmp42 = ret != 0;
2832#line 157
2833 __cil_tmp43 = (long )__cil_tmp42;
2834#line 157
2835 tmp___3 = __builtin_expect(__cil_tmp43, 0L);
2836 }
2837#line 157
2838 if (tmp___3 != 0L) {
2839#line 158
2840 goto out;
2841 } else {
2842
2843 }
2844 {
2845#line 160
2846 __cil_tmp44 = (unsigned long )priv;
2847#line 160
2848 __cil_tmp45 = __cil_tmp44 + 8;
2849#line 160
2850 __cil_tmp46 = *((struct mc13xxx **)__cil_tmp45);
2851#line 160
2852 ret = mc13xxx_reg_write(__cil_tmp46, 20U, seconds);
2853#line 161
2854 __cil_tmp47 = ret != 0;
2855#line 161
2856 __cil_tmp48 = (long )__cil_tmp47;
2857#line 161
2858 tmp___4 = __builtin_expect(__cil_tmp48, 0L);
2859 }
2860#line 161
2861 if (tmp___4 != 0L) {
2862#line 162
2863 goto out;
2864 } else {
2865
2866 }
2867 {
2868#line 165
2869 __cil_tmp49 = & alarmseconds;
2870#line 165
2871 __cil_tmp50 = *__cil_tmp49;
2872#line 165
2873 if (__cil_tmp50 <= 86399U) {
2874 {
2875#line 166
2876 __cil_tmp51 = (unsigned long )priv;
2877#line 166
2878 __cil_tmp52 = __cil_tmp51 + 8;
2879#line 166
2880 __cil_tmp53 = *((struct mc13xxx **)__cil_tmp52);
2881#line 166
2882 __cil_tmp54 = & alarmseconds;
2883#line 166
2884 __cil_tmp55 = *__cil_tmp54;
2885#line 166
2886 ret = mc13xxx_reg_write(__cil_tmp53, 21U, __cil_tmp55);
2887#line 168
2888 __cil_tmp56 = ret != 0;
2889#line 168
2890 __cil_tmp57 = (long )__cil_tmp56;
2891#line 168
2892 tmp___5 = __builtin_expect(__cil_tmp57, 0L);
2893 }
2894#line 168
2895 if (tmp___5 != 0L) {
2896#line 169
2897 goto out;
2898 } else {
2899
2900 }
2901 } else {
2902
2903 }
2904 }
2905 {
2906#line 172
2907 __cil_tmp58 = (unsigned long )priv;
2908#line 172
2909 __cil_tmp59 = __cil_tmp58 + 8;
2910#line 172
2911 __cil_tmp60 = *((struct mc13xxx **)__cil_tmp59);
2912#line 172
2913 ret = mc13xxx_irq_ack(__cil_tmp60, 31);
2914#line 173
2915 __cil_tmp61 = ret != 0;
2916#line 173
2917 __cil_tmp62 = (long )__cil_tmp61;
2918#line 173
2919 tmp___6 = __builtin_expect(__cil_tmp62, 0L);
2920 }
2921#line 173
2922 if (tmp___6 != 0L) {
2923#line 174
2924 goto out;
2925 } else {
2926
2927 }
2928 {
2929#line 176
2930 __cil_tmp63 = (unsigned long )priv;
2931#line 176
2932 __cil_tmp64 = __cil_tmp63 + 8;
2933#line 176
2934 __cil_tmp65 = *((struct mc13xxx **)__cil_tmp64);
2935#line 176
2936 ret = mc13xxx_irq_unmask(__cil_tmp65, 31);
2937 }
2938 out:
2939 {
2940#line 178
2941 __cil_tmp66 = (unsigned long )priv;
2942#line 178
2943 __cil_tmp67 = __cil_tmp66 + 16;
2944#line 178
2945 *((int *)__cil_tmp67) = ret == 0;
2946#line 180
2947 __cil_tmp68 = (unsigned long )priv;
2948#line 180
2949 __cil_tmp69 = __cil_tmp68 + 8;
2950#line 180
2951 __cil_tmp70 = *((struct mc13xxx **)__cil_tmp69);
2952#line 180
2953 mc13xxx_unlock(__cil_tmp70);
2954 }
2955#line 182
2956 return (ret);
2957}
2958}
2959#line 185 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
2960static int mc13xxx_rtc_read_alarm(struct device *dev , struct rtc_wkalrm *alarm )
2961{ struct mc13xxx_rtc *priv ;
2962 void *tmp ;
2963 unsigned int seconds ;
2964 unsigned int days ;
2965 unsigned long s1970 ;
2966 int enabled ;
2967 int pending ;
2968 int ret ;
2969 long tmp___0 ;
2970 long tmp___1 ;
2971 struct _ddebug descriptor ;
2972 long tmp___2 ;
2973 struct device const *__cil_tmp15 ;
2974 unsigned long __cil_tmp16 ;
2975 unsigned long __cil_tmp17 ;
2976 struct mc13xxx *__cil_tmp18 ;
2977 unsigned long __cil_tmp19 ;
2978 unsigned long __cil_tmp20 ;
2979 struct mc13xxx *__cil_tmp21 ;
2980 int __cil_tmp22 ;
2981 long __cil_tmp23 ;
2982 unsigned int *__cil_tmp24 ;
2983 unsigned int __cil_tmp25 ;
2984 unsigned long __cil_tmp26 ;
2985 unsigned long __cil_tmp27 ;
2986 struct mc13xxx *__cil_tmp28 ;
2987 int __cil_tmp29 ;
2988 long __cil_tmp30 ;
2989 unsigned long __cil_tmp31 ;
2990 unsigned long __cil_tmp32 ;
2991 struct mc13xxx *__cil_tmp33 ;
2992 unsigned long __cil_tmp34 ;
2993 unsigned long __cil_tmp35 ;
2994 struct mc13xxx *__cil_tmp36 ;
2995 int *__cil_tmp37 ;
2996 int __cil_tmp38 ;
2997 unsigned long __cil_tmp39 ;
2998 unsigned long __cil_tmp40 ;
2999 int *__cil_tmp41 ;
3000 int __cil_tmp42 ;
3001 unsigned int *__cil_tmp43 ;
3002 unsigned int __cil_tmp44 ;
3003 unsigned int *__cil_tmp45 ;
3004 unsigned int __cil_tmp46 ;
3005 unsigned int __cil_tmp47 ;
3006 unsigned int __cil_tmp48 ;
3007 unsigned long __cil_tmp49 ;
3008 unsigned long __cil_tmp50 ;
3009 struct rtc_time *__cil_tmp51 ;
3010 struct _ddebug *__cil_tmp52 ;
3011 unsigned long __cil_tmp53 ;
3012 unsigned long __cil_tmp54 ;
3013 unsigned long __cil_tmp55 ;
3014 unsigned long __cil_tmp56 ;
3015 unsigned long __cil_tmp57 ;
3016 unsigned long __cil_tmp58 ;
3017 unsigned char __cil_tmp59 ;
3018 long __cil_tmp60 ;
3019 long __cil_tmp61 ;
3020 struct device const *__cil_tmp62 ;
3021
3022 {
3023 {
3024#line 187
3025 __cil_tmp15 = (struct device const *)dev;
3026#line 187
3027 tmp = dev_get_drvdata(__cil_tmp15);
3028#line 187
3029 priv = (struct mc13xxx_rtc *)tmp;
3030#line 193
3031 __cil_tmp16 = (unsigned long )priv;
3032#line 193
3033 __cil_tmp17 = __cil_tmp16 + 8;
3034#line 193
3035 __cil_tmp18 = *((struct mc13xxx **)__cil_tmp17);
3036#line 193
3037 mc13xxx_lock(__cil_tmp18);
3038#line 195
3039 __cil_tmp19 = (unsigned long )priv;
3040#line 195
3041 __cil_tmp20 = __cil_tmp19 + 8;
3042#line 195
3043 __cil_tmp21 = *((struct mc13xxx **)__cil_tmp20);
3044#line 195
3045 ret = mc13xxx_reg_read(__cil_tmp21, 21U, & seconds);
3046#line 196
3047 __cil_tmp22 = ret != 0;
3048#line 196
3049 __cil_tmp23 = (long )__cil_tmp22;
3050#line 196
3051 tmp___0 = __builtin_expect(__cil_tmp23, 0L);
3052 }
3053#line 196
3054 if (tmp___0 != 0L) {
3055#line 197
3056 goto out;
3057 } else {
3058
3059 }
3060 {
3061#line 198
3062 __cil_tmp24 = & seconds;
3063#line 198
3064 __cil_tmp25 = *__cil_tmp24;
3065#line 198
3066 if (__cil_tmp25 > 86399U) {
3067#line 199
3068 ret = -61;
3069#line 200
3070 goto out;
3071 } else {
3072
3073 }
3074 }
3075 {
3076#line 203
3077 __cil_tmp26 = (unsigned long )priv;
3078#line 203
3079 __cil_tmp27 = __cil_tmp26 + 8;
3080#line 203
3081 __cil_tmp28 = *((struct mc13xxx **)__cil_tmp27);
3082#line 203
3083 ret = mc13xxx_reg_read(__cil_tmp28, 22U, & days);
3084#line 204
3085 __cil_tmp29 = ret != 0;
3086#line 204
3087 __cil_tmp30 = (long )__cil_tmp29;
3088#line 204
3089 tmp___1 = __builtin_expect(__cil_tmp30, 0L);
3090 }
3091#line 204
3092 if (tmp___1 != 0L) {
3093#line 205
3094 goto out;
3095 } else {
3096
3097 }
3098 {
3099#line 207
3100 __cil_tmp31 = (unsigned long )priv;
3101#line 207
3102 __cil_tmp32 = __cil_tmp31 + 8;
3103#line 207
3104 __cil_tmp33 = *((struct mc13xxx **)__cil_tmp32);
3105#line 207
3106 ret = mc13xxx_irq_status(__cil_tmp33, 25, & enabled, & pending);
3107 }
3108 out:
3109 {
3110#line 211
3111 __cil_tmp34 = (unsigned long )priv;
3112#line 211
3113 __cil_tmp35 = __cil_tmp34 + 8;
3114#line 211
3115 __cil_tmp36 = *((struct mc13xxx **)__cil_tmp35);
3116#line 211
3117 mc13xxx_unlock(__cil_tmp36);
3118 }
3119#line 213
3120 if (ret != 0) {
3121#line 214
3122 return (ret);
3123 } else {
3124
3125 }
3126 {
3127#line 216
3128 __cil_tmp37 = & enabled;
3129#line 216
3130 __cil_tmp38 = *__cil_tmp37;
3131#line 216
3132 *((unsigned char *)alarm) = (unsigned char )__cil_tmp38;
3133#line 217
3134 __cil_tmp39 = (unsigned long )alarm;
3135#line 217
3136 __cil_tmp40 = __cil_tmp39 + 1;
3137#line 217
3138 __cil_tmp41 = & pending;
3139#line 217
3140 __cil_tmp42 = *__cil_tmp41;
3141#line 217
3142 *((unsigned char *)__cil_tmp40) = (unsigned char )__cil_tmp42;
3143#line 219
3144 __cil_tmp43 = & seconds;
3145#line 219
3146 __cil_tmp44 = *__cil_tmp43;
3147#line 219
3148 __cil_tmp45 = & days;
3149#line 219
3150 __cil_tmp46 = *__cil_tmp45;
3151#line 219
3152 __cil_tmp47 = __cil_tmp46 * 86400U;
3153#line 219
3154 __cil_tmp48 = __cil_tmp47 + __cil_tmp44;
3155#line 219
3156 s1970 = (unsigned long )__cil_tmp48;
3157#line 221
3158 __cil_tmp49 = (unsigned long )alarm;
3159#line 221
3160 __cil_tmp50 = __cil_tmp49 + 4;
3161#line 221
3162 __cil_tmp51 = (struct rtc_time *)__cil_tmp50;
3163#line 221
3164 rtc_time_to_tm(s1970, __cil_tmp51);
3165#line 222
3166 __cil_tmp52 = & descriptor;
3167#line 222
3168 *((char const **)__cil_tmp52) = "rtc_mc13xxx";
3169#line 222
3170 __cil_tmp53 = (unsigned long )(& descriptor) + 8;
3171#line 222
3172 *((char const **)__cil_tmp53) = "mc13xxx_rtc_read_alarm";
3173#line 222
3174 __cil_tmp54 = (unsigned long )(& descriptor) + 16;
3175#line 222
3176 *((char const **)__cil_tmp54) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p";
3177#line 222
3178 __cil_tmp55 = (unsigned long )(& descriptor) + 24;
3179#line 222
3180 *((char const **)__cil_tmp55) = "%s: %lu\n";
3181#line 222
3182 __cil_tmp56 = (unsigned long )(& descriptor) + 32;
3183#line 222
3184 *((unsigned int *)__cil_tmp56) = 222U;
3185#line 222
3186 __cil_tmp57 = (unsigned long )(& descriptor) + 35;
3187#line 222
3188 *((unsigned char *)__cil_tmp57) = (unsigned char)1;
3189#line 222
3190 __cil_tmp58 = (unsigned long )(& descriptor) + 35;
3191#line 222
3192 __cil_tmp59 = *((unsigned char *)__cil_tmp58);
3193#line 222
3194 __cil_tmp60 = (long )__cil_tmp59;
3195#line 222
3196 __cil_tmp61 = __cil_tmp60 & 1L;
3197#line 222
3198 tmp___2 = __builtin_expect(__cil_tmp61, 0L);
3199 }
3200#line 222
3201 if (tmp___2 != 0L) {
3202 {
3203#line 222
3204 __cil_tmp62 = (struct device const *)dev;
3205#line 222
3206 __dynamic_dev_dbg(& descriptor, __cil_tmp62, "%s: %lu\n", "mc13xxx_rtc_read_alarm",
3207 s1970);
3208 }
3209 } else {
3210
3211 }
3212#line 224
3213 return (0);
3214}
3215}
3216#line 227 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
3217static int mc13xxx_rtc_set_alarm(struct device *dev , struct rtc_wkalrm *alarm )
3218{ struct mc13xxx_rtc *priv ;
3219 void *tmp ;
3220 unsigned long s1970 ;
3221 unsigned int seconds ;
3222 unsigned int days ;
3223 int ret ;
3224 long tmp___0 ;
3225 long tmp___1 ;
3226 long tmp___2 ;
3227 struct _ddebug descriptor ;
3228 char *tmp___3 ;
3229 long tmp___4 ;
3230 long tmp___5 ;
3231 long tmp___6 ;
3232 struct device const *__cil_tmp17 ;
3233 unsigned long __cil_tmp18 ;
3234 unsigned long __cil_tmp19 ;
3235 struct mc13xxx *__cil_tmp20 ;
3236 unsigned long __cil_tmp21 ;
3237 unsigned long __cil_tmp22 ;
3238 struct mc13xxx *__cil_tmp23 ;
3239 int __cil_tmp24 ;
3240 long __cil_tmp25 ;
3241 unsigned long __cil_tmp26 ;
3242 unsigned long __cil_tmp27 ;
3243 struct mc13xxx *__cil_tmp28 ;
3244 int __cil_tmp29 ;
3245 long __cil_tmp30 ;
3246 unsigned long __cil_tmp31 ;
3247 unsigned long __cil_tmp32 ;
3248 struct rtc_time *__cil_tmp33 ;
3249 int __cil_tmp34 ;
3250 long __cil_tmp35 ;
3251 struct _ddebug *__cil_tmp36 ;
3252 unsigned long __cil_tmp37 ;
3253 unsigned long __cil_tmp38 ;
3254 unsigned long __cil_tmp39 ;
3255 unsigned long __cil_tmp40 ;
3256 unsigned long __cil_tmp41 ;
3257 unsigned long __cil_tmp42 ;
3258 unsigned char __cil_tmp43 ;
3259 long __cil_tmp44 ;
3260 long __cil_tmp45 ;
3261 unsigned char __cil_tmp46 ;
3262 unsigned int __cil_tmp47 ;
3263 struct device const *__cil_tmp48 ;
3264 unsigned long *__cil_tmp49 ;
3265 unsigned long __cil_tmp50 ;
3266 unsigned char __cil_tmp51 ;
3267 unsigned int __cil_tmp52 ;
3268 int __cil_tmp53 ;
3269 long __cil_tmp54 ;
3270 unsigned long *__cil_tmp55 ;
3271 unsigned long __cil_tmp56 ;
3272 unsigned long __cil_tmp57 ;
3273 unsigned long *__cil_tmp58 ;
3274 unsigned long __cil_tmp59 ;
3275 unsigned long __cil_tmp60 ;
3276 unsigned long __cil_tmp61 ;
3277 unsigned long __cil_tmp62 ;
3278 struct mc13xxx *__cil_tmp63 ;
3279 int __cil_tmp64 ;
3280 long __cil_tmp65 ;
3281 unsigned long __cil_tmp66 ;
3282 unsigned long __cil_tmp67 ;
3283 struct mc13xxx *__cil_tmp68 ;
3284 unsigned long __cil_tmp69 ;
3285 unsigned long __cil_tmp70 ;
3286 struct mc13xxx *__cil_tmp71 ;
3287
3288 {
3289 {
3290#line 229
3291 __cil_tmp17 = (struct device const *)dev;
3292#line 229
3293 tmp = dev_get_drvdata(__cil_tmp17);
3294#line 229
3295 priv = (struct mc13xxx_rtc *)tmp;
3296#line 234
3297 __cil_tmp18 = (unsigned long )priv;
3298#line 234
3299 __cil_tmp19 = __cil_tmp18 + 8;
3300#line 234
3301 __cil_tmp20 = *((struct mc13xxx **)__cil_tmp19);
3302#line 234
3303 mc13xxx_lock(__cil_tmp20);
3304#line 237
3305 __cil_tmp21 = (unsigned long )priv;
3306#line 237
3307 __cil_tmp22 = __cil_tmp21 + 8;
3308#line 237
3309 __cil_tmp23 = *((struct mc13xxx **)__cil_tmp22);
3310#line 237
3311 ret = mc13xxx_reg_write(__cil_tmp23, 21U, 131071U);
3312#line 238
3313 __cil_tmp24 = ret != 0;
3314#line 238
3315 __cil_tmp25 = (long )__cil_tmp24;
3316#line 238
3317 tmp___0 = __builtin_expect(__cil_tmp25, 0L);
3318 }
3319#line 238
3320 if (tmp___0 != 0L) {
3321#line 239
3322 goto out;
3323 } else {
3324
3325 }
3326 {
3327#line 241
3328 __cil_tmp26 = (unsigned long )priv;
3329#line 241
3330 __cil_tmp27 = __cil_tmp26 + 8;
3331#line 241
3332 __cil_tmp28 = *((struct mc13xxx **)__cil_tmp27);
3333#line 241
3334 ret = mc13xxx_irq_ack(__cil_tmp28, 25);
3335#line 242
3336 __cil_tmp29 = ret != 0;
3337#line 242
3338 __cil_tmp30 = (long )__cil_tmp29;
3339#line 242
3340 tmp___1 = __builtin_expect(__cil_tmp30, 0L);
3341 }
3342#line 242
3343 if (tmp___1 != 0L) {
3344#line 243
3345 goto out;
3346 } else {
3347
3348 }
3349 {
3350#line 245
3351 __cil_tmp31 = (unsigned long )alarm;
3352#line 245
3353 __cil_tmp32 = __cil_tmp31 + 4;
3354#line 245
3355 __cil_tmp33 = (struct rtc_time *)__cil_tmp32;
3356#line 245
3357 ret = rtc_tm_to_time(__cil_tmp33, & s1970);
3358#line 246
3359 __cil_tmp34 = ret != 0;
3360#line 246
3361 __cil_tmp35 = (long )__cil_tmp34;
3362#line 246
3363 tmp___2 = __builtin_expect(__cil_tmp35, 0L);
3364 }
3365#line 246
3366 if (tmp___2 != 0L) {
3367#line 247
3368 goto out;
3369 } else {
3370
3371 }
3372 {
3373#line 249
3374 __cil_tmp36 = & descriptor;
3375#line 249
3376 *((char const **)__cil_tmp36) = "rtc_mc13xxx";
3377#line 249
3378 __cil_tmp37 = (unsigned long )(& descriptor) + 8;
3379#line 249
3380 *((char const **)__cil_tmp37) = "mc13xxx_rtc_set_alarm";
3381#line 249
3382 __cil_tmp38 = (unsigned long )(& descriptor) + 16;
3383#line 249
3384 *((char const **)__cil_tmp38) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p";
3385#line 249
3386 __cil_tmp39 = (unsigned long )(& descriptor) + 24;
3387#line 249
3388 *((char const **)__cil_tmp39) = "%s: o%2.s %lu\n";
3389#line 249
3390 __cil_tmp40 = (unsigned long )(& descriptor) + 32;
3391#line 249
3392 *((unsigned int *)__cil_tmp40) = 250U;
3393#line 249
3394 __cil_tmp41 = (unsigned long )(& descriptor) + 35;
3395#line 249
3396 *((unsigned char *)__cil_tmp41) = (unsigned char)1;
3397#line 249
3398 __cil_tmp42 = (unsigned long )(& descriptor) + 35;
3399#line 249
3400 __cil_tmp43 = *((unsigned char *)__cil_tmp42);
3401#line 249
3402 __cil_tmp44 = (long )__cil_tmp43;
3403#line 249
3404 __cil_tmp45 = __cil_tmp44 & 1L;
3405#line 249
3406 tmp___4 = __builtin_expect(__cil_tmp45, 0L);
3407 }
3408#line 249
3409 if (tmp___4 != 0L) {
3410 {
3411#line 249
3412 __cil_tmp46 = *((unsigned char *)alarm);
3413#line 249
3414 __cil_tmp47 = (unsigned int )__cil_tmp46;
3415#line 249
3416 if (__cil_tmp47 != 0U) {
3417#line 249
3418 tmp___3 = (char *)"n";
3419 } else {
3420#line 249
3421 tmp___3 = (char *)"ff";
3422 }
3423 }
3424 {
3425#line 249
3426 __cil_tmp48 = (struct device const *)dev;
3427#line 249
3428 __cil_tmp49 = & s1970;
3429#line 249
3430 __cil_tmp50 = *__cil_tmp49;
3431#line 249
3432 __dynamic_dev_dbg(& descriptor, __cil_tmp48, "%s: o%2.s %lu\n", "mc13xxx_rtc_set_alarm",
3433 tmp___3, __cil_tmp50);
3434 }
3435 } else {
3436
3437 }
3438 {
3439#line 252
3440 __cil_tmp51 = *((unsigned char *)alarm);
3441#line 252
3442 __cil_tmp52 = (unsigned int )__cil_tmp51;
3443#line 252
3444 ret = mc13xxx_rtc_irq_enable_unlocked(dev, __cil_tmp52, 25);
3445#line 254
3446 __cil_tmp53 = ret != 0;
3447#line 254
3448 __cil_tmp54 = (long )__cil_tmp53;
3449#line 254
3450 tmp___5 = __builtin_expect(__cil_tmp54, 0L);
3451 }
3452#line 254
3453 if (tmp___5 != 0L) {
3454#line 255
3455 goto out;
3456 } else {
3457
3458 }
3459 {
3460#line 257
3461 __cil_tmp55 = & s1970;
3462#line 257
3463 __cil_tmp56 = *__cil_tmp55;
3464#line 257
3465 __cil_tmp57 = __cil_tmp56 % 86400UL;
3466#line 257
3467 seconds = (unsigned int )__cil_tmp57;
3468#line 258
3469 __cil_tmp58 = & s1970;
3470#line 258
3471 __cil_tmp59 = *__cil_tmp58;
3472#line 258
3473 __cil_tmp60 = __cil_tmp59 / 86400UL;
3474#line 258
3475 days = (unsigned int )__cil_tmp60;
3476#line 260
3477 __cil_tmp61 = (unsigned long )priv;
3478#line 260
3479 __cil_tmp62 = __cil_tmp61 + 8;
3480#line 260
3481 __cil_tmp63 = *((struct mc13xxx **)__cil_tmp62);
3482#line 260
3483 ret = mc13xxx_reg_write(__cil_tmp63, 23U, days);
3484#line 261
3485 __cil_tmp64 = ret != 0;
3486#line 261
3487 __cil_tmp65 = (long )__cil_tmp64;
3488#line 261
3489 tmp___6 = __builtin_expect(__cil_tmp65, 0L);
3490 }
3491#line 261
3492 if (tmp___6 != 0L) {
3493#line 262
3494 goto out;
3495 } else {
3496
3497 }
3498 {
3499#line 264
3500 __cil_tmp66 = (unsigned long )priv;
3501#line 264
3502 __cil_tmp67 = __cil_tmp66 + 8;
3503#line 264
3504 __cil_tmp68 = *((struct mc13xxx **)__cil_tmp67);
3505#line 264
3506 ret = mc13xxx_reg_write(__cil_tmp68, 21U, seconds);
3507 }
3508 out:
3509 {
3510#line 267
3511 __cil_tmp69 = (unsigned long )priv;
3512#line 267
3513 __cil_tmp70 = __cil_tmp69 + 8;
3514#line 267
3515 __cil_tmp71 = *((struct mc13xxx **)__cil_tmp70);
3516#line 267
3517 mc13xxx_unlock(__cil_tmp71);
3518 }
3519#line 269
3520 return (ret);
3521}
3522}
3523#line 272 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
3524static irqreturn_t mc13xxx_rtc_alarm_handler(int irq , void *dev )
3525{ struct mc13xxx_rtc *priv ;
3526 struct mc13xxx *mc13xxx ;
3527 struct _ddebug descriptor ;
3528 long tmp ;
3529 unsigned long __cil_tmp7 ;
3530 unsigned long __cil_tmp8 ;
3531 struct _ddebug *__cil_tmp9 ;
3532 unsigned long __cil_tmp10 ;
3533 unsigned long __cil_tmp11 ;
3534 unsigned long __cil_tmp12 ;
3535 unsigned long __cil_tmp13 ;
3536 unsigned long __cil_tmp14 ;
3537 unsigned long __cil_tmp15 ;
3538 unsigned char __cil_tmp16 ;
3539 long __cil_tmp17 ;
3540 long __cil_tmp18 ;
3541 struct rtc_device *__cil_tmp19 ;
3542 struct device *__cil_tmp20 ;
3543 struct device const *__cil_tmp21 ;
3544 struct rtc_device *__cil_tmp22 ;
3545
3546 {
3547 {
3548#line 274
3549 priv = (struct mc13xxx_rtc *)dev;
3550#line 275
3551 __cil_tmp7 = (unsigned long )priv;
3552#line 275
3553 __cil_tmp8 = __cil_tmp7 + 8;
3554#line 275
3555 mc13xxx = *((struct mc13xxx **)__cil_tmp8);
3556#line 277
3557 __cil_tmp9 = & descriptor;
3558#line 277
3559 *((char const **)__cil_tmp9) = "rtc_mc13xxx";
3560#line 277
3561 __cil_tmp10 = (unsigned long )(& descriptor) + 8;
3562#line 277
3563 *((char const **)__cil_tmp10) = "mc13xxx_rtc_alarm_handler";
3564#line 277
3565 __cil_tmp11 = (unsigned long )(& descriptor) + 16;
3566#line 277
3567 *((char const **)__cil_tmp11) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p";
3568#line 277
3569 __cil_tmp12 = (unsigned long )(& descriptor) + 24;
3570#line 277
3571 *((char const **)__cil_tmp12) = "Alarm\n";
3572#line 277
3573 __cil_tmp13 = (unsigned long )(& descriptor) + 32;
3574#line 277
3575 *((unsigned int *)__cil_tmp13) = 277U;
3576#line 277
3577 __cil_tmp14 = (unsigned long )(& descriptor) + 35;
3578#line 277
3579 *((unsigned char *)__cil_tmp14) = (unsigned char)1;
3580#line 277
3581 __cil_tmp15 = (unsigned long )(& descriptor) + 35;
3582#line 277
3583 __cil_tmp16 = *((unsigned char *)__cil_tmp15);
3584#line 277
3585 __cil_tmp17 = (long )__cil_tmp16;
3586#line 277
3587 __cil_tmp18 = __cil_tmp17 & 1L;
3588#line 277
3589 tmp = __builtin_expect(__cil_tmp18, 0L);
3590 }
3591#line 277
3592 if (tmp != 0L) {
3593 {
3594#line 277
3595 __cil_tmp19 = *((struct rtc_device **)priv);
3596#line 277
3597 __cil_tmp20 = (struct device *)__cil_tmp19;
3598#line 277
3599 __cil_tmp21 = (struct device const *)__cil_tmp20;
3600#line 277
3601 __dynamic_dev_dbg(& descriptor, __cil_tmp21, "Alarm\n");
3602 }
3603 } else {
3604
3605 }
3606 {
3607#line 279
3608 __cil_tmp22 = *((struct rtc_device **)priv);
3609#line 279
3610 rtc_update_irq(__cil_tmp22, 1UL, 160UL);
3611#line 281
3612 mc13xxx_irq_ack(mc13xxx, irq);
3613 }
3614#line 283
3615 return ((irqreturn_t )1);
3616}
3617}
3618#line 286 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
3619static irqreturn_t mc13xxx_rtc_update_handler(int irq , void *dev )
3620{ struct mc13xxx_rtc *priv ;
3621 struct mc13xxx *mc13xxx ;
3622 struct _ddebug descriptor ;
3623 long tmp ;
3624 unsigned long __cil_tmp7 ;
3625 unsigned long __cil_tmp8 ;
3626 struct _ddebug *__cil_tmp9 ;
3627 unsigned long __cil_tmp10 ;
3628 unsigned long __cil_tmp11 ;
3629 unsigned long __cil_tmp12 ;
3630 unsigned long __cil_tmp13 ;
3631 unsigned long __cil_tmp14 ;
3632 unsigned long __cil_tmp15 ;
3633 unsigned char __cil_tmp16 ;
3634 long __cil_tmp17 ;
3635 long __cil_tmp18 ;
3636 struct rtc_device *__cil_tmp19 ;
3637 struct device *__cil_tmp20 ;
3638 struct device const *__cil_tmp21 ;
3639 struct rtc_device *__cil_tmp22 ;
3640
3641 {
3642 {
3643#line 288
3644 priv = (struct mc13xxx_rtc *)dev;
3645#line 289
3646 __cil_tmp7 = (unsigned long )priv;
3647#line 289
3648 __cil_tmp8 = __cil_tmp7 + 8;
3649#line 289
3650 mc13xxx = *((struct mc13xxx **)__cil_tmp8);
3651#line 291
3652 __cil_tmp9 = & descriptor;
3653#line 291
3654 *((char const **)__cil_tmp9) = "rtc_mc13xxx";
3655#line 291
3656 __cil_tmp10 = (unsigned long )(& descriptor) + 8;
3657#line 291
3658 *((char const **)__cil_tmp10) = "mc13xxx_rtc_update_handler";
3659#line 291
3660 __cil_tmp11 = (unsigned long )(& descriptor) + 16;
3661#line 291
3662 *((char const **)__cil_tmp11) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p";
3663#line 291
3664 __cil_tmp12 = (unsigned long )(& descriptor) + 24;
3665#line 291
3666 *((char const **)__cil_tmp12) = "1HZ\n";
3667#line 291
3668 __cil_tmp13 = (unsigned long )(& descriptor) + 32;
3669#line 291
3670 *((unsigned int *)__cil_tmp13) = 291U;
3671#line 291
3672 __cil_tmp14 = (unsigned long )(& descriptor) + 35;
3673#line 291
3674 *((unsigned char *)__cil_tmp14) = (unsigned char)1;
3675#line 291
3676 __cil_tmp15 = (unsigned long )(& descriptor) + 35;
3677#line 291
3678 __cil_tmp16 = *((unsigned char *)__cil_tmp15);
3679#line 291
3680 __cil_tmp17 = (long )__cil_tmp16;
3681#line 291
3682 __cil_tmp18 = __cil_tmp17 & 1L;
3683#line 291
3684 tmp = __builtin_expect(__cil_tmp18, 0L);
3685 }
3686#line 291
3687 if (tmp != 0L) {
3688 {
3689#line 291
3690 __cil_tmp19 = *((struct rtc_device **)priv);
3691#line 291
3692 __cil_tmp20 = (struct device *)__cil_tmp19;
3693#line 291
3694 __cil_tmp21 = (struct device const *)__cil_tmp20;
3695#line 291
3696 __dynamic_dev_dbg(& descriptor, __cil_tmp21, "1HZ\n");
3697 }
3698 } else {
3699
3700 }
3701 {
3702#line 293
3703 __cil_tmp22 = *((struct rtc_device **)priv);
3704#line 293
3705 rtc_update_irq(__cil_tmp22, 1UL, 144UL);
3706#line 295
3707 mc13xxx_irq_ack(mc13xxx, irq);
3708 }
3709#line 297
3710 return ((irqreturn_t )1);
3711}
3712}
3713#line 300 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
3714static int mc13xxx_rtc_alarm_irq_enable(struct device *dev , unsigned int enabled )
3715{ int tmp ;
3716
3717 {
3718 {
3719#line 303
3720 tmp = mc13xxx_rtc_irq_enable(dev, enabled, 25);
3721 }
3722#line 303
3723 return (tmp);
3724}
3725}
3726#line 306 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
3727static struct rtc_class_ops const mc13xxx_rtc_ops =
3728#line 306
3729 {(int (*)(struct device * ))0, (void (*)(struct device * ))0, (int (*)(struct device * ,
3730 unsigned int ,
3731 unsigned long ))0,
3732 & mc13xxx_rtc_read_time, (int (*)(struct device * , struct rtc_time * ))0, & mc13xxx_rtc_read_alarm,
3733 & mc13xxx_rtc_set_alarm, (int (*)(struct device * , struct seq_file * ))0, & mc13xxx_rtc_set_mmss,
3734 (int (*)(struct device * , int ))0, & mc13xxx_rtc_alarm_irq_enable};
3735#line 314 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
3736static irqreturn_t mc13xxx_rtc_reset_handler(int irq , void *dev )
3737{ struct mc13xxx_rtc *priv ;
3738 struct mc13xxx *mc13xxx ;
3739 struct _ddebug descriptor ;
3740 long tmp ;
3741 unsigned long __cil_tmp7 ;
3742 unsigned long __cil_tmp8 ;
3743 struct _ddebug *__cil_tmp9 ;
3744 unsigned long __cil_tmp10 ;
3745 unsigned long __cil_tmp11 ;
3746 unsigned long __cil_tmp12 ;
3747 unsigned long __cil_tmp13 ;
3748 unsigned long __cil_tmp14 ;
3749 unsigned long __cil_tmp15 ;
3750 unsigned char __cil_tmp16 ;
3751 long __cil_tmp17 ;
3752 long __cil_tmp18 ;
3753 struct rtc_device *__cil_tmp19 ;
3754 struct device *__cil_tmp20 ;
3755 struct device const *__cil_tmp21 ;
3756 unsigned long __cil_tmp22 ;
3757 unsigned long __cil_tmp23 ;
3758
3759 {
3760 {
3761#line 316
3762 priv = (struct mc13xxx_rtc *)dev;
3763#line 317
3764 __cil_tmp7 = (unsigned long )priv;
3765#line 317
3766 __cil_tmp8 = __cil_tmp7 + 8;
3767#line 317
3768 mc13xxx = *((struct mc13xxx **)__cil_tmp8);
3769#line 319
3770 __cil_tmp9 = & descriptor;
3771#line 319
3772 *((char const **)__cil_tmp9) = "rtc_mc13xxx";
3773#line 319
3774 __cil_tmp10 = (unsigned long )(& descriptor) + 8;
3775#line 319
3776 *((char const **)__cil_tmp10) = "mc13xxx_rtc_reset_handler";
3777#line 319
3778 __cil_tmp11 = (unsigned long )(& descriptor) + 16;
3779#line 319
3780 *((char const **)__cil_tmp11) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p";
3781#line 319
3782 __cil_tmp12 = (unsigned long )(& descriptor) + 24;
3783#line 319
3784 *((char const **)__cil_tmp12) = "RTCRST\n";
3785#line 319
3786 __cil_tmp13 = (unsigned long )(& descriptor) + 32;
3787#line 319
3788 *((unsigned int *)__cil_tmp13) = 319U;
3789#line 319
3790 __cil_tmp14 = (unsigned long )(& descriptor) + 35;
3791#line 319
3792 *((unsigned char *)__cil_tmp14) = (unsigned char)1;
3793#line 319
3794 __cil_tmp15 = (unsigned long )(& descriptor) + 35;
3795#line 319
3796 __cil_tmp16 = *((unsigned char *)__cil_tmp15);
3797#line 319
3798 __cil_tmp17 = (long )__cil_tmp16;
3799#line 319
3800 __cil_tmp18 = __cil_tmp17 & 1L;
3801#line 319
3802 tmp = __builtin_expect(__cil_tmp18, 0L);
3803 }
3804#line 319
3805 if (tmp != 0L) {
3806 {
3807#line 319
3808 __cil_tmp19 = *((struct rtc_device **)priv);
3809#line 319
3810 __cil_tmp20 = (struct device *)__cil_tmp19;
3811#line 319
3812 __cil_tmp21 = (struct device const *)__cil_tmp20;
3813#line 319
3814 __dynamic_dev_dbg(& descriptor, __cil_tmp21, "RTCRST\n");
3815 }
3816 } else {
3817
3818 }
3819 {
3820#line 320
3821 __cil_tmp22 = (unsigned long )priv;
3822#line 320
3823 __cil_tmp23 = __cil_tmp22 + 16;
3824#line 320
3825 *((int *)__cil_tmp23) = 0;
3826#line 322
3827 mc13xxx_irq_mask(mc13xxx, irq);
3828 }
3829#line 324
3830 return ((irqreturn_t )1);
3831}
3832}
3833#line 327 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
3834static int mc13xxx_rtc_probe(struct platform_device *pdev )
3835{ int ret ;
3836 struct mc13xxx_rtc *priv ;
3837 struct mc13xxx *mc13xxx ;
3838 int rtcrst_pending ;
3839 void *tmp ;
3840 void *tmp___0 ;
3841 long tmp___1 ;
3842 long tmp___2 ;
3843 struct mc13xxx_rtc *__cil_tmp10 ;
3844 unsigned long __cil_tmp11 ;
3845 unsigned long __cil_tmp12 ;
3846 unsigned long __cil_tmp13 ;
3847 unsigned long __cil_tmp14 ;
3848 struct device *__cil_tmp15 ;
3849 struct device const *__cil_tmp16 ;
3850 unsigned long __cil_tmp17 ;
3851 unsigned long __cil_tmp18 ;
3852 void *__cil_tmp19 ;
3853 void *__cil_tmp20 ;
3854 int *__cil_tmp21 ;
3855 unsigned long __cil_tmp22 ;
3856 unsigned long __cil_tmp23 ;
3857 int *__cil_tmp24 ;
3858 int __cil_tmp25 ;
3859 void *__cil_tmp26 ;
3860 void *__cil_tmp27 ;
3861 char const *__cil_tmp28 ;
3862 unsigned long __cil_tmp29 ;
3863 unsigned long __cil_tmp30 ;
3864 struct device *__cil_tmp31 ;
3865 struct rtc_device *__cil_tmp32 ;
3866 void const *__cil_tmp33 ;
3867 struct rtc_device *__cil_tmp34 ;
3868 void const *__cil_tmp35 ;
3869 void *__cil_tmp36 ;
3870 void *__cil_tmp37 ;
3871 void *__cil_tmp38 ;
3872 void *__cil_tmp39 ;
3873 void const *__cil_tmp40 ;
3874
3875 {
3876 {
3877#line 334
3878 tmp = kzalloc(24UL, 208U);
3879#line 334
3880 priv = (struct mc13xxx_rtc *)tmp;
3881 }
3882 {
3883#line 335
3884 __cil_tmp10 = (struct mc13xxx_rtc *)0;
3885#line 335
3886 __cil_tmp11 = (unsigned long )__cil_tmp10;
3887#line 335
3888 __cil_tmp12 = (unsigned long )priv;
3889#line 335
3890 if (__cil_tmp12 == __cil_tmp11) {
3891#line 336
3892 return (-12);
3893 } else {
3894
3895 }
3896 }
3897 {
3898#line 338
3899 __cil_tmp13 = (unsigned long )pdev;
3900#line 338
3901 __cil_tmp14 = __cil_tmp13 + 16;
3902#line 338
3903 __cil_tmp15 = *((struct device **)__cil_tmp14);
3904#line 338
3905 __cil_tmp16 = (struct device const *)__cil_tmp15;
3906#line 338
3907 tmp___0 = dev_get_drvdata(__cil_tmp16);
3908#line 338
3909 mc13xxx = (struct mc13xxx *)tmp___0;
3910#line 339
3911 __cil_tmp17 = (unsigned long )priv;
3912#line 339
3913 __cil_tmp18 = __cil_tmp17 + 8;
3914#line 339
3915 *((struct mc13xxx **)__cil_tmp18) = mc13xxx;
3916#line 341
3917 __cil_tmp19 = (void *)priv;
3918#line 341
3919 platform_set_drvdata(pdev, __cil_tmp19);
3920#line 343
3921 mc13xxx_lock(mc13xxx);
3922#line 345
3923 __cil_tmp20 = (void *)priv;
3924#line 345
3925 ret = mc13xxx_irq_request(mc13xxx, 31, & mc13xxx_rtc_reset_handler, "mc13xxx-rtc",
3926 __cil_tmp20);
3927 }
3928#line 347
3929 if (ret != 0) {
3930#line 348
3931 goto err_reset_irq_request;
3932 } else {
3933
3934 }
3935 {
3936#line 350
3937 __cil_tmp21 = (int *)0;
3938#line 350
3939 ret = mc13xxx_irq_status(mc13xxx, 31, __cil_tmp21, & rtcrst_pending);
3940 }
3941#line 352
3942 if (ret != 0) {
3943#line 353
3944 goto err_reset_irq_status;
3945 } else {
3946
3947 }
3948 {
3949#line 355
3950 __cil_tmp22 = (unsigned long )priv;
3951#line 355
3952 __cil_tmp23 = __cil_tmp22 + 16;
3953#line 355
3954 __cil_tmp24 = & rtcrst_pending;
3955#line 355
3956 __cil_tmp25 = *__cil_tmp24;
3957#line 355
3958 *((int *)__cil_tmp23) = __cil_tmp25 == 0;
3959#line 357
3960 __cil_tmp26 = (void *)priv;
3961#line 357
3962 ret = mc13xxx_irq_request_nounmask(mc13xxx, 24, & mc13xxx_rtc_update_handler, "mc13xxx-rtc",
3963 __cil_tmp26);
3964 }
3965#line 359
3966 if (ret != 0) {
3967#line 360
3968 goto err_update_irq_request;
3969 } else {
3970
3971 }
3972 {
3973#line 362
3974 __cil_tmp27 = (void *)priv;
3975#line 362
3976 ret = mc13xxx_irq_request_nounmask(mc13xxx, 25, & mc13xxx_rtc_alarm_handler, "mc13xxx-rtc",
3977 __cil_tmp27);
3978 }
3979#line 364
3980 if (ret != 0) {
3981#line 365
3982 goto err_alarm_irq_request;
3983 } else {
3984
3985 }
3986 {
3987#line 367
3988 mc13xxx_unlock(mc13xxx);
3989#line 369
3990 __cil_tmp28 = *((char const **)pdev);
3991#line 369
3992 __cil_tmp29 = (unsigned long )pdev;
3993#line 369
3994 __cil_tmp30 = __cil_tmp29 + 16;
3995#line 369
3996 __cil_tmp31 = (struct device *)__cil_tmp30;
3997#line 369
3998 *((struct rtc_device **)priv) = rtc_device_register(__cil_tmp28, __cil_tmp31, & mc13xxx_rtc_ops,
3999 & __this_module);
4000#line 371
4001 __cil_tmp32 = *((struct rtc_device **)priv);
4002#line 371
4003 __cil_tmp33 = (void const *)__cil_tmp32;
4004#line 371
4005 tmp___2 = IS_ERR(__cil_tmp33);
4006 }
4007#line 371
4008 if (tmp___2 != 0L) {
4009 {
4010#line 372
4011 __cil_tmp34 = *((struct rtc_device **)priv);
4012#line 372
4013 __cil_tmp35 = (void const *)__cil_tmp34;
4014#line 372
4015 tmp___1 = PTR_ERR(__cil_tmp35);
4016#line 372
4017 ret = (int )tmp___1;
4018#line 374
4019 mc13xxx_lock(mc13xxx);
4020#line 376
4021 __cil_tmp36 = (void *)priv;
4022#line 376
4023 mc13xxx_irq_free(mc13xxx, 25, __cil_tmp36);
4024 }
4025 err_alarm_irq_request:
4026 {
4027#line 379
4028 __cil_tmp37 = (void *)priv;
4029#line 379
4030 mc13xxx_irq_free(mc13xxx, 24, __cil_tmp37);
4031 }
4032 err_update_irq_request: ;
4033 err_reset_irq_status:
4034 {
4035#line 384
4036 __cil_tmp38 = (void *)priv;
4037#line 384
4038 mc13xxx_irq_free(mc13xxx, 31, __cil_tmp38);
4039 }
4040 err_reset_irq_request:
4041 {
4042#line 387
4043 mc13xxx_unlock(mc13xxx);
4044#line 389
4045 __cil_tmp39 = (void *)0;
4046#line 389
4047 platform_set_drvdata(pdev, __cil_tmp39);
4048#line 390
4049 __cil_tmp40 = (void const *)priv;
4050#line 390
4051 kfree(__cil_tmp40);
4052 }
4053 } else {
4054
4055 }
4056#line 393
4057 return (ret);
4058}
4059}
4060#line 396 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4061static int mc13xxx_rtc_remove(struct platform_device *pdev )
4062{ struct mc13xxx_rtc *priv ;
4063 void *tmp ;
4064 struct platform_device const *__cil_tmp4 ;
4065 unsigned long __cil_tmp5 ;
4066 unsigned long __cil_tmp6 ;
4067 struct mc13xxx *__cil_tmp7 ;
4068 struct rtc_device *__cil_tmp8 ;
4069 unsigned long __cil_tmp9 ;
4070 unsigned long __cil_tmp10 ;
4071 struct mc13xxx *__cil_tmp11 ;
4072 void *__cil_tmp12 ;
4073 unsigned long __cil_tmp13 ;
4074 unsigned long __cil_tmp14 ;
4075 struct mc13xxx *__cil_tmp15 ;
4076 void *__cil_tmp16 ;
4077 unsigned long __cil_tmp17 ;
4078 unsigned long __cil_tmp18 ;
4079 struct mc13xxx *__cil_tmp19 ;
4080 void *__cil_tmp20 ;
4081 unsigned long __cil_tmp21 ;
4082 unsigned long __cil_tmp22 ;
4083 struct mc13xxx *__cil_tmp23 ;
4084 void *__cil_tmp24 ;
4085 void const *__cil_tmp25 ;
4086
4087 {
4088 {
4089#line 398
4090 __cil_tmp4 = (struct platform_device const *)pdev;
4091#line 398
4092 tmp = platform_get_drvdata(__cil_tmp4);
4093#line 398
4094 priv = (struct mc13xxx_rtc *)tmp;
4095#line 400
4096 __cil_tmp5 = (unsigned long )priv;
4097#line 400
4098 __cil_tmp6 = __cil_tmp5 + 8;
4099#line 400
4100 __cil_tmp7 = *((struct mc13xxx **)__cil_tmp6);
4101#line 400
4102 mc13xxx_lock(__cil_tmp7);
4103#line 402
4104 __cil_tmp8 = *((struct rtc_device **)priv);
4105#line 402
4106 rtc_device_unregister(__cil_tmp8);
4107#line 404
4108 __cil_tmp9 = (unsigned long )priv;
4109#line 404
4110 __cil_tmp10 = __cil_tmp9 + 8;
4111#line 404
4112 __cil_tmp11 = *((struct mc13xxx **)__cil_tmp10);
4113#line 404
4114 __cil_tmp12 = (void *)priv;
4115#line 404
4116 mc13xxx_irq_free(__cil_tmp11, 25, __cil_tmp12);
4117#line 405
4118 __cil_tmp13 = (unsigned long )priv;
4119#line 405
4120 __cil_tmp14 = __cil_tmp13 + 8;
4121#line 405
4122 __cil_tmp15 = *((struct mc13xxx **)__cil_tmp14);
4123#line 405
4124 __cil_tmp16 = (void *)priv;
4125#line 405
4126 mc13xxx_irq_free(__cil_tmp15, 24, __cil_tmp16);
4127#line 406
4128 __cil_tmp17 = (unsigned long )priv;
4129#line 406
4130 __cil_tmp18 = __cil_tmp17 + 8;
4131#line 406
4132 __cil_tmp19 = *((struct mc13xxx **)__cil_tmp18);
4133#line 406
4134 __cil_tmp20 = (void *)priv;
4135#line 406
4136 mc13xxx_irq_free(__cil_tmp19, 31, __cil_tmp20);
4137#line 408
4138 __cil_tmp21 = (unsigned long )priv;
4139#line 408
4140 __cil_tmp22 = __cil_tmp21 + 8;
4141#line 408
4142 __cil_tmp23 = *((struct mc13xxx **)__cil_tmp22);
4143#line 408
4144 mc13xxx_unlock(__cil_tmp23);
4145#line 410
4146 __cil_tmp24 = (void *)0;
4147#line 410
4148 platform_set_drvdata(pdev, __cil_tmp24);
4149#line 412
4150 __cil_tmp25 = (void const *)priv;
4151#line 412
4152 kfree(__cil_tmp25);
4153 }
4154#line 414
4155 return (0);
4156}
4157}
4158#line 417 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4159static struct platform_device_id const mc13xxx_rtc_idtable[3U] = { {{(char )'m', (char )'c', (char )'1', (char )'3', (char )'7', (char )'8', (char )'3',
4160 (char )'-', (char )'r', (char )'t', (char )'c', (char )'\000', (char)0, (char)0,
4161 (char)0, (char)0, (char)0, (char)0, (char)0, (char)0}, 0UL},
4162 {{(char )'m', (char )'c', (char )'1', (char )'3', (char )'8', (char )'9', (char )'2',
4163 (char )'-', (char )'r', (char )'t', (char )'c', (char )'\000', (char)0, (char)0,
4164 (char)0, (char)0, (char)0, (char)0, (char)0, (char)0}, 0UL},
4165 {{(char)0, (char)0, (char)0, (char)0, (char)0, (char)0, (char)0, (char)0, (char)0,
4166 (char)0, (char)0, (char)0, (char)0, (char)0, (char)0, (char)0, (char)0, (char)0,
4167 (char)0, (char)0}, 0UL}};
4168#line 426 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4169static struct platform_driver mc13xxx_rtc_driver = {(int (*)(struct platform_device * ))0, & mc13xxx_rtc_remove, (void (*)(struct platform_device * ))0,
4170 (int (*)(struct platform_device * , pm_message_t ))0, (int (*)(struct platform_device * ))0,
4171 {"mc13xxx-rtc", (struct bus_type *)0, & __this_module, (char const *)0, (_Bool)0,
4172 (struct of_device_id const *)0, (int (*)(struct device * ))0, (int (*)(struct device * ))0,
4173 (void (*)(struct device * ))0, (int (*)(struct device * , pm_message_t ))0,
4174 (int (*)(struct device * ))0, (struct attribute_group const **)0, (struct dev_pm_ops const *)0,
4175 (struct driver_private *)0}, (struct platform_device_id const *)(& mc13xxx_rtc_idtable)};
4176#line 435 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4177static int mc13xxx_rtc_init(void)
4178{ int tmp ;
4179
4180 {
4181 {
4182#line 437
4183 tmp = platform_driver_probe(& mc13xxx_rtc_driver, & mc13xxx_rtc_probe);
4184 }
4185#line 437
4186 return (tmp);
4187}
4188}
4189#line 441 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4190static void mc13xxx_rtc_exit(void)
4191{
4192
4193 {
4194 {
4195#line 443
4196 platform_driver_unregister(& mc13xxx_rtc_driver);
4197 }
4198#line 444
4199 return;
4200}
4201}
4202#line 468
4203extern void ldv_check_final_state(void) ;
4204#line 474
4205extern void ldv_initialize(void) ;
4206#line 477
4207extern int __VERIFIER_nondet_int(void) ;
4208#line 480 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4209int LDV_IN_INTERRUPT ;
4210#line 483 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4211void main(void)
4212{ struct device *var_group1 ;
4213 struct rtc_time *var_group2 ;
4214 unsigned long var_mc13xxx_rtc_set_mmss_3_p1 ;
4215 struct rtc_wkalrm *var_group3 ;
4216 unsigned int var_mc13xxx_rtc_alarm_irq_enable_8_p1 ;
4217 int var_mc13xxx_rtc_alarm_handler_6_p0 ;
4218 void *var_mc13xxx_rtc_alarm_handler_6_p1 ;
4219 int var_mc13xxx_rtc_reset_handler_9_p0 ;
4220 void *var_mc13xxx_rtc_reset_handler_9_p1 ;
4221 int var_mc13xxx_rtc_update_handler_7_p0 ;
4222 void *var_mc13xxx_rtc_update_handler_7_p1 ;
4223 int tmp ;
4224 int tmp___0 ;
4225 int tmp___1 ;
4226
4227 {
4228 {
4229#line 585
4230 LDV_IN_INTERRUPT = 1;
4231#line 594
4232 ldv_initialize();
4233#line 606
4234 tmp = mc13xxx_rtc_init();
4235 }
4236#line 606
4237 if (tmp != 0) {
4238#line 607
4239 goto ldv_final;
4240 } else {
4241
4242 }
4243#line 613
4244 goto ldv_21146;
4245 ldv_21145:
4246 {
4247#line 616
4248 tmp___0 = __VERIFIER_nondet_int();
4249 }
4250#line 618
4251 if (tmp___0 == 0) {
4252#line 618
4253 goto case_0;
4254 } else
4255#line 640
4256 if (tmp___0 == 1) {
4257#line 640
4258 goto case_1;
4259 } else
4260#line 662
4261 if (tmp___0 == 2) {
4262#line 662
4263 goto case_2;
4264 } else
4265#line 684
4266 if (tmp___0 == 3) {
4267#line 684
4268 goto case_3;
4269 } else
4270#line 706
4271 if (tmp___0 == 4) {
4272#line 706
4273 goto case_4;
4274 } else
4275#line 728
4276 if (tmp___0 == 5) {
4277#line 728
4278 goto case_5;
4279 } else
4280#line 750
4281 if (tmp___0 == 6) {
4282#line 750
4283 goto case_6;
4284 } else
4285#line 772
4286 if (tmp___0 == 7) {
4287#line 772
4288 goto case_7;
4289 } else {
4290 {
4291#line 794
4292 goto switch_default;
4293#line 616
4294 if (0) {
4295 case_0:
4296 {
4297#line 632
4298 mc13xxx_rtc_read_time(var_group1, var_group2);
4299 }
4300#line 639
4301 goto ldv_21136;
4302 case_1:
4303 {
4304#line 654
4305 mc13xxx_rtc_set_mmss(var_group1, var_mc13xxx_rtc_set_mmss_3_p1);
4306 }
4307#line 661
4308 goto ldv_21136;
4309 case_2:
4310 {
4311#line 676
4312 mc13xxx_rtc_read_alarm(var_group1, var_group3);
4313 }
4314#line 683
4315 goto ldv_21136;
4316 case_3:
4317 {
4318#line 698
4319 mc13xxx_rtc_set_alarm(var_group1, var_group3);
4320 }
4321#line 705
4322 goto ldv_21136;
4323 case_4:
4324 {
4325#line 720
4326 mc13xxx_rtc_alarm_irq_enable(var_group1, var_mc13xxx_rtc_alarm_irq_enable_8_p1);
4327 }
4328#line 727
4329 goto ldv_21136;
4330 case_5:
4331 {
4332#line 731
4333 LDV_IN_INTERRUPT = 2;
4334#line 742
4335 mc13xxx_rtc_alarm_handler(var_mc13xxx_rtc_alarm_handler_6_p0, var_mc13xxx_rtc_alarm_handler_6_p1);
4336#line 743
4337 LDV_IN_INTERRUPT = 1;
4338 }
4339#line 749
4340 goto ldv_21136;
4341 case_6:
4342 {
4343#line 753
4344 LDV_IN_INTERRUPT = 2;
4345#line 764
4346 mc13xxx_rtc_reset_handler(var_mc13xxx_rtc_reset_handler_9_p0, var_mc13xxx_rtc_reset_handler_9_p1);
4347#line 765
4348 LDV_IN_INTERRUPT = 1;
4349 }
4350#line 771
4351 goto ldv_21136;
4352 case_7:
4353 {
4354#line 775
4355 LDV_IN_INTERRUPT = 2;
4356#line 786
4357 mc13xxx_rtc_update_handler(var_mc13xxx_rtc_update_handler_7_p0, var_mc13xxx_rtc_update_handler_7_p1);
4358#line 787
4359 LDV_IN_INTERRUPT = 1;
4360 }
4361#line 793
4362 goto ldv_21136;
4363 switch_default: ;
4364#line 794
4365 goto ldv_21136;
4366 } else {
4367 switch_break: ;
4368 }
4369 }
4370 }
4371 ldv_21136: ;
4372 ldv_21146:
4373 {
4374#line 613
4375 tmp___1 = __VERIFIER_nondet_int();
4376 }
4377#line 613
4378 if (tmp___1 != 0) {
4379#line 614
4380 goto ldv_21145;
4381 } else {
4382#line 616
4383 goto ldv_21147;
4384 }
4385 ldv_21147: ;
4386 {
4387#line 812
4388 mc13xxx_rtc_exit();
4389 }
4390 ldv_final:
4391 {
4392#line 815
4393 ldv_check_final_state();
4394 }
4395#line 818
4396 return;
4397}
4398}
4399#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
4400void ldv_blast_assert(void)
4401{
4402
4403 {
4404 ERROR: ;
4405#line 6
4406 goto ERROR;
4407}
4408}
4409#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
4410extern int __VERIFIER_nondet_int(void) ;
4411#line 839 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4412int ldv_spin = 0;
4413#line 843 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4414void ldv_check_alloc_flags(gfp_t flags )
4415{
4416
4417 {
4418#line 846
4419 if (ldv_spin != 0) {
4420#line 846
4421 if (flags != 32U) {
4422 {
4423#line 846
4424 ldv_blast_assert();
4425 }
4426 } else {
4427
4428 }
4429 } else {
4430
4431 }
4432#line 849
4433 return;
4434}
4435}
4436#line 849
4437extern struct page *ldv_some_page(void) ;
4438#line 852 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4439struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
4440{ struct page *tmp ;
4441
4442 {
4443#line 855
4444 if (ldv_spin != 0) {
4445#line 855
4446 if (flags != 32U) {
4447 {
4448#line 855
4449 ldv_blast_assert();
4450 }
4451 } else {
4452
4453 }
4454 } else {
4455
4456 }
4457 {
4458#line 857
4459 tmp = ldv_some_page();
4460 }
4461#line 857
4462 return (tmp);
4463}
4464}
4465#line 861 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4466void ldv_check_alloc_nonatomic(void)
4467{
4468
4469 {
4470#line 864
4471 if (ldv_spin != 0) {
4472 {
4473#line 864
4474 ldv_blast_assert();
4475 }
4476 } else {
4477
4478 }
4479#line 867
4480 return;
4481}
4482}
4483#line 868 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4484void ldv_spin_lock(void)
4485{
4486
4487 {
4488#line 871
4489 ldv_spin = 1;
4490#line 872
4491 return;
4492}
4493}
4494#line 875 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4495void ldv_spin_unlock(void)
4496{
4497
4498 {
4499#line 878
4500 ldv_spin = 0;
4501#line 879
4502 return;
4503}
4504}
4505#line 882 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4506int ldv_spin_trylock(void)
4507{ int is_lock ;
4508
4509 {
4510 {
4511#line 887
4512 is_lock = __VERIFIER_nondet_int();
4513 }
4514#line 889
4515 if (is_lock != 0) {
4516#line 892
4517 return (0);
4518 } else {
4519#line 897
4520 ldv_spin = 1;
4521#line 899
4522 return (1);
4523 }
4524}
4525}
4526#line 1066 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4527void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
4528{
4529
4530 {
4531 {
4532#line 1072
4533 ldv_check_alloc_flags(ldv_func_arg2);
4534#line 1074
4535 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
4536 }
4537#line 1075
4538 return ((void *)0);
4539}
4540}
4541#line 1077 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2656/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-mc13xxx.c.p"
4542__inline static void *kzalloc(size_t size , gfp_t flags )
4543{ void *tmp ;
4544
4545 {
4546 {
4547#line 1083
4548 ldv_check_alloc_flags(flags);
4549#line 1084
4550 tmp = __VERIFIER_nondet_pointer();
4551 }
4552#line 1084
4553 return (tmp);
4554}
4555}