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/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
883struct klist_node;
884#line 15
885struct klist_node;
886#line 37 "include/linux/klist.h"
887struct klist_node {
888 void *n_klist ;
889 struct list_head n_node ;
890 struct kref n_ref ;
891};
892#line 67
893struct dma_map_ops;
894#line 67 "include/linux/klist.h"
895struct dev_archdata {
896 void *acpi_handle ;
897 struct dma_map_ops *dma_ops ;
898 void *iommu ;
899};
900#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
901struct pdev_archdata {
902
903};
904#line 17
905struct device_private;
906#line 17
907struct device_private;
908#line 18
909struct device_driver;
910#line 18
911struct device_driver;
912#line 19
913struct driver_private;
914#line 19
915struct driver_private;
916#line 20
917struct class;
918#line 20
919struct class;
920#line 21
921struct subsys_private;
922#line 21
923struct subsys_private;
924#line 22
925struct bus_type;
926#line 22
927struct bus_type;
928#line 23
929struct device_node;
930#line 23
931struct device_node;
932#line 24
933struct iommu_ops;
934#line 24
935struct iommu_ops;
936#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
937struct bus_attribute {
938 struct attribute attr ;
939 ssize_t (*show)(struct bus_type * , char * ) ;
940 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
941};
942#line 51 "include/linux/device.h"
943struct device_attribute;
944#line 51
945struct driver_attribute;
946#line 51 "include/linux/device.h"
947struct bus_type {
948 char const *name ;
949 char const *dev_name ;
950 struct device *dev_root ;
951 struct bus_attribute *bus_attrs ;
952 struct device_attribute *dev_attrs ;
953 struct driver_attribute *drv_attrs ;
954 int (*match)(struct device * , struct device_driver * ) ;
955 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
956 int (*probe)(struct device * ) ;
957 int (*remove)(struct device * ) ;
958 void (*shutdown)(struct device * ) ;
959 int (*suspend)(struct device * , pm_message_t ) ;
960 int (*resume)(struct device * ) ;
961 struct dev_pm_ops const *pm ;
962 struct iommu_ops *iommu_ops ;
963 struct subsys_private *p ;
964};
965#line 125
966struct device_type;
967#line 182
968struct of_device_id;
969#line 182 "include/linux/device.h"
970struct device_driver {
971 char const *name ;
972 struct bus_type *bus ;
973 struct module *owner ;
974 char const *mod_name ;
975 bool suppress_bind_attrs ;
976 struct of_device_id const *of_match_table ;
977 int (*probe)(struct device * ) ;
978 int (*remove)(struct device * ) ;
979 void (*shutdown)(struct device * ) ;
980 int (*suspend)(struct device * , pm_message_t ) ;
981 int (*resume)(struct device * ) ;
982 struct attribute_group const **groups ;
983 struct dev_pm_ops const *pm ;
984 struct driver_private *p ;
985};
986#line 245 "include/linux/device.h"
987struct driver_attribute {
988 struct attribute attr ;
989 ssize_t (*show)(struct device_driver * , char * ) ;
990 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
991};
992#line 299
993struct class_attribute;
994#line 299 "include/linux/device.h"
995struct class {
996 char const *name ;
997 struct module *owner ;
998 struct class_attribute *class_attrs ;
999 struct device_attribute *dev_attrs ;
1000 struct bin_attribute *dev_bin_attrs ;
1001 struct kobject *dev_kobj ;
1002 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
1003 char *(*devnode)(struct device * , umode_t * ) ;
1004 void (*class_release)(struct class * ) ;
1005 void (*dev_release)(struct device * ) ;
1006 int (*suspend)(struct device * , pm_message_t ) ;
1007 int (*resume)(struct device * ) ;
1008 struct kobj_ns_type_operations const *ns_type ;
1009 void const *(*namespace)(struct device * ) ;
1010 struct dev_pm_ops const *pm ;
1011 struct subsys_private *p ;
1012};
1013#line 394 "include/linux/device.h"
1014struct class_attribute {
1015 struct attribute attr ;
1016 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
1017 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
1018 void const *(*namespace)(struct class * , struct class_attribute const * ) ;
1019};
1020#line 447 "include/linux/device.h"
1021struct device_type {
1022 char const *name ;
1023 struct attribute_group const **groups ;
1024 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
1025 char *(*devnode)(struct device * , umode_t * ) ;
1026 void (*release)(struct device * ) ;
1027 struct dev_pm_ops const *pm ;
1028};
1029#line 474 "include/linux/device.h"
1030struct device_attribute {
1031 struct attribute attr ;
1032 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
1033 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
1034 size_t ) ;
1035};
1036#line 557 "include/linux/device.h"
1037struct device_dma_parameters {
1038 unsigned int max_segment_size ;
1039 unsigned long segment_boundary_mask ;
1040};
1041#line 567
1042struct dma_coherent_mem;
1043#line 567 "include/linux/device.h"
1044struct device {
1045 struct device *parent ;
1046 struct device_private *p ;
1047 struct kobject kobj ;
1048 char const *init_name ;
1049 struct device_type const *type ;
1050 struct mutex mutex ;
1051 struct bus_type *bus ;
1052 struct device_driver *driver ;
1053 void *platform_data ;
1054 struct dev_pm_info power ;
1055 struct dev_pm_domain *pm_domain ;
1056 int numa_node ;
1057 u64 *dma_mask ;
1058 u64 coherent_dma_mask ;
1059 struct device_dma_parameters *dma_parms ;
1060 struct list_head dma_pools ;
1061 struct dma_coherent_mem *dma_mem ;
1062 struct dev_archdata archdata ;
1063 struct device_node *of_node ;
1064 dev_t devt ;
1065 u32 id ;
1066 spinlock_t devres_lock ;
1067 struct list_head devres_head ;
1068 struct klist_node knode_class ;
1069 struct class *class ;
1070 struct attribute_group const **groups ;
1071 void (*release)(struct device * ) ;
1072};
1073#line 681 "include/linux/device.h"
1074struct wakeup_source {
1075 char const *name ;
1076 struct list_head entry ;
1077 spinlock_t lock ;
1078 struct timer_list timer ;
1079 unsigned long timer_expires ;
1080 ktime_t total_time ;
1081 ktime_t max_time ;
1082 ktime_t last_time ;
1083 unsigned long event_count ;
1084 unsigned long active_count ;
1085 unsigned long relax_count ;
1086 unsigned long hit_count ;
1087 unsigned char active : 1 ;
1088};
1089#line 12 "include/linux/mod_devicetable.h"
1090typedef unsigned long kernel_ulong_t;
1091#line 215 "include/linux/mod_devicetable.h"
1092struct of_device_id {
1093 char name[32U] ;
1094 char type[32U] ;
1095 char compatible[128U] ;
1096 void *data ;
1097};
1098#line 492 "include/linux/mod_devicetable.h"
1099struct platform_device_id {
1100 char name[20U] ;
1101 kernel_ulong_t driver_data ;
1102};
1103#line 584
1104struct mfd_cell;
1105#line 584
1106struct mfd_cell;
1107#line 585 "include/linux/mod_devicetable.h"
1108struct platform_device {
1109 char const *name ;
1110 int id ;
1111 struct device dev ;
1112 u32 num_resources ;
1113 struct resource *resource ;
1114 struct platform_device_id const *id_entry ;
1115 struct mfd_cell *mfd_cell ;
1116 struct pdev_archdata archdata ;
1117};
1118#line 272 "include/linux/platform_device.h"
1119struct rtc_time {
1120 int tm_sec ;
1121 int tm_min ;
1122 int tm_hour ;
1123 int tm_mday ;
1124 int tm_mon ;
1125 int tm_year ;
1126 int tm_wday ;
1127 int tm_yday ;
1128 int tm_isdst ;
1129};
1130#line 31 "include/linux/rtc.h"
1131struct rtc_wkalrm {
1132 unsigned char enabled ;
1133 unsigned char pending ;
1134 struct rtc_time time ;
1135};
1136#line 348 "include/linux/irq.h"
1137struct proc_dir_entry;
1138#line 348
1139struct proc_dir_entry;
1140#line 41 "include/asm-generic/sections.h"
1141struct exception_table_entry {
1142 unsigned long insn ;
1143 unsigned long fixup ;
1144};
1145#line 189 "include/linux/hardirq.h"
1146struct timerqueue_node {
1147 struct rb_node node ;
1148 ktime_t expires ;
1149};
1150#line 12 "include/linux/timerqueue.h"
1151struct timerqueue_head {
1152 struct rb_root head ;
1153 struct timerqueue_node *next ;
1154};
1155#line 50
1156struct hrtimer_clock_base;
1157#line 50
1158struct hrtimer_clock_base;
1159#line 51
1160struct hrtimer_cpu_base;
1161#line 51
1162struct hrtimer_cpu_base;
1163#line 60
1164enum hrtimer_restart {
1165 HRTIMER_NORESTART = 0,
1166 HRTIMER_RESTART = 1
1167} ;
1168#line 65 "include/linux/timerqueue.h"
1169struct hrtimer {
1170 struct timerqueue_node node ;
1171 ktime_t _softexpires ;
1172 enum hrtimer_restart (*function)(struct hrtimer * ) ;
1173 struct hrtimer_clock_base *base ;
1174 unsigned long state ;
1175 int start_pid ;
1176 void *start_site ;
1177 char start_comm[16U] ;
1178};
1179#line 132 "include/linux/hrtimer.h"
1180struct hrtimer_clock_base {
1181 struct hrtimer_cpu_base *cpu_base ;
1182 int index ;
1183 clockid_t clockid ;
1184 struct timerqueue_head active ;
1185 ktime_t resolution ;
1186 ktime_t (*get_time)(void) ;
1187 ktime_t softirq_time ;
1188 ktime_t offset ;
1189};
1190#line 162 "include/linux/hrtimer.h"
1191struct hrtimer_cpu_base {
1192 raw_spinlock_t lock ;
1193 unsigned long active_bases ;
1194 ktime_t expires_next ;
1195 int hres_active ;
1196 int hang_detected ;
1197 unsigned long nr_events ;
1198 unsigned long nr_retries ;
1199 unsigned long nr_hangs ;
1200 ktime_t max_hang_time ;
1201 struct hrtimer_clock_base clock_base[3U] ;
1202};
1203#line 115 "include/linux/rtc.h"
1204struct path;
1205#line 115
1206struct path;
1207#line 116
1208struct inode;
1209#line 116
1210struct inode;
1211#line 117
1212struct dentry;
1213#line 117
1214struct dentry;
1215#line 118 "include/linux/rtc.h"
1216struct seq_file {
1217 char *buf ;
1218 size_t size ;
1219 size_t from ;
1220 size_t count ;
1221 loff_t index ;
1222 loff_t read_pos ;
1223 u64 version ;
1224 struct mutex lock ;
1225 struct seq_operations const *op ;
1226 int poll_event ;
1227 void *private ;
1228};
1229#line 30 "include/linux/seq_file.h"
1230struct seq_operations {
1231 void *(*start)(struct seq_file * , loff_t * ) ;
1232 void (*stop)(struct seq_file * , void * ) ;
1233 void *(*next)(struct seq_file * , void * , loff_t * ) ;
1234 int (*show)(struct seq_file * , void * ) ;
1235};
1236#line 89 "include/linux/kdev_t.h"
1237struct file_operations;
1238#line 89
1239struct file_operations;
1240#line 90 "include/linux/kdev_t.h"
1241struct cdev {
1242 struct kobject kobj ;
1243 struct module *owner ;
1244 struct file_operations const *ops ;
1245 struct list_head list ;
1246 dev_t dev ;
1247 unsigned int count ;
1248};
1249#line 33 "include/linux/cdev.h"
1250struct backing_dev_info;
1251#line 41 "include/asm-generic/poll.h"
1252struct block_device;
1253#line 41
1254struct block_device;
1255#line 93 "include/linux/bit_spinlock.h"
1256struct hlist_bl_node;
1257#line 93 "include/linux/bit_spinlock.h"
1258struct hlist_bl_head {
1259 struct hlist_bl_node *first ;
1260};
1261#line 36 "include/linux/list_bl.h"
1262struct hlist_bl_node {
1263 struct hlist_bl_node *next ;
1264 struct hlist_bl_node **pprev ;
1265};
1266#line 114 "include/linux/rculist_bl.h"
1267struct nameidata;
1268#line 114
1269struct nameidata;
1270#line 115
1271struct vfsmount;
1272#line 115
1273struct vfsmount;
1274#line 116 "include/linux/rculist_bl.h"
1275struct qstr {
1276 unsigned int hash ;
1277 unsigned int len ;
1278 unsigned char const *name ;
1279};
1280#line 72 "include/linux/dcache.h"
1281struct dentry_operations;
1282#line 72
1283struct super_block;
1284#line 72 "include/linux/dcache.h"
1285union __anonunion_d_u_137 {
1286 struct list_head d_child ;
1287 struct rcu_head d_rcu ;
1288};
1289#line 72 "include/linux/dcache.h"
1290struct dentry {
1291 unsigned int d_flags ;
1292 seqcount_t d_seq ;
1293 struct hlist_bl_node d_hash ;
1294 struct dentry *d_parent ;
1295 struct qstr d_name ;
1296 struct inode *d_inode ;
1297 unsigned char d_iname[32U] ;
1298 unsigned int d_count ;
1299 spinlock_t d_lock ;
1300 struct dentry_operations const *d_op ;
1301 struct super_block *d_sb ;
1302 unsigned long d_time ;
1303 void *d_fsdata ;
1304 struct list_head d_lru ;
1305 union __anonunion_d_u_137 d_u ;
1306 struct list_head d_subdirs ;
1307 struct list_head d_alias ;
1308};
1309#line 123 "include/linux/dcache.h"
1310struct dentry_operations {
1311 int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
1312 int (*d_hash)(struct dentry const * , struct inode const * , struct qstr * ) ;
1313 int (*d_compare)(struct dentry const * , struct inode const * , struct dentry const * ,
1314 struct inode const * , unsigned int , char const * , struct qstr const * ) ;
1315 int (*d_delete)(struct dentry const * ) ;
1316 void (*d_release)(struct dentry * ) ;
1317 void (*d_prune)(struct dentry * ) ;
1318 void (*d_iput)(struct dentry * , struct inode * ) ;
1319 char *(*d_dname)(struct dentry * , char * , int ) ;
1320 struct vfsmount *(*d_automount)(struct path * ) ;
1321 int (*d_manage)(struct dentry * , bool ) ;
1322};
1323#line 402 "include/linux/dcache.h"
1324struct path {
1325 struct vfsmount *mnt ;
1326 struct dentry *dentry ;
1327};
1328#line 58 "include/linux/radix-tree.h"
1329struct radix_tree_node;
1330#line 58 "include/linux/radix-tree.h"
1331struct radix_tree_root {
1332 unsigned int height ;
1333 gfp_t gfp_mask ;
1334 struct radix_tree_node *rnode ;
1335};
1336#line 377
1337struct prio_tree_node;
1338#line 19 "include/linux/prio_tree.h"
1339struct prio_tree_node {
1340 struct prio_tree_node *left ;
1341 struct prio_tree_node *right ;
1342 struct prio_tree_node *parent ;
1343 unsigned long start ;
1344 unsigned long last ;
1345};
1346#line 27 "include/linux/prio_tree.h"
1347struct prio_tree_root {
1348 struct prio_tree_node *prio_tree_node ;
1349 unsigned short index_bits ;
1350 unsigned short raw ;
1351};
1352#line 111
1353enum pid_type {
1354 PIDTYPE_PID = 0,
1355 PIDTYPE_PGID = 1,
1356 PIDTYPE_SID = 2,
1357 PIDTYPE_MAX = 3
1358} ;
1359#line 118
1360struct pid_namespace;
1361#line 118 "include/linux/prio_tree.h"
1362struct upid {
1363 int nr ;
1364 struct pid_namespace *ns ;
1365 struct hlist_node pid_chain ;
1366};
1367#line 56 "include/linux/pid.h"
1368struct pid {
1369 atomic_t count ;
1370 unsigned int level ;
1371 struct hlist_head tasks[3U] ;
1372 struct rcu_head rcu ;
1373 struct upid numbers[1U] ;
1374};
1375#line 45 "include/linux/semaphore.h"
1376struct fiemap_extent {
1377 __u64 fe_logical ;
1378 __u64 fe_physical ;
1379 __u64 fe_length ;
1380 __u64 fe_reserved64[2U] ;
1381 __u32 fe_flags ;
1382 __u32 fe_reserved[3U] ;
1383};
1384#line 38 "include/linux/fiemap.h"
1385struct shrink_control {
1386 gfp_t gfp_mask ;
1387 unsigned long nr_to_scan ;
1388};
1389#line 14 "include/linux/shrinker.h"
1390struct shrinker {
1391 int (*shrink)(struct shrinker * , struct shrink_control * ) ;
1392 int seeks ;
1393 long batch ;
1394 struct list_head list ;
1395 atomic_long_t nr_in_batch ;
1396};
1397#line 43
1398enum migrate_mode {
1399 MIGRATE_ASYNC = 0,
1400 MIGRATE_SYNC_LIGHT = 1,
1401 MIGRATE_SYNC = 2
1402} ;
1403#line 49
1404struct export_operations;
1405#line 49
1406struct export_operations;
1407#line 51
1408struct iovec;
1409#line 51
1410struct iovec;
1411#line 52
1412struct kiocb;
1413#line 52
1414struct kiocb;
1415#line 53
1416struct pipe_inode_info;
1417#line 53
1418struct pipe_inode_info;
1419#line 54
1420struct poll_table_struct;
1421#line 54
1422struct poll_table_struct;
1423#line 55
1424struct kstatfs;
1425#line 55
1426struct kstatfs;
1427#line 435 "include/linux/fs.h"
1428struct iattr {
1429 unsigned int ia_valid ;
1430 umode_t ia_mode ;
1431 uid_t ia_uid ;
1432 gid_t ia_gid ;
1433 loff_t ia_size ;
1434 struct timespec ia_atime ;
1435 struct timespec ia_mtime ;
1436 struct timespec ia_ctime ;
1437 struct file *ia_file ;
1438};
1439#line 119 "include/linux/quota.h"
1440struct if_dqinfo {
1441 __u64 dqi_bgrace ;
1442 __u64 dqi_igrace ;
1443 __u32 dqi_flags ;
1444 __u32 dqi_valid ;
1445};
1446#line 176 "include/linux/percpu_counter.h"
1447struct fs_disk_quota {
1448 __s8 d_version ;
1449 __s8 d_flags ;
1450 __u16 d_fieldmask ;
1451 __u32 d_id ;
1452 __u64 d_blk_hardlimit ;
1453 __u64 d_blk_softlimit ;
1454 __u64 d_ino_hardlimit ;
1455 __u64 d_ino_softlimit ;
1456 __u64 d_bcount ;
1457 __u64 d_icount ;
1458 __s32 d_itimer ;
1459 __s32 d_btimer ;
1460 __u16 d_iwarns ;
1461 __u16 d_bwarns ;
1462 __s32 d_padding2 ;
1463 __u64 d_rtb_hardlimit ;
1464 __u64 d_rtb_softlimit ;
1465 __u64 d_rtbcount ;
1466 __s32 d_rtbtimer ;
1467 __u16 d_rtbwarns ;
1468 __s16 d_padding3 ;
1469 char d_padding4[8U] ;
1470};
1471#line 75 "include/linux/dqblk_xfs.h"
1472struct fs_qfilestat {
1473 __u64 qfs_ino ;
1474 __u64 qfs_nblks ;
1475 __u32 qfs_nextents ;
1476};
1477#line 150 "include/linux/dqblk_xfs.h"
1478typedef struct fs_qfilestat fs_qfilestat_t;
1479#line 151 "include/linux/dqblk_xfs.h"
1480struct fs_quota_stat {
1481 __s8 qs_version ;
1482 __u16 qs_flags ;
1483 __s8 qs_pad ;
1484 fs_qfilestat_t qs_uquota ;
1485 fs_qfilestat_t qs_gquota ;
1486 __u32 qs_incoredqs ;
1487 __s32 qs_btimelimit ;
1488 __s32 qs_itimelimit ;
1489 __s32 qs_rtbtimelimit ;
1490 __u16 qs_bwarnlimit ;
1491 __u16 qs_iwarnlimit ;
1492};
1493#line 165
1494struct dquot;
1495#line 165
1496struct dquot;
1497#line 185 "include/linux/quota.h"
1498typedef __kernel_uid32_t qid_t;
1499#line 186 "include/linux/quota.h"
1500typedef long long qsize_t;
1501#line 189 "include/linux/quota.h"
1502struct mem_dqblk {
1503 qsize_t dqb_bhardlimit ;
1504 qsize_t dqb_bsoftlimit ;
1505 qsize_t dqb_curspace ;
1506 qsize_t dqb_rsvspace ;
1507 qsize_t dqb_ihardlimit ;
1508 qsize_t dqb_isoftlimit ;
1509 qsize_t dqb_curinodes ;
1510 time_t dqb_btime ;
1511 time_t dqb_itime ;
1512};
1513#line 211
1514struct quota_format_type;
1515#line 211
1516struct quota_format_type;
1517#line 212 "include/linux/quota.h"
1518struct mem_dqinfo {
1519 struct quota_format_type *dqi_format ;
1520 int dqi_fmt_id ;
1521 struct list_head dqi_dirty_list ;
1522 unsigned long dqi_flags ;
1523 unsigned int dqi_bgrace ;
1524 unsigned int dqi_igrace ;
1525 qsize_t dqi_maxblimit ;
1526 qsize_t dqi_maxilimit ;
1527 void *dqi_priv ;
1528};
1529#line 275 "include/linux/quota.h"
1530struct dquot {
1531 struct hlist_node dq_hash ;
1532 struct list_head dq_inuse ;
1533 struct list_head dq_free ;
1534 struct list_head dq_dirty ;
1535 struct mutex dq_lock ;
1536 atomic_t dq_count ;
1537 wait_queue_head_t dq_wait_unused ;
1538 struct super_block *dq_sb ;
1539 unsigned int dq_id ;
1540 loff_t dq_off ;
1541 unsigned long dq_flags ;
1542 short dq_type ;
1543 struct mem_dqblk dq_dqb ;
1544};
1545#line 303 "include/linux/quota.h"
1546struct quota_format_ops {
1547 int (*check_quota_file)(struct super_block * , int ) ;
1548 int (*read_file_info)(struct super_block * , int ) ;
1549 int (*write_file_info)(struct super_block * , int ) ;
1550 int (*free_file_info)(struct super_block * , int ) ;
1551 int (*read_dqblk)(struct dquot * ) ;
1552 int (*commit_dqblk)(struct dquot * ) ;
1553 int (*release_dqblk)(struct dquot * ) ;
1554};
1555#line 314 "include/linux/quota.h"
1556struct dquot_operations {
1557 int (*write_dquot)(struct dquot * ) ;
1558 struct dquot *(*alloc_dquot)(struct super_block * , int ) ;
1559 void (*destroy_dquot)(struct dquot * ) ;
1560 int (*acquire_dquot)(struct dquot * ) ;
1561 int (*release_dquot)(struct dquot * ) ;
1562 int (*mark_dirty)(struct dquot * ) ;
1563 int (*write_info)(struct super_block * , int ) ;
1564 qsize_t *(*get_reserved_space)(struct inode * ) ;
1565};
1566#line 328 "include/linux/quota.h"
1567struct quotactl_ops {
1568 int (*quota_on)(struct super_block * , int , int , struct path * ) ;
1569 int (*quota_on_meta)(struct super_block * , int , int ) ;
1570 int (*quota_off)(struct super_block * , int ) ;
1571 int (*quota_sync)(struct super_block * , int , int ) ;
1572 int (*get_info)(struct super_block * , int , struct if_dqinfo * ) ;
1573 int (*set_info)(struct super_block * , int , struct if_dqinfo * ) ;
1574 int (*get_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1575 int (*set_dqblk)(struct super_block * , int , qid_t , struct fs_disk_quota * ) ;
1576 int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1577 int (*set_xstate)(struct super_block * , unsigned int , int ) ;
1578};
1579#line 344 "include/linux/quota.h"
1580struct quota_format_type {
1581 int qf_fmt_id ;
1582 struct quota_format_ops const *qf_ops ;
1583 struct module *qf_owner ;
1584 struct quota_format_type *qf_next ;
1585};
1586#line 390 "include/linux/quota.h"
1587struct quota_info {
1588 unsigned int flags ;
1589 struct mutex dqio_mutex ;
1590 struct mutex dqonoff_mutex ;
1591 struct rw_semaphore dqptr_sem ;
1592 struct inode *files[2U] ;
1593 struct mem_dqinfo info[2U] ;
1594 struct quota_format_ops const *ops[2U] ;
1595};
1596#line 421
1597struct address_space;
1598#line 421
1599struct address_space;
1600#line 422
1601struct writeback_control;
1602#line 422
1603struct writeback_control;
1604#line 585 "include/linux/fs.h"
1605union __anonunion_arg_140 {
1606 char *buf ;
1607 void *data ;
1608};
1609#line 585 "include/linux/fs.h"
1610struct __anonstruct_read_descriptor_t_139 {
1611 size_t written ;
1612 size_t count ;
1613 union __anonunion_arg_140 arg ;
1614 int error ;
1615};
1616#line 585 "include/linux/fs.h"
1617typedef struct __anonstruct_read_descriptor_t_139 read_descriptor_t;
1618#line 588 "include/linux/fs.h"
1619struct address_space_operations {
1620 int (*writepage)(struct page * , struct writeback_control * ) ;
1621 int (*readpage)(struct file * , struct page * ) ;
1622 int (*writepages)(struct address_space * , struct writeback_control * ) ;
1623 int (*set_page_dirty)(struct page * ) ;
1624 int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1625 unsigned int ) ;
1626 int (*write_begin)(struct file * , struct address_space * , loff_t , unsigned int ,
1627 unsigned int , struct page ** , void ** ) ;
1628 int (*write_end)(struct file * , struct address_space * , loff_t , unsigned int ,
1629 unsigned int , struct page * , void * ) ;
1630 sector_t (*bmap)(struct address_space * , sector_t ) ;
1631 void (*invalidatepage)(struct page * , unsigned long ) ;
1632 int (*releasepage)(struct page * , gfp_t ) ;
1633 void (*freepage)(struct page * ) ;
1634 ssize_t (*direct_IO)(int , struct kiocb * , struct iovec const * , loff_t ,
1635 unsigned long ) ;
1636 int (*get_xip_mem)(struct address_space * , unsigned long , int , void ** , unsigned long * ) ;
1637 int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode ) ;
1638 int (*launder_page)(struct page * ) ;
1639 int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long ) ;
1640 int (*error_remove_page)(struct address_space * , struct page * ) ;
1641};
1642#line 642 "include/linux/fs.h"
1643struct address_space {
1644 struct inode *host ;
1645 struct radix_tree_root page_tree ;
1646 spinlock_t tree_lock ;
1647 unsigned int i_mmap_writable ;
1648 struct prio_tree_root i_mmap ;
1649 struct list_head i_mmap_nonlinear ;
1650 struct mutex i_mmap_mutex ;
1651 unsigned long nrpages ;
1652 unsigned long writeback_index ;
1653 struct address_space_operations const *a_ops ;
1654 unsigned long flags ;
1655 struct backing_dev_info *backing_dev_info ;
1656 spinlock_t private_lock ;
1657 struct list_head private_list ;
1658 struct address_space *assoc_mapping ;
1659};
1660#line 664
1661struct request_queue;
1662#line 664
1663struct request_queue;
1664#line 665
1665struct hd_struct;
1666#line 665
1667struct gendisk;
1668#line 665 "include/linux/fs.h"
1669struct block_device {
1670 dev_t bd_dev ;
1671 int bd_openers ;
1672 struct inode *bd_inode ;
1673 struct super_block *bd_super ;
1674 struct mutex bd_mutex ;
1675 struct list_head bd_inodes ;
1676 void *bd_claiming ;
1677 void *bd_holder ;
1678 int bd_holders ;
1679 bool bd_write_holder ;
1680 struct list_head bd_holder_disks ;
1681 struct block_device *bd_contains ;
1682 unsigned int bd_block_size ;
1683 struct hd_struct *bd_part ;
1684 unsigned int bd_part_count ;
1685 int bd_invalidated ;
1686 struct gendisk *bd_disk ;
1687 struct request_queue *bd_queue ;
1688 struct list_head bd_list ;
1689 unsigned long bd_private ;
1690 int bd_fsfreeze_count ;
1691 struct mutex bd_fsfreeze_mutex ;
1692};
1693#line 737
1694struct posix_acl;
1695#line 737
1696struct posix_acl;
1697#line 738
1698struct inode_operations;
1699#line 738 "include/linux/fs.h"
1700union __anonunion_ldv_18694_141 {
1701 unsigned int const i_nlink ;
1702 unsigned int __i_nlink ;
1703};
1704#line 738 "include/linux/fs.h"
1705union __anonunion_ldv_18713_142 {
1706 struct list_head i_dentry ;
1707 struct rcu_head i_rcu ;
1708};
1709#line 738
1710struct file_lock;
1711#line 738 "include/linux/fs.h"
1712union __anonunion_ldv_18729_143 {
1713 struct pipe_inode_info *i_pipe ;
1714 struct block_device *i_bdev ;
1715 struct cdev *i_cdev ;
1716};
1717#line 738 "include/linux/fs.h"
1718struct inode {
1719 umode_t i_mode ;
1720 unsigned short i_opflags ;
1721 uid_t i_uid ;
1722 gid_t i_gid ;
1723 unsigned int i_flags ;
1724 struct posix_acl *i_acl ;
1725 struct posix_acl *i_default_acl ;
1726 struct inode_operations const *i_op ;
1727 struct super_block *i_sb ;
1728 struct address_space *i_mapping ;
1729 void *i_security ;
1730 unsigned long i_ino ;
1731 union __anonunion_ldv_18694_141 ldv_18694 ;
1732 dev_t i_rdev ;
1733 struct timespec i_atime ;
1734 struct timespec i_mtime ;
1735 struct timespec i_ctime ;
1736 spinlock_t i_lock ;
1737 unsigned short i_bytes ;
1738 blkcnt_t i_blocks ;
1739 loff_t i_size ;
1740 unsigned long i_state ;
1741 struct mutex i_mutex ;
1742 unsigned long dirtied_when ;
1743 struct hlist_node i_hash ;
1744 struct list_head i_wb_list ;
1745 struct list_head i_lru ;
1746 struct list_head i_sb_list ;
1747 union __anonunion_ldv_18713_142 ldv_18713 ;
1748 atomic_t i_count ;
1749 unsigned int i_blkbits ;
1750 u64 i_version ;
1751 atomic_t i_dio_count ;
1752 atomic_t i_writecount ;
1753 struct file_operations const *i_fop ;
1754 struct file_lock *i_flock ;
1755 struct address_space i_data ;
1756 struct dquot *i_dquot[2U] ;
1757 struct list_head i_devices ;
1758 union __anonunion_ldv_18729_143 ldv_18729 ;
1759 __u32 i_generation ;
1760 __u32 i_fsnotify_mask ;
1761 struct hlist_head i_fsnotify_marks ;
1762 atomic_t i_readcount ;
1763 void *i_private ;
1764};
1765#line 941 "include/linux/fs.h"
1766struct fown_struct {
1767 rwlock_t lock ;
1768 struct pid *pid ;
1769 enum pid_type pid_type ;
1770 uid_t uid ;
1771 uid_t euid ;
1772 int signum ;
1773};
1774#line 949 "include/linux/fs.h"
1775struct file_ra_state {
1776 unsigned long start ;
1777 unsigned int size ;
1778 unsigned int async_size ;
1779 unsigned int ra_pages ;
1780 unsigned int mmap_miss ;
1781 loff_t prev_pos ;
1782};
1783#line 972 "include/linux/fs.h"
1784union __anonunion_f_u_144 {
1785 struct list_head fu_list ;
1786 struct rcu_head fu_rcuhead ;
1787};
1788#line 972 "include/linux/fs.h"
1789struct file {
1790 union __anonunion_f_u_144 f_u ;
1791 struct path f_path ;
1792 struct file_operations const *f_op ;
1793 spinlock_t f_lock ;
1794 int f_sb_list_cpu ;
1795 atomic_long_t f_count ;
1796 unsigned int f_flags ;
1797 fmode_t f_mode ;
1798 loff_t f_pos ;
1799 struct fown_struct f_owner ;
1800 struct cred const *f_cred ;
1801 struct file_ra_state f_ra ;
1802 u64 f_version ;
1803 void *f_security ;
1804 void *private_data ;
1805 struct list_head f_ep_links ;
1806 struct list_head f_tfile_llink ;
1807 struct address_space *f_mapping ;
1808 unsigned long f_mnt_write_state ;
1809};
1810#line 1111
1811struct files_struct;
1812#line 1111 "include/linux/fs.h"
1813typedef struct files_struct *fl_owner_t;
1814#line 1112 "include/linux/fs.h"
1815struct file_lock_operations {
1816 void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1817 void (*fl_release_private)(struct file_lock * ) ;
1818};
1819#line 1117 "include/linux/fs.h"
1820struct lock_manager_operations {
1821 int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1822 void (*lm_notify)(struct file_lock * ) ;
1823 int (*lm_grant)(struct file_lock * , struct file_lock * , int ) ;
1824 void (*lm_release_private)(struct file_lock * ) ;
1825 void (*lm_break)(struct file_lock * ) ;
1826 int (*lm_change)(struct file_lock ** , int ) ;
1827};
1828#line 1134
1829struct nlm_lockowner;
1830#line 1134
1831struct nlm_lockowner;
1832#line 1135 "include/linux/fs.h"
1833struct nfs_lock_info {
1834 u32 state ;
1835 struct nlm_lockowner *owner ;
1836 struct list_head list ;
1837};
1838#line 14 "include/linux/nfs_fs_i.h"
1839struct nfs4_lock_state;
1840#line 14
1841struct nfs4_lock_state;
1842#line 15 "include/linux/nfs_fs_i.h"
1843struct nfs4_lock_info {
1844 struct nfs4_lock_state *owner ;
1845};
1846#line 19
1847struct fasync_struct;
1848#line 19 "include/linux/nfs_fs_i.h"
1849struct __anonstruct_afs_146 {
1850 struct list_head link ;
1851 int state ;
1852};
1853#line 19 "include/linux/nfs_fs_i.h"
1854union __anonunion_fl_u_145 {
1855 struct nfs_lock_info nfs_fl ;
1856 struct nfs4_lock_info nfs4_fl ;
1857 struct __anonstruct_afs_146 afs ;
1858};
1859#line 19 "include/linux/nfs_fs_i.h"
1860struct file_lock {
1861 struct file_lock *fl_next ;
1862 struct list_head fl_link ;
1863 struct list_head fl_block ;
1864 fl_owner_t fl_owner ;
1865 unsigned int fl_flags ;
1866 unsigned char fl_type ;
1867 unsigned int fl_pid ;
1868 struct pid *fl_nspid ;
1869 wait_queue_head_t fl_wait ;
1870 struct file *fl_file ;
1871 loff_t fl_start ;
1872 loff_t fl_end ;
1873 struct fasync_struct *fl_fasync ;
1874 unsigned long fl_break_time ;
1875 unsigned long fl_downgrade_time ;
1876 struct file_lock_operations const *fl_ops ;
1877 struct lock_manager_operations const *fl_lmops ;
1878 union __anonunion_fl_u_145 fl_u ;
1879};
1880#line 1221 "include/linux/fs.h"
1881struct fasync_struct {
1882 spinlock_t fa_lock ;
1883 int magic ;
1884 int fa_fd ;
1885 struct fasync_struct *fa_next ;
1886 struct file *fa_file ;
1887 struct rcu_head fa_rcu ;
1888};
1889#line 1417
1890struct file_system_type;
1891#line 1417
1892struct super_operations;
1893#line 1417
1894struct xattr_handler;
1895#line 1417
1896struct mtd_info;
1897#line 1417 "include/linux/fs.h"
1898struct super_block {
1899 struct list_head s_list ;
1900 dev_t s_dev ;
1901 unsigned char s_dirt ;
1902 unsigned char s_blocksize_bits ;
1903 unsigned long s_blocksize ;
1904 loff_t s_maxbytes ;
1905 struct file_system_type *s_type ;
1906 struct super_operations const *s_op ;
1907 struct dquot_operations const *dq_op ;
1908 struct quotactl_ops const *s_qcop ;
1909 struct export_operations const *s_export_op ;
1910 unsigned long s_flags ;
1911 unsigned long s_magic ;
1912 struct dentry *s_root ;
1913 struct rw_semaphore s_umount ;
1914 struct mutex s_lock ;
1915 int s_count ;
1916 atomic_t s_active ;
1917 void *s_security ;
1918 struct xattr_handler const **s_xattr ;
1919 struct list_head s_inodes ;
1920 struct hlist_bl_head s_anon ;
1921 struct list_head *s_files ;
1922 struct list_head s_mounts ;
1923 struct list_head s_dentry_lru ;
1924 int s_nr_dentry_unused ;
1925 spinlock_t s_inode_lru_lock ;
1926 struct list_head s_inode_lru ;
1927 int s_nr_inodes_unused ;
1928 struct block_device *s_bdev ;
1929 struct backing_dev_info *s_bdi ;
1930 struct mtd_info *s_mtd ;
1931 struct hlist_node s_instances ;
1932 struct quota_info s_dquot ;
1933 int s_frozen ;
1934 wait_queue_head_t s_wait_unfrozen ;
1935 char s_id[32U] ;
1936 u8 s_uuid[16U] ;
1937 void *s_fs_info ;
1938 unsigned int s_max_links ;
1939 fmode_t s_mode ;
1940 u32 s_time_gran ;
1941 struct mutex s_vfs_rename_mutex ;
1942 char *s_subtype ;
1943 char *s_options ;
1944 struct dentry_operations const *s_d_op ;
1945 int cleancache_poolid ;
1946 struct shrinker s_shrink ;
1947 atomic_long_t s_remove_count ;
1948 int s_readonly_remount ;
1949};
1950#line 1563 "include/linux/fs.h"
1951struct fiemap_extent_info {
1952 unsigned int fi_flags ;
1953 unsigned int fi_extents_mapped ;
1954 unsigned int fi_extents_max ;
1955 struct fiemap_extent *fi_extents_start ;
1956};
1957#line 1602 "include/linux/fs.h"
1958struct file_operations {
1959 struct module *owner ;
1960 loff_t (*llseek)(struct file * , loff_t , int ) ;
1961 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
1962 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
1963 ssize_t (*aio_read)(struct kiocb * , struct iovec const * , unsigned long ,
1964 loff_t ) ;
1965 ssize_t (*aio_write)(struct kiocb * , struct iovec const * , unsigned long ,
1966 loff_t ) ;
1967 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
1968 loff_t , u64 , unsigned int ) ) ;
1969 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1970 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
1971 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
1972 int (*mmap)(struct file * , struct vm_area_struct * ) ;
1973 int (*open)(struct inode * , struct file * ) ;
1974 int (*flush)(struct file * , fl_owner_t ) ;
1975 int (*release)(struct inode * , struct file * ) ;
1976 int (*fsync)(struct file * , loff_t , loff_t , int ) ;
1977 int (*aio_fsync)(struct kiocb * , int ) ;
1978 int (*fasync)(int , struct file * , int ) ;
1979 int (*lock)(struct file * , int , struct file_lock * ) ;
1980 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
1981 int ) ;
1982 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
1983 unsigned long , unsigned long ) ;
1984 int (*check_flags)(int ) ;
1985 int (*flock)(struct file * , int , struct file_lock * ) ;
1986 ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t ,
1987 unsigned int ) ;
1988 ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t ,
1989 unsigned int ) ;
1990 int (*setlease)(struct file * , long , struct file_lock ** ) ;
1991 long (*fallocate)(struct file * , int , loff_t , loff_t ) ;
1992};
1993#line 1637 "include/linux/fs.h"
1994struct inode_operations {
1995 struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1996 void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1997 int (*permission)(struct inode * , int ) ;
1998 struct posix_acl *(*get_acl)(struct inode * , int ) ;
1999 int (*readlink)(struct dentry * , char * , int ) ;
2000 void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
2001 int (*create)(struct inode * , struct dentry * , umode_t , struct nameidata * ) ;
2002 int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
2003 int (*unlink)(struct inode * , struct dentry * ) ;
2004 int (*symlink)(struct inode * , struct dentry * , char const * ) ;
2005 int (*mkdir)(struct inode * , struct dentry * , umode_t ) ;
2006 int (*rmdir)(struct inode * , struct dentry * ) ;
2007 int (*mknod)(struct inode * , struct dentry * , umode_t , dev_t ) ;
2008 int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
2009 void (*truncate)(struct inode * ) ;
2010 int (*setattr)(struct dentry * , struct iattr * ) ;
2011 int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
2012 int (*setxattr)(struct dentry * , char const * , void const * , size_t , int ) ;
2013 ssize_t (*getxattr)(struct dentry * , char const * , void * , size_t ) ;
2014 ssize_t (*listxattr)(struct dentry * , char * , size_t ) ;
2015 int (*removexattr)(struct dentry * , char const * ) ;
2016 void (*truncate_range)(struct inode * , loff_t , loff_t ) ;
2017 int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64 , u64 ) ;
2018};
2019#line 1682 "include/linux/fs.h"
2020struct super_operations {
2021 struct inode *(*alloc_inode)(struct super_block * ) ;
2022 void (*destroy_inode)(struct inode * ) ;
2023 void (*dirty_inode)(struct inode * , int ) ;
2024 int (*write_inode)(struct inode * , struct writeback_control * ) ;
2025 int (*drop_inode)(struct inode * ) ;
2026 void (*evict_inode)(struct inode * ) ;
2027 void (*put_super)(struct super_block * ) ;
2028 void (*write_super)(struct super_block * ) ;
2029 int (*sync_fs)(struct super_block * , int ) ;
2030 int (*freeze_fs)(struct super_block * ) ;
2031 int (*unfreeze_fs)(struct super_block * ) ;
2032 int (*statfs)(struct dentry * , struct kstatfs * ) ;
2033 int (*remount_fs)(struct super_block * , int * , char * ) ;
2034 void (*umount_begin)(struct super_block * ) ;
2035 int (*show_options)(struct seq_file * , struct dentry * ) ;
2036 int (*show_devname)(struct seq_file * , struct dentry * ) ;
2037 int (*show_path)(struct seq_file * , struct dentry * ) ;
2038 int (*show_stats)(struct seq_file * , struct dentry * ) ;
2039 ssize_t (*quota_read)(struct super_block * , int , char * , size_t , loff_t ) ;
2040 ssize_t (*quota_write)(struct super_block * , int , char const * , size_t ,
2041 loff_t ) ;
2042 int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t ) ;
2043 int (*nr_cached_objects)(struct super_block * ) ;
2044 void (*free_cached_objects)(struct super_block * , int ) ;
2045};
2046#line 1834 "include/linux/fs.h"
2047struct file_system_type {
2048 char const *name ;
2049 int fs_flags ;
2050 struct dentry *(*mount)(struct file_system_type * , int , char const * , void * ) ;
2051 void (*kill_sb)(struct super_block * ) ;
2052 struct module *owner ;
2053 struct file_system_type *next ;
2054 struct hlist_head fs_supers ;
2055 struct lock_class_key s_lock_key ;
2056 struct lock_class_key s_umount_key ;
2057 struct lock_class_key s_vfs_rename_key ;
2058 struct lock_class_key i_lock_key ;
2059 struct lock_class_key i_mutex_key ;
2060 struct lock_class_key i_mutex_dir_key ;
2061};
2062#line 34 "include/linux/poll.h"
2063struct poll_table_struct {
2064 void (*_qproc)(struct file * , wait_queue_head_t * , struct poll_table_struct * ) ;
2065 unsigned long _key ;
2066};
2067#line 126 "include/linux/rtc.h"
2068struct rtc_class_ops {
2069 int (*open)(struct device * ) ;
2070 void (*release)(struct device * ) ;
2071 int (*ioctl)(struct device * , unsigned int , unsigned long ) ;
2072 int (*read_time)(struct device * , struct rtc_time * ) ;
2073 int (*set_time)(struct device * , struct rtc_time * ) ;
2074 int (*read_alarm)(struct device * , struct rtc_wkalrm * ) ;
2075 int (*set_alarm)(struct device * , struct rtc_wkalrm * ) ;
2076 int (*proc)(struct device * , struct seq_file * ) ;
2077 int (*set_mmss)(struct device * , unsigned long ) ;
2078 int (*read_callback)(struct device * , int ) ;
2079 int (*alarm_irq_enable)(struct device * , unsigned int ) ;
2080};
2081#line 156 "include/linux/rtc.h"
2082struct rtc_task {
2083 void (*func)(void * ) ;
2084 void *private_data ;
2085};
2086#line 162 "include/linux/rtc.h"
2087struct rtc_timer {
2088 struct rtc_task task ;
2089 struct timerqueue_node node ;
2090 ktime_t period ;
2091 int enabled ;
2092};
2093#line 170 "include/linux/rtc.h"
2094struct rtc_device {
2095 struct device dev ;
2096 struct module *owner ;
2097 int id ;
2098 char name[20U] ;
2099 struct rtc_class_ops const *ops ;
2100 struct mutex ops_lock ;
2101 struct cdev char_dev ;
2102 unsigned long flags ;
2103 unsigned long irq_data ;
2104 spinlock_t irq_lock ;
2105 wait_queue_head_t irq_queue ;
2106 struct fasync_struct *async_queue ;
2107 struct rtc_task *irq_task ;
2108 spinlock_t irq_task_lock ;
2109 int irq_freq ;
2110 int max_user_freq ;
2111 struct timerqueue_head timerqueue ;
2112 struct rtc_timer aie_timer ;
2113 struct rtc_timer uie_rtctimer ;
2114 struct hrtimer pie_timer ;
2115 int pie_enabled ;
2116 struct work_struct irqwork ;
2117 int uie_unsupported ;
2118 struct work_struct uie_task ;
2119 struct timer_list uie_timer ;
2120 unsigned int oldsecs ;
2121 unsigned char uie_irq_active : 1 ;
2122 unsigned char stop_uie_polling : 1 ;
2123 unsigned char uie_task_active : 1 ;
2124 unsigned char uie_timer_active : 1 ;
2125};
2126#line 8 "include/linux/bcd.h"
2127struct v3020_platform_data {
2128 int leftshift ;
2129 unsigned char use_gpio : 1 ;
2130 unsigned int gpio_cs ;
2131 unsigned int gpio_wr ;
2132 unsigned int gpio_rd ;
2133 unsigned int gpio_io ;
2134};
2135#line 28 "include/linux/of.h"
2136typedef u32 phandle;
2137#line 30 "include/linux/of.h"
2138struct property {
2139 char *name ;
2140 int length ;
2141 void *value ;
2142 struct property *next ;
2143 unsigned long _flags ;
2144 unsigned int unique_id ;
2145};
2146#line 39 "include/linux/of.h"
2147struct device_node {
2148 char const *name ;
2149 char const *type ;
2150 phandle phandle ;
2151 char *full_name ;
2152 struct property *properties ;
2153 struct property *deadprops ;
2154 struct device_node *parent ;
2155 struct device_node *child ;
2156 struct device_node *sibling ;
2157 struct device_node *next ;
2158 struct device_node *allnext ;
2159 struct proc_dir_entry *pde ;
2160 struct kref kref ;
2161 unsigned long _flags ;
2162 void *data ;
2163};
2164#line 69 "include/linux/io.h"
2165struct v3020;
2166#line 69
2167struct v3020;
2168#line 70 "include/linux/io.h"
2169struct v3020_chip_ops {
2170 int (*map_io)(struct v3020 * , struct platform_device * , struct v3020_platform_data * ) ;
2171 void (*unmap_io)(struct v3020 * ) ;
2172 unsigned char (*read_bit)(struct v3020 * ) ;
2173 void (*write_bit)(struct v3020 * , unsigned char ) ;
2174};
2175#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2176struct v3020_gpio {
2177 char const *name ;
2178 unsigned int gpio ;
2179};
2180#line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2181struct v3020 {
2182 void *ioaddress ;
2183 int leftshift ;
2184 struct v3020_gpio *gpio ;
2185 struct v3020_chip_ops *ops ;
2186 struct rtc_device *rtc ;
2187};
2188#line 1 "<compiler builtins>"
2189long __builtin_expect(long , long ) ;
2190#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2191void ldv_spin_lock(void) ;
2192#line 3
2193void ldv_spin_unlock(void) ;
2194#line 4
2195int ldv_spin_trylock(void) ;
2196#line 50 "include/linux/dynamic_debug.h"
2197extern int __dynamic_dev_dbg(struct _ddebug * , struct device const * , char const *
2198 , ...) ;
2199#line 27 "include/linux/err.h"
2200__inline static long PTR_ERR(void const *ptr )
2201{
2202
2203 {
2204#line 29
2205 return ((long )ptr);
2206}
2207}
2208#line 32 "include/linux/err.h"
2209__inline static long IS_ERR(void const *ptr )
2210{ long tmp ;
2211 unsigned long __cil_tmp3 ;
2212 int __cil_tmp4 ;
2213 long __cil_tmp5 ;
2214
2215 {
2216 {
2217#line 34
2218 __cil_tmp3 = (unsigned long )ptr;
2219#line 34
2220 __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;
2221#line 34
2222 __cil_tmp5 = (long )__cil_tmp4;
2223#line 34
2224 tmp = __builtin_expect(__cil_tmp5, 0L);
2225 }
2226#line 34
2227 return (tmp);
2228}
2229}
2230#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
2231__inline static unsigned int readl(void const volatile *addr )
2232{ unsigned int ret ;
2233 unsigned int volatile *__cil_tmp3 ;
2234
2235 {
2236#line 55
2237 __cil_tmp3 = (unsigned int volatile *)addr;
2238#line 55
2239 __asm__ volatile ("movl %1,%0": "=r" (ret): "m" (*__cil_tmp3): "memory");
2240#line 55
2241 return (ret);
2242}
2243}
2244#line 63 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
2245__inline static void writel(unsigned int val , void volatile *addr )
2246{ unsigned int volatile *__cil_tmp3 ;
2247
2248 {
2249#line 63
2250 __cil_tmp3 = (unsigned int volatile *)addr;
2251#line 63
2252 __asm__ volatile ("movl %0,%1": : "r" (val), "m" (*__cil_tmp3): "memory");
2253#line 64
2254 return;
2255}
2256}
2257#line 174
2258extern void *ioremap_nocache(resource_size_t , unsigned long ) ;
2259#line 182 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
2260__inline static void *ioremap(resource_size_t offset , unsigned long size )
2261{ void *tmp ;
2262
2263 {
2264 {
2265#line 184
2266 tmp = ioremap_nocache(offset, size);
2267 }
2268#line 184
2269 return (tmp);
2270}
2271}
2272#line 187
2273extern void iounmap(void volatile * ) ;
2274#line 26 "include/linux/export.h"
2275extern struct module __this_module ;
2276#line 161 "include/linux/slab.h"
2277extern void kfree(void const * ) ;
2278#line 220 "include/linux/slub_def.h"
2279extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
2280#line 223
2281void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
2282#line 353 "include/linux/slab.h"
2283__inline static void *kzalloc(size_t size , gfp_t flags ) ;
2284#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2285extern void *__VERIFIER_nondet_pointer(void) ;
2286#line 11
2287void ldv_check_alloc_flags(gfp_t flags ) ;
2288#line 12
2289void ldv_check_alloc_nonatomic(void) ;
2290#line 14
2291struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
2292#line 792 "include/linux/device.h"
2293extern void *dev_get_drvdata(struct device const * ) ;
2294#line 793
2295extern int dev_set_drvdata(struct device * , void * ) ;
2296#line 898
2297extern int _dev_info(struct device const * , char const * , ...) ;
2298#line 183 "include/linux/platform_device.h"
2299__inline static void *platform_get_drvdata(struct platform_device const *pdev )
2300{ void *tmp ;
2301 unsigned long __cil_tmp3 ;
2302 unsigned long __cil_tmp4 ;
2303 struct device const *__cil_tmp5 ;
2304
2305 {
2306 {
2307#line 185
2308 __cil_tmp3 = (unsigned long )pdev;
2309#line 185
2310 __cil_tmp4 = __cil_tmp3 + 16;
2311#line 185
2312 __cil_tmp5 = (struct device const *)__cil_tmp4;
2313#line 185
2314 tmp = dev_get_drvdata(__cil_tmp5);
2315 }
2316#line 185
2317 return (tmp);
2318}
2319}
2320#line 188 "include/linux/platform_device.h"
2321__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
2322{ unsigned long __cil_tmp3 ;
2323 unsigned long __cil_tmp4 ;
2324 struct device *__cil_tmp5 ;
2325
2326 {
2327 {
2328#line 190
2329 __cil_tmp3 = (unsigned long )pdev;
2330#line 190
2331 __cil_tmp4 = __cil_tmp3 + 16;
2332#line 190
2333 __cil_tmp5 = (struct device *)__cil_tmp4;
2334#line 190
2335 dev_set_drvdata(__cil_tmp5, data);
2336 }
2337#line 191
2338 return;
2339}
2340}
2341#line 221 "include/linux/rtc.h"
2342extern struct rtc_device *rtc_device_register(char const * , struct device * , struct rtc_class_ops const * ,
2343 struct module * ) ;
2344#line 225
2345extern void rtc_device_unregister(struct rtc_device * ) ;
2346#line 6 "include/linux/bcd.h"
2347extern unsigned int bcd2bin(unsigned char ) ;
2348#line 7
2349extern unsigned char bin2bcd(unsigned int ) ;
2350#line 10 "include/asm-generic/delay.h"
2351extern void __const_udelay(unsigned long ) ;
2352#line 153 "include/asm-generic/gpio.h"
2353extern int gpio_request(unsigned int , char const * ) ;
2354#line 154
2355extern void gpio_free(unsigned int ) ;
2356#line 156
2357extern int gpio_direction_input(unsigned int ) ;
2358#line 157
2359extern int gpio_direction_output(unsigned int , int ) ;
2360#line 169
2361extern int __gpio_get_value(unsigned int ) ;
2362#line 170
2363extern void __gpio_set_value(unsigned int , int ) ;
2364#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
2365__inline static int gpio_get_value(unsigned int gpio )
2366{ int tmp ;
2367
2368 {
2369 {
2370#line 28
2371 tmp = __gpio_get_value(gpio);
2372 }
2373#line 28
2374 return (tmp);
2375}
2376}
2377#line 31 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/gpio.h"
2378__inline static void gpio_set_value(unsigned int gpio , int value )
2379{
2380
2381 {
2382 {
2383#line 33
2384 __gpio_set_value(gpio, value);
2385 }
2386#line 34
2387 return;
2388}
2389}
2390#line 86 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2391static int v3020_mmio_map(struct v3020 *chip , struct platform_device *pdev , struct v3020_platform_data *pdata )
2392{ unsigned long __cil_tmp4 ;
2393 unsigned long __cil_tmp5 ;
2394 u32 __cil_tmp6 ;
2395 unsigned long __cil_tmp7 ;
2396 unsigned long __cil_tmp8 ;
2397 struct resource *__cil_tmp9 ;
2398 unsigned long __cil_tmp10 ;
2399 unsigned long __cil_tmp11 ;
2400 unsigned long __cil_tmp12 ;
2401 unsigned long __cil_tmp13 ;
2402 unsigned long __cil_tmp14 ;
2403 unsigned long __cil_tmp15 ;
2404 unsigned long __cil_tmp16 ;
2405 struct resource *__cil_tmp17 ;
2406 resource_size_t __cil_tmp18 ;
2407 void *__cil_tmp19 ;
2408 unsigned long __cil_tmp20 ;
2409 void *__cil_tmp21 ;
2410 unsigned long __cil_tmp22 ;
2411
2412 {
2413 {
2414#line 89
2415 __cil_tmp4 = (unsigned long )pdev;
2416#line 89
2417 __cil_tmp5 = __cil_tmp4 + 1168;
2418#line 89
2419 __cil_tmp6 = *((u32 *)__cil_tmp5);
2420#line 89
2421 if (__cil_tmp6 != 1U) {
2422#line 90
2423 return (-16);
2424 } else {
2425
2426 }
2427 }
2428 {
2429#line 92
2430 __cil_tmp7 = (unsigned long )pdev;
2431#line 92
2432 __cil_tmp8 = __cil_tmp7 + 1176;
2433#line 92
2434 __cil_tmp9 = *((struct resource **)__cil_tmp8);
2435#line 92
2436 __cil_tmp10 = (unsigned long )__cil_tmp9;
2437#line 92
2438 __cil_tmp11 = __cil_tmp10 + 24;
2439#line 92
2440 __cil_tmp12 = *((unsigned long *)__cil_tmp11);
2441#line 92
2442 if (__cil_tmp12 != 512UL) {
2443#line 93
2444 return (-16);
2445 } else {
2446
2447 }
2448 }
2449 {
2450#line 95
2451 __cil_tmp13 = (unsigned long )chip;
2452#line 95
2453 __cil_tmp14 = __cil_tmp13 + 8;
2454#line 95
2455 *((int *)__cil_tmp14) = *((int *)pdata);
2456#line 96
2457 __cil_tmp15 = (unsigned long )pdev;
2458#line 96
2459 __cil_tmp16 = __cil_tmp15 + 1176;
2460#line 96
2461 __cil_tmp17 = *((struct resource **)__cil_tmp16);
2462#line 96
2463 __cil_tmp18 = *((resource_size_t *)__cil_tmp17);
2464#line 96
2465 *((void **)chip) = ioremap(__cil_tmp18, 1UL);
2466 }
2467 {
2468#line 97
2469 __cil_tmp19 = (void *)0;
2470#line 97
2471 __cil_tmp20 = (unsigned long )__cil_tmp19;
2472#line 97
2473 __cil_tmp21 = *((void **)chip);
2474#line 97
2475 __cil_tmp22 = (unsigned long )__cil_tmp21;
2476#line 97
2477 if (__cil_tmp22 == __cil_tmp20) {
2478#line 98
2479 return (-16);
2480 } else {
2481
2482 }
2483 }
2484#line 100
2485 return (0);
2486}
2487}
2488#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2489static void v3020_mmio_unmap(struct v3020 *chip )
2490{ void *__cil_tmp2 ;
2491 void volatile *__cil_tmp3 ;
2492
2493 {
2494 {
2495#line 105
2496 __cil_tmp2 = *((void **)chip);
2497#line 105
2498 __cil_tmp3 = (void volatile *)__cil_tmp2;
2499#line 105
2500 iounmap(__cil_tmp3);
2501 }
2502#line 106
2503 return;
2504}
2505}
2506#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2507static void v3020_mmio_write_bit(struct v3020 *chip , unsigned char bit )
2508{ unsigned long __cil_tmp3 ;
2509 unsigned long __cil_tmp4 ;
2510 int __cil_tmp5 ;
2511 int __cil_tmp6 ;
2512 int __cil_tmp7 ;
2513 unsigned int __cil_tmp8 ;
2514 void *__cil_tmp9 ;
2515 void volatile *__cil_tmp10 ;
2516
2517 {
2518 {
2519#line 110
2520 __cil_tmp3 = (unsigned long )chip;
2521#line 110
2522 __cil_tmp4 = __cil_tmp3 + 8;
2523#line 110
2524 __cil_tmp5 = *((int *)__cil_tmp4);
2525#line 110
2526 __cil_tmp6 = (int )bit;
2527#line 110
2528 __cil_tmp7 = __cil_tmp6 << __cil_tmp5;
2529#line 110
2530 __cil_tmp8 = (unsigned int )__cil_tmp7;
2531#line 110
2532 __cil_tmp9 = *((void **)chip);
2533#line 110
2534 __cil_tmp10 = (void volatile *)__cil_tmp9;
2535#line 110
2536 writel(__cil_tmp8, __cil_tmp10);
2537 }
2538#line 111
2539 return;
2540}
2541}
2542#line 113 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2543static unsigned char v3020_mmio_read_bit(struct v3020 *chip )
2544{ unsigned int tmp ;
2545 void *__cil_tmp3 ;
2546 void const volatile *__cil_tmp4 ;
2547 unsigned long __cil_tmp5 ;
2548 unsigned long __cil_tmp6 ;
2549 int __cil_tmp7 ;
2550 int __cil_tmp8 ;
2551 unsigned int __cil_tmp9 ;
2552 unsigned int __cil_tmp10 ;
2553 int __cil_tmp11 ;
2554
2555 {
2556 {
2557#line 115
2558 __cil_tmp3 = *((void **)chip);
2559#line 115
2560 __cil_tmp4 = (void const volatile *)__cil_tmp3;
2561#line 115
2562 tmp = readl(__cil_tmp4);
2563 }
2564 {
2565#line 115
2566 __cil_tmp5 = (unsigned long )chip;
2567#line 115
2568 __cil_tmp6 = __cil_tmp5 + 8;
2569#line 115
2570 __cil_tmp7 = *((int *)__cil_tmp6);
2571#line 115
2572 __cil_tmp8 = 1 << __cil_tmp7;
2573#line 115
2574 __cil_tmp9 = (unsigned int )__cil_tmp8;
2575#line 115
2576 __cil_tmp10 = tmp & __cil_tmp9;
2577#line 115
2578 __cil_tmp11 = __cil_tmp10 != 0U;
2579#line 115
2580 return ((unsigned char )__cil_tmp11);
2581 }
2582}
2583}
2584#line 118 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2585static struct v3020_chip_ops v3020_mmio_ops = {& v3020_mmio_map, & v3020_mmio_unmap, & v3020_mmio_read_bit, & v3020_mmio_write_bit};
2586#line 125 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2587static struct v3020_gpio v3020_gpio[4U] = { {"RTC CS", 0U},
2588 {"RTC WR", 0U},
2589 {"RTC RD", 0U},
2590 {"RTC IO", 0U}};
2591#line 132 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2592static int v3020_gpio_map(struct v3020 *chip , struct platform_device *pdev , struct v3020_platform_data *pdata )
2593{ int i ;
2594 int err ;
2595 unsigned long __cil_tmp6 ;
2596 unsigned long __cil_tmp7 ;
2597 unsigned long __cil_tmp8 ;
2598 unsigned long __cil_tmp9 ;
2599 unsigned long __cil_tmp10 ;
2600 unsigned long __cil_tmp11 ;
2601 unsigned long __cil_tmp12 ;
2602 unsigned long __cil_tmp13 ;
2603 unsigned long __cil_tmp14 ;
2604 unsigned long __cil_tmp15 ;
2605 unsigned long __cil_tmp16 ;
2606 unsigned long __cil_tmp17 ;
2607 unsigned long __cil_tmp18 ;
2608 unsigned long __cil_tmp19 ;
2609 unsigned long __cil_tmp20 ;
2610 unsigned long __cil_tmp21 ;
2611 unsigned long __cil_tmp22 ;
2612 unsigned long __cil_tmp23 ;
2613 unsigned long __cil_tmp24 ;
2614 unsigned long __cil_tmp25 ;
2615 unsigned long __cil_tmp26 ;
2616 unsigned long __cil_tmp27 ;
2617 unsigned long __cil_tmp28 ;
2618 unsigned int __cil_tmp29 ;
2619 unsigned long __cil_tmp30 ;
2620 unsigned long __cil_tmp31 ;
2621 char const *__cil_tmp32 ;
2622 unsigned long __cil_tmp33 ;
2623 unsigned long __cil_tmp34 ;
2624 unsigned long __cil_tmp35 ;
2625 unsigned int __cil_tmp36 ;
2626 unsigned int __cil_tmp37 ;
2627 unsigned long __cil_tmp38 ;
2628 unsigned long __cil_tmp39 ;
2629 unsigned long __cil_tmp40 ;
2630 unsigned long __cil_tmp41 ;
2631 unsigned long __cil_tmp42 ;
2632 unsigned int __cil_tmp43 ;
2633
2634 {
2635#line 137
2636 __cil_tmp6 = 0 * 16UL;
2637#line 137
2638 __cil_tmp7 = __cil_tmp6 + 8;
2639#line 137
2640 __cil_tmp8 = (unsigned long )(v3020_gpio) + __cil_tmp7;
2641#line 137
2642 __cil_tmp9 = (unsigned long )pdata;
2643#line 137
2644 __cil_tmp10 = __cil_tmp9 + 8;
2645#line 137
2646 *((unsigned int *)__cil_tmp8) = *((unsigned int *)__cil_tmp10);
2647#line 138
2648 __cil_tmp11 = 1 * 16UL;
2649#line 138
2650 __cil_tmp12 = __cil_tmp11 + 8;
2651#line 138
2652 __cil_tmp13 = (unsigned long )(v3020_gpio) + __cil_tmp12;
2653#line 138
2654 __cil_tmp14 = (unsigned long )pdata;
2655#line 138
2656 __cil_tmp15 = __cil_tmp14 + 12;
2657#line 138
2658 *((unsigned int *)__cil_tmp13) = *((unsigned int *)__cil_tmp15);
2659#line 139
2660 __cil_tmp16 = 2 * 16UL;
2661#line 139
2662 __cil_tmp17 = __cil_tmp16 + 8;
2663#line 139
2664 __cil_tmp18 = (unsigned long )(v3020_gpio) + __cil_tmp17;
2665#line 139
2666 __cil_tmp19 = (unsigned long )pdata;
2667#line 139
2668 __cil_tmp20 = __cil_tmp19 + 16;
2669#line 139
2670 *((unsigned int *)__cil_tmp18) = *((unsigned int *)__cil_tmp20);
2671#line 140
2672 __cil_tmp21 = 3 * 16UL;
2673#line 140
2674 __cil_tmp22 = __cil_tmp21 + 8;
2675#line 140
2676 __cil_tmp23 = (unsigned long )(v3020_gpio) + __cil_tmp22;
2677#line 140
2678 __cil_tmp24 = (unsigned long )pdata;
2679#line 140
2680 __cil_tmp25 = __cil_tmp24 + 20;
2681#line 140
2682 *((unsigned int *)__cil_tmp23) = *((unsigned int *)__cil_tmp25);
2683#line 142
2684 i = 0;
2685#line 142
2686 goto ldv_21245;
2687 ldv_21244:
2688 {
2689#line 143
2690 __cil_tmp26 = i * 16UL;
2691#line 143
2692 __cil_tmp27 = __cil_tmp26 + 8;
2693#line 143
2694 __cil_tmp28 = (unsigned long )(v3020_gpio) + __cil_tmp27;
2695#line 143
2696 __cil_tmp29 = *((unsigned int *)__cil_tmp28);
2697#line 143
2698 __cil_tmp30 = i * 16UL;
2699#line 143
2700 __cil_tmp31 = (unsigned long )(v3020_gpio) + __cil_tmp30;
2701#line 143
2702 __cil_tmp32 = *((char const **)__cil_tmp31);
2703#line 143
2704 err = gpio_request(__cil_tmp29, __cil_tmp32);
2705 }
2706#line 144
2707 if (err != 0) {
2708#line 145
2709 goto err_request;
2710 } else {
2711
2712 }
2713 {
2714#line 147
2715 __cil_tmp33 = i * 16UL;
2716#line 147
2717 __cil_tmp34 = __cil_tmp33 + 8;
2718#line 147
2719 __cil_tmp35 = (unsigned long )(v3020_gpio) + __cil_tmp34;
2720#line 147
2721 __cil_tmp36 = *((unsigned int *)__cil_tmp35);
2722#line 147
2723 gpio_direction_output(__cil_tmp36, 1);
2724#line 142
2725 i = i + 1;
2726 }
2727 ldv_21245: ;
2728 {
2729#line 142
2730 __cil_tmp37 = (unsigned int )i;
2731#line 142
2732 if (__cil_tmp37 <= 3U) {
2733#line 143
2734 goto ldv_21244;
2735 } else {
2736#line 145
2737 goto ldv_21246;
2738 }
2739 }
2740 ldv_21246:
2741#line 150
2742 __cil_tmp38 = (unsigned long )chip;
2743#line 150
2744 __cil_tmp39 = __cil_tmp38 + 16;
2745#line 150
2746 *((struct v3020_gpio **)__cil_tmp39) = (struct v3020_gpio *)(& v3020_gpio);
2747#line 152
2748 return (0);
2749 err_request: ;
2750#line 155
2751 goto ldv_21248;
2752 ldv_21247:
2753 {
2754#line 156
2755 __cil_tmp40 = i * 16UL;
2756#line 156
2757 __cil_tmp41 = __cil_tmp40 + 8;
2758#line 156
2759 __cil_tmp42 = (unsigned long )(v3020_gpio) + __cil_tmp41;
2760#line 156
2761 __cil_tmp43 = *((unsigned int *)__cil_tmp42);
2762#line 156
2763 gpio_free(__cil_tmp43);
2764 }
2765 ldv_21248:
2766#line 155
2767 i = i - 1;
2768#line 155
2769 if (i >= 0) {
2770#line 156
2771 goto ldv_21247;
2772 } else {
2773#line 158
2774 goto ldv_21249;
2775 }
2776 ldv_21249: ;
2777#line 158
2778 return (err);
2779}
2780}
2781#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2782static void v3020_gpio_unmap(struct v3020 *chip )
2783{ int i ;
2784 unsigned long __cil_tmp3 ;
2785 unsigned long __cil_tmp4 ;
2786 unsigned long __cil_tmp5 ;
2787 unsigned int __cil_tmp6 ;
2788 unsigned int __cil_tmp7 ;
2789
2790 {
2791#line 165
2792 i = 0;
2793#line 165
2794 goto ldv_21257;
2795 ldv_21256:
2796 {
2797#line 166
2798 __cil_tmp3 = i * 16UL;
2799#line 166
2800 __cil_tmp4 = __cil_tmp3 + 8;
2801#line 166
2802 __cil_tmp5 = (unsigned long )(v3020_gpio) + __cil_tmp4;
2803#line 166
2804 __cil_tmp6 = *((unsigned int *)__cil_tmp5);
2805#line 166
2806 gpio_free(__cil_tmp6);
2807#line 165
2808 i = i + 1;
2809 }
2810 ldv_21257: ;
2811 {
2812#line 165
2813 __cil_tmp7 = (unsigned int )i;
2814#line 165
2815 if (__cil_tmp7 <= 3U) {
2816#line 166
2817 goto ldv_21256;
2818 } else {
2819#line 168
2820 goto ldv_21258;
2821 }
2822 }
2823 ldv_21258: ;
2824#line 170
2825 return;
2826}
2827}
2828#line 169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2829static void v3020_gpio_write_bit(struct v3020 *chip , unsigned char bit )
2830{ unsigned long __cil_tmp3 ;
2831 unsigned long __cil_tmp4 ;
2832 struct v3020_gpio *__cil_tmp5 ;
2833 struct v3020_gpio *__cil_tmp6 ;
2834 unsigned long __cil_tmp7 ;
2835 unsigned long __cil_tmp8 ;
2836 unsigned int __cil_tmp9 ;
2837 int __cil_tmp10 ;
2838 unsigned long __cil_tmp11 ;
2839 unsigned long __cil_tmp12 ;
2840 struct v3020_gpio *__cil_tmp13 ;
2841 unsigned long __cil_tmp14 ;
2842 unsigned long __cil_tmp15 ;
2843 unsigned int __cil_tmp16 ;
2844 unsigned long __cil_tmp17 ;
2845 unsigned long __cil_tmp18 ;
2846 struct v3020_gpio *__cil_tmp19 ;
2847 struct v3020_gpio *__cil_tmp20 ;
2848 unsigned long __cil_tmp21 ;
2849 unsigned long __cil_tmp22 ;
2850 unsigned int __cil_tmp23 ;
2851 unsigned long __cil_tmp24 ;
2852 unsigned long __cil_tmp25 ;
2853 struct v3020_gpio *__cil_tmp26 ;
2854 struct v3020_gpio *__cil_tmp27 ;
2855 unsigned long __cil_tmp28 ;
2856 unsigned long __cil_tmp29 ;
2857 unsigned int __cil_tmp30 ;
2858 unsigned long __cil_tmp31 ;
2859 unsigned long __cil_tmp32 ;
2860 struct v3020_gpio *__cil_tmp33 ;
2861 unsigned long __cil_tmp34 ;
2862 unsigned long __cil_tmp35 ;
2863 unsigned int __cil_tmp36 ;
2864
2865 {
2866 {
2867#line 171
2868 __cil_tmp3 = (unsigned long )chip;
2869#line 171
2870 __cil_tmp4 = __cil_tmp3 + 16;
2871#line 171
2872 __cil_tmp5 = *((struct v3020_gpio **)__cil_tmp4);
2873#line 171
2874 __cil_tmp6 = __cil_tmp5 + 3UL;
2875#line 171
2876 __cil_tmp7 = (unsigned long )__cil_tmp6;
2877#line 171
2878 __cil_tmp8 = __cil_tmp7 + 8;
2879#line 171
2880 __cil_tmp9 = *((unsigned int *)__cil_tmp8);
2881#line 171
2882 __cil_tmp10 = (int )bit;
2883#line 171
2884 gpio_direction_output(__cil_tmp9, __cil_tmp10);
2885#line 172
2886 __cil_tmp11 = (unsigned long )chip;
2887#line 172
2888 __cil_tmp12 = __cil_tmp11 + 16;
2889#line 172
2890 __cil_tmp13 = *((struct v3020_gpio **)__cil_tmp12);
2891#line 172
2892 __cil_tmp14 = (unsigned long )__cil_tmp13;
2893#line 172
2894 __cil_tmp15 = __cil_tmp14 + 8;
2895#line 172
2896 __cil_tmp16 = *((unsigned int *)__cil_tmp15);
2897#line 172
2898 gpio_set_value(__cil_tmp16, 0);
2899#line 173
2900 __cil_tmp17 = (unsigned long )chip;
2901#line 173
2902 __cil_tmp18 = __cil_tmp17 + 16;
2903#line 173
2904 __cil_tmp19 = *((struct v3020_gpio **)__cil_tmp18);
2905#line 173
2906 __cil_tmp20 = __cil_tmp19 + 1UL;
2907#line 173
2908 __cil_tmp21 = (unsigned long )__cil_tmp20;
2909#line 173
2910 __cil_tmp22 = __cil_tmp21 + 8;
2911#line 173
2912 __cil_tmp23 = *((unsigned int *)__cil_tmp22);
2913#line 173
2914 gpio_set_value(__cil_tmp23, 0);
2915#line 174
2916 __const_udelay(4295UL);
2917#line 175
2918 __cil_tmp24 = (unsigned long )chip;
2919#line 175
2920 __cil_tmp25 = __cil_tmp24 + 16;
2921#line 175
2922 __cil_tmp26 = *((struct v3020_gpio **)__cil_tmp25);
2923#line 175
2924 __cil_tmp27 = __cil_tmp26 + 1UL;
2925#line 175
2926 __cil_tmp28 = (unsigned long )__cil_tmp27;
2927#line 175
2928 __cil_tmp29 = __cil_tmp28 + 8;
2929#line 175
2930 __cil_tmp30 = *((unsigned int *)__cil_tmp29);
2931#line 175
2932 gpio_set_value(__cil_tmp30, 1);
2933#line 176
2934 __cil_tmp31 = (unsigned long )chip;
2935#line 176
2936 __cil_tmp32 = __cil_tmp31 + 16;
2937#line 176
2938 __cil_tmp33 = *((struct v3020_gpio **)__cil_tmp32);
2939#line 176
2940 __cil_tmp34 = (unsigned long )__cil_tmp33;
2941#line 176
2942 __cil_tmp35 = __cil_tmp34 + 8;
2943#line 176
2944 __cil_tmp36 = *((unsigned int *)__cil_tmp35);
2945#line 176
2946 gpio_set_value(__cil_tmp36, 1);
2947 }
2948#line 177
2949 return;
2950}
2951}
2952#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
2953static unsigned char v3020_gpio_read_bit(struct v3020 *chip )
2954{ int bit ;
2955 int tmp ;
2956 unsigned long __cil_tmp4 ;
2957 unsigned long __cil_tmp5 ;
2958 struct v3020_gpio *__cil_tmp6 ;
2959 struct v3020_gpio *__cil_tmp7 ;
2960 unsigned long __cil_tmp8 ;
2961 unsigned long __cil_tmp9 ;
2962 unsigned int __cil_tmp10 ;
2963 unsigned long __cil_tmp11 ;
2964 unsigned long __cil_tmp12 ;
2965 struct v3020_gpio *__cil_tmp13 ;
2966 unsigned long __cil_tmp14 ;
2967 unsigned long __cil_tmp15 ;
2968 unsigned int __cil_tmp16 ;
2969 unsigned long __cil_tmp17 ;
2970 unsigned long __cil_tmp18 ;
2971 struct v3020_gpio *__cil_tmp19 ;
2972 struct v3020_gpio *__cil_tmp20 ;
2973 unsigned long __cil_tmp21 ;
2974 unsigned long __cil_tmp22 ;
2975 unsigned int __cil_tmp23 ;
2976 unsigned long __cil_tmp24 ;
2977 unsigned long __cil_tmp25 ;
2978 struct v3020_gpio *__cil_tmp26 ;
2979 struct v3020_gpio *__cil_tmp27 ;
2980 unsigned long __cil_tmp28 ;
2981 unsigned long __cil_tmp29 ;
2982 unsigned int __cil_tmp30 ;
2983 unsigned long __cil_tmp31 ;
2984 unsigned long __cil_tmp32 ;
2985 struct v3020_gpio *__cil_tmp33 ;
2986 struct v3020_gpio *__cil_tmp34 ;
2987 unsigned long __cil_tmp35 ;
2988 unsigned long __cil_tmp36 ;
2989 unsigned int __cil_tmp37 ;
2990 unsigned long __cil_tmp38 ;
2991 unsigned long __cil_tmp39 ;
2992 struct v3020_gpio *__cil_tmp40 ;
2993 unsigned long __cil_tmp41 ;
2994 unsigned long __cil_tmp42 ;
2995 unsigned int __cil_tmp43 ;
2996
2997 {
2998 {
2999#line 183
3000 __cil_tmp4 = (unsigned long )chip;
3001#line 183
3002 __cil_tmp5 = __cil_tmp4 + 16;
3003#line 183
3004 __cil_tmp6 = *((struct v3020_gpio **)__cil_tmp5);
3005#line 183
3006 __cil_tmp7 = __cil_tmp6 + 3UL;
3007#line 183
3008 __cil_tmp8 = (unsigned long )__cil_tmp7;
3009#line 183
3010 __cil_tmp9 = __cil_tmp8 + 8;
3011#line 183
3012 __cil_tmp10 = *((unsigned int *)__cil_tmp9);
3013#line 183
3014 gpio_direction_input(__cil_tmp10);
3015#line 184
3016 __cil_tmp11 = (unsigned long )chip;
3017#line 184
3018 __cil_tmp12 = __cil_tmp11 + 16;
3019#line 184
3020 __cil_tmp13 = *((struct v3020_gpio **)__cil_tmp12);
3021#line 184
3022 __cil_tmp14 = (unsigned long )__cil_tmp13;
3023#line 184
3024 __cil_tmp15 = __cil_tmp14 + 8;
3025#line 184
3026 __cil_tmp16 = *((unsigned int *)__cil_tmp15);
3027#line 184
3028 gpio_set_value(__cil_tmp16, 0);
3029#line 185
3030 __cil_tmp17 = (unsigned long )chip;
3031#line 185
3032 __cil_tmp18 = __cil_tmp17 + 16;
3033#line 185
3034 __cil_tmp19 = *((struct v3020_gpio **)__cil_tmp18);
3035#line 185
3036 __cil_tmp20 = __cil_tmp19 + 2UL;
3037#line 185
3038 __cil_tmp21 = (unsigned long )__cil_tmp20;
3039#line 185
3040 __cil_tmp22 = __cil_tmp21 + 8;
3041#line 185
3042 __cil_tmp23 = *((unsigned int *)__cil_tmp22);
3043#line 185
3044 gpio_set_value(__cil_tmp23, 0);
3045#line 186
3046 __const_udelay(4295UL);
3047#line 187
3048 __cil_tmp24 = (unsigned long )chip;
3049#line 187
3050 __cil_tmp25 = __cil_tmp24 + 16;
3051#line 187
3052 __cil_tmp26 = *((struct v3020_gpio **)__cil_tmp25);
3053#line 187
3054 __cil_tmp27 = __cil_tmp26 + 3UL;
3055#line 187
3056 __cil_tmp28 = (unsigned long )__cil_tmp27;
3057#line 187
3058 __cil_tmp29 = __cil_tmp28 + 8;
3059#line 187
3060 __cil_tmp30 = *((unsigned int *)__cil_tmp29);
3061#line 187
3062 tmp = gpio_get_value(__cil_tmp30);
3063#line 187
3064 bit = tmp != 0;
3065#line 188
3066 __const_udelay(4295UL);
3067#line 189
3068 __cil_tmp31 = (unsigned long )chip;
3069#line 189
3070 __cil_tmp32 = __cil_tmp31 + 16;
3071#line 189
3072 __cil_tmp33 = *((struct v3020_gpio **)__cil_tmp32);
3073#line 189
3074 __cil_tmp34 = __cil_tmp33 + 2UL;
3075#line 189
3076 __cil_tmp35 = (unsigned long )__cil_tmp34;
3077#line 189
3078 __cil_tmp36 = __cil_tmp35 + 8;
3079#line 189
3080 __cil_tmp37 = *((unsigned int *)__cil_tmp36);
3081#line 189
3082 gpio_set_value(__cil_tmp37, 1);
3083#line 190
3084 __cil_tmp38 = (unsigned long )chip;
3085#line 190
3086 __cil_tmp39 = __cil_tmp38 + 16;
3087#line 190
3088 __cil_tmp40 = *((struct v3020_gpio **)__cil_tmp39);
3089#line 190
3090 __cil_tmp41 = (unsigned long )__cil_tmp40;
3091#line 190
3092 __cil_tmp42 = __cil_tmp41 + 8;
3093#line 190
3094 __cil_tmp43 = *((unsigned int *)__cil_tmp42);
3095#line 190
3096 gpio_set_value(__cil_tmp43, 1);
3097 }
3098#line 192
3099 return ((unsigned char )bit);
3100}
3101}
3102#line 195 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
3103static struct v3020_chip_ops v3020_gpio_ops = {& v3020_gpio_map, & v3020_gpio_unmap, & v3020_gpio_read_bit, & v3020_gpio_write_bit};
3104#line 202 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
3105static void v3020_set_reg(struct v3020 *chip , unsigned char address , unsigned char data )
3106{ int i ;
3107 unsigned char tmp ;
3108 unsigned long __cil_tmp6 ;
3109 unsigned long __cil_tmp7 ;
3110 struct v3020_chip_ops *__cil_tmp8 ;
3111 unsigned long __cil_tmp9 ;
3112 unsigned long __cil_tmp10 ;
3113 void (*__cil_tmp11)(struct v3020 * , unsigned char ) ;
3114 int __cil_tmp12 ;
3115 int __cil_tmp13 ;
3116 unsigned char __cil_tmp14 ;
3117 int __cil_tmp15 ;
3118 int __cil_tmp16 ;
3119 unsigned int __cil_tmp17 ;
3120 unsigned long __cil_tmp18 ;
3121 unsigned long __cil_tmp19 ;
3122 struct v3020_chip_ops *__cil_tmp20 ;
3123 unsigned long __cil_tmp21 ;
3124 unsigned long __cil_tmp22 ;
3125 void (*__cil_tmp23)(struct v3020 * , unsigned char ) ;
3126 int __cil_tmp24 ;
3127 int __cil_tmp25 ;
3128 unsigned char __cil_tmp26 ;
3129 int __cil_tmp27 ;
3130 int __cil_tmp28 ;
3131
3132 {
3133#line 208
3134 tmp = address;
3135#line 209
3136 i = 0;
3137#line 209
3138 goto ldv_21276;
3139 ldv_21275:
3140 {
3141#line 210
3142 __cil_tmp6 = (unsigned long )chip;
3143#line 210
3144 __cil_tmp7 = __cil_tmp6 + 24;
3145#line 210
3146 __cil_tmp8 = *((struct v3020_chip_ops **)__cil_tmp7);
3147#line 210
3148 __cil_tmp9 = (unsigned long )__cil_tmp8;
3149#line 210
3150 __cil_tmp10 = __cil_tmp9 + 24;
3151#line 210
3152 __cil_tmp11 = *((void (**)(struct v3020 * , unsigned char ))__cil_tmp10);
3153#line 210
3154 __cil_tmp12 = (int )tmp;
3155#line 210
3156 __cil_tmp13 = __cil_tmp12 & 1;
3157#line 210
3158 __cil_tmp14 = (unsigned char )__cil_tmp13;
3159#line 210
3160 (*__cil_tmp11)(chip, __cil_tmp14);
3161#line 211
3162 __cil_tmp15 = (int )tmp;
3163#line 211
3164 __cil_tmp16 = __cil_tmp15 >> 1;
3165#line 211
3166 tmp = (unsigned char )__cil_tmp16;
3167#line 212
3168 __const_udelay(4295UL);
3169#line 209
3170 i = i + 1;
3171 }
3172 ldv_21276: ;
3173#line 209
3174 if (i <= 3) {
3175#line 210
3176 goto ldv_21275;
3177 } else {
3178#line 212
3179 goto ldv_21277;
3180 }
3181 ldv_21277: ;
3182 {
3183#line 216
3184 __cil_tmp17 = (unsigned int )address;
3185#line 216
3186 if (__cil_tmp17 <= 13U) {
3187#line 217
3188 i = 0;
3189#line 217
3190 goto ldv_21279;
3191 ldv_21278:
3192 {
3193#line 218
3194 __cil_tmp18 = (unsigned long )chip;
3195#line 218
3196 __cil_tmp19 = __cil_tmp18 + 24;
3197#line 218
3198 __cil_tmp20 = *((struct v3020_chip_ops **)__cil_tmp19);
3199#line 218
3200 __cil_tmp21 = (unsigned long )__cil_tmp20;
3201#line 218
3202 __cil_tmp22 = __cil_tmp21 + 24;
3203#line 218
3204 __cil_tmp23 = *((void (**)(struct v3020 * , unsigned char ))__cil_tmp22);
3205#line 218
3206 __cil_tmp24 = (int )data;
3207#line 218
3208 __cil_tmp25 = __cil_tmp24 & 1;
3209#line 218
3210 __cil_tmp26 = (unsigned char )__cil_tmp25;
3211#line 218
3212 (*__cil_tmp23)(chip, __cil_tmp26);
3213#line 219
3214 __cil_tmp27 = (int )data;
3215#line 219
3216 __cil_tmp28 = __cil_tmp27 >> 1;
3217#line 219
3218 data = (unsigned char )__cil_tmp28;
3219#line 220
3220 __const_udelay(4295UL);
3221#line 217
3222 i = i + 1;
3223 }
3224 ldv_21279: ;
3225#line 217
3226 if (i <= 7) {
3227#line 218
3228 goto ldv_21278;
3229 } else {
3230#line 220
3231 goto ldv_21280;
3232 }
3233 ldv_21280: ;
3234 } else {
3235
3236 }
3237 }
3238#line 223
3239 return;
3240}
3241}
3242#line 225 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
3243static unsigned char v3020_get_reg(struct v3020 *chip , unsigned char address )
3244{ unsigned int data ;
3245 int i ;
3246 unsigned char tmp ;
3247 unsigned long __cil_tmp6 ;
3248 unsigned long __cil_tmp7 ;
3249 struct v3020_chip_ops *__cil_tmp8 ;
3250 unsigned long __cil_tmp9 ;
3251 unsigned long __cil_tmp10 ;
3252 void (*__cil_tmp11)(struct v3020 * , unsigned char ) ;
3253 int __cil_tmp12 ;
3254 int __cil_tmp13 ;
3255 unsigned char __cil_tmp14 ;
3256 int __cil_tmp15 ;
3257 int __cil_tmp16 ;
3258 unsigned long __cil_tmp17 ;
3259 unsigned long __cil_tmp18 ;
3260 struct v3020_chip_ops *__cil_tmp19 ;
3261 unsigned long __cil_tmp20 ;
3262 unsigned long __cil_tmp21 ;
3263 unsigned char (*__cil_tmp22)(struct v3020 * ) ;
3264 unsigned int __cil_tmp23 ;
3265
3266 {
3267#line 227
3268 data = 0U;
3269#line 230
3270 i = 0;
3271#line 230
3272 goto ldv_21288;
3273 ldv_21287:
3274 {
3275#line 231
3276 __cil_tmp6 = (unsigned long )chip;
3277#line 231
3278 __cil_tmp7 = __cil_tmp6 + 24;
3279#line 231
3280 __cil_tmp8 = *((struct v3020_chip_ops **)__cil_tmp7);
3281#line 231
3282 __cil_tmp9 = (unsigned long )__cil_tmp8;
3283#line 231
3284 __cil_tmp10 = __cil_tmp9 + 24;
3285#line 231
3286 __cil_tmp11 = *((void (**)(struct v3020 * , unsigned char ))__cil_tmp10);
3287#line 231
3288 __cil_tmp12 = (int )address;
3289#line 231
3290 __cil_tmp13 = __cil_tmp12 & 1;
3291#line 231
3292 __cil_tmp14 = (unsigned char )__cil_tmp13;
3293#line 231
3294 (*__cil_tmp11)(chip, __cil_tmp14);
3295#line 232
3296 __cil_tmp15 = (int )address;
3297#line 232
3298 __cil_tmp16 = __cil_tmp15 >> 1;
3299#line 232
3300 address = (unsigned char )__cil_tmp16;
3301#line 233
3302 __const_udelay(4295UL);
3303#line 230
3304 i = i + 1;
3305 }
3306 ldv_21288: ;
3307#line 230
3308 if (i <= 3) {
3309#line 231
3310 goto ldv_21287;
3311 } else {
3312#line 233
3313 goto ldv_21289;
3314 }
3315 ldv_21289:
3316#line 236
3317 i = 0;
3318#line 236
3319 goto ldv_21291;
3320 ldv_21290:
3321 {
3322#line 237
3323 data = data >> 1;
3324#line 238
3325 __cil_tmp17 = (unsigned long )chip;
3326#line 238
3327 __cil_tmp18 = __cil_tmp17 + 24;
3328#line 238
3329 __cil_tmp19 = *((struct v3020_chip_ops **)__cil_tmp18);
3330#line 238
3331 __cil_tmp20 = (unsigned long )__cil_tmp19;
3332#line 238
3333 __cil_tmp21 = __cil_tmp20 + 16;
3334#line 238
3335 __cil_tmp22 = *((unsigned char (**)(struct v3020 * ))__cil_tmp21);
3336#line 238
3337 tmp = (*__cil_tmp22)(chip);
3338 }
3339 {
3340#line 238
3341 __cil_tmp23 = (unsigned int )tmp;
3342#line 238
3343 if (__cil_tmp23 != 0U) {
3344#line 239
3345 data = data | 128U;
3346 } else {
3347
3348 }
3349 }
3350 {
3351#line 240
3352 __const_udelay(4295UL);
3353#line 236
3354 i = i + 1;
3355 }
3356 ldv_21291: ;
3357#line 236
3358 if (i <= 7) {
3359#line 237
3360 goto ldv_21290;
3361 } else {
3362#line 239
3363 goto ldv_21292;
3364 }
3365 ldv_21292: ;
3366#line 243
3367 return ((unsigned char )data);
3368}
3369}
3370#line 246 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
3371static int v3020_read_time(struct device *dev , struct rtc_time *dt )
3372{ struct v3020 *chip ;
3373 void *tmp ;
3374 int tmp___0 ;
3375 unsigned char tmp___1 ;
3376 unsigned int tmp___2 ;
3377 unsigned char tmp___3 ;
3378 unsigned int tmp___4 ;
3379 unsigned char tmp___5 ;
3380 unsigned int tmp___6 ;
3381 unsigned char tmp___7 ;
3382 unsigned int tmp___8 ;
3383 unsigned char tmp___9 ;
3384 unsigned int tmp___10 ;
3385 unsigned char tmp___11 ;
3386 unsigned int tmp___12 ;
3387 unsigned char tmp___13 ;
3388 unsigned int tmp___14 ;
3389 struct _ddebug descriptor ;
3390 long tmp___15 ;
3391 struct _ddebug descriptor___0 ;
3392 long tmp___16 ;
3393 struct _ddebug descriptor___1 ;
3394 long tmp___17 ;
3395 struct _ddebug descriptor___2 ;
3396 long tmp___18 ;
3397 struct _ddebug descriptor___3 ;
3398 long tmp___19 ;
3399 struct _ddebug descriptor___4 ;
3400 long tmp___20 ;
3401 struct _ddebug descriptor___5 ;
3402 long tmp___21 ;
3403 struct _ddebug descriptor___6 ;
3404 long tmp___22 ;
3405 struct device const *__cil_tmp36 ;
3406 unsigned char __cil_tmp37 ;
3407 int __cil_tmp38 ;
3408 unsigned char __cil_tmp39 ;
3409 unsigned char __cil_tmp40 ;
3410 int __cil_tmp41 ;
3411 unsigned char __cil_tmp42 ;
3412 unsigned long __cil_tmp43 ;
3413 unsigned long __cil_tmp44 ;
3414 unsigned char __cil_tmp45 ;
3415 int __cil_tmp46 ;
3416 unsigned char __cil_tmp47 ;
3417 unsigned long __cil_tmp48 ;
3418 unsigned long __cil_tmp49 ;
3419 unsigned char __cil_tmp50 ;
3420 int __cil_tmp51 ;
3421 unsigned char __cil_tmp52 ;
3422 unsigned long __cil_tmp53 ;
3423 unsigned long __cil_tmp54 ;
3424 unsigned char __cil_tmp55 ;
3425 int __cil_tmp56 ;
3426 unsigned char __cil_tmp57 ;
3427 unsigned long __cil_tmp58 ;
3428 unsigned long __cil_tmp59 ;
3429 unsigned int __cil_tmp60 ;
3430 unsigned char __cil_tmp61 ;
3431 int __cil_tmp62 ;
3432 unsigned char __cil_tmp63 ;
3433 unsigned long __cil_tmp64 ;
3434 unsigned long __cil_tmp65 ;
3435 unsigned char __cil_tmp66 ;
3436 int __cil_tmp67 ;
3437 unsigned char __cil_tmp68 ;
3438 unsigned long __cil_tmp69 ;
3439 unsigned long __cil_tmp70 ;
3440 unsigned int __cil_tmp71 ;
3441 struct _ddebug *__cil_tmp72 ;
3442 unsigned long __cil_tmp73 ;
3443 unsigned long __cil_tmp74 ;
3444 unsigned long __cil_tmp75 ;
3445 unsigned long __cil_tmp76 ;
3446 unsigned long __cil_tmp77 ;
3447 unsigned long __cil_tmp78 ;
3448 unsigned char __cil_tmp79 ;
3449 long __cil_tmp80 ;
3450 long __cil_tmp81 ;
3451 struct device const *__cil_tmp82 ;
3452 struct _ddebug *__cil_tmp83 ;
3453 unsigned long __cil_tmp84 ;
3454 unsigned long __cil_tmp85 ;
3455 unsigned long __cil_tmp86 ;
3456 unsigned long __cil_tmp87 ;
3457 unsigned long __cil_tmp88 ;
3458 unsigned long __cil_tmp89 ;
3459 unsigned char __cil_tmp90 ;
3460 long __cil_tmp91 ;
3461 long __cil_tmp92 ;
3462 struct device const *__cil_tmp93 ;
3463 unsigned long __cil_tmp94 ;
3464 unsigned long __cil_tmp95 ;
3465 int __cil_tmp96 ;
3466 struct _ddebug *__cil_tmp97 ;
3467 unsigned long __cil_tmp98 ;
3468 unsigned long __cil_tmp99 ;
3469 unsigned long __cil_tmp100 ;
3470 unsigned long __cil_tmp101 ;
3471 unsigned long __cil_tmp102 ;
3472 unsigned long __cil_tmp103 ;
3473 unsigned char __cil_tmp104 ;
3474 long __cil_tmp105 ;
3475 long __cil_tmp106 ;
3476 struct device const *__cil_tmp107 ;
3477 unsigned long __cil_tmp108 ;
3478 unsigned long __cil_tmp109 ;
3479 int __cil_tmp110 ;
3480 struct _ddebug *__cil_tmp111 ;
3481 unsigned long __cil_tmp112 ;
3482 unsigned long __cil_tmp113 ;
3483 unsigned long __cil_tmp114 ;
3484 unsigned long __cil_tmp115 ;
3485 unsigned long __cil_tmp116 ;
3486 unsigned long __cil_tmp117 ;
3487 unsigned char __cil_tmp118 ;
3488 long __cil_tmp119 ;
3489 long __cil_tmp120 ;
3490 struct device const *__cil_tmp121 ;
3491 int __cil_tmp122 ;
3492 struct _ddebug *__cil_tmp123 ;
3493 unsigned long __cil_tmp124 ;
3494 unsigned long __cil_tmp125 ;
3495 unsigned long __cil_tmp126 ;
3496 unsigned long __cil_tmp127 ;
3497 unsigned long __cil_tmp128 ;
3498 unsigned long __cil_tmp129 ;
3499 unsigned char __cil_tmp130 ;
3500 long __cil_tmp131 ;
3501 long __cil_tmp132 ;
3502 struct device const *__cil_tmp133 ;
3503 unsigned long __cil_tmp134 ;
3504 unsigned long __cil_tmp135 ;
3505 int __cil_tmp136 ;
3506 struct _ddebug *__cil_tmp137 ;
3507 unsigned long __cil_tmp138 ;
3508 unsigned long __cil_tmp139 ;
3509 unsigned long __cil_tmp140 ;
3510 unsigned long __cil_tmp141 ;
3511 unsigned long __cil_tmp142 ;
3512 unsigned long __cil_tmp143 ;
3513 unsigned char __cil_tmp144 ;
3514 long __cil_tmp145 ;
3515 long __cil_tmp146 ;
3516 struct device const *__cil_tmp147 ;
3517 unsigned long __cil_tmp148 ;
3518 unsigned long __cil_tmp149 ;
3519 int __cil_tmp150 ;
3520 struct _ddebug *__cil_tmp151 ;
3521 unsigned long __cil_tmp152 ;
3522 unsigned long __cil_tmp153 ;
3523 unsigned long __cil_tmp154 ;
3524 unsigned long __cil_tmp155 ;
3525 unsigned long __cil_tmp156 ;
3526 unsigned long __cil_tmp157 ;
3527 unsigned char __cil_tmp158 ;
3528 long __cil_tmp159 ;
3529 long __cil_tmp160 ;
3530 struct device const *__cil_tmp161 ;
3531 unsigned long __cil_tmp162 ;
3532 unsigned long __cil_tmp163 ;
3533 int __cil_tmp164 ;
3534 struct _ddebug *__cil_tmp165 ;
3535 unsigned long __cil_tmp166 ;
3536 unsigned long __cil_tmp167 ;
3537 unsigned long __cil_tmp168 ;
3538 unsigned long __cil_tmp169 ;
3539 unsigned long __cil_tmp170 ;
3540 unsigned long __cil_tmp171 ;
3541 unsigned char __cil_tmp172 ;
3542 long __cil_tmp173 ;
3543 long __cil_tmp174 ;
3544 struct device const *__cil_tmp175 ;
3545 unsigned long __cil_tmp176 ;
3546 unsigned long __cil_tmp177 ;
3547 int __cil_tmp178 ;
3548
3549 {
3550 {
3551#line 248
3552 __cil_tmp36 = (struct device const *)dev;
3553#line 248
3554 tmp = dev_get_drvdata(__cil_tmp36);
3555#line 248
3556 chip = (struct v3020 *)tmp;
3557#line 252
3558 v3020_set_reg(chip, (unsigned char)15, (unsigned char)0);
3559#line 255
3560 tmp___1 = v3020_get_reg(chip, (unsigned char)2);
3561#line 255
3562 tmp___0 = (int )tmp___1;
3563#line 256
3564 __cil_tmp37 = (unsigned char )tmp___0;
3565#line 256
3566 __cil_tmp38 = (int )__cil_tmp37;
3567#line 256
3568 __cil_tmp39 = (unsigned char )__cil_tmp38;
3569#line 256
3570 tmp___2 = bcd2bin(__cil_tmp39);
3571#line 256
3572 *((int *)dt) = (int )tmp___2;
3573#line 257
3574 tmp___3 = v3020_get_reg(chip, (unsigned char)3);
3575#line 257
3576 tmp___0 = (int )tmp___3;
3577#line 258
3578 __cil_tmp40 = (unsigned char )tmp___0;
3579#line 258
3580 __cil_tmp41 = (int )__cil_tmp40;
3581#line 258
3582 __cil_tmp42 = (unsigned char )__cil_tmp41;
3583#line 258
3584 tmp___4 = bcd2bin(__cil_tmp42);
3585#line 258
3586 __cil_tmp43 = (unsigned long )dt;
3587#line 258
3588 __cil_tmp44 = __cil_tmp43 + 4;
3589#line 258
3590 *((int *)__cil_tmp44) = (int )tmp___4;
3591#line 259
3592 tmp___5 = v3020_get_reg(chip, (unsigned char)4);
3593#line 259
3594 tmp___0 = (int )tmp___5;
3595#line 260
3596 __cil_tmp45 = (unsigned char )tmp___0;
3597#line 260
3598 __cil_tmp46 = (int )__cil_tmp45;
3599#line 260
3600 __cil_tmp47 = (unsigned char )__cil_tmp46;
3601#line 260
3602 tmp___6 = bcd2bin(__cil_tmp47);
3603#line 260
3604 __cil_tmp48 = (unsigned long )dt;
3605#line 260
3606 __cil_tmp49 = __cil_tmp48 + 8;
3607#line 260
3608 *((int *)__cil_tmp49) = (int )tmp___6;
3609#line 261
3610 tmp___7 = v3020_get_reg(chip, (unsigned char)5);
3611#line 261
3612 tmp___0 = (int )tmp___7;
3613#line 262
3614 __cil_tmp50 = (unsigned char )tmp___0;
3615#line 262
3616 __cil_tmp51 = (int )__cil_tmp50;
3617#line 262
3618 __cil_tmp52 = (unsigned char )__cil_tmp51;
3619#line 262
3620 tmp___8 = bcd2bin(__cil_tmp52);
3621#line 262
3622 __cil_tmp53 = (unsigned long )dt;
3623#line 262
3624 __cil_tmp54 = __cil_tmp53 + 12;
3625#line 262
3626 *((int *)__cil_tmp54) = (int )tmp___8;
3627#line 263
3628 tmp___9 = v3020_get_reg(chip, (unsigned char)6);
3629#line 263
3630 tmp___0 = (int )tmp___9;
3631#line 264
3632 __cil_tmp55 = (unsigned char )tmp___0;
3633#line 264
3634 __cil_tmp56 = (int )__cil_tmp55;
3635#line 264
3636 __cil_tmp57 = (unsigned char )__cil_tmp56;
3637#line 264
3638 tmp___10 = bcd2bin(__cil_tmp57);
3639#line 264
3640 __cil_tmp58 = (unsigned long )dt;
3641#line 264
3642 __cil_tmp59 = __cil_tmp58 + 16;
3643#line 264
3644 __cil_tmp60 = tmp___10 - 1U;
3645#line 264
3646 *((int *)__cil_tmp59) = (int )__cil_tmp60;
3647#line 265
3648 tmp___11 = v3020_get_reg(chip, (unsigned char)8);
3649#line 265
3650 tmp___0 = (int )tmp___11;
3651#line 266
3652 __cil_tmp61 = (unsigned char )tmp___0;
3653#line 266
3654 __cil_tmp62 = (int )__cil_tmp61;
3655#line 266
3656 __cil_tmp63 = (unsigned char )__cil_tmp62;
3657#line 266
3658 tmp___12 = bcd2bin(__cil_tmp63);
3659#line 266
3660 __cil_tmp64 = (unsigned long )dt;
3661#line 266
3662 __cil_tmp65 = __cil_tmp64 + 24;
3663#line 266
3664 *((int *)__cil_tmp65) = (int )tmp___12;
3665#line 267
3666 tmp___13 = v3020_get_reg(chip, (unsigned char)7);
3667#line 267
3668 tmp___0 = (int )tmp___13;
3669#line 268
3670 __cil_tmp66 = (unsigned char )tmp___0;
3671#line 268
3672 __cil_tmp67 = (int )__cil_tmp66;
3673#line 268
3674 __cil_tmp68 = (unsigned char )__cil_tmp67;
3675#line 268
3676 tmp___14 = bcd2bin(__cil_tmp68);
3677#line 268
3678 __cil_tmp69 = (unsigned long )dt;
3679#line 268
3680 __cil_tmp70 = __cil_tmp69 + 20;
3681#line 268
3682 __cil_tmp71 = tmp___14 + 100U;
3683#line 268
3684 *((int *)__cil_tmp70) = (int )__cil_tmp71;
3685#line 270
3686 __cil_tmp72 = & descriptor;
3687#line 270
3688 *((char const **)__cil_tmp72) = "rtc_v3020";
3689#line 270
3690 __cil_tmp73 = (unsigned long )(& descriptor) + 8;
3691#line 270
3692 *((char const **)__cil_tmp73) = "v3020_read_time";
3693#line 270
3694 __cil_tmp74 = (unsigned long )(& descriptor) + 16;
3695#line 270
3696 *((char const **)__cil_tmp74) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
3697#line 270
3698 __cil_tmp75 = (unsigned long )(& descriptor) + 24;
3699#line 270
3700 *((char const **)__cil_tmp75) = "\n%s : Read RTC values\n";
3701#line 270
3702 __cil_tmp76 = (unsigned long )(& descriptor) + 32;
3703#line 270
3704 *((unsigned int *)__cil_tmp76) = 270U;
3705#line 270
3706 __cil_tmp77 = (unsigned long )(& descriptor) + 35;
3707#line 270
3708 *((unsigned char *)__cil_tmp77) = (unsigned char)1;
3709#line 270
3710 __cil_tmp78 = (unsigned long )(& descriptor) + 35;
3711#line 270
3712 __cil_tmp79 = *((unsigned char *)__cil_tmp78);
3713#line 270
3714 __cil_tmp80 = (long )__cil_tmp79;
3715#line 270
3716 __cil_tmp81 = __cil_tmp80 & 1L;
3717#line 270
3718 tmp___15 = __builtin_expect(__cil_tmp81, 0L);
3719 }
3720#line 270
3721 if (tmp___15 != 0L) {
3722 {
3723#line 270
3724 __cil_tmp82 = (struct device const *)dev;
3725#line 270
3726 __dynamic_dev_dbg(& descriptor, __cil_tmp82, "\n%s : Read RTC values\n", "v3020_read_time");
3727 }
3728 } else {
3729
3730 }
3731 {
3732#line 271
3733 __cil_tmp83 = & descriptor___0;
3734#line 271
3735 *((char const **)__cil_tmp83) = "rtc_v3020";
3736#line 271
3737 __cil_tmp84 = (unsigned long )(& descriptor___0) + 8;
3738#line 271
3739 *((char const **)__cil_tmp84) = "v3020_read_time";
3740#line 271
3741 __cil_tmp85 = (unsigned long )(& descriptor___0) + 16;
3742#line 271
3743 *((char const **)__cil_tmp85) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
3744#line 271
3745 __cil_tmp86 = (unsigned long )(& descriptor___0) + 24;
3746#line 271
3747 *((char const **)__cil_tmp86) = "tm_hour: %i\n";
3748#line 271
3749 __cil_tmp87 = (unsigned long )(& descriptor___0) + 32;
3750#line 271
3751 *((unsigned int *)__cil_tmp87) = 271U;
3752#line 271
3753 __cil_tmp88 = (unsigned long )(& descriptor___0) + 35;
3754#line 271
3755 *((unsigned char *)__cil_tmp88) = (unsigned char)1;
3756#line 271
3757 __cil_tmp89 = (unsigned long )(& descriptor___0) + 35;
3758#line 271
3759 __cil_tmp90 = *((unsigned char *)__cil_tmp89);
3760#line 271
3761 __cil_tmp91 = (long )__cil_tmp90;
3762#line 271
3763 __cil_tmp92 = __cil_tmp91 & 1L;
3764#line 271
3765 tmp___16 = __builtin_expect(__cil_tmp92, 0L);
3766 }
3767#line 271
3768 if (tmp___16 != 0L) {
3769 {
3770#line 271
3771 __cil_tmp93 = (struct device const *)dev;
3772#line 271
3773 __cil_tmp94 = (unsigned long )dt;
3774#line 271
3775 __cil_tmp95 = __cil_tmp94 + 8;
3776#line 271
3777 __cil_tmp96 = *((int *)__cil_tmp95);
3778#line 271
3779 __dynamic_dev_dbg(& descriptor___0, __cil_tmp93, "tm_hour: %i\n", __cil_tmp96);
3780 }
3781 } else {
3782
3783 }
3784 {
3785#line 272
3786 __cil_tmp97 = & descriptor___1;
3787#line 272
3788 *((char const **)__cil_tmp97) = "rtc_v3020";
3789#line 272
3790 __cil_tmp98 = (unsigned long )(& descriptor___1) + 8;
3791#line 272
3792 *((char const **)__cil_tmp98) = "v3020_read_time";
3793#line 272
3794 __cil_tmp99 = (unsigned long )(& descriptor___1) + 16;
3795#line 272
3796 *((char const **)__cil_tmp99) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
3797#line 272
3798 __cil_tmp100 = (unsigned long )(& descriptor___1) + 24;
3799#line 272
3800 *((char const **)__cil_tmp100) = "tm_min : %i\n";
3801#line 272
3802 __cil_tmp101 = (unsigned long )(& descriptor___1) + 32;
3803#line 272
3804 *((unsigned int *)__cil_tmp101) = 272U;
3805#line 272
3806 __cil_tmp102 = (unsigned long )(& descriptor___1) + 35;
3807#line 272
3808 *((unsigned char *)__cil_tmp102) = (unsigned char)1;
3809#line 272
3810 __cil_tmp103 = (unsigned long )(& descriptor___1) + 35;
3811#line 272
3812 __cil_tmp104 = *((unsigned char *)__cil_tmp103);
3813#line 272
3814 __cil_tmp105 = (long )__cil_tmp104;
3815#line 272
3816 __cil_tmp106 = __cil_tmp105 & 1L;
3817#line 272
3818 tmp___17 = __builtin_expect(__cil_tmp106, 0L);
3819 }
3820#line 272
3821 if (tmp___17 != 0L) {
3822 {
3823#line 272
3824 __cil_tmp107 = (struct device const *)dev;
3825#line 272
3826 __cil_tmp108 = (unsigned long )dt;
3827#line 272
3828 __cil_tmp109 = __cil_tmp108 + 4;
3829#line 272
3830 __cil_tmp110 = *((int *)__cil_tmp109);
3831#line 272
3832 __dynamic_dev_dbg(& descriptor___1, __cil_tmp107, "tm_min : %i\n", __cil_tmp110);
3833 }
3834 } else {
3835
3836 }
3837 {
3838#line 273
3839 __cil_tmp111 = & descriptor___2;
3840#line 273
3841 *((char const **)__cil_tmp111) = "rtc_v3020";
3842#line 273
3843 __cil_tmp112 = (unsigned long )(& descriptor___2) + 8;
3844#line 273
3845 *((char const **)__cil_tmp112) = "v3020_read_time";
3846#line 273
3847 __cil_tmp113 = (unsigned long )(& descriptor___2) + 16;
3848#line 273
3849 *((char const **)__cil_tmp113) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
3850#line 273
3851 __cil_tmp114 = (unsigned long )(& descriptor___2) + 24;
3852#line 273
3853 *((char const **)__cil_tmp114) = "tm_sec : %i\n";
3854#line 273
3855 __cil_tmp115 = (unsigned long )(& descriptor___2) + 32;
3856#line 273
3857 *((unsigned int *)__cil_tmp115) = 273U;
3858#line 273
3859 __cil_tmp116 = (unsigned long )(& descriptor___2) + 35;
3860#line 273
3861 *((unsigned char *)__cil_tmp116) = (unsigned char)1;
3862#line 273
3863 __cil_tmp117 = (unsigned long )(& descriptor___2) + 35;
3864#line 273
3865 __cil_tmp118 = *((unsigned char *)__cil_tmp117);
3866#line 273
3867 __cil_tmp119 = (long )__cil_tmp118;
3868#line 273
3869 __cil_tmp120 = __cil_tmp119 & 1L;
3870#line 273
3871 tmp___18 = __builtin_expect(__cil_tmp120, 0L);
3872 }
3873#line 273
3874 if (tmp___18 != 0L) {
3875 {
3876#line 273
3877 __cil_tmp121 = (struct device const *)dev;
3878#line 273
3879 __cil_tmp122 = *((int *)dt);
3880#line 273
3881 __dynamic_dev_dbg(& descriptor___2, __cil_tmp121, "tm_sec : %i\n", __cil_tmp122);
3882 }
3883 } else {
3884
3885 }
3886 {
3887#line 274
3888 __cil_tmp123 = & descriptor___3;
3889#line 274
3890 *((char const **)__cil_tmp123) = "rtc_v3020";
3891#line 274
3892 __cil_tmp124 = (unsigned long )(& descriptor___3) + 8;
3893#line 274
3894 *((char const **)__cil_tmp124) = "v3020_read_time";
3895#line 274
3896 __cil_tmp125 = (unsigned long )(& descriptor___3) + 16;
3897#line 274
3898 *((char const **)__cil_tmp125) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
3899#line 274
3900 __cil_tmp126 = (unsigned long )(& descriptor___3) + 24;
3901#line 274
3902 *((char const **)__cil_tmp126) = "tm_year: %i\n";
3903#line 274
3904 __cil_tmp127 = (unsigned long )(& descriptor___3) + 32;
3905#line 274
3906 *((unsigned int *)__cil_tmp127) = 274U;
3907#line 274
3908 __cil_tmp128 = (unsigned long )(& descriptor___3) + 35;
3909#line 274
3910 *((unsigned char *)__cil_tmp128) = (unsigned char)1;
3911#line 274
3912 __cil_tmp129 = (unsigned long )(& descriptor___3) + 35;
3913#line 274
3914 __cil_tmp130 = *((unsigned char *)__cil_tmp129);
3915#line 274
3916 __cil_tmp131 = (long )__cil_tmp130;
3917#line 274
3918 __cil_tmp132 = __cil_tmp131 & 1L;
3919#line 274
3920 tmp___19 = __builtin_expect(__cil_tmp132, 0L);
3921 }
3922#line 274
3923 if (tmp___19 != 0L) {
3924 {
3925#line 274
3926 __cil_tmp133 = (struct device const *)dev;
3927#line 274
3928 __cil_tmp134 = (unsigned long )dt;
3929#line 274
3930 __cil_tmp135 = __cil_tmp134 + 20;
3931#line 274
3932 __cil_tmp136 = *((int *)__cil_tmp135);
3933#line 274
3934 __dynamic_dev_dbg(& descriptor___3, __cil_tmp133, "tm_year: %i\n", __cil_tmp136);
3935 }
3936 } else {
3937
3938 }
3939 {
3940#line 275
3941 __cil_tmp137 = & descriptor___4;
3942#line 275
3943 *((char const **)__cil_tmp137) = "rtc_v3020";
3944#line 275
3945 __cil_tmp138 = (unsigned long )(& descriptor___4) + 8;
3946#line 275
3947 *((char const **)__cil_tmp138) = "v3020_read_time";
3948#line 275
3949 __cil_tmp139 = (unsigned long )(& descriptor___4) + 16;
3950#line 275
3951 *((char const **)__cil_tmp139) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
3952#line 275
3953 __cil_tmp140 = (unsigned long )(& descriptor___4) + 24;
3954#line 275
3955 *((char const **)__cil_tmp140) = "tm_mon : %i\n";
3956#line 275
3957 __cil_tmp141 = (unsigned long )(& descriptor___4) + 32;
3958#line 275
3959 *((unsigned int *)__cil_tmp141) = 275U;
3960#line 275
3961 __cil_tmp142 = (unsigned long )(& descriptor___4) + 35;
3962#line 275
3963 *((unsigned char *)__cil_tmp142) = (unsigned char)1;
3964#line 275
3965 __cil_tmp143 = (unsigned long )(& descriptor___4) + 35;
3966#line 275
3967 __cil_tmp144 = *((unsigned char *)__cil_tmp143);
3968#line 275
3969 __cil_tmp145 = (long )__cil_tmp144;
3970#line 275
3971 __cil_tmp146 = __cil_tmp145 & 1L;
3972#line 275
3973 tmp___20 = __builtin_expect(__cil_tmp146, 0L);
3974 }
3975#line 275
3976 if (tmp___20 != 0L) {
3977 {
3978#line 275
3979 __cil_tmp147 = (struct device const *)dev;
3980#line 275
3981 __cil_tmp148 = (unsigned long )dt;
3982#line 275
3983 __cil_tmp149 = __cil_tmp148 + 16;
3984#line 275
3985 __cil_tmp150 = *((int *)__cil_tmp149);
3986#line 275
3987 __dynamic_dev_dbg(& descriptor___4, __cil_tmp147, "tm_mon : %i\n", __cil_tmp150);
3988 }
3989 } else {
3990
3991 }
3992 {
3993#line 276
3994 __cil_tmp151 = & descriptor___5;
3995#line 276
3996 *((char const **)__cil_tmp151) = "rtc_v3020";
3997#line 276
3998 __cil_tmp152 = (unsigned long )(& descriptor___5) + 8;
3999#line 276
4000 *((char const **)__cil_tmp152) = "v3020_read_time";
4001#line 276
4002 __cil_tmp153 = (unsigned long )(& descriptor___5) + 16;
4003#line 276
4004 *((char const **)__cil_tmp153) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4005#line 276
4006 __cil_tmp154 = (unsigned long )(& descriptor___5) + 24;
4007#line 276
4008 *((char const **)__cil_tmp154) = "tm_mday: %i\n";
4009#line 276
4010 __cil_tmp155 = (unsigned long )(& descriptor___5) + 32;
4011#line 276
4012 *((unsigned int *)__cil_tmp155) = 276U;
4013#line 276
4014 __cil_tmp156 = (unsigned long )(& descriptor___5) + 35;
4015#line 276
4016 *((unsigned char *)__cil_tmp156) = (unsigned char)1;
4017#line 276
4018 __cil_tmp157 = (unsigned long )(& descriptor___5) + 35;
4019#line 276
4020 __cil_tmp158 = *((unsigned char *)__cil_tmp157);
4021#line 276
4022 __cil_tmp159 = (long )__cil_tmp158;
4023#line 276
4024 __cil_tmp160 = __cil_tmp159 & 1L;
4025#line 276
4026 tmp___21 = __builtin_expect(__cil_tmp160, 0L);
4027 }
4028#line 276
4029 if (tmp___21 != 0L) {
4030 {
4031#line 276
4032 __cil_tmp161 = (struct device const *)dev;
4033#line 276
4034 __cil_tmp162 = (unsigned long )dt;
4035#line 276
4036 __cil_tmp163 = __cil_tmp162 + 12;
4037#line 276
4038 __cil_tmp164 = *((int *)__cil_tmp163);
4039#line 276
4040 __dynamic_dev_dbg(& descriptor___5, __cil_tmp161, "tm_mday: %i\n", __cil_tmp164);
4041 }
4042 } else {
4043
4044 }
4045 {
4046#line 277
4047 __cil_tmp165 = & descriptor___6;
4048#line 277
4049 *((char const **)__cil_tmp165) = "rtc_v3020";
4050#line 277
4051 __cil_tmp166 = (unsigned long )(& descriptor___6) + 8;
4052#line 277
4053 *((char const **)__cil_tmp166) = "v3020_read_time";
4054#line 277
4055 __cil_tmp167 = (unsigned long )(& descriptor___6) + 16;
4056#line 277
4057 *((char const **)__cil_tmp167) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4058#line 277
4059 __cil_tmp168 = (unsigned long )(& descriptor___6) + 24;
4060#line 277
4061 *((char const **)__cil_tmp168) = "tm_wday: %i\n";
4062#line 277
4063 __cil_tmp169 = (unsigned long )(& descriptor___6) + 32;
4064#line 277
4065 *((unsigned int *)__cil_tmp169) = 277U;
4066#line 277
4067 __cil_tmp170 = (unsigned long )(& descriptor___6) + 35;
4068#line 277
4069 *((unsigned char *)__cil_tmp170) = (unsigned char)1;
4070#line 277
4071 __cil_tmp171 = (unsigned long )(& descriptor___6) + 35;
4072#line 277
4073 __cil_tmp172 = *((unsigned char *)__cil_tmp171);
4074#line 277
4075 __cil_tmp173 = (long )__cil_tmp172;
4076#line 277
4077 __cil_tmp174 = __cil_tmp173 & 1L;
4078#line 277
4079 tmp___22 = __builtin_expect(__cil_tmp174, 0L);
4080 }
4081#line 277
4082 if (tmp___22 != 0L) {
4083 {
4084#line 277
4085 __cil_tmp175 = (struct device const *)dev;
4086#line 277
4087 __cil_tmp176 = (unsigned long )dt;
4088#line 277
4089 __cil_tmp177 = __cil_tmp176 + 24;
4090#line 277
4091 __cil_tmp178 = *((int *)__cil_tmp177);
4092#line 277
4093 __dynamic_dev_dbg(& descriptor___6, __cil_tmp175, "tm_wday: %i\n", __cil_tmp178);
4094 }
4095 } else {
4096
4097 }
4098#line 279
4099 return (0);
4100}
4101}
4102#line 283 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
4103static int v3020_set_time(struct device *dev , struct rtc_time *dt )
4104{ struct v3020 *chip ;
4105 void *tmp ;
4106 struct _ddebug descriptor ;
4107 long tmp___0 ;
4108 struct _ddebug descriptor___0 ;
4109 long tmp___1 ;
4110 struct _ddebug descriptor___1 ;
4111 long tmp___2 ;
4112 struct _ddebug descriptor___2 ;
4113 long tmp___3 ;
4114 struct _ddebug descriptor___3 ;
4115 long tmp___4 ;
4116 struct _ddebug descriptor___4 ;
4117 long tmp___5 ;
4118 struct _ddebug descriptor___5 ;
4119 long tmp___6 ;
4120 unsigned char tmp___7 ;
4121 unsigned char tmp___8 ;
4122 unsigned char tmp___9 ;
4123 unsigned char tmp___10 ;
4124 unsigned char tmp___11 ;
4125 unsigned char tmp___12 ;
4126 unsigned char tmp___13 ;
4127 struct device const *__cil_tmp26 ;
4128 struct _ddebug *__cil_tmp27 ;
4129 unsigned long __cil_tmp28 ;
4130 unsigned long __cil_tmp29 ;
4131 unsigned long __cil_tmp30 ;
4132 unsigned long __cil_tmp31 ;
4133 unsigned long __cil_tmp32 ;
4134 unsigned long __cil_tmp33 ;
4135 unsigned char __cil_tmp34 ;
4136 long __cil_tmp35 ;
4137 long __cil_tmp36 ;
4138 struct device const *__cil_tmp37 ;
4139 struct _ddebug *__cil_tmp38 ;
4140 unsigned long __cil_tmp39 ;
4141 unsigned long __cil_tmp40 ;
4142 unsigned long __cil_tmp41 ;
4143 unsigned long __cil_tmp42 ;
4144 unsigned long __cil_tmp43 ;
4145 unsigned long __cil_tmp44 ;
4146 unsigned char __cil_tmp45 ;
4147 long __cil_tmp46 ;
4148 long __cil_tmp47 ;
4149 struct device const *__cil_tmp48 ;
4150 int __cil_tmp49 ;
4151 struct _ddebug *__cil_tmp50 ;
4152 unsigned long __cil_tmp51 ;
4153 unsigned long __cil_tmp52 ;
4154 unsigned long __cil_tmp53 ;
4155 unsigned long __cil_tmp54 ;
4156 unsigned long __cil_tmp55 ;
4157 unsigned long __cil_tmp56 ;
4158 unsigned char __cil_tmp57 ;
4159 long __cil_tmp58 ;
4160 long __cil_tmp59 ;
4161 struct device const *__cil_tmp60 ;
4162 unsigned long __cil_tmp61 ;
4163 unsigned long __cil_tmp62 ;
4164 int __cil_tmp63 ;
4165 struct _ddebug *__cil_tmp64 ;
4166 unsigned long __cil_tmp65 ;
4167 unsigned long __cil_tmp66 ;
4168 unsigned long __cil_tmp67 ;
4169 unsigned long __cil_tmp68 ;
4170 unsigned long __cil_tmp69 ;
4171 unsigned long __cil_tmp70 ;
4172 unsigned char __cil_tmp71 ;
4173 long __cil_tmp72 ;
4174 long __cil_tmp73 ;
4175 struct device const *__cil_tmp74 ;
4176 unsigned long __cil_tmp75 ;
4177 unsigned long __cil_tmp76 ;
4178 int __cil_tmp77 ;
4179 struct _ddebug *__cil_tmp78 ;
4180 unsigned long __cil_tmp79 ;
4181 unsigned long __cil_tmp80 ;
4182 unsigned long __cil_tmp81 ;
4183 unsigned long __cil_tmp82 ;
4184 unsigned long __cil_tmp83 ;
4185 unsigned long __cil_tmp84 ;
4186 unsigned char __cil_tmp85 ;
4187 long __cil_tmp86 ;
4188 long __cil_tmp87 ;
4189 struct device const *__cil_tmp88 ;
4190 unsigned long __cil_tmp89 ;
4191 unsigned long __cil_tmp90 ;
4192 int __cil_tmp91 ;
4193 struct _ddebug *__cil_tmp92 ;
4194 unsigned long __cil_tmp93 ;
4195 unsigned long __cil_tmp94 ;
4196 unsigned long __cil_tmp95 ;
4197 unsigned long __cil_tmp96 ;
4198 unsigned long __cil_tmp97 ;
4199 unsigned long __cil_tmp98 ;
4200 unsigned char __cil_tmp99 ;
4201 long __cil_tmp100 ;
4202 long __cil_tmp101 ;
4203 struct device const *__cil_tmp102 ;
4204 unsigned long __cil_tmp103 ;
4205 unsigned long __cil_tmp104 ;
4206 int __cil_tmp105 ;
4207 struct _ddebug *__cil_tmp106 ;
4208 unsigned long __cil_tmp107 ;
4209 unsigned long __cil_tmp108 ;
4210 unsigned long __cil_tmp109 ;
4211 unsigned long __cil_tmp110 ;
4212 unsigned long __cil_tmp111 ;
4213 unsigned long __cil_tmp112 ;
4214 unsigned char __cil_tmp113 ;
4215 long __cil_tmp114 ;
4216 long __cil_tmp115 ;
4217 struct device const *__cil_tmp116 ;
4218 unsigned long __cil_tmp117 ;
4219 unsigned long __cil_tmp118 ;
4220 int __cil_tmp119 ;
4221 int __cil_tmp120 ;
4222 unsigned int __cil_tmp121 ;
4223 int __cil_tmp122 ;
4224 unsigned char __cil_tmp123 ;
4225 unsigned long __cil_tmp124 ;
4226 unsigned long __cil_tmp125 ;
4227 int __cil_tmp126 ;
4228 unsigned int __cil_tmp127 ;
4229 int __cil_tmp128 ;
4230 unsigned char __cil_tmp129 ;
4231 unsigned long __cil_tmp130 ;
4232 unsigned long __cil_tmp131 ;
4233 int __cil_tmp132 ;
4234 unsigned int __cil_tmp133 ;
4235 int __cil_tmp134 ;
4236 unsigned char __cil_tmp135 ;
4237 unsigned long __cil_tmp136 ;
4238 unsigned long __cil_tmp137 ;
4239 int __cil_tmp138 ;
4240 unsigned int __cil_tmp139 ;
4241 int __cil_tmp140 ;
4242 unsigned char __cil_tmp141 ;
4243 unsigned long __cil_tmp142 ;
4244 unsigned long __cil_tmp143 ;
4245 int __cil_tmp144 ;
4246 int __cil_tmp145 ;
4247 unsigned int __cil_tmp146 ;
4248 int __cil_tmp147 ;
4249 unsigned char __cil_tmp148 ;
4250 unsigned long __cil_tmp149 ;
4251 unsigned long __cil_tmp150 ;
4252 int __cil_tmp151 ;
4253 unsigned int __cil_tmp152 ;
4254 int __cil_tmp153 ;
4255 unsigned char __cil_tmp154 ;
4256 unsigned long __cil_tmp155 ;
4257 unsigned long __cil_tmp156 ;
4258 int __cil_tmp157 ;
4259 int __cil_tmp158 ;
4260 unsigned int __cil_tmp159 ;
4261 int __cil_tmp160 ;
4262 unsigned char __cil_tmp161 ;
4263
4264 {
4265 {
4266#line 285
4267 __cil_tmp26 = (struct device const *)dev;
4268#line 285
4269 tmp = dev_get_drvdata(__cil_tmp26);
4270#line 285
4271 chip = (struct v3020 *)tmp;
4272#line 287
4273 __cil_tmp27 = & descriptor;
4274#line 287
4275 *((char const **)__cil_tmp27) = "rtc_v3020";
4276#line 287
4277 __cil_tmp28 = (unsigned long )(& descriptor) + 8;
4278#line 287
4279 *((char const **)__cil_tmp28) = "v3020_set_time";
4280#line 287
4281 __cil_tmp29 = (unsigned long )(& descriptor) + 16;
4282#line 287
4283 *((char const **)__cil_tmp29) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4284#line 287
4285 __cil_tmp30 = (unsigned long )(& descriptor) + 24;
4286#line 287
4287 *((char const **)__cil_tmp30) = "\n%s : Setting RTC values\n";
4288#line 287
4289 __cil_tmp31 = (unsigned long )(& descriptor) + 32;
4290#line 287
4291 *((unsigned int *)__cil_tmp31) = 287U;
4292#line 287
4293 __cil_tmp32 = (unsigned long )(& descriptor) + 35;
4294#line 287
4295 *((unsigned char *)__cil_tmp32) = (unsigned char)1;
4296#line 287
4297 __cil_tmp33 = (unsigned long )(& descriptor) + 35;
4298#line 287
4299 __cil_tmp34 = *((unsigned char *)__cil_tmp33);
4300#line 287
4301 __cil_tmp35 = (long )__cil_tmp34;
4302#line 287
4303 __cil_tmp36 = __cil_tmp35 & 1L;
4304#line 287
4305 tmp___0 = __builtin_expect(__cil_tmp36, 0L);
4306 }
4307#line 287
4308 if (tmp___0 != 0L) {
4309 {
4310#line 287
4311 __cil_tmp37 = (struct device const *)dev;
4312#line 287
4313 __dynamic_dev_dbg(& descriptor, __cil_tmp37, "\n%s : Setting RTC values\n", "v3020_set_time");
4314 }
4315 } else {
4316
4317 }
4318 {
4319#line 288
4320 __cil_tmp38 = & descriptor___0;
4321#line 288
4322 *((char const **)__cil_tmp38) = "rtc_v3020";
4323#line 288
4324 __cil_tmp39 = (unsigned long )(& descriptor___0) + 8;
4325#line 288
4326 *((char const **)__cil_tmp39) = "v3020_set_time";
4327#line 288
4328 __cil_tmp40 = (unsigned long )(& descriptor___0) + 16;
4329#line 288
4330 *((char const **)__cil_tmp40) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4331#line 288
4332 __cil_tmp41 = (unsigned long )(& descriptor___0) + 24;
4333#line 288
4334 *((char const **)__cil_tmp41) = "tm_sec : %i\n";
4335#line 288
4336 __cil_tmp42 = (unsigned long )(& descriptor___0) + 32;
4337#line 288
4338 *((unsigned int *)__cil_tmp42) = 288U;
4339#line 288
4340 __cil_tmp43 = (unsigned long )(& descriptor___0) + 35;
4341#line 288
4342 *((unsigned char *)__cil_tmp43) = (unsigned char)1;
4343#line 288
4344 __cil_tmp44 = (unsigned long )(& descriptor___0) + 35;
4345#line 288
4346 __cil_tmp45 = *((unsigned char *)__cil_tmp44);
4347#line 288
4348 __cil_tmp46 = (long )__cil_tmp45;
4349#line 288
4350 __cil_tmp47 = __cil_tmp46 & 1L;
4351#line 288
4352 tmp___1 = __builtin_expect(__cil_tmp47, 0L);
4353 }
4354#line 288
4355 if (tmp___1 != 0L) {
4356 {
4357#line 288
4358 __cil_tmp48 = (struct device const *)dev;
4359#line 288
4360 __cil_tmp49 = *((int *)dt);
4361#line 288
4362 __dynamic_dev_dbg(& descriptor___0, __cil_tmp48, "tm_sec : %i\n", __cil_tmp49);
4363 }
4364 } else {
4365
4366 }
4367 {
4368#line 289
4369 __cil_tmp50 = & descriptor___1;
4370#line 289
4371 *((char const **)__cil_tmp50) = "rtc_v3020";
4372#line 289
4373 __cil_tmp51 = (unsigned long )(& descriptor___1) + 8;
4374#line 289
4375 *((char const **)__cil_tmp51) = "v3020_set_time";
4376#line 289
4377 __cil_tmp52 = (unsigned long )(& descriptor___1) + 16;
4378#line 289
4379 *((char const **)__cil_tmp52) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4380#line 289
4381 __cil_tmp53 = (unsigned long )(& descriptor___1) + 24;
4382#line 289
4383 *((char const **)__cil_tmp53) = "tm_min : %i\n";
4384#line 289
4385 __cil_tmp54 = (unsigned long )(& descriptor___1) + 32;
4386#line 289
4387 *((unsigned int *)__cil_tmp54) = 289U;
4388#line 289
4389 __cil_tmp55 = (unsigned long )(& descriptor___1) + 35;
4390#line 289
4391 *((unsigned char *)__cil_tmp55) = (unsigned char)1;
4392#line 289
4393 __cil_tmp56 = (unsigned long )(& descriptor___1) + 35;
4394#line 289
4395 __cil_tmp57 = *((unsigned char *)__cil_tmp56);
4396#line 289
4397 __cil_tmp58 = (long )__cil_tmp57;
4398#line 289
4399 __cil_tmp59 = __cil_tmp58 & 1L;
4400#line 289
4401 tmp___2 = __builtin_expect(__cil_tmp59, 0L);
4402 }
4403#line 289
4404 if (tmp___2 != 0L) {
4405 {
4406#line 289
4407 __cil_tmp60 = (struct device const *)dev;
4408#line 289
4409 __cil_tmp61 = (unsigned long )dt;
4410#line 289
4411 __cil_tmp62 = __cil_tmp61 + 4;
4412#line 289
4413 __cil_tmp63 = *((int *)__cil_tmp62);
4414#line 289
4415 __dynamic_dev_dbg(& descriptor___1, __cil_tmp60, "tm_min : %i\n", __cil_tmp63);
4416 }
4417 } else {
4418
4419 }
4420 {
4421#line 290
4422 __cil_tmp64 = & descriptor___2;
4423#line 290
4424 *((char const **)__cil_tmp64) = "rtc_v3020";
4425#line 290
4426 __cil_tmp65 = (unsigned long )(& descriptor___2) + 8;
4427#line 290
4428 *((char const **)__cil_tmp65) = "v3020_set_time";
4429#line 290
4430 __cil_tmp66 = (unsigned long )(& descriptor___2) + 16;
4431#line 290
4432 *((char const **)__cil_tmp66) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4433#line 290
4434 __cil_tmp67 = (unsigned long )(& descriptor___2) + 24;
4435#line 290
4436 *((char const **)__cil_tmp67) = "tm_hour: %i\n";
4437#line 290
4438 __cil_tmp68 = (unsigned long )(& descriptor___2) + 32;
4439#line 290
4440 *((unsigned int *)__cil_tmp68) = 290U;
4441#line 290
4442 __cil_tmp69 = (unsigned long )(& descriptor___2) + 35;
4443#line 290
4444 *((unsigned char *)__cil_tmp69) = (unsigned char)1;
4445#line 290
4446 __cil_tmp70 = (unsigned long )(& descriptor___2) + 35;
4447#line 290
4448 __cil_tmp71 = *((unsigned char *)__cil_tmp70);
4449#line 290
4450 __cil_tmp72 = (long )__cil_tmp71;
4451#line 290
4452 __cil_tmp73 = __cil_tmp72 & 1L;
4453#line 290
4454 tmp___3 = __builtin_expect(__cil_tmp73, 0L);
4455 }
4456#line 290
4457 if (tmp___3 != 0L) {
4458 {
4459#line 290
4460 __cil_tmp74 = (struct device const *)dev;
4461#line 290
4462 __cil_tmp75 = (unsigned long )dt;
4463#line 290
4464 __cil_tmp76 = __cil_tmp75 + 8;
4465#line 290
4466 __cil_tmp77 = *((int *)__cil_tmp76);
4467#line 290
4468 __dynamic_dev_dbg(& descriptor___2, __cil_tmp74, "tm_hour: %i\n", __cil_tmp77);
4469 }
4470 } else {
4471
4472 }
4473 {
4474#line 291
4475 __cil_tmp78 = & descriptor___3;
4476#line 291
4477 *((char const **)__cil_tmp78) = "rtc_v3020";
4478#line 291
4479 __cil_tmp79 = (unsigned long )(& descriptor___3) + 8;
4480#line 291
4481 *((char const **)__cil_tmp79) = "v3020_set_time";
4482#line 291
4483 __cil_tmp80 = (unsigned long )(& descriptor___3) + 16;
4484#line 291
4485 *((char const **)__cil_tmp80) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4486#line 291
4487 __cil_tmp81 = (unsigned long )(& descriptor___3) + 24;
4488#line 291
4489 *((char const **)__cil_tmp81) = "tm_mday: %i\n";
4490#line 291
4491 __cil_tmp82 = (unsigned long )(& descriptor___3) + 32;
4492#line 291
4493 *((unsigned int *)__cil_tmp82) = 291U;
4494#line 291
4495 __cil_tmp83 = (unsigned long )(& descriptor___3) + 35;
4496#line 291
4497 *((unsigned char *)__cil_tmp83) = (unsigned char)1;
4498#line 291
4499 __cil_tmp84 = (unsigned long )(& descriptor___3) + 35;
4500#line 291
4501 __cil_tmp85 = *((unsigned char *)__cil_tmp84);
4502#line 291
4503 __cil_tmp86 = (long )__cil_tmp85;
4504#line 291
4505 __cil_tmp87 = __cil_tmp86 & 1L;
4506#line 291
4507 tmp___4 = __builtin_expect(__cil_tmp87, 0L);
4508 }
4509#line 291
4510 if (tmp___4 != 0L) {
4511 {
4512#line 291
4513 __cil_tmp88 = (struct device const *)dev;
4514#line 291
4515 __cil_tmp89 = (unsigned long )dt;
4516#line 291
4517 __cil_tmp90 = __cil_tmp89 + 12;
4518#line 291
4519 __cil_tmp91 = *((int *)__cil_tmp90);
4520#line 291
4521 __dynamic_dev_dbg(& descriptor___3, __cil_tmp88, "tm_mday: %i\n", __cil_tmp91);
4522 }
4523 } else {
4524
4525 }
4526 {
4527#line 292
4528 __cil_tmp92 = & descriptor___4;
4529#line 292
4530 *((char const **)__cil_tmp92) = "rtc_v3020";
4531#line 292
4532 __cil_tmp93 = (unsigned long )(& descriptor___4) + 8;
4533#line 292
4534 *((char const **)__cil_tmp93) = "v3020_set_time";
4535#line 292
4536 __cil_tmp94 = (unsigned long )(& descriptor___4) + 16;
4537#line 292
4538 *((char const **)__cil_tmp94) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4539#line 292
4540 __cil_tmp95 = (unsigned long )(& descriptor___4) + 24;
4541#line 292
4542 *((char const **)__cil_tmp95) = "tm_wday: %i\n";
4543#line 292
4544 __cil_tmp96 = (unsigned long )(& descriptor___4) + 32;
4545#line 292
4546 *((unsigned int *)__cil_tmp96) = 292U;
4547#line 292
4548 __cil_tmp97 = (unsigned long )(& descriptor___4) + 35;
4549#line 292
4550 *((unsigned char *)__cil_tmp97) = (unsigned char)1;
4551#line 292
4552 __cil_tmp98 = (unsigned long )(& descriptor___4) + 35;
4553#line 292
4554 __cil_tmp99 = *((unsigned char *)__cil_tmp98);
4555#line 292
4556 __cil_tmp100 = (long )__cil_tmp99;
4557#line 292
4558 __cil_tmp101 = __cil_tmp100 & 1L;
4559#line 292
4560 tmp___5 = __builtin_expect(__cil_tmp101, 0L);
4561 }
4562#line 292
4563 if (tmp___5 != 0L) {
4564 {
4565#line 292
4566 __cil_tmp102 = (struct device const *)dev;
4567#line 292
4568 __cil_tmp103 = (unsigned long )dt;
4569#line 292
4570 __cil_tmp104 = __cil_tmp103 + 24;
4571#line 292
4572 __cil_tmp105 = *((int *)__cil_tmp104);
4573#line 292
4574 __dynamic_dev_dbg(& descriptor___4, __cil_tmp102, "tm_wday: %i\n", __cil_tmp105);
4575 }
4576 } else {
4577
4578 }
4579 {
4580#line 293
4581 __cil_tmp106 = & descriptor___5;
4582#line 293
4583 *((char const **)__cil_tmp106) = "rtc_v3020";
4584#line 293
4585 __cil_tmp107 = (unsigned long )(& descriptor___5) + 8;
4586#line 293
4587 *((char const **)__cil_tmp107) = "v3020_set_time";
4588#line 293
4589 __cil_tmp108 = (unsigned long )(& descriptor___5) + 16;
4590#line 293
4591 *((char const **)__cil_tmp108) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p";
4592#line 293
4593 __cil_tmp109 = (unsigned long )(& descriptor___5) + 24;
4594#line 293
4595 *((char const **)__cil_tmp109) = "tm_year: %i\n";
4596#line 293
4597 __cil_tmp110 = (unsigned long )(& descriptor___5) + 32;
4598#line 293
4599 *((unsigned int *)__cil_tmp110) = 293U;
4600#line 293
4601 __cil_tmp111 = (unsigned long )(& descriptor___5) + 35;
4602#line 293
4603 *((unsigned char *)__cil_tmp111) = (unsigned char)1;
4604#line 293
4605 __cil_tmp112 = (unsigned long )(& descriptor___5) + 35;
4606#line 293
4607 __cil_tmp113 = *((unsigned char *)__cil_tmp112);
4608#line 293
4609 __cil_tmp114 = (long )__cil_tmp113;
4610#line 293
4611 __cil_tmp115 = __cil_tmp114 & 1L;
4612#line 293
4613 tmp___6 = __builtin_expect(__cil_tmp115, 0L);
4614 }
4615#line 293
4616 if (tmp___6 != 0L) {
4617 {
4618#line 293
4619 __cil_tmp116 = (struct device const *)dev;
4620#line 293
4621 __cil_tmp117 = (unsigned long )dt;
4622#line 293
4623 __cil_tmp118 = __cil_tmp117 + 20;
4624#line 293
4625 __cil_tmp119 = *((int *)__cil_tmp118);
4626#line 293
4627 __dynamic_dev_dbg(& descriptor___5, __cil_tmp116, "tm_year: %i\n", __cil_tmp119);
4628 }
4629 } else {
4630
4631 }
4632 {
4633#line 296
4634 __cil_tmp120 = *((int *)dt);
4635#line 296
4636 __cil_tmp121 = (unsigned int )__cil_tmp120;
4637#line 296
4638 tmp___7 = bin2bcd(__cil_tmp121);
4639#line 296
4640 __cil_tmp122 = (int )tmp___7;
4641#line 296
4642 __cil_tmp123 = (unsigned char )__cil_tmp122;
4643#line 296
4644 v3020_set_reg(chip, (unsigned char)2, __cil_tmp123);
4645#line 297
4646 __cil_tmp124 = (unsigned long )dt;
4647#line 297
4648 __cil_tmp125 = __cil_tmp124 + 4;
4649#line 297
4650 __cil_tmp126 = *((int *)__cil_tmp125);
4651#line 297
4652 __cil_tmp127 = (unsigned int )__cil_tmp126;
4653#line 297
4654 tmp___8 = bin2bcd(__cil_tmp127);
4655#line 297
4656 __cil_tmp128 = (int )tmp___8;
4657#line 297
4658 __cil_tmp129 = (unsigned char )__cil_tmp128;
4659#line 297
4660 v3020_set_reg(chip, (unsigned char)3, __cil_tmp129);
4661#line 298
4662 __cil_tmp130 = (unsigned long )dt;
4663#line 298
4664 __cil_tmp131 = __cil_tmp130 + 8;
4665#line 298
4666 __cil_tmp132 = *((int *)__cil_tmp131);
4667#line 298
4668 __cil_tmp133 = (unsigned int )__cil_tmp132;
4669#line 298
4670 tmp___9 = bin2bcd(__cil_tmp133);
4671#line 298
4672 __cil_tmp134 = (int )tmp___9;
4673#line 298
4674 __cil_tmp135 = (unsigned char )__cil_tmp134;
4675#line 298
4676 v3020_set_reg(chip, (unsigned char)4, __cil_tmp135);
4677#line 299
4678 __cil_tmp136 = (unsigned long )dt;
4679#line 299
4680 __cil_tmp137 = __cil_tmp136 + 12;
4681#line 299
4682 __cil_tmp138 = *((int *)__cil_tmp137);
4683#line 299
4684 __cil_tmp139 = (unsigned int )__cil_tmp138;
4685#line 299
4686 tmp___10 = bin2bcd(__cil_tmp139);
4687#line 299
4688 __cil_tmp140 = (int )tmp___10;
4689#line 299
4690 __cil_tmp141 = (unsigned char )__cil_tmp140;
4691#line 299
4692 v3020_set_reg(chip, (unsigned char)5, __cil_tmp141);
4693#line 300
4694 __cil_tmp142 = (unsigned long )dt;
4695#line 300
4696 __cil_tmp143 = __cil_tmp142 + 16;
4697#line 300
4698 __cil_tmp144 = *((int *)__cil_tmp143);
4699#line 300
4700 __cil_tmp145 = __cil_tmp144 + 1;
4701#line 300
4702 __cil_tmp146 = (unsigned int )__cil_tmp145;
4703#line 300
4704 tmp___11 = bin2bcd(__cil_tmp146);
4705#line 300
4706 __cil_tmp147 = (int )tmp___11;
4707#line 300
4708 __cil_tmp148 = (unsigned char )__cil_tmp147;
4709#line 300
4710 v3020_set_reg(chip, (unsigned char)6, __cil_tmp148);
4711#line 301
4712 __cil_tmp149 = (unsigned long )dt;
4713#line 301
4714 __cil_tmp150 = __cil_tmp149 + 24;
4715#line 301
4716 __cil_tmp151 = *((int *)__cil_tmp150);
4717#line 301
4718 __cil_tmp152 = (unsigned int )__cil_tmp151;
4719#line 301
4720 tmp___12 = bin2bcd(__cil_tmp152);
4721#line 301
4722 __cil_tmp153 = (int )tmp___12;
4723#line 301
4724 __cil_tmp154 = (unsigned char )__cil_tmp153;
4725#line 301
4726 v3020_set_reg(chip, (unsigned char)8, __cil_tmp154);
4727#line 302
4728 __cil_tmp155 = (unsigned long )dt;
4729#line 302
4730 __cil_tmp156 = __cil_tmp155 + 20;
4731#line 302
4732 __cil_tmp157 = *((int *)__cil_tmp156);
4733#line 302
4734 __cil_tmp158 = __cil_tmp157 % 100;
4735#line 302
4736 __cil_tmp159 = (unsigned int )__cil_tmp158;
4737#line 302
4738 tmp___13 = bin2bcd(__cil_tmp159);
4739#line 302
4740 __cil_tmp160 = (int )tmp___13;
4741#line 302
4742 __cil_tmp161 = (unsigned char )__cil_tmp160;
4743#line 302
4744 v3020_set_reg(chip, (unsigned char)7, __cil_tmp161);
4745#line 305
4746 v3020_set_reg(chip, (unsigned char)14, (unsigned char)0);
4747 }
4748#line 311
4749 return (0);
4750}
4751}
4752#line 314 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
4753static struct rtc_class_ops const v3020_rtc_ops =
4754#line 314
4755 {(int (*)(struct device * ))0, (void (*)(struct device * ))0, (int (*)(struct device * ,
4756 unsigned int ,
4757 unsigned long ))0,
4758 & v3020_read_time, & v3020_set_time, (int (*)(struct device * , struct rtc_wkalrm * ))0,
4759 (int (*)(struct device * , struct rtc_wkalrm * ))0, (int (*)(struct device * ,
4760 struct seq_file * ))0,
4761 (int (*)(struct device * , unsigned long ))0, (int (*)(struct device * , int ))0,
4762 (int (*)(struct device * , unsigned int ))0};
4763#line 319 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
4764static int rtc_probe(struct platform_device *pdev )
4765{ struct v3020_platform_data *pdata ;
4766 struct v3020 *chip ;
4767 int retval ;
4768 int i ;
4769 int temp ;
4770 void *tmp ;
4771 unsigned char tmp___0 ;
4772 unsigned char tmp___1 ;
4773 long tmp___2 ;
4774 long tmp___3 ;
4775 unsigned long __cil_tmp12 ;
4776 unsigned long __cil_tmp13 ;
4777 unsigned long __cil_tmp14 ;
4778 void *__cil_tmp15 ;
4779 struct v3020 *__cil_tmp16 ;
4780 unsigned long __cil_tmp17 ;
4781 unsigned long __cil_tmp18 ;
4782 unsigned char *__cil_tmp19 ;
4783 unsigned char *__cil_tmp20 ;
4784 unsigned char __cil_tmp21 ;
4785 unsigned int __cil_tmp22 ;
4786 unsigned long __cil_tmp23 ;
4787 unsigned long __cil_tmp24 ;
4788 unsigned long __cil_tmp25 ;
4789 unsigned long __cil_tmp26 ;
4790 unsigned long __cil_tmp27 ;
4791 unsigned long __cil_tmp28 ;
4792 struct v3020_chip_ops *__cil_tmp29 ;
4793 int (*__cil_tmp30)(struct v3020 * , struct platform_device * , struct v3020_platform_data * ) ;
4794 unsigned long __cil_tmp31 ;
4795 unsigned long __cil_tmp32 ;
4796 struct v3020_chip_ops *__cil_tmp33 ;
4797 unsigned long __cil_tmp34 ;
4798 unsigned long __cil_tmp35 ;
4799 unsigned char (*__cil_tmp36)(struct v3020 * ) ;
4800 unsigned int __cil_tmp37 ;
4801 unsigned char *__cil_tmp38 ;
4802 unsigned char *__cil_tmp39 ;
4803 unsigned char __cil_tmp40 ;
4804 unsigned int __cil_tmp41 ;
4805 unsigned long __cil_tmp42 ;
4806 unsigned long __cil_tmp43 ;
4807 struct device *__cil_tmp44 ;
4808 struct device const *__cil_tmp45 ;
4809 unsigned long __cil_tmp46 ;
4810 unsigned long __cil_tmp47 ;
4811 struct v3020_gpio *__cil_tmp48 ;
4812 unsigned long __cil_tmp49 ;
4813 unsigned long __cil_tmp50 ;
4814 unsigned int __cil_tmp51 ;
4815 unsigned long __cil_tmp52 ;
4816 unsigned long __cil_tmp53 ;
4817 struct v3020_gpio *__cil_tmp54 ;
4818 struct v3020_gpio *__cil_tmp55 ;
4819 unsigned long __cil_tmp56 ;
4820 unsigned long __cil_tmp57 ;
4821 unsigned int __cil_tmp58 ;
4822 unsigned long __cil_tmp59 ;
4823 unsigned long __cil_tmp60 ;
4824 struct v3020_gpio *__cil_tmp61 ;
4825 struct v3020_gpio *__cil_tmp62 ;
4826 unsigned long __cil_tmp63 ;
4827 unsigned long __cil_tmp64 ;
4828 unsigned int __cil_tmp65 ;
4829 unsigned long __cil_tmp66 ;
4830 unsigned long __cil_tmp67 ;
4831 struct v3020_gpio *__cil_tmp68 ;
4832 struct v3020_gpio *__cil_tmp69 ;
4833 unsigned long __cil_tmp70 ;
4834 unsigned long __cil_tmp71 ;
4835 unsigned int __cil_tmp72 ;
4836 unsigned long __cil_tmp73 ;
4837 unsigned long __cil_tmp74 ;
4838 struct device *__cil_tmp75 ;
4839 struct device const *__cil_tmp76 ;
4840 unsigned long __cil_tmp77 ;
4841 unsigned long __cil_tmp78 ;
4842 struct resource *__cil_tmp79 ;
4843 resource_size_t __cil_tmp80 ;
4844 unsigned long __cil_tmp81 ;
4845 unsigned long __cil_tmp82 ;
4846 int __cil_tmp83 ;
4847 void *__cil_tmp84 ;
4848 unsigned long __cil_tmp85 ;
4849 unsigned long __cil_tmp86 ;
4850 unsigned long __cil_tmp87 ;
4851 unsigned long __cil_tmp88 ;
4852 struct device *__cil_tmp89 ;
4853 unsigned long __cil_tmp90 ;
4854 unsigned long __cil_tmp91 ;
4855 struct rtc_device *__cil_tmp92 ;
4856 void const *__cil_tmp93 ;
4857 unsigned long __cil_tmp94 ;
4858 unsigned long __cil_tmp95 ;
4859 struct rtc_device *__cil_tmp96 ;
4860 void const *__cil_tmp97 ;
4861 unsigned long __cil_tmp98 ;
4862 unsigned long __cil_tmp99 ;
4863 struct v3020_chip_ops *__cil_tmp100 ;
4864 unsigned long __cil_tmp101 ;
4865 unsigned long __cil_tmp102 ;
4866 void (*__cil_tmp103)(struct v3020 * ) ;
4867 void const *__cil_tmp104 ;
4868
4869 {
4870 {
4871#line 321
4872 __cil_tmp12 = 16 + 280;
4873#line 321
4874 __cil_tmp13 = (unsigned long )pdev;
4875#line 321
4876 __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
4877#line 321
4878 __cil_tmp15 = *((void **)__cil_tmp14);
4879#line 321
4880 pdata = (struct v3020_platform_data *)__cil_tmp15;
4881#line 323
4882 retval = -16;
4883#line 327
4884 tmp = kzalloc(40UL, 208U);
4885#line 327
4886 chip = (struct v3020 *)tmp;
4887 }
4888 {
4889#line 328
4890 __cil_tmp16 = (struct v3020 *)0;
4891#line 328
4892 __cil_tmp17 = (unsigned long )__cil_tmp16;
4893#line 328
4894 __cil_tmp18 = (unsigned long )chip;
4895#line 328
4896 if (__cil_tmp18 == __cil_tmp17) {
4897#line 329
4898 return (-12);
4899 } else {
4900
4901 }
4902 }
4903 {
4904#line 331
4905 __cil_tmp19 = (unsigned char *)pdata;
4906#line 331
4907 __cil_tmp20 = __cil_tmp19 + 4UL;
4908#line 331
4909 __cil_tmp21 = *__cil_tmp20;
4910#line 331
4911 __cil_tmp22 = (unsigned int )__cil_tmp21;
4912#line 331
4913 if (__cil_tmp22 != 0U) {
4914#line 332
4915 __cil_tmp23 = (unsigned long )chip;
4916#line 332
4917 __cil_tmp24 = __cil_tmp23 + 24;
4918#line 332
4919 *((struct v3020_chip_ops **)__cil_tmp24) = & v3020_gpio_ops;
4920 } else {
4921#line 334
4922 __cil_tmp25 = (unsigned long )chip;
4923#line 334
4924 __cil_tmp26 = __cil_tmp25 + 24;
4925#line 334
4926 *((struct v3020_chip_ops **)__cil_tmp26) = & v3020_mmio_ops;
4927 }
4928 }
4929 {
4930#line 336
4931 __cil_tmp27 = (unsigned long )chip;
4932#line 336
4933 __cil_tmp28 = __cil_tmp27 + 24;
4934#line 336
4935 __cil_tmp29 = *((struct v3020_chip_ops **)__cil_tmp28);
4936#line 336
4937 __cil_tmp30 = *((int (**)(struct v3020 * , struct platform_device * , struct v3020_platform_data * ))__cil_tmp29);
4938#line 336
4939 retval = (*__cil_tmp30)(chip, pdev, pdata);
4940 }
4941#line 337
4942 if (retval != 0) {
4943#line 338
4944 goto err_chip;
4945 } else {
4946
4947 }
4948#line 342
4949 i = 0;
4950#line 342
4951 goto ldv_21332;
4952 ldv_21331:
4953 {
4954#line 343
4955 __cil_tmp31 = (unsigned long )chip;
4956#line 343
4957 __cil_tmp32 = __cil_tmp31 + 24;
4958#line 343
4959 __cil_tmp33 = *((struct v3020_chip_ops **)__cil_tmp32);
4960#line 343
4961 __cil_tmp34 = (unsigned long )__cil_tmp33;
4962#line 343
4963 __cil_tmp35 = __cil_tmp34 + 16;
4964#line 343
4965 __cil_tmp36 = *((unsigned char (**)(struct v3020 * ))__cil_tmp35);
4966#line 343
4967 tmp___0 = (*__cil_tmp36)(chip);
4968#line 343
4969 temp = (int )tmp___0;
4970#line 342
4971 i = i + 1;
4972 }
4973 ldv_21332: ;
4974#line 342
4975 if (i <= 7) {
4976#line 343
4977 goto ldv_21331;
4978 } else {
4979#line 345
4980 goto ldv_21333;
4981 }
4982 ldv_21333:
4983 {
4984#line 347
4985 v3020_set_reg(chip, (unsigned char)2, (unsigned char)51);
4986#line 348
4987 tmp___1 = v3020_get_reg(chip, (unsigned char)2);
4988 }
4989 {
4990#line 348
4991 __cil_tmp37 = (unsigned int )tmp___1;
4992#line 348
4993 if (__cil_tmp37 != 51U) {
4994#line 349
4995 retval = -19;
4996#line 350
4997 goto err_io;
4998 } else {
4999
5000 }
5001 }
5002 {
5003#line 355
5004 v3020_set_reg(chip, (unsigned char)0, (unsigned char)0);
5005 }
5006 {
5007#line 357
5008 __cil_tmp38 = (unsigned char *)pdata;
5009#line 357
5010 __cil_tmp39 = __cil_tmp38 + 4UL;
5011#line 357
5012 __cil_tmp40 = *__cil_tmp39;
5013#line 357
5014 __cil_tmp41 = (unsigned int )__cil_tmp40;
5015#line 357
5016 if (__cil_tmp41 != 0U) {
5017 {
5018#line 358
5019 __cil_tmp42 = (unsigned long )pdev;
5020#line 358
5021 __cil_tmp43 = __cil_tmp42 + 16;
5022#line 358
5023 __cil_tmp44 = (struct device *)__cil_tmp43;
5024#line 358
5025 __cil_tmp45 = (struct device const *)__cil_tmp44;
5026#line 358
5027 __cil_tmp46 = (unsigned long )chip;
5028#line 358
5029 __cil_tmp47 = __cil_tmp46 + 16;
5030#line 358
5031 __cil_tmp48 = *((struct v3020_gpio **)__cil_tmp47);
5032#line 358
5033 __cil_tmp49 = (unsigned long )__cil_tmp48;
5034#line 358
5035 __cil_tmp50 = __cil_tmp49 + 8;
5036#line 358
5037 __cil_tmp51 = *((unsigned int *)__cil_tmp50);
5038#line 358
5039 __cil_tmp52 = (unsigned long )chip;
5040#line 358
5041 __cil_tmp53 = __cil_tmp52 + 16;
5042#line 358
5043 __cil_tmp54 = *((struct v3020_gpio **)__cil_tmp53);
5044#line 358
5045 __cil_tmp55 = __cil_tmp54 + 1UL;
5046#line 358
5047 __cil_tmp56 = (unsigned long )__cil_tmp55;
5048#line 358
5049 __cil_tmp57 = __cil_tmp56 + 8;
5050#line 358
5051 __cil_tmp58 = *((unsigned int *)__cil_tmp57);
5052#line 358
5053 __cil_tmp59 = (unsigned long )chip;
5054#line 358
5055 __cil_tmp60 = __cil_tmp59 + 16;
5056#line 358
5057 __cil_tmp61 = *((struct v3020_gpio **)__cil_tmp60);
5058#line 358
5059 __cil_tmp62 = __cil_tmp61 + 2UL;
5060#line 358
5061 __cil_tmp63 = (unsigned long )__cil_tmp62;
5062#line 358
5063 __cil_tmp64 = __cil_tmp63 + 8;
5064#line 358
5065 __cil_tmp65 = *((unsigned int *)__cil_tmp64);
5066#line 358
5067 __cil_tmp66 = (unsigned long )chip;
5068#line 358
5069 __cil_tmp67 = __cil_tmp66 + 16;
5070#line 358
5071 __cil_tmp68 = *((struct v3020_gpio **)__cil_tmp67);
5072#line 358
5073 __cil_tmp69 = __cil_tmp68 + 3UL;
5074#line 358
5075 __cil_tmp70 = (unsigned long )__cil_tmp69;
5076#line 358
5077 __cil_tmp71 = __cil_tmp70 + 8;
5078#line 358
5079 __cil_tmp72 = *((unsigned int *)__cil_tmp71);
5080#line 358
5081 _dev_info(__cil_tmp45, "Chip available at GPIOs %d, %d, %d, %d\n", __cil_tmp51,
5082 __cil_tmp58, __cil_tmp65, __cil_tmp72);
5083 }
5084 } else {
5085 {
5086#line 363
5087 __cil_tmp73 = (unsigned long )pdev;
5088#line 363
5089 __cil_tmp74 = __cil_tmp73 + 16;
5090#line 363
5091 __cil_tmp75 = (struct device *)__cil_tmp74;
5092#line 363
5093 __cil_tmp76 = (struct device const *)__cil_tmp75;
5094#line 363
5095 __cil_tmp77 = (unsigned long )pdev;
5096#line 363
5097 __cil_tmp78 = __cil_tmp77 + 1176;
5098#line 363
5099 __cil_tmp79 = *((struct resource **)__cil_tmp78);
5100#line 363
5101 __cil_tmp80 = *((resource_size_t *)__cil_tmp79);
5102#line 363
5103 __cil_tmp81 = (unsigned long )chip;
5104#line 363
5105 __cil_tmp82 = __cil_tmp81 + 8;
5106#line 363
5107 __cil_tmp83 = *((int *)__cil_tmp82);
5108#line 363
5109 _dev_info(__cil_tmp76, "Chip available at physical address 0x%llx,data connected to D%d\n",
5110 __cil_tmp80, __cil_tmp83);
5111 }
5112 }
5113 }
5114 {
5115#line 369
5116 __cil_tmp84 = (void *)chip;
5117#line 369
5118 platform_set_drvdata(pdev, __cil_tmp84);
5119#line 371
5120 __cil_tmp85 = (unsigned long )chip;
5121#line 371
5122 __cil_tmp86 = __cil_tmp85 + 32;
5123#line 371
5124 __cil_tmp87 = (unsigned long )pdev;
5125#line 371
5126 __cil_tmp88 = __cil_tmp87 + 16;
5127#line 371
5128 __cil_tmp89 = (struct device *)__cil_tmp88;
5129#line 371
5130 *((struct rtc_device **)__cil_tmp86) = rtc_device_register("v3020", __cil_tmp89,
5131 & v3020_rtc_ops, & __this_module);
5132#line 373
5133 __cil_tmp90 = (unsigned long )chip;
5134#line 373
5135 __cil_tmp91 = __cil_tmp90 + 32;
5136#line 373
5137 __cil_tmp92 = *((struct rtc_device **)__cil_tmp91);
5138#line 373
5139 __cil_tmp93 = (void const *)__cil_tmp92;
5140#line 373
5141 tmp___3 = IS_ERR(__cil_tmp93);
5142 }
5143#line 373
5144 if (tmp___3 != 0L) {
5145 {
5146#line 374
5147 __cil_tmp94 = (unsigned long )chip;
5148#line 374
5149 __cil_tmp95 = __cil_tmp94 + 32;
5150#line 374
5151 __cil_tmp96 = *((struct rtc_device **)__cil_tmp95);
5152#line 374
5153 __cil_tmp97 = (void const *)__cil_tmp96;
5154#line 374
5155 tmp___2 = PTR_ERR(__cil_tmp97);
5156#line 374
5157 retval = (int )tmp___2;
5158 }
5159#line 375
5160 goto err_io;
5161 } else {
5162
5163 }
5164#line 378
5165 return (0);
5166 err_io:
5167 {
5168#line 381
5169 __cil_tmp98 = (unsigned long )chip;
5170#line 381
5171 __cil_tmp99 = __cil_tmp98 + 24;
5172#line 381
5173 __cil_tmp100 = *((struct v3020_chip_ops **)__cil_tmp99);
5174#line 381
5175 __cil_tmp101 = (unsigned long )__cil_tmp100;
5176#line 381
5177 __cil_tmp102 = __cil_tmp101 + 8;
5178#line 381
5179 __cil_tmp103 = *((void (**)(struct v3020 * ))__cil_tmp102);
5180#line 381
5181 (*__cil_tmp103)(chip);
5182 }
5183 err_chip:
5184 {
5185#line 383
5186 __cil_tmp104 = (void const *)chip;
5187#line 383
5188 kfree(__cil_tmp104);
5189 }
5190#line 385
5191 return (retval);
5192}
5193}
5194#line 388 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5195static int rtc_remove(struct platform_device *dev )
5196{ struct v3020 *chip ;
5197 void *tmp ;
5198 struct rtc_device *rtc ;
5199 struct platform_device const *__cil_tmp5 ;
5200 unsigned long __cil_tmp6 ;
5201 unsigned long __cil_tmp7 ;
5202 struct rtc_device *__cil_tmp8 ;
5203 unsigned long __cil_tmp9 ;
5204 unsigned long __cil_tmp10 ;
5205 unsigned long __cil_tmp11 ;
5206 unsigned long __cil_tmp12 ;
5207 struct v3020_chip_ops *__cil_tmp13 ;
5208 unsigned long __cil_tmp14 ;
5209 unsigned long __cil_tmp15 ;
5210 void (*__cil_tmp16)(struct v3020 * ) ;
5211 void const *__cil_tmp17 ;
5212
5213 {
5214 {
5215#line 390
5216 __cil_tmp5 = (struct platform_device const *)dev;
5217#line 390
5218 tmp = platform_get_drvdata(__cil_tmp5);
5219#line 390
5220 chip = (struct v3020 *)tmp;
5221#line 391
5222 __cil_tmp6 = (unsigned long )chip;
5223#line 391
5224 __cil_tmp7 = __cil_tmp6 + 32;
5225#line 391
5226 rtc = *((struct rtc_device **)__cil_tmp7);
5227 }
5228 {
5229#line 393
5230 __cil_tmp8 = (struct rtc_device *)0;
5231#line 393
5232 __cil_tmp9 = (unsigned long )__cil_tmp8;
5233#line 393
5234 __cil_tmp10 = (unsigned long )rtc;
5235#line 393
5236 if (__cil_tmp10 != __cil_tmp9) {
5237 {
5238#line 394
5239 rtc_device_unregister(rtc);
5240 }
5241 } else {
5242
5243 }
5244 }
5245 {
5246#line 396
5247 __cil_tmp11 = (unsigned long )chip;
5248#line 396
5249 __cil_tmp12 = __cil_tmp11 + 24;
5250#line 396
5251 __cil_tmp13 = *((struct v3020_chip_ops **)__cil_tmp12);
5252#line 396
5253 __cil_tmp14 = (unsigned long )__cil_tmp13;
5254#line 396
5255 __cil_tmp15 = __cil_tmp14 + 8;
5256#line 396
5257 __cil_tmp16 = *((void (**)(struct v3020 * ))__cil_tmp15);
5258#line 396
5259 (*__cil_tmp16)(chip);
5260#line 397
5261 __cil_tmp17 = (void const *)chip;
5262#line 397
5263 kfree(__cil_tmp17);
5264 }
5265#line 399
5266 return (0);
5267}
5268}
5269#line 434
5270extern void ldv_check_final_state(void) ;
5271#line 437
5272extern void ldv_check_return_value(int ) ;
5273#line 440
5274extern void ldv_initialize(void) ;
5275#line 443
5276extern int __VERIFIER_nondet_int(void) ;
5277#line 446 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5278int LDV_IN_INTERRUPT ;
5279#line 449 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5280void main(void)
5281{ struct v3020 *var_group1 ;
5282 struct platform_device *var_group2 ;
5283 struct v3020_platform_data *var_v3020_mmio_map_0_p2 ;
5284 unsigned char var_v3020_mmio_write_bit_2_p1 ;
5285 struct v3020_platform_data *var_v3020_gpio_map_4_p2 ;
5286 unsigned char var_v3020_gpio_write_bit_6_p1 ;
5287 struct device *var_group3 ;
5288 struct rtc_time *var_group4 ;
5289 int res_rtc_probe_12 ;
5290 int ldv_s_rtc_device_driver_platform_driver ;
5291 int tmp ;
5292 int tmp___0 ;
5293 int __cil_tmp13 ;
5294 unsigned char __cil_tmp14 ;
5295 int __cil_tmp15 ;
5296 unsigned char __cil_tmp16 ;
5297
5298 {
5299 {
5300#line 599
5301 ldv_s_rtc_device_driver_platform_driver = 0;
5302#line 583
5303 LDV_IN_INTERRUPT = 1;
5304#line 592
5305 ldv_initialize();
5306 }
5307#line 602
5308 goto ldv_21399;
5309 ldv_21398:
5310 {
5311#line 606
5312 tmp = __VERIFIER_nondet_int();
5313 }
5314#line 608
5315 if (tmp == 0) {
5316#line 608
5317 goto case_0;
5318 } else
5319#line 630
5320 if (tmp == 1) {
5321#line 630
5322 goto case_1;
5323 } else
5324#line 652
5325 if (tmp == 2) {
5326#line 652
5327 goto case_2;
5328 } else
5329#line 674
5330 if (tmp == 3) {
5331#line 674
5332 goto case_3;
5333 } else
5334#line 696
5335 if (tmp == 4) {
5336#line 696
5337 goto case_4;
5338 } else
5339#line 718
5340 if (tmp == 5) {
5341#line 718
5342 goto case_5;
5343 } else
5344#line 740
5345 if (tmp == 6) {
5346#line 740
5347 goto case_6;
5348 } else
5349#line 762
5350 if (tmp == 7) {
5351#line 762
5352 goto case_7;
5353 } else
5354#line 784
5355 if (tmp == 8) {
5356#line 784
5357 goto case_8;
5358 } else
5359#line 806
5360 if (tmp == 9) {
5361#line 806
5362 goto case_9;
5363 } else
5364#line 828
5365 if (tmp == 10) {
5366#line 828
5367 goto case_10;
5368 } else
5369#line 853
5370 if (tmp == 11) {
5371#line 853
5372 goto case_11;
5373 } else {
5374 {
5375#line 875
5376 goto switch_default;
5377#line 606
5378 if (0) {
5379 case_0:
5380 {
5381#line 622
5382 v3020_mmio_map(var_group1, var_group2, var_v3020_mmio_map_0_p2);
5383 }
5384#line 629
5385 goto ldv_21384;
5386 case_1:
5387 {
5388#line 644
5389 v3020_mmio_unmap(var_group1);
5390 }
5391#line 651
5392 goto ldv_21384;
5393 case_2:
5394 {
5395#line 666
5396 v3020_mmio_read_bit(var_group1);
5397 }
5398#line 673
5399 goto ldv_21384;
5400 case_3:
5401 {
5402#line 688
5403 __cil_tmp13 = (int )var_v3020_mmio_write_bit_2_p1;
5404#line 688
5405 __cil_tmp14 = (unsigned char )__cil_tmp13;
5406#line 688
5407 v3020_mmio_write_bit(var_group1, __cil_tmp14);
5408 }
5409#line 695
5410 goto ldv_21384;
5411 case_4:
5412 {
5413#line 710
5414 v3020_gpio_map(var_group1, var_group2, var_v3020_gpio_map_4_p2);
5415 }
5416#line 717
5417 goto ldv_21384;
5418 case_5:
5419 {
5420#line 732
5421 v3020_gpio_unmap(var_group1);
5422 }
5423#line 739
5424 goto ldv_21384;
5425 case_6:
5426 {
5427#line 754
5428 v3020_gpio_read_bit(var_group1);
5429 }
5430#line 761
5431 goto ldv_21384;
5432 case_7:
5433 {
5434#line 776
5435 __cil_tmp15 = (int )var_v3020_gpio_write_bit_6_p1;
5436#line 776
5437 __cil_tmp16 = (unsigned char )__cil_tmp15;
5438#line 776
5439 v3020_gpio_write_bit(var_group1, __cil_tmp16);
5440 }
5441#line 783
5442 goto ldv_21384;
5443 case_8:
5444 {
5445#line 798
5446 v3020_read_time(var_group3, var_group4);
5447 }
5448#line 805
5449 goto ldv_21384;
5450 case_9:
5451 {
5452#line 820
5453 v3020_set_time(var_group3, var_group4);
5454 }
5455#line 827
5456 goto ldv_21384;
5457 case_10: ;
5458#line 831
5459 if (ldv_s_rtc_device_driver_platform_driver == 0) {
5460 {
5461#line 842
5462 res_rtc_probe_12 = rtc_probe(var_group2);
5463#line 843
5464 ldv_check_return_value(res_rtc_probe_12);
5465 }
5466#line 844
5467 if (res_rtc_probe_12 != 0) {
5468#line 845
5469 goto ldv_module_exit;
5470 } else {
5471
5472 }
5473#line 846
5474 ldv_s_rtc_device_driver_platform_driver = ldv_s_rtc_device_driver_platform_driver + 1;
5475 } else {
5476
5477 }
5478#line 852
5479 goto ldv_21384;
5480 case_11: ;
5481#line 856
5482 if (ldv_s_rtc_device_driver_platform_driver == 1) {
5483 {
5484#line 867
5485 rtc_remove(var_group2);
5486#line 868
5487 ldv_s_rtc_device_driver_platform_driver = 0;
5488 }
5489 } else {
5490
5491 }
5492#line 874
5493 goto ldv_21384;
5494 switch_default: ;
5495#line 875
5496 goto ldv_21384;
5497 } else {
5498 switch_break: ;
5499 }
5500 }
5501 }
5502 ldv_21384: ;
5503 ldv_21399:
5504 {
5505#line 602
5506 tmp___0 = __VERIFIER_nondet_int();
5507 }
5508#line 602
5509 if (tmp___0 != 0) {
5510#line 604
5511 goto ldv_21398;
5512 } else
5513#line 602
5514 if (ldv_s_rtc_device_driver_platform_driver != 0) {
5515#line 604
5516 goto ldv_21398;
5517 } else {
5518#line 606
5519 goto ldv_21400;
5520 }
5521 ldv_21400: ;
5522 ldv_module_exit: ;
5523 {
5524#line 884
5525 ldv_check_final_state();
5526 }
5527#line 887
5528 return;
5529}
5530}
5531#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
5532void ldv_blast_assert(void)
5533{
5534
5535 {
5536 ERROR: ;
5537#line 6
5538 goto ERROR;
5539}
5540}
5541#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
5542extern int __VERIFIER_nondet_int(void) ;
5543#line 908 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5544int ldv_spin = 0;
5545#line 912 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5546void ldv_check_alloc_flags(gfp_t flags )
5547{
5548
5549 {
5550#line 915
5551 if (ldv_spin != 0) {
5552#line 915
5553 if (flags != 32U) {
5554 {
5555#line 915
5556 ldv_blast_assert();
5557 }
5558 } else {
5559
5560 }
5561 } else {
5562
5563 }
5564#line 918
5565 return;
5566}
5567}
5568#line 918
5569extern struct page *ldv_some_page(void) ;
5570#line 921 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5571struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
5572{ struct page *tmp ;
5573
5574 {
5575#line 924
5576 if (ldv_spin != 0) {
5577#line 924
5578 if (flags != 32U) {
5579 {
5580#line 924
5581 ldv_blast_assert();
5582 }
5583 } else {
5584
5585 }
5586 } else {
5587
5588 }
5589 {
5590#line 926
5591 tmp = ldv_some_page();
5592 }
5593#line 926
5594 return (tmp);
5595}
5596}
5597#line 930 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5598void ldv_check_alloc_nonatomic(void)
5599{
5600
5601 {
5602#line 933
5603 if (ldv_spin != 0) {
5604 {
5605#line 933
5606 ldv_blast_assert();
5607 }
5608 } else {
5609
5610 }
5611#line 936
5612 return;
5613}
5614}
5615#line 937 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5616void ldv_spin_lock(void)
5617{
5618
5619 {
5620#line 940
5621 ldv_spin = 1;
5622#line 941
5623 return;
5624}
5625}
5626#line 944 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5627void ldv_spin_unlock(void)
5628{
5629
5630 {
5631#line 947
5632 ldv_spin = 0;
5633#line 948
5634 return;
5635}
5636}
5637#line 951 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5638int ldv_spin_trylock(void)
5639{ int is_lock ;
5640
5641 {
5642 {
5643#line 956
5644 is_lock = __VERIFIER_nondet_int();
5645 }
5646#line 958
5647 if (is_lock != 0) {
5648#line 961
5649 return (0);
5650 } else {
5651#line 966
5652 ldv_spin = 1;
5653#line 968
5654 return (1);
5655 }
5656}
5657}
5658#line 1135 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5659void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
5660{
5661
5662 {
5663 {
5664#line 1141
5665 ldv_check_alloc_flags(ldv_func_arg2);
5666#line 1143
5667 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
5668 }
5669#line 1144
5670 return ((void *)0);
5671}
5672}
5673#line 1146 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/2673/dscv_tempdir/dscv/ri/43_1a/drivers/rtc/rtc-v3020.c.p"
5674__inline static void *kzalloc(size_t size , gfp_t flags )
5675{ void *tmp ;
5676
5677 {
5678 {
5679#line 1152
5680 ldv_check_alloc_flags(flags);
5681#line 1153
5682 tmp = __VERIFIER_nondet_pointer();
5683 }
5684#line 1153
5685 return (tmp);
5686}
5687}