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