1
2
3
4#line 20 "include/asm-generic/int-ll64.h"
5typedef unsigned char __u8;
6#line 23 "include/asm-generic/int-ll64.h"
7typedef unsigned short __u16;
8#line 26 "include/asm-generic/int-ll64.h"
9typedef unsigned int __u32;
10#line 30 "include/asm-generic/int-ll64.h"
11typedef unsigned long long __u64;
12#line 45 "include/asm-generic/int-ll64.h"
13typedef short s16;
14#line 46 "include/asm-generic/int-ll64.h"
15typedef unsigned short u16;
16#line 49 "include/asm-generic/int-ll64.h"
17typedef unsigned int u32;
18#line 14 "include/asm-generic/posix_types.h"
19typedef long __kernel_long_t;
20#line 15 "include/asm-generic/posix_types.h"
21typedef unsigned long __kernel_ulong_t;
22#line 75 "include/asm-generic/posix_types.h"
23typedef __kernel_ulong_t __kernel_size_t;
24#line 76 "include/asm-generic/posix_types.h"
25typedef __kernel_long_t __kernel_ssize_t;
26#line 27 "include/linux/types.h"
27typedef unsigned short umode_t;
28#line 38 "include/linux/types.h"
29typedef _Bool bool;
30#line 63 "include/linux/types.h"
31typedef __kernel_size_t size_t;
32#line 68 "include/linux/types.h"
33typedef __kernel_ssize_t ssize_t;
34#line 219 "include/linux/types.h"
35struct __anonstruct_atomic_t_7 {
36 int counter ;
37};
38#line 219 "include/linux/types.h"
39typedef struct __anonstruct_atomic_t_7 atomic_t;
40#line 229 "include/linux/types.h"
41struct list_head {
42 struct list_head *next ;
43 struct list_head *prev ;
44};
45#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
46struct module;
47#line 56
48struct module;
49#line 146 "include/linux/init.h"
50typedef void (*ctor_fn_t)(void);
51#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
52struct task_struct;
53#line 20
54struct task_struct;
55#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
56struct task_struct;
57#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
58struct task_struct;
59#line 329
60struct arch_spinlock;
61#line 329
62struct arch_spinlock;
63#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
64struct task_struct;
65#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
66struct task_struct;
67#line 10 "include/asm-generic/bug.h"
68struct bug_entry {
69 int bug_addr_disp ;
70 int file_disp ;
71 unsigned short line ;
72 unsigned short flags ;
73};
74#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
75struct static_key;
76#line 234
77struct static_key;
78#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
79typedef u16 __ticket_t;
80#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
81typedef u32 __ticketpair_t;
82#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
83struct __raw_tickets {
84 __ticket_t head ;
85 __ticket_t tail ;
86};
87#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
88union __anonunion____missing_field_name_36 {
89 __ticketpair_t head_tail ;
90 struct __raw_tickets tickets ;
91};
92#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
93struct arch_spinlock {
94 union __anonunion____missing_field_name_36 __annonCompField17 ;
95};
96#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
97typedef struct arch_spinlock arch_spinlock_t;
98#line 12 "include/linux/lockdep.h"
99struct task_struct;
100#line 20 "include/linux/spinlock_types.h"
101struct raw_spinlock {
102 arch_spinlock_t raw_lock ;
103 unsigned int magic ;
104 unsigned int owner_cpu ;
105 void *owner ;
106};
107#line 64 "include/linux/spinlock_types.h"
108union __anonunion____missing_field_name_39 {
109 struct raw_spinlock rlock ;
110};
111#line 64 "include/linux/spinlock_types.h"
112struct spinlock {
113 union __anonunion____missing_field_name_39 __annonCompField19 ;
114};
115#line 64 "include/linux/spinlock_types.h"
116typedef struct spinlock spinlock_t;
117#line 55 "include/linux/wait.h"
118struct task_struct;
119#line 48 "include/linux/mutex.h"
120struct mutex {
121 atomic_t count ;
122 spinlock_t wait_lock ;
123 struct list_head wait_list ;
124 struct task_struct *owner ;
125 char const *name ;
126 void *magic ;
127};
128#line 188 "include/linux/rcupdate.h"
129struct notifier_block;
130#line 188
131struct notifier_block;
132#line 50 "include/linux/notifier.h"
133struct notifier_block {
134 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
135 struct notifier_block *next ;
136 int priority ;
137};
138#line 10 "include/linux/timer.h"
139struct tvec_base;
140#line 10
141struct tvec_base;
142#line 12 "include/linux/timer.h"
143struct timer_list {
144 struct list_head entry ;
145 unsigned long expires ;
146 struct tvec_base *base ;
147 void (*function)(unsigned long ) ;
148 unsigned long data ;
149 int slack ;
150 int start_pid ;
151 void *start_site ;
152 char start_comm[16] ;
153};
154#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
155struct task_struct;
156#line 18 "include/linux/elf.h"
157typedef __u64 Elf64_Addr;
158#line 19 "include/linux/elf.h"
159typedef __u16 Elf64_Half;
160#line 23 "include/linux/elf.h"
161typedef __u32 Elf64_Word;
162#line 24 "include/linux/elf.h"
163typedef __u64 Elf64_Xword;
164#line 194 "include/linux/elf.h"
165struct elf64_sym {
166 Elf64_Word st_name ;
167 unsigned char st_info ;
168 unsigned char st_other ;
169 Elf64_Half st_shndx ;
170 Elf64_Addr st_value ;
171 Elf64_Xword st_size ;
172};
173#line 194 "include/linux/elf.h"
174typedef struct elf64_sym Elf64_Sym;
175#line 20 "include/linux/kobject_ns.h"
176struct sock;
177#line 20
178struct sock;
179#line 21
180struct kobject;
181#line 21
182struct kobject;
183#line 27
184enum kobj_ns_type {
185 KOBJ_NS_TYPE_NONE = 0,
186 KOBJ_NS_TYPE_NET = 1,
187 KOBJ_NS_TYPES = 2
188} ;
189#line 40 "include/linux/kobject_ns.h"
190struct kobj_ns_type_operations {
191 enum kobj_ns_type type ;
192 void *(*grab_current_ns)(void) ;
193 void const *(*netlink_ns)(struct sock *sk ) ;
194 void const *(*initial_ns)(void) ;
195 void (*drop_ns)(void * ) ;
196};
197#line 22 "include/linux/sysfs.h"
198struct kobject;
199#line 23
200struct module;
201#line 24
202enum kobj_ns_type;
203#line 26 "include/linux/sysfs.h"
204struct attribute {
205 char const *name ;
206 umode_t mode ;
207};
208#line 112 "include/linux/sysfs.h"
209struct sysfs_ops {
210 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
211 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
212 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
213};
214#line 118
215struct sysfs_dirent;
216#line 118
217struct sysfs_dirent;
218#line 22 "include/linux/kref.h"
219struct kref {
220 atomic_t refcount ;
221};
222#line 60 "include/linux/kobject.h"
223struct kset;
224#line 60
225struct kobj_type;
226#line 60 "include/linux/kobject.h"
227struct kobject {
228 char const *name ;
229 struct list_head entry ;
230 struct kobject *parent ;
231 struct kset *kset ;
232 struct kobj_type *ktype ;
233 struct sysfs_dirent *sd ;
234 struct kref kref ;
235 unsigned int state_initialized : 1 ;
236 unsigned int state_in_sysfs : 1 ;
237 unsigned int state_add_uevent_sent : 1 ;
238 unsigned int state_remove_uevent_sent : 1 ;
239 unsigned int uevent_suppress : 1 ;
240};
241#line 108 "include/linux/kobject.h"
242struct kobj_type {
243 void (*release)(struct kobject *kobj ) ;
244 struct sysfs_ops const *sysfs_ops ;
245 struct attribute **default_attrs ;
246 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
247 void const *(*namespace)(struct kobject *kobj ) ;
248};
249#line 116 "include/linux/kobject.h"
250struct kobj_uevent_env {
251 char *envp[32] ;
252 int envp_idx ;
253 char buf[2048] ;
254 int buflen ;
255};
256#line 123 "include/linux/kobject.h"
257struct kset_uevent_ops {
258 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
259 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
260 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
261};
262#line 140
263struct sock;
264#line 159 "include/linux/kobject.h"
265struct kset {
266 struct list_head list ;
267 spinlock_t list_lock ;
268 struct kobject kobj ;
269 struct kset_uevent_ops const *uevent_ops ;
270};
271#line 39 "include/linux/moduleparam.h"
272struct kernel_param;
273#line 39
274struct kernel_param;
275#line 41 "include/linux/moduleparam.h"
276struct kernel_param_ops {
277 int (*set)(char const *val , struct kernel_param const *kp ) ;
278 int (*get)(char *buffer , struct kernel_param const *kp ) ;
279 void (*free)(void *arg ) ;
280};
281#line 50
282struct kparam_string;
283#line 50
284struct kparam_array;
285#line 50 "include/linux/moduleparam.h"
286union __anonunion____missing_field_name_199 {
287 void *arg ;
288 struct kparam_string const *str ;
289 struct kparam_array const *arr ;
290};
291#line 50 "include/linux/moduleparam.h"
292struct kernel_param {
293 char const *name ;
294 struct kernel_param_ops const *ops ;
295 u16 perm ;
296 s16 level ;
297 union __anonunion____missing_field_name_199 __annonCompField32 ;
298};
299#line 63 "include/linux/moduleparam.h"
300struct kparam_string {
301 unsigned int maxlen ;
302 char *string ;
303};
304#line 69 "include/linux/moduleparam.h"
305struct kparam_array {
306 unsigned int max ;
307 unsigned int elemsize ;
308 unsigned int *num ;
309 struct kernel_param_ops const *ops ;
310 void *elem ;
311};
312#line 445
313struct module;
314#line 80 "include/linux/jump_label.h"
315struct module;
316#line 143 "include/linux/jump_label.h"
317struct static_key {
318 atomic_t enabled ;
319};
320#line 22 "include/linux/tracepoint.h"
321struct module;
322#line 23
323struct tracepoint;
324#line 23
325struct tracepoint;
326#line 25 "include/linux/tracepoint.h"
327struct tracepoint_func {
328 void *func ;
329 void *data ;
330};
331#line 30 "include/linux/tracepoint.h"
332struct tracepoint {
333 char const *name ;
334 struct static_key key ;
335 void (*regfunc)(void) ;
336 void (*unregfunc)(void) ;
337 struct tracepoint_func *funcs ;
338};
339#line 19 "include/linux/export.h"
340struct kernel_symbol {
341 unsigned long value ;
342 char const *name ;
343};
344#line 8 "include/asm-generic/module.h"
345struct mod_arch_specific {
346
347};
348#line 35 "include/linux/module.h"
349struct module;
350#line 37
351struct module_param_attrs;
352#line 37 "include/linux/module.h"
353struct module_kobject {
354 struct kobject kobj ;
355 struct module *mod ;
356 struct kobject *drivers_dir ;
357 struct module_param_attrs *mp ;
358};
359#line 44 "include/linux/module.h"
360struct module_attribute {
361 struct attribute attr ;
362 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
363 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
364 size_t count ) ;
365 void (*setup)(struct module * , char const * ) ;
366 int (*test)(struct module * ) ;
367 void (*free)(struct module * ) ;
368};
369#line 71
370struct exception_table_entry;
371#line 71
372struct exception_table_entry;
373#line 182
374struct notifier_block;
375#line 199
376enum module_state {
377 MODULE_STATE_LIVE = 0,
378 MODULE_STATE_COMING = 1,
379 MODULE_STATE_GOING = 2
380} ;
381#line 215 "include/linux/module.h"
382struct module_ref {
383 unsigned long incs ;
384 unsigned long decs ;
385} __attribute__((__aligned__((2) * (sizeof(unsigned long )) ))) ;
386#line 220
387struct module_sect_attrs;
388#line 220
389struct module_notes_attrs;
390#line 220
391struct ftrace_event_call;
392#line 220 "include/linux/module.h"
393struct module {
394 enum module_state state ;
395 struct list_head list ;
396 char name[64UL - sizeof(unsigned long )] ;
397 struct module_kobject mkobj ;
398 struct module_attribute *modinfo_attrs ;
399 char const *version ;
400 char const *srcversion ;
401 struct kobject *holders_dir ;
402 struct kernel_symbol const *syms ;
403 unsigned long const *crcs ;
404 unsigned int num_syms ;
405 struct kernel_param *kp ;
406 unsigned int num_kp ;
407 unsigned int num_gpl_syms ;
408 struct kernel_symbol const *gpl_syms ;
409 unsigned long const *gpl_crcs ;
410 struct kernel_symbol const *unused_syms ;
411 unsigned long const *unused_crcs ;
412 unsigned int num_unused_syms ;
413 unsigned int num_unused_gpl_syms ;
414 struct kernel_symbol const *unused_gpl_syms ;
415 unsigned long const *unused_gpl_crcs ;
416 struct kernel_symbol const *gpl_future_syms ;
417 unsigned long const *gpl_future_crcs ;
418 unsigned int num_gpl_future_syms ;
419 unsigned int num_exentries ;
420 struct exception_table_entry *extable ;
421 int (*init)(void) ;
422 void *module_init ;
423 void *module_core ;
424 unsigned int init_size ;
425 unsigned int core_size ;
426 unsigned int init_text_size ;
427 unsigned int core_text_size ;
428 unsigned int init_ro_size ;
429 unsigned int core_ro_size ;
430 struct mod_arch_specific arch ;
431 unsigned int taints ;
432 unsigned int num_bugs ;
433 struct list_head bug_list ;
434 struct bug_entry *bug_table ;
435 Elf64_Sym *symtab ;
436 Elf64_Sym *core_symtab ;
437 unsigned int num_symtab ;
438 unsigned int core_num_syms ;
439 char *strtab ;
440 char *core_strtab ;
441 struct module_sect_attrs *sect_attrs ;
442 struct module_notes_attrs *notes_attrs ;
443 char *args ;
444 void *percpu ;
445 unsigned int percpu_size ;
446 unsigned int num_tracepoints ;
447 struct tracepoint * const *tracepoints_ptrs ;
448 unsigned int num_trace_bprintk_fmt ;
449 char const **trace_bprintk_fmt_start ;
450 struct ftrace_event_call **trace_events ;
451 unsigned int num_trace_events ;
452 struct list_head source_list ;
453 struct list_head target_list ;
454 struct task_struct *waiter ;
455 void (*exit)(void) ;
456 struct module_ref *refptr ;
457 ctor_fn_t *ctors ;
458 unsigned int num_ctors ;
459};
460#line 17 "include/linux/watchdog.h"
461struct watchdog_info {
462 __u32 options ;
463 __u32 firmware_version ;
464 __u8 identity[32] ;
465};
466#line 58
467struct watchdog_ops;
468#line 58
469struct watchdog_ops;
470#line 59
471struct watchdog_device;
472#line 59
473struct watchdog_device;
474#line 77 "include/linux/watchdog.h"
475struct watchdog_ops {
476 struct module *owner ;
477 int (*start)(struct watchdog_device * ) ;
478 int (*stop)(struct watchdog_device * ) ;
479 int (*ping)(struct watchdog_device * ) ;
480 unsigned int (*status)(struct watchdog_device * ) ;
481 int (*set_timeout)(struct watchdog_device * , unsigned int ) ;
482 unsigned int (*get_timeleft)(struct watchdog_device * ) ;
483 long (*ioctl)(struct watchdog_device * , unsigned int , unsigned long ) ;
484};
485#line 107 "include/linux/watchdog.h"
486struct watchdog_device {
487 struct watchdog_info const *info ;
488 struct watchdog_ops const *ops ;
489 unsigned int bootstatus ;
490 unsigned int timeout ;
491 unsigned int min_timeout ;
492 unsigned int max_timeout ;
493 void *driver_data ;
494 unsigned long status ;
495};
496#line 1 "<compiler builtins>"
497long __builtin_expect(long val , long res ) ;
498#line 59 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
499__inline static void ( __attribute__((__always_inline__)) set_bit)(unsigned int nr ,
500 unsigned long volatile *addr ) __attribute__((__no_instrument_function__)) ;
501#line 59 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
502__inline static void ( __attribute__((__always_inline__)) set_bit)(unsigned int nr ,
503 unsigned long volatile *addr )
504{ long volatile *__cil_tmp3 ;
505
506 {
507#line 68
508 __cil_tmp3 = (long volatile *)addr;
509#line 68
510 __asm__ volatile (".section .smp_locks,\"a\"\n"
511 ".balign 4\n"
512 ".long 671f - .\n"
513 ".previous\n"
514 "671:"
515 "\n\tlock; "
516 "bts %1,%0": "+m" (*__cil_tmp3): "Ir" (nr): "memory");
517#line 71
518 return;
519}
520}
521#line 100 "include/linux/printk.h"
522extern int ( printk)(char const *fmt , ...) ;
523#line 202 "include/linux/kernel.h"
524extern __attribute__((__noreturn__)) void ( panic)(char const *fmt
525 , ...) ;
526#line 152 "include/linux/mutex.h"
527void mutex_lock(struct mutex *lock ) ;
528#line 153
529int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
530#line 154
531int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
532#line 168
533int mutex_trylock(struct mutex *lock ) ;
534#line 169
535void mutex_unlock(struct mutex *lock ) ;
536#line 170
537int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
538#line 82 "include/linux/jiffies.h"
539extern unsigned long volatile jiffies __attribute__((__section__(".data"))) ;
540#line 36 "include/linux/timer.h"
541extern struct tvec_base boot_tvec_bases ;
542#line 210
543extern int del_timer(struct timer_list *timer ) ;
544#line 211
545extern int mod_timer(struct timer_list *timer , unsigned long expires ) ;
546#line 356 "include/linux/moduleparam.h"
547extern struct kernel_param_ops param_ops_int ;
548#line 361
549extern struct kernel_param_ops param_ops_uint ;
550#line 382
551extern struct kernel_param_ops param_ops_bool ;
552#line 26 "include/linux/export.h"
553extern struct module __this_module ;
554#line 67 "include/linux/module.h"
555int init_module(void) ;
556#line 68
557void cleanup_module(void) ;
558#line 132 "include/linux/watchdog.h"
559__inline static void watchdog_set_nowayout(struct watchdog_device *wdd , bool nowayout ) __attribute__((__no_instrument_function__)) ;
560#line 132 "include/linux/watchdog.h"
561__inline static void watchdog_set_nowayout(struct watchdog_device *wdd , bool nowayout )
562{ unsigned long __cil_tmp3 ;
563 unsigned long __cil_tmp4 ;
564 unsigned long *__cil_tmp5 ;
565 unsigned long volatile *__cil_tmp6 ;
566
567 {
568#line 134
569 if (nowayout) {
570 {
571#line 135
572 __cil_tmp3 = (unsigned long )wdd;
573#line 135
574 __cil_tmp4 = __cil_tmp3 + 40;
575#line 135
576 __cil_tmp5 = (unsigned long *)__cil_tmp4;
577#line 135
578 __cil_tmp6 = (unsigned long volatile *)__cil_tmp5;
579#line 135
580 set_bit(3U, __cil_tmp6);
581 }
582 } else {
583
584 }
585#line 136
586 return;
587}
588}
589#line 150
590extern int watchdog_register_device(struct watchdog_device * ) ;
591#line 151
592extern void watchdog_unregister_device(struct watchdog_device * ) ;
593#line 47 "include/linux/reboot.h"
594extern int register_reboot_notifier(struct notifier_block * ) ;
595#line 48
596extern int unregister_reboot_notifier(struct notifier_block * ) ;
597#line 84
598extern void emergency_restart(void) ;
599#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
600static unsigned int soft_margin = 60U;
601#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
602static char const __param_str_soft_margin[12] =
603#line 56
604 { (char const )'s', (char const )'o', (char const )'f', (char const )'t',
605 (char const )'_', (char const )'m', (char const )'a', (char const )'r',
606 (char const )'g', (char const )'i', (char const )'n', (char const )'\000'};
607#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
608static struct kernel_param const __param_soft_margin __attribute__((__used__, __unused__,
609__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_soft_margin, (struct kernel_param_ops const *)(& param_ops_uint),
610 (u16 )0, (s16 )0, {(void *)(& soft_margin)}};
611#line 56 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
612static char const __mod_soft_margintype56[26] __attribute__((__used__, __unused__,
613__section__(".modinfo"), __aligned__(1))) =
614#line 56
615 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
616 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
617 (char const )'=', (char const )'s', (char const )'o', (char const )'f',
618 (char const )'t', (char const )'_', (char const )'m', (char const )'a',
619 (char const )'r', (char const )'g', (char const )'i', (char const )'n',
620 (char const )':', (char const )'u', (char const )'i', (char const )'n',
621 (char const )'t', (char const )'\000'};
622#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
623static char const __mod_soft_margin59[88] __attribute__((__used__, __unused__,
624__section__(".modinfo"), __aligned__(1))) =
625#line 57
626 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
627 (char const )'=', (char const )'s', (char const )'o', (char const )'f',
628 (char const )'t', (char const )'_', (char const )'m', (char const )'a',
629 (char const )'r', (char const )'g', (char const )'i', (char const )'n',
630 (char const )':', (char const )'W', (char const )'a', (char const )'t',
631 (char const )'c', (char const )'h', (char const )'d', (char const )'o',
632 (char const )'g', (char const )' ', (char const )'s', (char const )'o',
633 (char const )'f', (char const )'t', (char const )'_', (char const )'m',
634 (char const )'a', (char const )'r', (char const )'g', (char const )'i',
635 (char const )'n', (char const )' ', (char const )'i', (char const )'n',
636 (char const )' ', (char const )'s', (char const )'e', (char const )'c',
637 (char const )'o', (char const )'n', (char const )'d', (char const )'s',
638 (char const )'.', (char const )' ', (char const )'(', (char const )'0',
639 (char const )' ', (char const )'<', (char const )' ', (char const )'s',
640 (char const )'o', (char const )'f', (char const )'t', (char const )'_',
641 (char const )'m', (char const )'a', (char const )'r', (char const )'g',
642 (char const )'i', (char const )'n', (char const )' ', (char const )'<',
643 (char const )' ', (char const )'6', (char const )'5', (char const )'5',
644 (char const )'3', (char const )'6', (char const )',', (char const )' ',
645 (char const )'d', (char const )'e', (char const )'f', (char const )'a',
646 (char const )'u', (char const )'l', (char const )'t', (char const )'=',
647 (char const )'6', (char const )'0', (char const )')', (char const )'\000'};
648#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
649static bool nowayout = (bool )1;
650#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
651static char const __param_str_nowayout[9] =
652#line 62
653 { (char const )'n', (char const )'o', (char const )'w', (char const )'a',
654 (char const )'y', (char const )'o', (char const )'u', (char const )'t',
655 (char const )'\000'};
656#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
657static struct kernel_param const __param_nowayout __attribute__((__used__, __unused__,
658__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_nowayout, (struct kernel_param_ops const *)(& param_ops_bool), (u16 )0,
659 (s16 )0, {(void *)(& nowayout)}};
660#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
661static char const __mod_nowayouttype62[23] __attribute__((__used__, __unused__,
662__section__(".modinfo"), __aligned__(1))) =
663#line 62
664 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
665 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
666 (char const )'=', (char const )'n', (char const )'o', (char const )'w',
667 (char const )'a', (char const )'y', (char const )'o', (char const )'u',
668 (char const )'t', (char const )':', (char const )'b', (char const )'o',
669 (char const )'o', (char const )'l', (char const )'\000'};
670#line 63 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
671static char const __mod_nowayout65[66] __attribute__((__used__, __unused__, __section__(".modinfo"),
672__aligned__(1))) =
673#line 63
674 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
675 (char const )'=', (char const )'n', (char const )'o', (char const )'w',
676 (char const )'a', (char const )'y', (char const )'o', (char const )'u',
677 (char const )'t', (char const )':', (char const )'W', (char const )'a',
678 (char const )'t', (char const )'c', (char const )'h', (char const )'d',
679 (char const )'o', (char const )'g', (char const )' ', (char const )'c',
680 (char const )'a', (char const )'n', (char const )'n', (char const )'o',
681 (char const )'t', (char const )' ', (char const )'b', (char const )'e',
682 (char const )' ', (char const )'s', (char const )'t', (char const )'o',
683 (char const )'p', (char const )'p', (char const )'e', (char const )'d',
684 (char const )' ', (char const )'o', (char const )'n', (char const )'c',
685 (char const )'e', (char const )' ', (char const )'s', (char const )'t',
686 (char const )'a', (char const )'r', (char const )'t', (char const )'e',
687 (char const )'d', (char const )' ', (char const )'(', (char const )'d',
688 (char const )'e', (char const )'f', (char const )'a', (char const )'u',
689 (char const )'l', (char const )'t', (char const )'=', (char const )'1',
690 (char const )')', (char const )'\000'};
691#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
692static int soft_noboot = 0;
693#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
694static char const __param_str_soft_noboot[12] =
695#line 68
696 { (char const )'s', (char const )'o', (char const )'f', (char const )'t',
697 (char const )'_', (char const )'n', (char const )'o', (char const )'b',
698 (char const )'o', (char const )'o', (char const )'t', (char const )'\000'};
699#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
700static struct kernel_param const __param_soft_noboot __attribute__((__used__, __unused__,
701__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_soft_noboot, (struct kernel_param_ops const *)(& param_ops_int),
702 (u16 )0, (s16 )0, {(void *)(& soft_noboot)}};
703#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
704static char const __mod_soft_noboottype68[25] __attribute__((__used__, __unused__,
705__section__(".modinfo"), __aligned__(1))) =
706#line 68
707 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
708 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
709 (char const )'=', (char const )'s', (char const )'o', (char const )'f',
710 (char const )'t', (char const )'_', (char const )'n', (char const )'o',
711 (char const )'b', (char const )'o', (char const )'o', (char const )'t',
712 (char const )':', (char const )'i', (char const )'n', (char const )'t',
713 (char const )'\000'};
714#line 69 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
715static char const __mod_soft_noboot70[85] __attribute__((__used__, __unused__,
716__section__(".modinfo"), __aligned__(1))) =
717#line 69
718 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
719 (char const )'=', (char const )'s', (char const )'o', (char const )'f',
720 (char const )'t', (char const )'_', (char const )'n', (char const )'o',
721 (char const )'b', (char const )'o', (char const )'o', (char const )'t',
722 (char const )':', (char const )'S', (char const )'o', (char const )'f',
723 (char const )'t', (char const )'d', (char const )'o', (char const )'g',
724 (char const )' ', (char const )'a', (char const )'c', (char const )'t',
725 (char const )'i', (char const )'o', (char const )'n', (char const )',',
726 (char const )' ', (char const )'s', (char const )'e', (char const )'t',
727 (char const )' ', (char const )'t', (char const )'o', (char const )' ',
728 (char const )'1', (char const )' ', (char const )'t', (char const )'o',
729 (char const )' ', (char const )'i', (char const )'g', (char const )'n',
730 (char const )'o', (char const )'r', (char const )'e', (char const )' ',
731 (char const )'r', (char const )'e', (char const )'b', (char const )'o',
732 (char const )'o', (char const )'t', (char const )'s', (char const )',',
733 (char const )' ', (char const )'0', (char const )' ', (char const )'t',
734 (char const )'o', (char const )' ', (char const )'r', (char const )'e',
735 (char const )'b', (char const )'o', (char const )'o', (char const )'t',
736 (char const )' ', (char const )'(', (char const )'d', (char const )'e',
737 (char const )'f', (char const )'a', (char const )'u', (char const )'l',
738 (char const )'t', (char const )'=', (char const )'0', (char const )')',
739 (char const )'\000'};
740#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
741static int soft_panic ;
742#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
743static char const __param_str_soft_panic[11] =
744#line 73
745 { (char const )'s', (char const )'o', (char const )'f', (char const )'t',
746 (char const )'_', (char const )'p', (char const )'a', (char const )'n',
747 (char const )'i', (char const )'c', (char const )'\000'};
748#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
749static struct kernel_param const __param_soft_panic __attribute__((__used__, __unused__,
750__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_soft_panic, (struct kernel_param_ops const *)(& param_ops_int),
751 (u16 )0, (s16 )0, {(void *)(& soft_panic)}};
752#line 73 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
753static char const __mod_soft_panictype73[24] __attribute__((__used__, __unused__,
754__section__(".modinfo"), __aligned__(1))) =
755#line 73
756 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
757 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
758 (char const )'=', (char const )'s', (char const )'o', (char const )'f',
759 (char const )'t', (char const )'_', (char const )'p', (char const )'a',
760 (char const )'n', (char const )'i', (char const )'c', (char const )':',
761 (char const )'i', (char const )'n', (char const )'t', (char const )'\000'};
762#line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
763static char const __mod_soft_panic75[75] __attribute__((__used__, __unused__, __section__(".modinfo"),
764__aligned__(1))) =
765#line 74
766 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
767 (char const )'=', (char const )'s', (char const )'o', (char const )'f',
768 (char const )'t', (char const )'_', (char const )'p', (char const )'a',
769 (char const )'n', (char const )'i', (char const )'c', (char const )':',
770 (char const )'S', (char const )'o', (char const )'f', (char const )'t',
771 (char const )'d', (char const )'o', (char const )'g', (char const )' ',
772 (char const )'a', (char const )'c', (char const )'t', (char const )'i',
773 (char const )'o', (char const )'n', (char const )',', (char const )' ',
774 (char const )'s', (char const )'e', (char const )'t', (char const )' ',
775 (char const )'t', (char const )'o', (char const )' ', (char const )'1',
776 (char const )' ', (char const )'t', (char const )'o', (char const )' ',
777 (char const )'p', (char const )'a', (char const )'n', (char const )'i',
778 (char const )'c', (char const )',', (char const )' ', (char const )'0',
779 (char const )' ', (char const )'t', (char const )'o', (char const )' ',
780 (char const )'r', (char const )'e', (char const )'b', (char const )'o',
781 (char const )'o', (char const )'t', (char const )' ', (char const )'(',
782 (char const )'d', (char const )'e', (char const )'f', (char const )'a',
783 (char const )'u', (char const )'l', (char const )'t', (char const )'=',
784 (char const )'0', (char const )')', (char const )'\000'};
785#line 81
786static void watchdog_fire(unsigned long data ) ;
787#line 83 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
788static struct timer_list watchdog_ticktock =
789#line 83
790 {{(struct list_head *)0, (struct list_head *)((void *)1953723489)}, 0UL, & boot_tvec_bases,
791 & watchdog_fire, 0UL, -1, 0, (void *)0, {(char)0, (char)0, (char)0, (char)0, (char)0,
792 (char)0, (char)0, (char)0, (char)0, (char)0,
793 (char)0, (char)0, (char)0, (char)0, (char)0,
794 (char)0}};
795#line 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
796static void watchdog_fire(unsigned long data )
797{ int *__cil_tmp2 ;
798 int *__cil_tmp3 ;
799
800 {
801 {
802#line 92
803 __cil_tmp2 = & soft_noboot;
804#line 92
805 if (*__cil_tmp2) {
806 {
807#line 93
808 printk("<2>softdog: Triggered - Reboot ignored\n");
809 }
810 } else {
811 {
812#line 94
813 __cil_tmp3 = & soft_panic;
814#line 94
815 if (*__cil_tmp3) {
816 {
817#line 95
818 printk("<2>softdog: Initiating panic\n");
819#line 96
820 panic("Software Watchdog Timer expired");
821 }
822 } else {
823 {
824#line 98
825 printk("<2>softdog: Initiating system reboot\n");
826#line 99
827 emergency_restart();
828#line 100
829 printk("<2>softdog: Reboot didn\'t ?????\n");
830 }
831 }
832 }
833 }
834 }
835#line 102
836 return;
837}
838}
839#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
840static int softdog_ping(struct watchdog_device *w )
841{ unsigned long __cil_tmp2 ;
842 unsigned long __cil_tmp3 ;
843 unsigned int __cil_tmp4 ;
844 unsigned int __cil_tmp5 ;
845 unsigned long volatile __cil_tmp6 ;
846 unsigned long volatile __cil_tmp7 ;
847 unsigned long __cil_tmp8 ;
848
849 {
850 {
851#line 110
852 __cil_tmp2 = (unsigned long )w;
853#line 110
854 __cil_tmp3 = __cil_tmp2 + 20;
855#line 110
856 __cil_tmp4 = *((unsigned int *)__cil_tmp3);
857#line 110
858 __cil_tmp5 = __cil_tmp4 * 250U;
859#line 110
860 __cil_tmp6 = (unsigned long volatile )__cil_tmp5;
861#line 110
862 __cil_tmp7 = jiffies + __cil_tmp6;
863#line 110
864 __cil_tmp8 = (unsigned long )__cil_tmp7;
865#line 110
866 mod_timer(& watchdog_ticktock, __cil_tmp8);
867 }
868#line 111
869 return (0);
870}
871}
872#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
873static int softdog_stop(struct watchdog_device *w )
874{
875
876 {
877 {
878#line 116
879 del_timer(& watchdog_ticktock);
880 }
881#line 117
882 return (0);
883}
884}
885#line 120 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
886static int softdog_set_timeout(struct watchdog_device *w , unsigned int t )
887{ unsigned long __cil_tmp3 ;
888 unsigned long __cil_tmp4 ;
889
890 {
891#line 122
892 __cil_tmp3 = (unsigned long )w;
893#line 122
894 __cil_tmp4 = __cil_tmp3 + 20;
895#line 122
896 *((unsigned int *)__cil_tmp4) = t;
897#line 123
898 return (0);
899}
900}
901#line 130 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
902static int softdog_notify_sys(struct notifier_block *this , unsigned long code , void *unused )
903{ void *__cil_tmp4 ;
904 struct watchdog_device *__cil_tmp5 ;
905 void *__cil_tmp6 ;
906 struct watchdog_device *__cil_tmp7 ;
907
908 {
909#line 133
910 if (code == 1UL) {
911 {
912#line 135
913 __cil_tmp4 = (void *)0;
914#line 135
915 __cil_tmp5 = (struct watchdog_device *)__cil_tmp4;
916#line 135
917 softdog_stop(__cil_tmp5);
918 }
919 } else
920#line 133
921 if (code == 2UL) {
922 {
923#line 135
924 __cil_tmp6 = (void *)0;
925#line 135
926 __cil_tmp7 = (struct watchdog_device *)__cil_tmp6;
927#line 135
928 softdog_stop(__cil_tmp7);
929 }
930 } else {
931
932 }
933#line 136
934 return (0);
935}
936}
937#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
938static struct notifier_block softdog_notifier = {& softdog_notify_sys, (struct notifier_block *)0, 0};
939#line 147 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
940static struct watchdog_info softdog_info = {(__u32 )33152, 0U, {(__u8 )'S', (__u8 )'o', (__u8 )'f', (__u8 )'t', (__u8 )'w',
941 (__u8 )'a', (__u8 )'r', (__u8 )'e', (__u8 )' ', (__u8 )'W',
942 (__u8 )'a', (__u8 )'t', (__u8 )'c', (__u8 )'h', (__u8 )'d',
943 (__u8 )'o', (__u8 )'g', (__u8 )'\000', (unsigned char)0, (unsigned char)0,
944 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
945 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
946 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0}};
947#line 152 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
948static struct watchdog_ops softdog_ops =
949#line 152
950 {& __this_module, & softdog_ping, & softdog_stop, & softdog_ping, (unsigned int (*)(struct watchdog_device * ))0,
951 & softdog_set_timeout, (unsigned int (*)(struct watchdog_device * ))0, (long (*)(struct watchdog_device * ,
952 unsigned int ,
953 unsigned long ))0};
954#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
955static struct watchdog_device softdog_dev =
956#line 160
957 {(struct watchdog_info const *)(& softdog_info), (struct watchdog_ops const *)(& softdog_ops),
958 0U, 0U, 1U, 65535U, (void *)0, 0UL};
959#line 167
960static int watchdog_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
961#line 167 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
962static int watchdog_init(void)
963{ int ret ;
964 unsigned int *__cil_tmp2 ;
965 unsigned int __cil_tmp3 ;
966 unsigned int *__cil_tmp4 ;
967 unsigned int __cil_tmp5 ;
968 unsigned long __cil_tmp6 ;
969 unsigned int *__cil_tmp7 ;
970 bool *__cil_tmp8 ;
971 bool __cil_tmp9 ;
972 int *__cil_tmp10 ;
973 int __cil_tmp11 ;
974 unsigned int *__cil_tmp12 ;
975 unsigned int __cil_tmp13 ;
976 int *__cil_tmp14 ;
977 int __cil_tmp15 ;
978 bool *__cil_tmp16 ;
979 bool __cil_tmp17 ;
980 int __cil_tmp18 ;
981
982 {
983 {
984#line 173
985 __cil_tmp2 = & soft_margin;
986#line 173
987 __cil_tmp3 = *__cil_tmp2;
988#line 173
989 if (__cil_tmp3 < 1U) {
990 {
991#line 174
992 printk("<6>softdog: soft_margin must be 0 < soft_margin < 65536, using %d\n",
993 60);
994 }
995#line 176
996 return (-22);
997 } else {
998 {
999#line 173
1000 __cil_tmp4 = & soft_margin;
1001#line 173
1002 __cil_tmp5 = *__cil_tmp4;
1003#line 173
1004 if (__cil_tmp5 > 65535U) {
1005 {
1006#line 174
1007 printk("<6>softdog: soft_margin must be 0 < soft_margin < 65536, using %d\n",
1008 60);
1009 }
1010#line 176
1011 return (-22);
1012 } else {
1013
1014 }
1015 }
1016 }
1017 }
1018 {
1019#line 178
1020 __cil_tmp6 = (unsigned long )(& softdog_dev) + 20;
1021#line 178
1022 __cil_tmp7 = & soft_margin;
1023#line 178
1024 *((unsigned int *)__cil_tmp6) = *__cil_tmp7;
1025#line 180
1026 __cil_tmp8 = & nowayout;
1027#line 180
1028 __cil_tmp9 = *__cil_tmp8;
1029#line 180
1030 watchdog_set_nowayout(& softdog_dev, __cil_tmp9);
1031#line 182
1032 ret = register_reboot_notifier(& softdog_notifier);
1033 }
1034#line 183
1035 if (ret) {
1036 {
1037#line 184
1038 printk("<3>softdog: cannot register reboot notifier (err=%d)\n", ret);
1039 }
1040#line 185
1041 return (ret);
1042 } else {
1043
1044 }
1045 {
1046#line 188
1047 ret = watchdog_register_device(& softdog_dev);
1048 }
1049#line 189
1050 if (ret) {
1051 {
1052#line 190
1053 unregister_reboot_notifier(& softdog_notifier);
1054 }
1055#line 191
1056 return (ret);
1057 } else {
1058
1059 }
1060 {
1061#line 194
1062 __cil_tmp10 = & soft_noboot;
1063#line 194
1064 __cil_tmp11 = *__cil_tmp10;
1065#line 194
1066 __cil_tmp12 = & soft_margin;
1067#line 194
1068 __cil_tmp13 = *__cil_tmp12;
1069#line 194
1070 __cil_tmp14 = & soft_panic;
1071#line 194
1072 __cil_tmp15 = *__cil_tmp14;
1073#line 194
1074 __cil_tmp16 = & nowayout;
1075#line 194
1076 __cil_tmp17 = *__cil_tmp16;
1077#line 194
1078 __cil_tmp18 = (int )__cil_tmp17;
1079#line 194
1080 printk("<6>softdog: Software Watchdog Timer: 0.08 initialized. soft_noboot=%d soft_margin=%d sec soft_panic=%d (nowayout=%d)\n",
1081 __cil_tmp11, __cil_tmp13, __cil_tmp15, __cil_tmp18);
1082 }
1083#line 197
1084 return (0);
1085}
1086}
1087#line 200
1088static void watchdog_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
1089#line 200 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1090static void watchdog_exit(void)
1091{
1092
1093 {
1094 {
1095#line 202
1096 watchdog_unregister_device(& softdog_dev);
1097#line 203
1098 unregister_reboot_notifier(& softdog_notifier);
1099 }
1100#line 204
1101 return;
1102}
1103}
1104#line 206 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1105int init_module(void)
1106{ int tmp ;
1107
1108 {
1109 {
1110#line 206
1111 tmp = watchdog_init();
1112 }
1113#line 206
1114 return (tmp);
1115}
1116}
1117#line 207 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1118void cleanup_module(void)
1119{
1120
1121 {
1122 {
1123#line 207
1124 watchdog_exit();
1125 }
1126#line 207
1127 return;
1128}
1129}
1130#line 209 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1131static char const __mod_author209[16] __attribute__((__used__, __unused__, __section__(".modinfo"),
1132__aligned__(1))) =
1133#line 209
1134 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
1135 (char const )'o', (char const )'r', (char const )'=', (char const )'A',
1136 (char const )'l', (char const )'a', (char const )'n', (char const )' ',
1137 (char const )'C', (char const )'o', (char const )'x', (char const )'\000'};
1138#line 210 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1139static char const __mod_description210[44] __attribute__((__used__, __unused__,
1140__section__(".modinfo"), __aligned__(1))) =
1141#line 210
1142 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
1143 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
1144 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
1145 (char const )'S', (char const )'o', (char const )'f', (char const )'t',
1146 (char const )'w', (char const )'a', (char const )'r', (char const )'e',
1147 (char const )' ', (char const )'W', (char const )'a', (char const )'t',
1148 (char const )'c', (char const )'h', (char const )'d', (char const )'o',
1149 (char const )'g', (char const )' ', (char const )'D', (char const )'e',
1150 (char const )'v', (char const )'i', (char const )'c', (char const )'e',
1151 (char const )' ', (char const )'D', (char const )'r', (char const )'i',
1152 (char const )'v', (char const )'e', (char const )'r', (char const )'\000'};
1153#line 211 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1154static char const __mod_license211[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
1155__aligned__(1))) =
1156#line 211
1157 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
1158 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
1159 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
1160#line 212 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1161static char const __mod_alias212[24] __attribute__((__used__, __unused__, __section__(".modinfo"),
1162__aligned__(1))) =
1163#line 212
1164 { (char const )'a', (char const )'l', (char const )'i', (char const )'a',
1165 (char const )'s', (char const )'=', (char const )'c', (char const )'h',
1166 (char const )'a', (char const )'r', (char const )'-', (char const )'m',
1167 (char const )'a', (char const )'j', (char const )'o', (char const )'r',
1168 (char const )'-', (char const )'1', (char const )'0', (char const )'-',
1169 (char const )'1', (char const )'3', (char const )'0', (char const )'\000'};
1170#line 230
1171void ldv_check_final_state(void) ;
1172#line 236
1173extern void ldv_initialize(void) ;
1174#line 239
1175extern int __VERIFIER_nondet_int(void) ;
1176#line 242 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1177int LDV_IN_INTERRUPT ;
1178#line 245 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1179void main(void)
1180{ struct notifier_block *var_group1 ;
1181 unsigned long var_softdog_notify_sys_4_p1 ;
1182 void *var_softdog_notify_sys_4_p2 ;
1183 struct watchdog_device *var_group2 ;
1184 unsigned int var_softdog_set_timeout_3_p1 ;
1185 int tmp ;
1186 int tmp___0 ;
1187 int tmp___1 ;
1188
1189 {
1190 {
1191#line 291
1192 LDV_IN_INTERRUPT = 1;
1193#line 300
1194 ldv_initialize();
1195#line 309
1196 tmp = watchdog_init();
1197 }
1198#line 309
1199 if (tmp) {
1200#line 310
1201 goto ldv_final;
1202 } else {
1203
1204 }
1205 {
1206#line 316
1207 while (1) {
1208 while_continue: ;
1209 {
1210#line 316
1211 tmp___1 = __VERIFIER_nondet_int();
1212 }
1213#line 316
1214 if (tmp___1) {
1215
1216 } else {
1217#line 316
1218 goto while_break;
1219 }
1220 {
1221#line 319
1222 tmp___0 = __VERIFIER_nondet_int();
1223 }
1224#line 321
1225 if (tmp___0 == 0) {
1226#line 321
1227 goto case_0;
1228 } else
1229#line 340
1230 if (tmp___0 == 1) {
1231#line 340
1232 goto case_1;
1233 } else
1234#line 359
1235 if (tmp___0 == 2) {
1236#line 359
1237 goto case_2;
1238 } else
1239#line 378
1240 if (tmp___0 == 3) {
1241#line 378
1242 goto case_3;
1243 } else {
1244 {
1245#line 397
1246 goto switch_default;
1247#line 319
1248 if (0) {
1249 case_0:
1250 {
1251#line 332
1252 softdog_notify_sys(var_group1, var_softdog_notify_sys_4_p1, var_softdog_notify_sys_4_p2);
1253 }
1254#line 339
1255 goto switch_break;
1256 case_1:
1257 {
1258#line 351
1259 softdog_ping(var_group2);
1260 }
1261#line 358
1262 goto switch_break;
1263 case_2:
1264 {
1265#line 370
1266 softdog_stop(var_group2);
1267 }
1268#line 377
1269 goto switch_break;
1270 case_3:
1271 {
1272#line 389
1273 softdog_set_timeout(var_group2, var_softdog_set_timeout_3_p1);
1274 }
1275#line 396
1276 goto switch_break;
1277 switch_default:
1278#line 397
1279 goto switch_break;
1280 } else {
1281 switch_break: ;
1282 }
1283 }
1284 }
1285 }
1286 while_break: ;
1287 }
1288 {
1289#line 412
1290 watchdog_exit();
1291 }
1292 ldv_final:
1293 {
1294#line 415
1295 ldv_check_final_state();
1296 }
1297#line 418
1298 return;
1299}
1300}
1301#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1302void ldv_blast_assert(void)
1303{
1304
1305 {
1306 ERROR:
1307#line 6
1308 goto ERROR;
1309}
1310}
1311#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1312extern int __VERIFIER_nondet_int(void) ;
1313#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1314int ldv_mutex = 1;
1315#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1316int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1317{ int nondetermined ;
1318
1319 {
1320#line 29
1321 if (ldv_mutex == 1) {
1322
1323 } else {
1324 {
1325#line 29
1326 ldv_blast_assert();
1327 }
1328 }
1329 {
1330#line 32
1331 nondetermined = __VERIFIER_nondet_int();
1332 }
1333#line 35
1334 if (nondetermined) {
1335#line 38
1336 ldv_mutex = 2;
1337#line 40
1338 return (0);
1339 } else {
1340#line 45
1341 return (-4);
1342 }
1343}
1344}
1345#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1346int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1347{ int nondetermined ;
1348
1349 {
1350#line 57
1351 if (ldv_mutex == 1) {
1352
1353 } else {
1354 {
1355#line 57
1356 ldv_blast_assert();
1357 }
1358 }
1359 {
1360#line 60
1361 nondetermined = __VERIFIER_nondet_int();
1362 }
1363#line 63
1364 if (nondetermined) {
1365#line 66
1366 ldv_mutex = 2;
1367#line 68
1368 return (0);
1369 } else {
1370#line 73
1371 return (-4);
1372 }
1373}
1374}
1375#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1376int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1377{ int atomic_value_after_dec ;
1378
1379 {
1380#line 83
1381 if (ldv_mutex == 1) {
1382
1383 } else {
1384 {
1385#line 83
1386 ldv_blast_assert();
1387 }
1388 }
1389 {
1390#line 86
1391 atomic_value_after_dec = __VERIFIER_nondet_int();
1392 }
1393#line 89
1394 if (atomic_value_after_dec == 0) {
1395#line 92
1396 ldv_mutex = 2;
1397#line 94
1398 return (1);
1399 } else {
1400
1401 }
1402#line 98
1403 return (0);
1404}
1405}
1406#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1407void mutex_lock(struct mutex *lock )
1408{
1409
1410 {
1411#line 108
1412 if (ldv_mutex == 1) {
1413
1414 } else {
1415 {
1416#line 108
1417 ldv_blast_assert();
1418 }
1419 }
1420#line 110
1421 ldv_mutex = 2;
1422#line 111
1423 return;
1424}
1425}
1426#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1427int mutex_trylock(struct mutex *lock )
1428{ int nondetermined ;
1429
1430 {
1431#line 121
1432 if (ldv_mutex == 1) {
1433
1434 } else {
1435 {
1436#line 121
1437 ldv_blast_assert();
1438 }
1439 }
1440 {
1441#line 124
1442 nondetermined = __VERIFIER_nondet_int();
1443 }
1444#line 127
1445 if (nondetermined) {
1446#line 130
1447 ldv_mutex = 2;
1448#line 132
1449 return (1);
1450 } else {
1451#line 137
1452 return (0);
1453 }
1454}
1455}
1456#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1457void mutex_unlock(struct mutex *lock )
1458{
1459
1460 {
1461#line 147
1462 if (ldv_mutex == 2) {
1463
1464 } else {
1465 {
1466#line 147
1467 ldv_blast_assert();
1468 }
1469 }
1470#line 149
1471 ldv_mutex = 1;
1472#line 150
1473 return;
1474}
1475}
1476#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1477void ldv_check_final_state(void)
1478{
1479
1480 {
1481#line 156
1482 if (ldv_mutex == 1) {
1483
1484 } else {
1485 {
1486#line 156
1487 ldv_blast_assert();
1488 }
1489 }
1490#line 157
1491 return;
1492}
1493}
1494#line 427 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/16422/dscv_tempdir/dscv/ri/32_1/drivers/watchdog/softdog.c.common.c"
1495long s__builtin_expect(long val , long res )
1496{
1497
1498 {
1499#line 428
1500 return (val);
1501}
1502}