1
2
3
4#line 23 "include/asm-generic/int-ll64.h"
5typedef unsigned short __u16;
6#line 26 "include/asm-generic/int-ll64.h"
7typedef unsigned int __u32;
8#line 30 "include/asm-generic/int-ll64.h"
9typedef unsigned long long __u64;
10#line 43 "include/asm-generic/int-ll64.h"
11typedef unsigned char u8;
12#line 46 "include/asm-generic/int-ll64.h"
13typedef unsigned short u16;
14#line 49 "include/asm-generic/int-ll64.h"
15typedef unsigned int u32;
16#line 51 "include/asm-generic/int-ll64.h"
17typedef long long s64;
18#line 52 "include/asm-generic/int-ll64.h"
19typedef unsigned long long u64;
20#line 14 "include/asm-generic/posix_types.h"
21typedef long __kernel_long_t;
22#line 15 "include/asm-generic/posix_types.h"
23typedef unsigned long __kernel_ulong_t;
24#line 75 "include/asm-generic/posix_types.h"
25typedef __kernel_ulong_t __kernel_size_t;
26#line 76 "include/asm-generic/posix_types.h"
27typedef __kernel_long_t __kernel_ssize_t;
28#line 27 "include/linux/types.h"
29typedef unsigned short umode_t;
30#line 63 "include/linux/types.h"
31typedef __kernel_size_t size_t;
32#line 68 "include/linux/types.h"
33typedef __kernel_ssize_t ssize_t;
34#line 116 "include/linux/types.h"
35typedef __u16 uint16_t;
36#line 117 "include/linux/types.h"
37typedef __u32 uint32_t;
38#line 120 "include/linux/types.h"
39typedef __u64 uint64_t;
40#line 202 "include/linux/types.h"
41typedef unsigned int gfp_t;
42#line 221 "include/linux/types.h"
43struct __anonstruct_atomic_t_6 {
44 int counter ;
45};
46#line 221 "include/linux/types.h"
47typedef struct __anonstruct_atomic_t_6 atomic_t;
48#line 226 "include/linux/types.h"
49struct __anonstruct_atomic64_t_7 {
50 long counter ;
51};
52#line 226 "include/linux/types.h"
53typedef struct __anonstruct_atomic64_t_7 atomic64_t;
54#line 227 "include/linux/types.h"
55struct list_head {
56 struct list_head *next ;
57 struct list_head *prev ;
58};
59#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
60struct page;
61#line 58
62struct page;
63#line 26 "include/asm-generic/getorder.h"
64struct task_struct;
65#line 26
66struct task_struct;
67#line 339 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
68struct cpumask;
69#line 339
70struct cpumask;
71#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
72struct arch_spinlock;
73#line 327
74struct arch_spinlock;
75#line 89 "include/linux/bug.h"
76struct cpumask {
77 unsigned long bits[64U] ;
78};
79#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
80struct kmem_cache;
81#line 23 "include/asm-generic/atomic-long.h"
82typedef atomic64_t atomic_long_t;
83#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
84typedef u16 __ticket_t;
85#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
86typedef u32 __ticketpair_t;
87#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
88struct __raw_tickets {
89 __ticket_t head ;
90 __ticket_t tail ;
91};
92#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
93union __anonunion_ldv_5907_29 {
94 __ticketpair_t head_tail ;
95 struct __raw_tickets tickets ;
96};
97#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
98struct arch_spinlock {
99 union __anonunion_ldv_5907_29 ldv_5907 ;
100};
101#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
102typedef struct arch_spinlock arch_spinlock_t;
103#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
104struct lockdep_map;
105#line 34
106struct lockdep_map;
107#line 55 "include/linux/debug_locks.h"
108struct stack_trace {
109 unsigned int nr_entries ;
110 unsigned int max_entries ;
111 unsigned long *entries ;
112 int skip ;
113};
114#line 26 "include/linux/stacktrace.h"
115struct lockdep_subclass_key {
116 char __one_byte ;
117};
118#line 53 "include/linux/lockdep.h"
119struct lock_class_key {
120 struct lockdep_subclass_key subkeys[8U] ;
121};
122#line 59 "include/linux/lockdep.h"
123struct lock_class {
124 struct list_head hash_entry ;
125 struct list_head lock_entry ;
126 struct lockdep_subclass_key *key ;
127 unsigned int subclass ;
128 unsigned int dep_gen_id ;
129 unsigned long usage_mask ;
130 struct stack_trace usage_traces[13U] ;
131 struct list_head locks_after ;
132 struct list_head locks_before ;
133 unsigned int version ;
134 unsigned long ops ;
135 char const *name ;
136 int name_version ;
137 unsigned long contention_point[4U] ;
138 unsigned long contending_point[4U] ;
139};
140#line 144 "include/linux/lockdep.h"
141struct lockdep_map {
142 struct lock_class_key *key ;
143 struct lock_class *class_cache[2U] ;
144 char const *name ;
145 int cpu ;
146 unsigned long ip ;
147};
148#line 556 "include/linux/lockdep.h"
149struct raw_spinlock {
150 arch_spinlock_t raw_lock ;
151 unsigned int magic ;
152 unsigned int owner_cpu ;
153 void *owner ;
154 struct lockdep_map dep_map ;
155};
156#line 33 "include/linux/spinlock_types.h"
157struct __anonstruct_ldv_6122_33 {
158 u8 __padding[24U] ;
159 struct lockdep_map dep_map ;
160};
161#line 33 "include/linux/spinlock_types.h"
162union __anonunion_ldv_6123_32 {
163 struct raw_spinlock rlock ;
164 struct __anonstruct_ldv_6122_33 ldv_6122 ;
165};
166#line 33 "include/linux/spinlock_types.h"
167struct spinlock {
168 union __anonunion_ldv_6123_32 ldv_6123 ;
169};
170#line 76 "include/linux/spinlock_types.h"
171typedef struct spinlock spinlock_t;
172#line 312 "include/linux/jiffies.h"
173union ktime {
174 s64 tv64 ;
175};
176#line 59 "include/linux/ktime.h"
177typedef union ktime ktime_t;
178#line 445 "include/linux/elf.h"
179struct sock;
180#line 445
181struct sock;
182#line 446
183struct kobject;
184#line 446
185struct kobject;
186#line 447
187enum kobj_ns_type {
188 KOBJ_NS_TYPE_NONE = 0,
189 KOBJ_NS_TYPE_NET = 1,
190 KOBJ_NS_TYPES = 2
191} ;
192#line 453 "include/linux/elf.h"
193struct kobj_ns_type_operations {
194 enum kobj_ns_type type ;
195 void *(*grab_current_ns)(void) ;
196 void const *(*netlink_ns)(struct sock * ) ;
197 void const *(*initial_ns)(void) ;
198 void (*drop_ns)(void * ) ;
199};
200#line 57 "include/linux/kobject_ns.h"
201struct attribute {
202 char const *name ;
203 umode_t mode ;
204 struct lock_class_key *key ;
205 struct lock_class_key skey ;
206};
207#line 98 "include/linux/sysfs.h"
208struct sysfs_ops {
209 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
210 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
211 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
212};
213#line 117
214struct sysfs_dirent;
215#line 117
216struct sysfs_dirent;
217#line 182 "include/linux/sysfs.h"
218struct kref {
219 atomic_t refcount ;
220};
221#line 49 "include/linux/kobject.h"
222struct kset;
223#line 49
224struct kobj_type;
225#line 49 "include/linux/kobject.h"
226struct kobject {
227 char const *name ;
228 struct list_head entry ;
229 struct kobject *parent ;
230 struct kset *kset ;
231 struct kobj_type *ktype ;
232 struct sysfs_dirent *sd ;
233 struct kref kref ;
234 unsigned char state_initialized : 1 ;
235 unsigned char state_in_sysfs : 1 ;
236 unsigned char state_add_uevent_sent : 1 ;
237 unsigned char state_remove_uevent_sent : 1 ;
238 unsigned char uevent_suppress : 1 ;
239};
240#line 107 "include/linux/kobject.h"
241struct kobj_type {
242 void (*release)(struct kobject * ) ;
243 struct sysfs_ops const *sysfs_ops ;
244 struct attribute **default_attrs ;
245 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
246 void const *(*namespace)(struct kobject * ) ;
247};
248#line 115 "include/linux/kobject.h"
249struct kobj_uevent_env {
250 char *envp[32U] ;
251 int envp_idx ;
252 char buf[2048U] ;
253 int buflen ;
254};
255#line 122 "include/linux/kobject.h"
256struct kset_uevent_ops {
257 int (* const filter)(struct kset * , struct kobject * ) ;
258 char const *(* const name)(struct kset * , struct kobject * ) ;
259 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
260};
261#line 139 "include/linux/kobject.h"
262struct kset {
263 struct list_head list ;
264 spinlock_t list_lock ;
265 struct kobject kobj ;
266 struct kset_uevent_ops const *uevent_ops ;
267};
268#line 88 "include/linux/kmemleak.h"
269struct kmem_cache_cpu {
270 void **freelist ;
271 unsigned long tid ;
272 struct page *page ;
273 struct page *partial ;
274 int node ;
275 unsigned int stat[26U] ;
276};
277#line 55 "include/linux/slub_def.h"
278struct kmem_cache_node {
279 spinlock_t list_lock ;
280 unsigned long nr_partial ;
281 struct list_head partial ;
282 atomic_long_t nr_slabs ;
283 atomic_long_t total_objects ;
284 struct list_head full ;
285};
286#line 66 "include/linux/slub_def.h"
287struct kmem_cache_order_objects {
288 unsigned long x ;
289};
290#line 76 "include/linux/slub_def.h"
291struct kmem_cache {
292 struct kmem_cache_cpu *cpu_slab ;
293 unsigned long flags ;
294 unsigned long min_partial ;
295 int size ;
296 int objsize ;
297 int offset ;
298 int cpu_partial ;
299 struct kmem_cache_order_objects oo ;
300 struct kmem_cache_order_objects max ;
301 struct kmem_cache_order_objects min ;
302 gfp_t allocflags ;
303 int refcount ;
304 void (*ctor)(void * ) ;
305 int inuse ;
306 int align ;
307 int reserved ;
308 char const *name ;
309 struct list_head list ;
310 struct kobject kobj ;
311 int remote_node_defrag_ratio ;
312 struct kmem_cache_node *node[1024U] ;
313};
314#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
315enum irqreturn {
316 IRQ_NONE = 0,
317 IRQ_HANDLED = 1,
318 IRQ_WAKE_THREAD = 2
319} ;
320#line 16 "include/linux/irqreturn.h"
321typedef enum irqreturn irqreturn_t;
322#line 348 "include/linux/irq.h"
323struct proc_dir_entry;
324#line 348
325struct proc_dir_entry;
326#line 350
327struct irqaction;
328#line 257 "include/linux/hrtimer.h"
329struct clock_event_device;
330#line 257
331struct clock_event_device;
332#line 92 "include/linux/interrupt.h"
333struct irqaction {
334 irqreturn_t (*handler)(int , void * ) ;
335 unsigned long flags ;
336 void *dev_id ;
337 void *percpu_dev_id ;
338 struct irqaction *next ;
339 int irq ;
340 irqreturn_t (*thread_fn)(int , void * ) ;
341 struct task_struct *thread ;
342 unsigned long thread_flags ;
343 unsigned long thread_mask ;
344 char const *name ;
345 struct proc_dir_entry *dir ;
346};
347#line 180 "include/linux/cs5535.h"
348struct cs5535_mfgpt_timer;
349#line 180
350struct cs5535_mfgpt_timer;
351#line 350 "include/linux/clocksource.h"
352enum clock_event_mode {
353 CLOCK_EVT_MODE_UNUSED = 0,
354 CLOCK_EVT_MODE_SHUTDOWN = 1,
355 CLOCK_EVT_MODE_PERIODIC = 2,
356 CLOCK_EVT_MODE_ONESHOT = 3,
357 CLOCK_EVT_MODE_RESUME = 4
358} ;
359#line 371 "include/linux/clocksource.h"
360struct clock_event_device {
361 void (*event_handler)(struct clock_event_device * ) ;
362 int (*set_next_event)(unsigned long , struct clock_event_device * ) ;
363 int (*set_next_ktime)(ktime_t , struct clock_event_device * ) ;
364 ktime_t next_event ;
365 u64 max_delta_ns ;
366 u64 min_delta_ns ;
367 u32 mult ;
368 u32 shift ;
369 enum clock_event_mode mode ;
370 unsigned int features ;
371 unsigned long retries ;
372 void (*broadcast)(struct cpumask const * ) ;
373 void (*set_mode)(enum clock_event_mode , struct clock_event_device * ) ;
374 unsigned long min_delta_ticks ;
375 unsigned long max_delta_ticks ;
376 char const *name ;
377 int rating ;
378 int irq ;
379 struct cpumask const *cpumask ;
380 struct list_head list ;
381};
382#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
383void ldv_spin_lock(void) ;
384#line 3
385void ldv_spin_unlock(void) ;
386#line 4
387int ldv_spin_trylock(void) ;
388#line 101 "include/linux/printk.h"
389extern int printk(char const * , ...) ;
390#line 220 "include/linux/slub_def.h"
391extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
392#line 223
393void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
394#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
395void ldv_check_alloc_flags(gfp_t flags ) ;
396#line 12
397void ldv_check_alloc_nonatomic(void) ;
398#line 14
399struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
400#line 382 "include/linux/irq.h"
401extern int setup_irq(unsigned int , struct irqaction * ) ;
402#line 213 "include/linux/cs5535.h"
403extern uint16_t cs5535_mfgpt_read(struct cs5535_mfgpt_timer * , uint16_t ) ;
404#line 215
405extern void cs5535_mfgpt_write(struct cs5535_mfgpt_timer * , uint16_t , uint16_t ) ;
406#line 220
407extern int cs5535_mfgpt_set_irq(struct cs5535_mfgpt_timer * , int , int * , int ) ;
408#line 222
409extern struct cs5535_mfgpt_timer *cs5535_mfgpt_alloc_timer(int , int ) ;
410#line 224
411extern void cs5535_mfgpt_free_timer(struct cs5535_mfgpt_timer * ) ;
412#line 226 "include/linux/cs5535.h"
413__inline static int cs5535_mfgpt_setup_irq(struct cs5535_mfgpt_timer *timer , int cmp ,
414 int *irq )
415{ int tmp ;
416
417 {
418 {
419#line 229
420 tmp = cs5535_mfgpt_set_irq(timer, cmp, irq, 1);
421 }
422#line 229
423 return (tmp);
424}
425}
426#line 232 "include/linux/cs5535.h"
427__inline static int cs5535_mfgpt_release_irq(struct cs5535_mfgpt_timer *timer , int cmp ,
428 int *irq )
429{ int tmp ;
430
431 {
432 {
433#line 235
434 tmp = cs5535_mfgpt_set_irq(timer, cmp, irq, 0);
435 }
436#line 235
437 return (tmp);
438}
439}
440#line 121 "include/linux/clockchips.h"
441__inline static unsigned long div_sc(unsigned long ticks , unsigned long nsec , int shift )
442{ uint64_t tmp ;
443 uint32_t __base ;
444 uint32_t __rem ;
445 unsigned long long __cil_tmp7 ;
446 uint64_t __cil_tmp8 ;
447 unsigned long long __cil_tmp9 ;
448 uint64_t __cil_tmp10 ;
449
450 {
451#line 124
452 __cil_tmp7 = (unsigned long long )ticks;
453#line 124
454 tmp = __cil_tmp7 << shift;
455#line 126
456 __base = (uint32_t )nsec;
457#line 126
458 __cil_tmp8 = (uint64_t )__base;
459#line 126
460 __cil_tmp9 = tmp % __cil_tmp8;
461#line 126
462 __rem = (uint32_t )__cil_tmp9;
463#line 126
464 __cil_tmp10 = (uint64_t )__base;
465#line 126
466 tmp = tmp / __cil_tmp10;
467#line 127
468 return ((unsigned long )tmp);
469}
470}
471#line 131
472extern u64 clockevent_delta2ns(unsigned long , struct clock_event_device * ) ;
473#line 133
474extern void clockevents_register_device(struct clock_event_device * ) ;
475#line 39 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
476static int timer_irq ;
477#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
478static unsigned int cs5535_tick_mode = 1U;
479#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
480static struct cs5535_mfgpt_timer *cs5535_event_clock ;
481#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
482static void disable_timer(struct cs5535_mfgpt_timer *timer )
483{ uint16_t __cil_tmp2 ;
484 uint16_t __cil_tmp3 ;
485
486 {
487 {
488#line 81
489 __cil_tmp2 = (uint16_t )6;
490#line 81
491 __cil_tmp3 = (uint16_t )32767;
492#line 81
493 cs5535_mfgpt_write(timer, __cil_tmp2, __cil_tmp3);
494 }
495#line 82
496 return;
497}
498}
499#line 86 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
500static void start_timer(struct cs5535_mfgpt_timer *timer , uint16_t delta )
501{ uint16_t __cil_tmp3 ;
502 int __cil_tmp4 ;
503 uint16_t __cil_tmp5 ;
504 uint16_t __cil_tmp6 ;
505 uint16_t __cil_tmp7 ;
506 uint16_t __cil_tmp8 ;
507 uint16_t __cil_tmp9 ;
508
509 {
510 {
511#line 88
512 __cil_tmp3 = (uint16_t )2;
513#line 88
514 __cil_tmp4 = (int )delta;
515#line 88
516 __cil_tmp5 = (uint16_t )__cil_tmp4;
517#line 88
518 cs5535_mfgpt_write(timer, __cil_tmp3, __cil_tmp5);
519#line 89
520 __cil_tmp6 = (uint16_t )4;
521#line 89
522 __cil_tmp7 = (uint16_t )0;
523#line 89
524 cs5535_mfgpt_write(timer, __cil_tmp6, __cil_tmp7);
525#line 91
526 __cil_tmp8 = (uint16_t )6;
527#line 91
528 __cil_tmp9 = (uint16_t )49152;
529#line 91
530 cs5535_mfgpt_write(timer, __cil_tmp8, __cil_tmp9);
531 }
532#line 92
533 return;
534}
535}
536#line 95 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
537static void mfgpt_set_mode(enum clock_event_mode mode , struct clock_event_device *evt )
538{ unsigned int __cil_tmp3 ;
539 uint16_t __cil_tmp4 ;
540
541 {
542 {
543#line 98
544 disable_timer(cs5535_event_clock);
545 }
546 {
547#line 100
548 __cil_tmp3 = (unsigned int )mode;
549#line 100
550 if (__cil_tmp3 == 2U) {
551 {
552#line 101
553 __cil_tmp4 = (uint16_t )8;
554#line 101
555 start_timer(cs5535_event_clock, __cil_tmp4);
556 }
557 } else {
558
559 }
560 }
561#line 103
562 cs5535_tick_mode = (unsigned int )mode;
563#line 104
564 return;
565}
566}
567#line 106 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
568static int mfgpt_next_event(unsigned long delta , struct clock_event_device *evt )
569{ uint16_t __cil_tmp3 ;
570 int __cil_tmp4 ;
571 uint16_t __cil_tmp5 ;
572
573 {
574 {
575#line 108
576 __cil_tmp3 = (uint16_t )delta;
577#line 108
578 __cil_tmp4 = (int )__cil_tmp3;
579#line 108
580 __cil_tmp5 = (uint16_t )__cil_tmp4;
581#line 108
582 start_timer(cs5535_event_clock, __cil_tmp5);
583 }
584#line 109
585 return (0);
586}
587}
588#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
589static struct clock_event_device cs5535_clockevent =
590#line 112
591 {(void (*)(struct clock_event_device * ))0, & mfgpt_next_event, (int (*)(ktime_t ,
592 struct clock_event_device * ))0,
593 {0LL}, 0ULL, 0ULL, 0U, 32U, 0, 3U, 0UL, (void (*)(struct cpumask const * ))0,
594 & mfgpt_set_mode, 0UL, 0UL, "cs5535-clockevt", 250, 0, (struct cpumask const *)0,
595 {(struct list_head *)0, (struct list_head *)0}};
596#line 121 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
597static irqreturn_t mfgpt_tick(int irq , void *dev_id )
598{ uint16_t val ;
599 uint16_t tmp ;
600 uint16_t __cil_tmp5 ;
601 int __cil_tmp6 ;
602 int __cil_tmp7 ;
603 uint16_t __cil_tmp8 ;
604 uint16_t __cil_tmp9 ;
605 uint16_t __cil_tmp10 ;
606 uint16_t __cil_tmp11 ;
607 struct clock_event_device *__cil_tmp12 ;
608 void (*__cil_tmp13)(struct clock_event_device * ) ;
609
610 {
611 {
612#line 123
613 __cil_tmp5 = (uint16_t )6;
614#line 123
615 tmp = cs5535_mfgpt_read(cs5535_event_clock, __cil_tmp5);
616#line 123
617 val = tmp;
618 }
619 {
620#line 126
621 __cil_tmp6 = (int )val;
622#line 126
623 __cil_tmp7 = __cil_tmp6 & 28672;
624#line 126
625 if (__cil_tmp7 == 0) {
626#line 127
627 return ((irqreturn_t )0);
628 } else {
629
630 }
631 }
632 {
633#line 130
634 disable_timer(cs5535_event_clock);
635 }
636#line 132
637 if (cs5535_tick_mode == 1U) {
638#line 133
639 return ((irqreturn_t )1);
640 } else {
641
642 }
643 {
644#line 136
645 __cil_tmp8 = (uint16_t )4;
646#line 136
647 __cil_tmp9 = (uint16_t )0;
648#line 136
649 cs5535_mfgpt_write(cs5535_event_clock, __cil_tmp8, __cil_tmp9);
650 }
651#line 140
652 if (cs5535_tick_mode == 2U) {
653 {
654#line 141
655 __cil_tmp10 = (uint16_t )6;
656#line 141
657 __cil_tmp11 = (uint16_t )49152;
658#line 141
659 cs5535_mfgpt_write(cs5535_event_clock, __cil_tmp10, __cil_tmp11);
660 }
661 } else {
662
663 }
664 {
665#line 144
666 __cil_tmp12 = & cs5535_clockevent;
667#line 144
668 __cil_tmp13 = *((void (**)(struct clock_event_device * ))__cil_tmp12);
669#line 144
670 (*__cil_tmp13)(& cs5535_clockevent);
671 }
672#line 145
673 return ((irqreturn_t )1);
674}
675}
676#line 148 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
677static struct irqaction mfgptirq =
678#line 148
679 {& mfgpt_tick, 84640UL, (void *)0, (void *)0, (struct irqaction *)0, 0, (irqreturn_t (*)(int ,
680 void * ))0,
681 (struct task_struct *)0, 0UL, 0UL, "cs5535-clockevt", (struct proc_dir_entry *)0};
682#line 154 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
683static int cs5535_mfgpt_init(void)
684{ struct cs5535_mfgpt_timer *timer ;
685 int ret ;
686 uint16_t val ;
687 int tmp ;
688 unsigned long tmp___0 ;
689 struct cs5535_mfgpt_timer *__cil_tmp6 ;
690 unsigned long __cil_tmp7 ;
691 unsigned long __cil_tmp8 ;
692 int *__cil_tmp9 ;
693 int __cil_tmp10 ;
694 int *__cil_tmp11 ;
695 int __cil_tmp12 ;
696 unsigned int __cil_tmp13 ;
697 uint16_t __cil_tmp14 ;
698 int __cil_tmp15 ;
699 uint16_t __cil_tmp16 ;
700 unsigned long __cil_tmp17 ;
701 u32 __cil_tmp18 ;
702 int __cil_tmp19 ;
703 unsigned long __cil_tmp20 ;
704 unsigned long __cil_tmp21 ;
705 unsigned long __cil_tmp22 ;
706 int *__cil_tmp23 ;
707 int __cil_tmp24 ;
708
709 {
710 {
711#line 160
712 timer = cs5535_mfgpt_alloc_timer(-1, 1);
713 }
714 {
715#line 161
716 __cil_tmp6 = (struct cs5535_mfgpt_timer *)0;
717#line 161
718 __cil_tmp7 = (unsigned long )__cil_tmp6;
719#line 161
720 __cil_tmp8 = (unsigned long )timer;
721#line 161
722 if (__cil_tmp8 == __cil_tmp7) {
723 {
724#line 162
725 printk("<3>cs5535-clockevt: Could not allocate MFPGT timer\n");
726 }
727#line 163
728 return (-19);
729 } else {
730
731 }
732 }
733 {
734#line 165
735 cs5535_event_clock = timer;
736#line 168
737 tmp = cs5535_mfgpt_setup_irq(timer, 1, & timer_irq);
738 }
739#line 168
740 if (tmp != 0) {
741 {
742#line 169
743 __cil_tmp9 = & timer_irq;
744#line 169
745 __cil_tmp10 = *__cil_tmp9;
746#line 169
747 printk("<3>cs5535-clockevt: Could not set up IRQ %d\n", __cil_tmp10);
748 }
749#line 171
750 goto err_timer;
751 } else {
752
753 }
754 {
755#line 175
756 __cil_tmp11 = & timer_irq;
757#line 175
758 __cil_tmp12 = *__cil_tmp11;
759#line 175
760 __cil_tmp13 = (unsigned int )__cil_tmp12;
761#line 175
762 ret = setup_irq(__cil_tmp13, & mfgptirq);
763 }
764#line 176
765 if (ret != 0) {
766 {
767#line 177
768 printk("<3>cs5535-clockevt: Unable to set up the interrupt.\n");
769 }
770#line 178
771 goto err_irq;
772 } else {
773
774 }
775 {
776#line 182
777 val = (uint16_t )772U;
778#line 184
779 __cil_tmp14 = (uint16_t )6;
780#line 184
781 __cil_tmp15 = (int )val;
782#line 184
783 __cil_tmp16 = (uint16_t )__cil_tmp15;
784#line 184
785 cs5535_mfgpt_write(cs5535_event_clock, __cil_tmp14, __cil_tmp16);
786#line 187
787 __cil_tmp17 = (unsigned long )(& cs5535_clockevent) + 52;
788#line 187
789 __cil_tmp18 = *((u32 *)__cil_tmp17);
790#line 187
791 __cil_tmp19 = (int )__cil_tmp18;
792#line 187
793 tmp___0 = div_sc(2048UL, 1000000000UL, __cil_tmp19);
794#line 187
795 __cil_tmp20 = (unsigned long )(& cs5535_clockevent) + 48;
796#line 187
797 *((u32 *)__cil_tmp20) = (u32 )tmp___0;
798#line 189
799 __cil_tmp21 = (unsigned long )(& cs5535_clockevent) + 40;
800#line 189
801 *((u64 *)__cil_tmp21) = clockevent_delta2ns(15UL, & cs5535_clockevent);
802#line 191
803 __cil_tmp22 = (unsigned long )(& cs5535_clockevent) + 32;
804#line 191
805 *((u64 *)__cil_tmp22) = clockevent_delta2ns(65534UL, & cs5535_clockevent);
806#line 194
807 __cil_tmp23 = & timer_irq;
808#line 194
809 __cil_tmp24 = *__cil_tmp23;
810#line 194
811 printk("<6>cs5535-clockevt: Registering MFGPT timer as a clock event, using IRQ %d\n",
812 __cil_tmp24);
813#line 197
814 clockevents_register_device(& cs5535_clockevent);
815 }
816#line 199
817 return (0);
818 err_irq:
819 {
820#line 202
821 cs5535_mfgpt_release_irq(cs5535_event_clock, 1, & timer_irq);
822 }
823 err_timer:
824 {
825#line 204
826 cs5535_mfgpt_free_timer(cs5535_event_clock);
827#line 205
828 printk("<3>cs5535-clockevt: Unable to set up the MFGPT clock source\n");
829 }
830#line 206
831 return (-5);
832}
833}
834#line 231
835extern void ldv_check_final_state(void) ;
836#line 237
837extern void ldv_initialize(void) ;
838#line 240
839extern int __VERIFIER_nondet_int(void) ;
840#line 243 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
841int LDV_IN_INTERRUPT ;
842#line 246 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
843void main(void)
844{ enum clock_event_mode var_mfgpt_set_mode_2_p0 ;
845 struct clock_event_device *var_group1 ;
846 unsigned long var_mfgpt_next_event_3_p0 ;
847 int var_mfgpt_tick_4_p0 ;
848 void *var_mfgpt_tick_4_p1 ;
849 int tmp ;
850 int tmp___0 ;
851 int tmp___1 ;
852
853 {
854 {
855#line 306
856 LDV_IN_INTERRUPT = 1;
857#line 315
858 ldv_initialize();
859#line 327
860 tmp = cs5535_mfgpt_init();
861 }
862#line 327
863 if (tmp != 0) {
864#line 328
865 goto ldv_final;
866 } else {
867
868 }
869#line 336
870 goto ldv_16170;
871 ldv_16169:
872 {
873#line 339
874 tmp___0 = __VERIFIER_nondet_int();
875 }
876#line 341
877 if (tmp___0 == 0) {
878#line 341
879 goto case_0;
880 } else
881#line 363
882 if (tmp___0 == 1) {
883#line 363
884 goto case_1;
885 } else
886#line 385
887 if (tmp___0 == 2) {
888#line 385
889 goto case_2;
890 } else
891#line 407
892 if (tmp___0 == 3) {
893#line 407
894 goto case_3;
895 } else {
896 {
897#line 429
898 goto switch_default;
899#line 339
900 if (0) {
901 case_0:
902 {
903#line 355
904 mfgpt_set_mode(var_mfgpt_set_mode_2_p0, var_group1);
905 }
906#line 362
907 goto ldv_16164;
908 case_1:
909 {
910#line 377
911 mfgpt_next_event(var_mfgpt_next_event_3_p0, var_group1);
912 }
913#line 384
914 goto ldv_16164;
915 case_2:
916 {
917#line 399
918 mfgpt_tick(var_mfgpt_tick_4_p0, var_mfgpt_tick_4_p1);
919 }
920#line 406
921 goto ldv_16164;
922 case_3:
923 {
924#line 410
925 LDV_IN_INTERRUPT = 2;
926#line 421
927 mfgpt_tick(var_mfgpt_tick_4_p0, var_mfgpt_tick_4_p1);
928#line 422
929 LDV_IN_INTERRUPT = 1;
930 }
931#line 428
932 goto ldv_16164;
933 switch_default: ;
934#line 429
935 goto ldv_16164;
936 } else {
937 switch_break: ;
938 }
939 }
940 }
941 ldv_16164: ;
942 ldv_16170:
943 {
944#line 336
945 tmp___1 = __VERIFIER_nondet_int();
946 }
947#line 336
948 if (tmp___1 != 0) {
949#line 337
950 goto ldv_16169;
951 } else {
952#line 339
953 goto ldv_16171;
954 }
955 ldv_16171: ;
956
957 ldv_final:
958 {
959#line 438
960 ldv_check_final_state();
961 }
962#line 441
963 return;
964}
965}
966#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
967void ldv_blast_assert(void)
968{
969
970 {
971 ERROR: ;
972#line 6
973 goto ERROR;
974}
975}
976#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
977extern int __VERIFIER_nondet_int(void) ;
978#line 462 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
979int ldv_spin = 0;
980#line 466 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
981void ldv_check_alloc_flags(gfp_t flags )
982{
983
984 {
985#line 469
986 if (ldv_spin != 0) {
987#line 469
988 if (flags != 32U) {
989 {
990#line 469
991 ldv_blast_assert();
992 }
993 } else {
994
995 }
996 } else {
997
998 }
999#line 472
1000 return;
1001}
1002}
1003#line 472
1004extern struct page *ldv_some_page(void) ;
1005#line 475 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
1006struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1007{ struct page *tmp ;
1008
1009 {
1010#line 478
1011 if (ldv_spin != 0) {
1012#line 478
1013 if (flags != 32U) {
1014 {
1015#line 478
1016 ldv_blast_assert();
1017 }
1018 } else {
1019
1020 }
1021 } else {
1022
1023 }
1024 {
1025#line 480
1026 tmp = ldv_some_page();
1027 }
1028#line 480
1029 return (tmp);
1030}
1031}
1032#line 484 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
1033void ldv_check_alloc_nonatomic(void)
1034{
1035
1036 {
1037#line 487
1038 if (ldv_spin != 0) {
1039 {
1040#line 487
1041 ldv_blast_assert();
1042 }
1043 } else {
1044
1045 }
1046#line 490
1047 return;
1048}
1049}
1050#line 491 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
1051void ldv_spin_lock(void)
1052{
1053
1054 {
1055#line 494
1056 ldv_spin = 1;
1057#line 495
1058 return;
1059}
1060}
1061#line 498 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
1062void ldv_spin_unlock(void)
1063{
1064
1065 {
1066#line 501
1067 ldv_spin = 0;
1068#line 502
1069 return;
1070}
1071}
1072#line 505 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
1073int ldv_spin_trylock(void)
1074{ int is_lock ;
1075
1076 {
1077 {
1078#line 510
1079 is_lock = __VERIFIER_nondet_int();
1080 }
1081#line 512
1082 if (is_lock != 0) {
1083#line 515
1084 return (0);
1085 } else {
1086#line 520
1087 ldv_spin = 1;
1088#line 522
1089 return (1);
1090 }
1091}
1092}
1093#line 689 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11167/dscv_tempdir/dscv/ri/43_1a/drivers/clocksource/cs5535-clockevt.c.p"
1094void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1095{
1096
1097 {
1098 {
1099#line 695
1100 ldv_check_alloc_flags(ldv_func_arg2);
1101#line 697
1102 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1103 }
1104#line 698
1105 return ((void *)0);
1106}
1107}