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