1
2
3
4#line 45 "include/asm-generic/int-ll64.h"
5typedef short s16;
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 219 "include/linux/types.h"
11struct __anonstruct_atomic_t_7 {
12 int counter ;
13};
14#line 219 "include/linux/types.h"
15typedef struct __anonstruct_atomic_t_7 atomic_t;
16#line 229 "include/linux/types.h"
17struct list_head {
18 struct list_head *next ;
19 struct list_head *prev ;
20};
21#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
22struct task_struct;
23#line 20
24struct task_struct;
25#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
26struct task_struct;
27#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
28struct task_struct;
29#line 329
30struct arch_spinlock;
31#line 329
32struct arch_spinlock;
33#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
34struct task_struct;
35#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
36struct task_struct;
37#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
38typedef u16 __ticket_t;
39#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
40typedef u32 __ticketpair_t;
41#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
42struct __raw_tickets {
43 __ticket_t head ;
44 __ticket_t tail ;
45};
46#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
47union __anonunion____missing_field_name_36 {
48 __ticketpair_t head_tail ;
49 struct __raw_tickets tickets ;
50};
51#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
52struct arch_spinlock {
53 union __anonunion____missing_field_name_36 __annonCompField17 ;
54};
55#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
56typedef struct arch_spinlock arch_spinlock_t;
57#line 12 "include/linux/lockdep.h"
58struct task_struct;
59#line 20 "include/linux/spinlock_types.h"
60struct raw_spinlock {
61 arch_spinlock_t raw_lock ;
62 unsigned int magic ;
63 unsigned int owner_cpu ;
64 void *owner ;
65};
66#line 64 "include/linux/spinlock_types.h"
67union __anonunion____missing_field_name_39 {
68 struct raw_spinlock rlock ;
69};
70#line 64 "include/linux/spinlock_types.h"
71struct spinlock {
72 union __anonunion____missing_field_name_39 __annonCompField19 ;
73};
74#line 64 "include/linux/spinlock_types.h"
75typedef struct spinlock spinlock_t;
76#line 55 "include/linux/wait.h"
77struct task_struct;
78#line 48 "include/linux/mutex.h"
79struct mutex {
80 atomic_t count ;
81 spinlock_t wait_lock ;
82 struct list_head wait_list ;
83 struct task_struct *owner ;
84 char const *name ;
85 void *magic ;
86};
87#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
88struct task_struct;
89#line 39 "include/linux/moduleparam.h"
90struct kernel_param;
91#line 39
92struct kernel_param;
93#line 41 "include/linux/moduleparam.h"
94struct kernel_param_ops {
95 int (*set)(char const *val , struct kernel_param const *kp ) ;
96 int (*get)(char *buffer , struct kernel_param const *kp ) ;
97 void (*free)(void *arg ) ;
98};
99#line 50
100struct kparam_string;
101#line 50
102struct kparam_array;
103#line 50 "include/linux/moduleparam.h"
104union __anonunion____missing_field_name_199 {
105 void *arg ;
106 struct kparam_string const *str ;
107 struct kparam_array const *arr ;
108};
109#line 50 "include/linux/moduleparam.h"
110struct kernel_param {
111 char const *name ;
112 struct kernel_param_ops const *ops ;
113 u16 perm ;
114 s16 level ;
115 union __anonunion____missing_field_name_199 __annonCompField32 ;
116};
117#line 63 "include/linux/moduleparam.h"
118struct kparam_string {
119 unsigned int maxlen ;
120 char *string ;
121};
122#line 69 "include/linux/moduleparam.h"
123struct kparam_array {
124 unsigned int max ;
125 unsigned int elemsize ;
126 unsigned int *num ;
127 struct kernel_param_ops const *ops ;
128 void *elem ;
129};
130#line 19 "include/linux/export.h"
131struct kernel_symbol {
132 unsigned long value ;
133 char const *name ;
134};
135#line 1 "<compiler builtins>"
136long __builtin_expect(long val , long res ) ;
137#line 100 "include/linux/printk.h"
138extern int ( printk)(char const *fmt , ...) ;
139#line 152 "include/linux/mutex.h"
140void mutex_lock(struct mutex *lock ) ;
141#line 153
142int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
143#line 154
144int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
145#line 168
146int mutex_trylock(struct mutex *lock ) ;
147#line 169
148void mutex_unlock(struct mutex *lock ) ;
149#line 170
150int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
151#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
152__inline static void outb(unsigned char value , int port ) __attribute__((__no_instrument_function__)) ;
153#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
154__inline static void outb(unsigned char value , int port )
155{
156
157 {
158#line 308
159 __asm__ volatile ("out"
160 "b"
161 " %"
162 "b"
163 "0, %w1": : "a" (value), "Nd" (port));
164#line 308
165 return;
166}
167}
168#line 308
169__inline static unsigned char inb(int port ) __attribute__((__no_instrument_function__)) ;
170#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
171__inline static unsigned char inb(int port )
172{ unsigned char value ;
173
174 {
175#line 308
176 __asm__ volatile ("in"
177 "b"
178 " %w1, %"
179 "b"
180 "0": "=a" (value): "Nd" (port));
181#line 308
182 return (value);
183}
184}
185#line 310
186__inline static void outl(unsigned int value , int port ) __attribute__((__no_instrument_function__)) ;
187#line 310 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
188__inline static void outl(unsigned int value , int port )
189{
190
191 {
192#line 310
193 __asm__ volatile ("out"
194 "l"
195 " %"
196 ""
197 "0, %w1": : "a" (value), "Nd" (port));
198#line 310
199 return;
200}
201}
202#line 310
203__inline static unsigned int inl(int port ) __attribute__((__no_instrument_function__)) ;
204#line 310 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
205__inline static unsigned int inl(int port )
206{ unsigned int value ;
207
208 {
209#line 310
210 __asm__ volatile ("in"
211 "l"
212 " %w1, %"
213 ""
214 "0": "=a" (value): "Nd" (port));
215#line 310
216 return (value);
217}
218}
219#line 356 "include/linux/moduleparam.h"
220extern struct kernel_param_ops param_ops_int ;
221#line 67 "include/linux/module.h"
222int init_module(void) ;
223#line 68
224void cleanup_module(void) ;
225#line 3 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/watchdog/iTCO_vendor.h"
226void iTCO_vendor_pre_start(unsigned long acpibase , unsigned int heartbeat ) ;
227#line 4
228void iTCO_vendor_pre_stop(unsigned long acpibase ) ;
229#line 5
230void iTCO_vendor_pre_keepalive(unsigned long acpibase , unsigned int heartbeat ) ;
231#line 6
232void iTCO_vendor_pre_set_heartbeat(unsigned int heartbeat ) ;
233#line 7
234int iTCO_vendor_check_noreboot_on(void) ;
235#line 52 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
236static int vendorsupport ;
237#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
238static char const __param_str_vendorsupport[14] =
239#line 53
240 { (char const )'v', (char const )'e', (char const )'n', (char const )'d',
241 (char const )'o', (char const )'r', (char const )'s', (char const )'u',
242 (char const )'p', (char const )'p', (char const )'o', (char const )'r',
243 (char const )'t', (char const )'\000'};
244#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
245static struct kernel_param const __param_vendorsupport __attribute__((__used__,
246__unused__, __section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_vendorsupport, (struct kernel_param_ops const *)(& param_ops_int),
247 (u16 )0, (s16 )0, {(void *)(& vendorsupport)}};
248#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
249static char const __mod_vendorsupporttype53[27] __attribute__((__used__, __unused__,
250__section__(".modinfo"), __aligned__(1))) =
251#line 53
252 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
253 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
254 (char const )'=', (char const )'v', (char const )'e', (char const )'n',
255 (char const )'d', (char const )'o', (char const )'r', (char const )'s',
256 (char const )'u', (char const )'p', (char const )'p', (char const )'o',
257 (char const )'r', (char const )'t', (char const )':', (char const )'i',
258 (char const )'n', (char const )'t', (char const )'\000'};
259#line 54 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
260static char const __mod_vendorsupport56[133] __attribute__((__used__, __unused__,
261__section__(".modinfo"), __aligned__(1))) =
262#line 54
263 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
264 (char const )'=', (char const )'v', (char const )'e', (char const )'n',
265 (char const )'d', (char const )'o', (char const )'r', (char const )'s',
266 (char const )'u', (char const )'p', (char const )'p', (char const )'o',
267 (char const )'r', (char const )'t', (char const )':', (char const )'i',
268 (char const )'T', (char const )'C', (char const )'O', (char const )' ',
269 (char const )'v', (char const )'e', (char const )'n', (char const )'d',
270 (char const )'o', (char const )'r', (char const )' ', (char const )'s',
271 (char const )'p', (char const )'e', (char const )'c', (char const )'i',
272 (char const )'f', (char const )'i', (char const )'c', (char const )' ',
273 (char const )'s', (char const )'u', (char const )'p', (char const )'p',
274 (char const )'o', (char const )'r', (char const )'t', (char const )' ',
275 (char const )'m', (char const )'o', (char const )'d', (char const )'e',
276 (char const )',', (char const )' ', (char const )'d', (char const )'e',
277 (char const )'f', (char const )'a', (char const )'u', (char const )'l',
278 (char const )'t', (char const )'=', (char const )'0', (char const )' ',
279 (char const )'(', (char const )'n', (char const )'o', (char const )'n',
280 (char const )'e', (char const )')', (char const )',', (char const )' ',
281 (char const )'1', (char const )'=', (char const )'S', (char const )'u',
282 (char const )'p', (char const )'e', (char const )'r', (char const )'M',
283 (char const )'i', (char const )'c', (char const )'r', (char const )'o',
284 (char const )' ', (char const )'P', (char const )'e', (char const )'n',
285 (char const )'t', (char const )'3', (char const )',', (char const )' ',
286 (char const )'2', (char const )'=', (char const )'S', (char const )'u',
287 (char const )'p', (char const )'e', (char const )'r', (char const )'M',
288 (char const )'i', (char const )'c', (char const )'r', (char const )'o',
289 (char const )' ', (char const )'P', (char const )'e', (char const )'n',
290 (char const )'t', (char const )'4', (char const )'+', (char const )',',
291 (char const )' ', (char const )'9', (char const )'1', (char const )'1',
292 (char const )'=', (char const )'B', (char const )'r', (char const )'o',
293 (char const )'k', (char const )'e', (char const )'n', (char const )' ',
294 (char const )'S', (char const )'M', (char const )'I', (char const )' ',
295 (char const )'B', (char const )'I', (char const )'O', (char const )'S',
296 (char const )'\000'};
297#line 86 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
298static void supermicro_old_pre_start(unsigned long acpibase )
299{ unsigned long val32 ;
300 unsigned int tmp ;
301 unsigned long __cil_tmp4 ;
302 int __cil_tmp5 ;
303 unsigned int __cil_tmp6 ;
304 unsigned long __cil_tmp7 ;
305 int __cil_tmp8 ;
306
307 {
308 {
309#line 91
310 __cil_tmp4 = acpibase + 48UL;
311#line 91
312 __cil_tmp5 = (int )__cil_tmp4;
313#line 91
314 tmp = inl(__cil_tmp5);
315#line 91
316 val32 = (unsigned long )tmp;
317#line 92
318 val32 = val32 & 4294959103UL;
319#line 93
320 __cil_tmp6 = (unsigned int )val32;
321#line 93
322 __cil_tmp7 = acpibase + 48UL;
323#line 93
324 __cil_tmp8 = (int )__cil_tmp7;
325#line 93
326 outl(__cil_tmp6, __cil_tmp8);
327 }
328#line 94
329 return;
330}
331}
332#line 96 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
333static void supermicro_old_pre_stop(unsigned long acpibase )
334{ unsigned long val32 ;
335 unsigned int tmp ;
336 unsigned long __cil_tmp4 ;
337 int __cil_tmp5 ;
338 unsigned int __cil_tmp6 ;
339 unsigned long __cil_tmp7 ;
340 int __cil_tmp8 ;
341
342 {
343 {
344#line 101
345 __cil_tmp4 = acpibase + 48UL;
346#line 101
347 __cil_tmp5 = (int )__cil_tmp4;
348#line 101
349 tmp = inl(__cil_tmp5);
350#line 101
351 val32 = (unsigned long )tmp;
352#line 102
353 val32 = val32 | 8192UL;
354#line 103
355 __cil_tmp6 = (unsigned int )val32;
356#line 103
357 __cil_tmp7 = acpibase + 48UL;
358#line 103
359 __cil_tmp8 = (int )__cil_tmp7;
360#line 103
361 outl(__cil_tmp6, __cil_tmp8);
362 }
363#line 104
364 return;
365}
366}
367#line 171 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
368static void supermicro_new_unlock_watchdog(void)
369{
370
371 {
372 {
373#line 174
374 outb((unsigned char)135, 46);
375#line 175
376 outb((unsigned char)135, 46);
377#line 177
378 outb((unsigned char)7, 46);
379#line 178
380 outb((unsigned char)8, 47);
381 }
382#line 179
383 return;
384}
385}
386#line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
387static void supermicro_new_lock_watchdog(void)
388{
389
390 {
391 {
392#line 183
393 outb((unsigned char)170, 46);
394 }
395#line 184
396 return;
397}
398}
399#line 186 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
400static void supermicro_new_pre_start(unsigned int heartbeat )
401{ unsigned int val ;
402 unsigned char tmp ;
403 unsigned char tmp___0 ;
404 unsigned char tmp___1 ;
405 unsigned char __cil_tmp6 ;
406 unsigned int __cil_tmp7 ;
407 unsigned char __cil_tmp8 ;
408 unsigned char __cil_tmp9 ;
409 unsigned char __cil_tmp10 ;
410
411 {
412 {
413#line 190
414 supermicro_new_unlock_watchdog();
415#line 193
416 outb((unsigned char)245, 46);
417#line 194
418 tmp = inb(47);
419#line 194
420 val = (unsigned int )tmp;
421#line 195
422 val = val & 247U;
423#line 196
424 __cil_tmp6 = (unsigned char )val;
425#line 196
426 outb(__cil_tmp6, 47);
427#line 199
428 outb((unsigned char)246, 46);
429#line 200
430 __cil_tmp7 = heartbeat & 255U;
431#line 200
432 __cil_tmp8 = (unsigned char )__cil_tmp7;
433#line 200
434 outb(__cil_tmp8, 47);
435#line 203
436 outb((unsigned char)247, 46);
437#line 204
438 tmp___0 = inb(47);
439#line 204
440 val = (unsigned int )tmp___0;
441#line 205
442 val = val & 63U;
443#line 206
444 __cil_tmp9 = (unsigned char )val;
445#line 206
446 outb(__cil_tmp9, 47);
447#line 209
448 outb((unsigned char)48, 46);
449#line 210
450 tmp___1 = inb(47);
451#line 210
452 val = (unsigned int )tmp___1;
453#line 211
454 val = val | 1U;
455#line 212
456 __cil_tmp10 = (unsigned char )val;
457#line 212
458 outb(__cil_tmp10, 47);
459#line 214
460 supermicro_new_lock_watchdog();
461 }
462#line 215
463 return;
464}
465}
466#line 217 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
467static void supermicro_new_pre_stop(void)
468{ unsigned int val ;
469 unsigned char tmp ;
470 unsigned char __cil_tmp3 ;
471
472 {
473 {
474#line 221
475 supermicro_new_unlock_watchdog();
476#line 224
477 outb((unsigned char)48, 46);
478#line 225
479 tmp = inb(47);
480#line 225
481 val = (unsigned int )tmp;
482#line 226
483 val = val & 254U;
484#line 227
485 __cil_tmp3 = (unsigned char )val;
486#line 227
487 outb(__cil_tmp3, 47);
488#line 229
489 supermicro_new_lock_watchdog();
490 }
491#line 230
492 return;
493}
494}
495#line 232 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
496static void supermicro_new_pre_set_heartbeat(unsigned int heartbeat )
497{ unsigned int __cil_tmp2 ;
498 unsigned char __cil_tmp3 ;
499
500 {
501 {
502#line 234
503 supermicro_new_unlock_watchdog();
504#line 237
505 outb((unsigned char)246, 46);
506#line 238
507 __cil_tmp2 = heartbeat & 255U;
508#line 238
509 __cil_tmp3 = (unsigned char )__cil_tmp2;
510#line 238
511 outb(__cil_tmp3, 47);
512#line 240
513 supermicro_new_lock_watchdog();
514 }
515#line 241
516 return;
517}
518}
519#line 274 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
520static void broken_bios_start(unsigned long acpibase )
521{ unsigned long val32 ;
522 unsigned int tmp ;
523 unsigned long __cil_tmp4 ;
524 int __cil_tmp5 ;
525 unsigned int __cil_tmp6 ;
526 unsigned long __cil_tmp7 ;
527 int __cil_tmp8 ;
528
529 {
530 {
531#line 278
532 __cil_tmp4 = acpibase + 48UL;
533#line 278
534 __cil_tmp5 = (int )__cil_tmp4;
535#line 278
536 tmp = inl(__cil_tmp5);
537#line 278
538 val32 = (unsigned long )tmp;
539#line 281
540 val32 = val32 & 4294959102UL;
541#line 282
542 __cil_tmp6 = (unsigned int )val32;
543#line 282
544 __cil_tmp7 = acpibase + 48UL;
545#line 282
546 __cil_tmp8 = (int )__cil_tmp7;
547#line 282
548 outl(__cil_tmp6, __cil_tmp8);
549 }
550#line 283
551 return;
552}
553}
554#line 285 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
555static void broken_bios_stop(unsigned long acpibase )
556{ unsigned long val32 ;
557 unsigned int tmp ;
558 unsigned long __cil_tmp4 ;
559 int __cil_tmp5 ;
560 unsigned int __cil_tmp6 ;
561 unsigned long __cil_tmp7 ;
562 int __cil_tmp8 ;
563
564 {
565 {
566#line 289
567 __cil_tmp4 = acpibase + 48UL;
568#line 289
569 __cil_tmp5 = (int )__cil_tmp4;
570#line 289
571 tmp = inl(__cil_tmp5);
572#line 289
573 val32 = (unsigned long )tmp;
574#line 292
575 val32 = val32 | 8193UL;
576#line 293
577 __cil_tmp6 = (unsigned int )val32;
578#line 293
579 __cil_tmp7 = acpibase + 48UL;
580#line 293
581 __cil_tmp8 = (int )__cil_tmp7;
582#line 293
583 outl(__cil_tmp6, __cil_tmp8);
584 }
585#line 294
586 return;
587}
588}
589#line 300 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
590void iTCO_vendor_pre_start(unsigned long acpibase , unsigned int heartbeat )
591{ int *__cil_tmp3 ;
592
593 {
594 {
595#line 303
596 __cil_tmp3 = & vendorsupport;
597#line 304
598 if (*__cil_tmp3 == 1) {
599#line 304
600 goto case_1;
601 } else
602#line 307
603 if (*__cil_tmp3 == 2) {
604#line 307
605 goto case_2;
606 } else
607#line 310
608 if (*__cil_tmp3 == 911) {
609#line 310
610 goto case_911;
611 } else
612#line 303
613 if (0) {
614 case_1:
615 {
616#line 305
617 supermicro_old_pre_start(acpibase);
618 }
619#line 306
620 goto switch_break;
621 case_2:
622 {
623#line 308
624 supermicro_new_pre_start(heartbeat);
625 }
626#line 309
627 goto switch_break;
628 case_911:
629 {
630#line 311
631 broken_bios_start(acpibase);
632 }
633#line 312
634 goto switch_break;
635 } else {
636 switch_break: ;
637 }
638 }
639#line 314
640 return;
641}
642}
643#line 315
644extern void *__crc_iTCO_vendor_pre_start __attribute__((__weak__)) ;
645#line 315 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
646static unsigned long const __kcrctab_iTCO_vendor_pre_start __attribute__((__used__,
647__unused__, __section__("___kcrctab+iTCO_vendor_pre_start"))) = (unsigned long const )((unsigned long )(& __crc_iTCO_vendor_pre_start));
648#line 315 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
649static char const __kstrtab_iTCO_vendor_pre_start[22] __attribute__((__section__("__ksymtab_strings"),
650__aligned__(1))) =
651#line 315
652 { (char const )'i', (char const )'T', (char const )'C', (char const )'O',
653 (char const )'_', (char const )'v', (char const )'e', (char const )'n',
654 (char const )'d', (char const )'o', (char const )'r', (char const )'_',
655 (char const )'p', (char const )'r', (char const )'e', (char const )'_',
656 (char const )'s', (char const )'t', (char const )'a', (char const )'r',
657 (char const )'t', (char const )'\000'};
658#line 315 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
659static struct kernel_symbol const __ksymtab_iTCO_vendor_pre_start __attribute__((__used__,
660__unused__, __section__("___ksymtab+iTCO_vendor_pre_start"))) = {(unsigned long )(& iTCO_vendor_pre_start), __kstrtab_iTCO_vendor_pre_start};
661#line 317 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
662void iTCO_vendor_pre_stop(unsigned long acpibase )
663{ int *__cil_tmp2 ;
664
665 {
666 {
667#line 319
668 __cil_tmp2 = & vendorsupport;
669#line 320
670 if (*__cil_tmp2 == 1) {
671#line 320
672 goto case_1;
673 } else
674#line 323
675 if (*__cil_tmp2 == 2) {
676#line 323
677 goto case_2;
678 } else
679#line 326
680 if (*__cil_tmp2 == 911) {
681#line 326
682 goto case_911;
683 } else
684#line 319
685 if (0) {
686 case_1:
687 {
688#line 321
689 supermicro_old_pre_stop(acpibase);
690 }
691#line 322
692 goto switch_break;
693 case_2:
694 {
695#line 324
696 supermicro_new_pre_stop();
697 }
698#line 325
699 goto switch_break;
700 case_911:
701 {
702#line 327
703 broken_bios_stop(acpibase);
704 }
705#line 328
706 goto switch_break;
707 } else {
708 switch_break: ;
709 }
710 }
711#line 330
712 return;
713}
714}
715#line 331
716extern void *__crc_iTCO_vendor_pre_stop __attribute__((__weak__)) ;
717#line 331 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
718static unsigned long const __kcrctab_iTCO_vendor_pre_stop __attribute__((__used__,
719__unused__, __section__("___kcrctab+iTCO_vendor_pre_stop"))) = (unsigned long const )((unsigned long )(& __crc_iTCO_vendor_pre_stop));
720#line 331 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
721static char const __kstrtab_iTCO_vendor_pre_stop[21] __attribute__((__section__("__ksymtab_strings"),
722__aligned__(1))) =
723#line 331
724 { (char const )'i', (char const )'T', (char const )'C', (char const )'O',
725 (char const )'_', (char const )'v', (char const )'e', (char const )'n',
726 (char const )'d', (char const )'o', (char const )'r', (char const )'_',
727 (char const )'p', (char const )'r', (char const )'e', (char const )'_',
728 (char const )'s', (char const )'t', (char const )'o', (char const )'p',
729 (char const )'\000'};
730#line 331 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
731static struct kernel_symbol const __ksymtab_iTCO_vendor_pre_stop __attribute__((__used__,
732__unused__, __section__("___ksymtab+iTCO_vendor_pre_stop"))) = {(unsigned long )(& iTCO_vendor_pre_stop), __kstrtab_iTCO_vendor_pre_stop};
733#line 333 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
734void iTCO_vendor_pre_keepalive(unsigned long acpibase , unsigned int heartbeat )
735{ int *__cil_tmp3 ;
736 int __cil_tmp4 ;
737
738 {
739 {
740#line 335
741 __cil_tmp3 = & vendorsupport;
742#line 335
743 __cil_tmp4 = *__cil_tmp3;
744#line 335
745 if (__cil_tmp4 == 2) {
746 {
747#line 336
748 supermicro_new_pre_set_heartbeat(heartbeat);
749 }
750 } else {
751
752 }
753 }
754#line 337
755 return;
756}
757}
758#line 338
759extern void *__crc_iTCO_vendor_pre_keepalive __attribute__((__weak__)) ;
760#line 338 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
761static unsigned long const __kcrctab_iTCO_vendor_pre_keepalive __attribute__((__used__,
762__unused__, __section__("___kcrctab+iTCO_vendor_pre_keepalive"))) = (unsigned long const )((unsigned long )(& __crc_iTCO_vendor_pre_keepalive));
763#line 338 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
764static char const __kstrtab_iTCO_vendor_pre_keepalive[26] __attribute__((__section__("__ksymtab_strings"),
765__aligned__(1))) =
766#line 338
767 { (char const )'i', (char const )'T', (char const )'C', (char const )'O',
768 (char const )'_', (char const )'v', (char const )'e', (char const )'n',
769 (char const )'d', (char const )'o', (char const )'r', (char const )'_',
770 (char const )'p', (char const )'r', (char const )'e', (char const )'_',
771 (char const )'k', (char const )'e', (char const )'e', (char const )'p',
772 (char const )'a', (char const )'l', (char const )'i', (char const )'v',
773 (char const )'e', (char const )'\000'};
774#line 338 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
775static struct kernel_symbol const __ksymtab_iTCO_vendor_pre_keepalive __attribute__((__used__,
776__unused__, __section__("___ksymtab+iTCO_vendor_pre_keepalive"))) = {(unsigned long )(& iTCO_vendor_pre_keepalive), __kstrtab_iTCO_vendor_pre_keepalive};
777#line 340 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
778void iTCO_vendor_pre_set_heartbeat(unsigned int heartbeat )
779{ int *__cil_tmp2 ;
780 int __cil_tmp3 ;
781
782 {
783 {
784#line 342
785 __cil_tmp2 = & vendorsupport;
786#line 342
787 __cil_tmp3 = *__cil_tmp2;
788#line 342
789 if (__cil_tmp3 == 2) {
790 {
791#line 343
792 supermicro_new_pre_set_heartbeat(heartbeat);
793 }
794 } else {
795
796 }
797 }
798#line 344
799 return;
800}
801}
802#line 345
803extern void *__crc_iTCO_vendor_pre_set_heartbeat __attribute__((__weak__)) ;
804#line 345 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
805static unsigned long const __kcrctab_iTCO_vendor_pre_set_heartbeat __attribute__((__used__,
806__unused__, __section__("___kcrctab+iTCO_vendor_pre_set_heartbeat"))) = (unsigned long const )((unsigned long )(& __crc_iTCO_vendor_pre_set_heartbeat));
807#line 345 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
808static char const __kstrtab_iTCO_vendor_pre_set_heartbeat[30] __attribute__((__section__("__ksymtab_strings"),
809__aligned__(1))) =
810#line 345
811 { (char const )'i', (char const )'T', (char const )'C', (char const )'O',
812 (char const )'_', (char const )'v', (char const )'e', (char const )'n',
813 (char const )'d', (char const )'o', (char const )'r', (char const )'_',
814 (char const )'p', (char const )'r', (char const )'e', (char const )'_',
815 (char const )'s', (char const )'e', (char const )'t', (char const )'_',
816 (char const )'h', (char const )'e', (char const )'a', (char const )'r',
817 (char const )'t', (char const )'b', (char const )'e', (char const )'a',
818 (char const )'t', (char const )'\000'};
819#line 345 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
820static struct kernel_symbol const __ksymtab_iTCO_vendor_pre_set_heartbeat __attribute__((__used__,
821__unused__, __section__("___ksymtab+iTCO_vendor_pre_set_heartbeat"))) = {(unsigned long )(& iTCO_vendor_pre_set_heartbeat), __kstrtab_iTCO_vendor_pre_set_heartbeat};
822#line 347 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
823int iTCO_vendor_check_noreboot_on(void)
824{ int *__cil_tmp1 ;
825
826 {
827 {
828#line 349
829 __cil_tmp1 = & vendorsupport;
830#line 350
831 if (*__cil_tmp1 == 1) {
832#line 350
833 goto case_1;
834 } else {
835 {
836#line 352
837 goto switch_default;
838#line 349
839 if (0) {
840 case_1:
841#line 351
842 return (0);
843 switch_default:
844#line 353
845 return (1);
846 } else {
847 switch_break: ;
848 }
849 }
850 }
851 }
852}
853}
854#line 356
855extern void *__crc_iTCO_vendor_check_noreboot_on __attribute__((__weak__)) ;
856#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
857static unsigned long const __kcrctab_iTCO_vendor_check_noreboot_on __attribute__((__used__,
858__unused__, __section__("___kcrctab+iTCO_vendor_check_noreboot_on"))) = (unsigned long const )((unsigned long )(& __crc_iTCO_vendor_check_noreboot_on));
859#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
860static char const __kstrtab_iTCO_vendor_check_noreboot_on[30] __attribute__((__section__("__ksymtab_strings"),
861__aligned__(1))) =
862#line 356
863 { (char const )'i', (char const )'T', (char const )'C', (char const )'O',
864 (char const )'_', (char const )'v', (char const )'e', (char const )'n',
865 (char const )'d', (char const )'o', (char const )'r', (char const )'_',
866 (char const )'c', (char const )'h', (char const )'e', (char const )'c',
867 (char const )'k', (char const )'_', (char const )'n', (char const )'o',
868 (char const )'r', (char const )'e', (char const )'b', (char const )'o',
869 (char const )'o', (char const )'t', (char const )'_', (char const )'o',
870 (char const )'n', (char const )'\000'};
871#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
872static struct kernel_symbol const __ksymtab_iTCO_vendor_check_noreboot_on __attribute__((__used__,
873__unused__, __section__("___ksymtab+iTCO_vendor_check_noreboot_on"))) = {(unsigned long )(& iTCO_vendor_check_noreboot_on), __kstrtab_iTCO_vendor_check_noreboot_on};
874#line 358
875static int iTCO_vendor_init_module(void) __attribute__((__section__(".init.text"),
876__no_instrument_function__)) ;
877#line 358 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
878static int iTCO_vendor_init_module(void)
879{ int *__cil_tmp1 ;
880 int __cil_tmp2 ;
881
882 {
883 {
884#line 360
885 __cil_tmp1 = & vendorsupport;
886#line 360
887 __cil_tmp2 = *__cil_tmp1;
888#line 360
889 printk("<6>iTCO_vendor_support: vendor-support=%d\n", __cil_tmp2);
890 }
891#line 361
892 return (0);
893}
894}
895#line 364
896static void iTCO_vendor_exit_module(void) __attribute__((__section__(".exit.text"),
897__no_instrument_function__)) ;
898#line 364 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
899static void iTCO_vendor_exit_module(void)
900{
901
902 {
903 {
904#line 366
905 printk("<6>iTCO_vendor_support: Module Unloaded\n");
906 }
907#line 367
908 return;
909}
910}
911#line 369 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
912int init_module(void)
913{ int tmp ;
914
915 {
916 {
917#line 369
918 tmp = iTCO_vendor_init_module();
919 }
920#line 369
921 return (tmp);
922}
923}
924#line 370 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
925void cleanup_module(void)
926{
927
928 {
929 {
930#line 370
931 iTCO_vendor_exit_module();
932 }
933#line 370
934 return;
935}
936}
937#line 372 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
938static char const __mod_author373[74] __attribute__((__used__, __unused__, __section__(".modinfo"),
939__aligned__(1))) =
940#line 372
941 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
942 (char const )'o', (char const )'r', (char const )'=', (char const )'W',
943 (char const )'i', (char const )'m', (char const )' ', (char const )'V',
944 (char const )'a', (char const )'n', (char const )' ', (char const )'S',
945 (char const )'e', (char const )'b', (char const )'r', (char const )'o',
946 (char const )'e', (char const )'c', (char const )'k', (char const )' ',
947 (char const )'<', (char const )'w', (char const )'i', (char const )'m',
948 (char const )'@', (char const )'i', (char const )'g', (char const )'u',
949 (char const )'a', (char const )'n', (char const )'a', (char const )'.',
950 (char const )'b', (char const )'e', (char const )'>', (char const )',',
951 (char const )' ', (char const )'R', (char const )'.', (char const )' ',
952 (char const )'S', (char const )'e', (char const )'r', (char const )'e',
953 (char const )'t', (char const )'n', (char const )'y', (char const )' ',
954 (char const )'<', (char const )'l', (char const )'k', (char const )'p',
955 (char const )'a', (char const )'t', (char const )'c', (char const )'h',
956 (char const )'e', (char const )'s', (char const )'@', (char const )'p',
957 (char const )'a', (char const )'y', (char const )'p', (char const )'c',
958 (char const )'.', (char const )'c', (char const )'o', (char const )'m',
959 (char const )'>', (char const )'\000'};
960#line 374 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
961static char const __mod_description374[68] __attribute__((__used__, __unused__,
962__section__(".modinfo"), __aligned__(1))) =
963#line 374
964 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
965 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
966 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
967 (char const )'I', (char const )'n', (char const )'t', (char const )'e',
968 (char const )'l', (char const )' ', (char const )'T', (char const )'C',
969 (char const )'O', (char const )' ', (char const )'V', (char const )'e',
970 (char const )'n', (char const )'d', (char const )'o', (char const )'r',
971 (char const )' ', (char const )'S', (char const )'p', (char const )'e',
972 (char const )'c', (char const )'i', (char const )'f', (char const )'i',
973 (char const )'c', (char const )' ', (char const )'W', (char const )'a',
974 (char const )'t', (char const )'c', (char const )'h', (char const )'D',
975 (char const )'o', (char const )'g', (char const )' ', (char const )'T',
976 (char const )'i', (char const )'m', (char const )'e', (char const )'r',
977 (char const )' ', (char const )'D', (char const )'r', (char const )'i',
978 (char const )'v', (char const )'e', (char const )'r', (char const )' ',
979 (char const )'S', (char const )'u', (char const )'p', (char const )'p',
980 (char const )'o', (char const )'r', (char const )'t', (char const )'\000'};
981#line 375 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
982static char const __mod_version375[13] __attribute__((__used__, __unused__, __section__(".modinfo"),
983__aligned__(1))) =
984#line 375
985 { (char const )'v', (char const )'e', (char const )'r', (char const )'s',
986 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
987 (char const )'1', (char const )'.', (char const )'0', (char const )'4',
988 (char const )'\000'};
989#line 376 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
990static char const __mod_license376[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
991__aligned__(1))) =
992#line 376
993 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
994 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
995 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
996#line 395
997void ldv_check_final_state(void) ;
998#line 401
999extern void ldv_initialize(void) ;
1000#line 404
1001extern int __VERIFIER_nondet_int(void) ;
1002#line 407 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
1003int LDV_IN_INTERRUPT ;
1004#line 410 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
1005void main(void)
1006{ int tmp ;
1007 int tmp___0 ;
1008 int tmp___1 ;
1009
1010 {
1011 {
1012#line 422
1013 LDV_IN_INTERRUPT = 1;
1014#line 431
1015 ldv_initialize();
1016#line 457
1017 tmp = iTCO_vendor_init_module();
1018 }
1019#line 457
1020 if (tmp) {
1021#line 458
1022 goto ldv_final;
1023 } else {
1024
1025 }
1026 {
1027#line 460
1028 while (1) {
1029 while_continue: ;
1030 {
1031#line 460
1032 tmp___1 = __VERIFIER_nondet_int();
1033 }
1034#line 460
1035 if (tmp___1) {
1036
1037 } else {
1038#line 460
1039 goto while_break;
1040 }
1041 {
1042#line 463
1043 tmp___0 = __VERIFIER_nondet_int();
1044 }
1045 {
1046#line 465
1047 goto switch_default;
1048#line 463
1049 if (0) {
1050 switch_default:
1051#line 465
1052 goto switch_break;
1053 } else {
1054 switch_break: ;
1055 }
1056 }
1057 }
1058 while_break: ;
1059 }
1060 {
1061#line 497
1062 iTCO_vendor_exit_module();
1063 }
1064 ldv_final:
1065 {
1066#line 500
1067 ldv_check_final_state();
1068 }
1069#line 503
1070 return;
1071}
1072}
1073#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1074void ldv_blast_assert(void)
1075{
1076
1077 {
1078 ERROR:
1079#line 6
1080 goto ERROR;
1081}
1082}
1083#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1084extern int __VERIFIER_nondet_int(void) ;
1085#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1086int ldv_mutex = 1;
1087#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1088int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1089{ int nondetermined ;
1090
1091 {
1092#line 29
1093 if (ldv_mutex == 1) {
1094
1095 } else {
1096 {
1097#line 29
1098 ldv_blast_assert();
1099 }
1100 }
1101 {
1102#line 32
1103 nondetermined = __VERIFIER_nondet_int();
1104 }
1105#line 35
1106 if (nondetermined) {
1107#line 38
1108 ldv_mutex = 2;
1109#line 40
1110 return (0);
1111 } else {
1112#line 45
1113 return (-4);
1114 }
1115}
1116}
1117#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1118int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1119{ int nondetermined ;
1120
1121 {
1122#line 57
1123 if (ldv_mutex == 1) {
1124
1125 } else {
1126 {
1127#line 57
1128 ldv_blast_assert();
1129 }
1130 }
1131 {
1132#line 60
1133 nondetermined = __VERIFIER_nondet_int();
1134 }
1135#line 63
1136 if (nondetermined) {
1137#line 66
1138 ldv_mutex = 2;
1139#line 68
1140 return (0);
1141 } else {
1142#line 73
1143 return (-4);
1144 }
1145}
1146}
1147#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1148int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1149{ int atomic_value_after_dec ;
1150
1151 {
1152#line 83
1153 if (ldv_mutex == 1) {
1154
1155 } else {
1156 {
1157#line 83
1158 ldv_blast_assert();
1159 }
1160 }
1161 {
1162#line 86
1163 atomic_value_after_dec = __VERIFIER_nondet_int();
1164 }
1165#line 89
1166 if (atomic_value_after_dec == 0) {
1167#line 92
1168 ldv_mutex = 2;
1169#line 94
1170 return (1);
1171 } else {
1172
1173 }
1174#line 98
1175 return (0);
1176}
1177}
1178#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1179void mutex_lock(struct mutex *lock )
1180{
1181
1182 {
1183#line 108
1184 if (ldv_mutex == 1) {
1185
1186 } else {
1187 {
1188#line 108
1189 ldv_blast_assert();
1190 }
1191 }
1192#line 110
1193 ldv_mutex = 2;
1194#line 111
1195 return;
1196}
1197}
1198#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1199int mutex_trylock(struct mutex *lock )
1200{ int nondetermined ;
1201
1202 {
1203#line 121
1204 if (ldv_mutex == 1) {
1205
1206 } else {
1207 {
1208#line 121
1209 ldv_blast_assert();
1210 }
1211 }
1212 {
1213#line 124
1214 nondetermined = __VERIFIER_nondet_int();
1215 }
1216#line 127
1217 if (nondetermined) {
1218#line 130
1219 ldv_mutex = 2;
1220#line 132
1221 return (1);
1222 } else {
1223#line 137
1224 return (0);
1225 }
1226}
1227}
1228#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1229void mutex_unlock(struct mutex *lock )
1230{
1231
1232 {
1233#line 147
1234 if (ldv_mutex == 2) {
1235
1236 } else {
1237 {
1238#line 147
1239 ldv_blast_assert();
1240 }
1241 }
1242#line 149
1243 ldv_mutex = 1;
1244#line 150
1245 return;
1246}
1247}
1248#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1249void ldv_check_final_state(void)
1250{
1251
1252 {
1253#line 156
1254 if (ldv_mutex == 1) {
1255
1256 } else {
1257 {
1258#line 156
1259 ldv_blast_assert();
1260 }
1261 }
1262#line 157
1263 return;
1264}
1265}
1266#line 512 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16403/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/iTCO_vendor_support.c.common.c"
1267long s__builtin_expect(long val , long res )
1268{
1269
1270 {
1271#line 513
1272 return (val);
1273}
1274}