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 43 "include/asm-generic/int-ll64.h"
13typedef unsigned char u8;
14#line 45 "include/asm-generic/int-ll64.h"
15typedef short s16;
16#line 46 "include/asm-generic/int-ll64.h"
17typedef unsigned short u16;
18#line 49 "include/asm-generic/int-ll64.h"
19typedef unsigned int u32;
20#line 14 "include/asm-generic/posix_types.h"
21typedef long __kernel_long_t;
22#line 15 "include/asm-generic/posix_types.h"
23typedef unsigned long __kernel_ulong_t;
24#line 75 "include/asm-generic/posix_types.h"
25typedef __kernel_ulong_t __kernel_size_t;
26#line 76 "include/asm-generic/posix_types.h"
27typedef __kernel_long_t __kernel_ssize_t;
28#line 27 "include/linux/types.h"
29typedef unsigned short umode_t;
30#line 38 "include/linux/types.h"
31typedef _Bool bool;
32#line 63 "include/linux/types.h"
33typedef __kernel_size_t size_t;
34#line 68 "include/linux/types.h"
35typedef __kernel_ssize_t ssize_t;
36#line 202 "include/linux/types.h"
37typedef unsigned int gfp_t;
38#line 221 "include/linux/types.h"
39struct __anonstruct_atomic_t_6 {
40 int counter ;
41};
42#line 221 "include/linux/types.h"
43typedef struct __anonstruct_atomic_t_6 atomic_t;
44#line 226 "include/linux/types.h"
45struct __anonstruct_atomic64_t_7 {
46 long counter ;
47};
48#line 226 "include/linux/types.h"
49typedef struct __anonstruct_atomic64_t_7 atomic64_t;
50#line 227 "include/linux/types.h"
51struct list_head {
52 struct list_head *next ;
53 struct list_head *prev ;
54};
55#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
56struct module;
57#line 55
58struct module;
59#line 146 "include/linux/init.h"
60typedef void (*ctor_fn_t)(void);
61#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
62struct page;
63#line 58
64struct page;
65#line 26 "include/asm-generic/getorder.h"
66struct task_struct;
67#line 26
68struct task_struct;
69#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
70struct arch_spinlock;
71#line 327
72struct arch_spinlock;
73#line 306 "include/linux/bitmap.h"
74struct bug_entry {
75 int bug_addr_disp ;
76 int file_disp ;
77 unsigned short line ;
78 unsigned short flags ;
79};
80#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
81struct static_key;
82#line 234
83struct static_key;
84#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
85struct kmem_cache;
86#line 23 "include/asm-generic/atomic-long.h"
87typedef atomic64_t atomic_long_t;
88#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
89typedef u16 __ticket_t;
90#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
91typedef u32 __ticketpair_t;
92#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
93struct __raw_tickets {
94 __ticket_t head ;
95 __ticket_t tail ;
96};
97#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
98union __anonunion_ldv_5907_29 {
99 __ticketpair_t head_tail ;
100 struct __raw_tickets tickets ;
101};
102#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
103struct arch_spinlock {
104 union __anonunion_ldv_5907_29 ldv_5907 ;
105};
106#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
107typedef struct arch_spinlock arch_spinlock_t;
108#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
109struct lockdep_map;
110#line 34
111struct lockdep_map;
112#line 55 "include/linux/debug_locks.h"
113struct stack_trace {
114 unsigned int nr_entries ;
115 unsigned int max_entries ;
116 unsigned long *entries ;
117 int skip ;
118};
119#line 26 "include/linux/stacktrace.h"
120struct lockdep_subclass_key {
121 char __one_byte ;
122};
123#line 53 "include/linux/lockdep.h"
124struct lock_class_key {
125 struct lockdep_subclass_key subkeys[8U] ;
126};
127#line 59 "include/linux/lockdep.h"
128struct lock_class {
129 struct list_head hash_entry ;
130 struct list_head lock_entry ;
131 struct lockdep_subclass_key *key ;
132 unsigned int subclass ;
133 unsigned int dep_gen_id ;
134 unsigned long usage_mask ;
135 struct stack_trace usage_traces[13U] ;
136 struct list_head locks_after ;
137 struct list_head locks_before ;
138 unsigned int version ;
139 unsigned long ops ;
140 char const *name ;
141 int name_version ;
142 unsigned long contention_point[4U] ;
143 unsigned long contending_point[4U] ;
144};
145#line 144 "include/linux/lockdep.h"
146struct lockdep_map {
147 struct lock_class_key *key ;
148 struct lock_class *class_cache[2U] ;
149 char const *name ;
150 int cpu ;
151 unsigned long ip ;
152};
153#line 556 "include/linux/lockdep.h"
154struct raw_spinlock {
155 arch_spinlock_t raw_lock ;
156 unsigned int magic ;
157 unsigned int owner_cpu ;
158 void *owner ;
159 struct lockdep_map dep_map ;
160};
161#line 33 "include/linux/spinlock_types.h"
162struct __anonstruct_ldv_6122_33 {
163 u8 __padding[24U] ;
164 struct lockdep_map dep_map ;
165};
166#line 33 "include/linux/spinlock_types.h"
167union __anonunion_ldv_6123_32 {
168 struct raw_spinlock rlock ;
169 struct __anonstruct_ldv_6122_33 ldv_6122 ;
170};
171#line 33 "include/linux/spinlock_types.h"
172struct spinlock {
173 union __anonunion_ldv_6123_32 ldv_6123 ;
174};
175#line 76 "include/linux/spinlock_types.h"
176typedef struct spinlock spinlock_t;
177#line 188 "include/linux/rcupdate.h"
178struct notifier_block;
179#line 188
180struct notifier_block;
181#line 239 "include/linux/srcu.h"
182struct notifier_block {
183 int (*notifier_call)(struct notifier_block * , unsigned long , void * ) ;
184 struct notifier_block *next ;
185 int priority ;
186};
187#line 341 "include/linux/ktime.h"
188struct tvec_base;
189#line 341
190struct tvec_base;
191#line 342 "include/linux/ktime.h"
192struct timer_list {
193 struct list_head entry ;
194 unsigned long expires ;
195 struct tvec_base *base ;
196 void (*function)(unsigned long ) ;
197 unsigned long data ;
198 int slack ;
199 int start_pid ;
200 void *start_site ;
201 char start_comm[16U] ;
202 struct lockdep_map lockdep_map ;
203};
204#line 18 "include/linux/elf.h"
205typedef __u64 Elf64_Addr;
206#line 19 "include/linux/elf.h"
207typedef __u16 Elf64_Half;
208#line 23 "include/linux/elf.h"
209typedef __u32 Elf64_Word;
210#line 24 "include/linux/elf.h"
211typedef __u64 Elf64_Xword;
212#line 193 "include/linux/elf.h"
213struct elf64_sym {
214 Elf64_Word st_name ;
215 unsigned char st_info ;
216 unsigned char st_other ;
217 Elf64_Half st_shndx ;
218 Elf64_Addr st_value ;
219 Elf64_Xword st_size ;
220};
221#line 201 "include/linux/elf.h"
222typedef struct elf64_sym Elf64_Sym;
223#line 445
224struct sock;
225#line 445
226struct sock;
227#line 446
228struct kobject;
229#line 446
230struct kobject;
231#line 447
232enum kobj_ns_type {
233 KOBJ_NS_TYPE_NONE = 0,
234 KOBJ_NS_TYPE_NET = 1,
235 KOBJ_NS_TYPES = 2
236} ;
237#line 453 "include/linux/elf.h"
238struct kobj_ns_type_operations {
239 enum kobj_ns_type type ;
240 void *(*grab_current_ns)(void) ;
241 void const *(*netlink_ns)(struct sock * ) ;
242 void const *(*initial_ns)(void) ;
243 void (*drop_ns)(void * ) ;
244};
245#line 57 "include/linux/kobject_ns.h"
246struct attribute {
247 char const *name ;
248 umode_t mode ;
249 struct lock_class_key *key ;
250 struct lock_class_key skey ;
251};
252#line 98 "include/linux/sysfs.h"
253struct sysfs_ops {
254 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
255 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
256 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
257};
258#line 117
259struct sysfs_dirent;
260#line 117
261struct sysfs_dirent;
262#line 182 "include/linux/sysfs.h"
263struct kref {
264 atomic_t refcount ;
265};
266#line 49 "include/linux/kobject.h"
267struct kset;
268#line 49
269struct kobj_type;
270#line 49 "include/linux/kobject.h"
271struct kobject {
272 char const *name ;
273 struct list_head entry ;
274 struct kobject *parent ;
275 struct kset *kset ;
276 struct kobj_type *ktype ;
277 struct sysfs_dirent *sd ;
278 struct kref kref ;
279 unsigned char state_initialized : 1 ;
280 unsigned char state_in_sysfs : 1 ;
281 unsigned char state_add_uevent_sent : 1 ;
282 unsigned char state_remove_uevent_sent : 1 ;
283 unsigned char uevent_suppress : 1 ;
284};
285#line 107 "include/linux/kobject.h"
286struct kobj_type {
287 void (*release)(struct kobject * ) ;
288 struct sysfs_ops const *sysfs_ops ;
289 struct attribute **default_attrs ;
290 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
291 void const *(*namespace)(struct kobject * ) ;
292};
293#line 115 "include/linux/kobject.h"
294struct kobj_uevent_env {
295 char *envp[32U] ;
296 int envp_idx ;
297 char buf[2048U] ;
298 int buflen ;
299};
300#line 122 "include/linux/kobject.h"
301struct kset_uevent_ops {
302 int (* const filter)(struct kset * , struct kobject * ) ;
303 char const *(* const name)(struct kset * , struct kobject * ) ;
304 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
305};
306#line 139 "include/linux/kobject.h"
307struct kset {
308 struct list_head list ;
309 spinlock_t list_lock ;
310 struct kobject kobj ;
311 struct kset_uevent_ops const *uevent_ops ;
312};
313#line 215
314struct kernel_param;
315#line 215
316struct kernel_param;
317#line 216 "include/linux/kobject.h"
318struct kernel_param_ops {
319 int (*set)(char const * , struct kernel_param const * ) ;
320 int (*get)(char * , struct kernel_param const * ) ;
321 void (*free)(void * ) ;
322};
323#line 49 "include/linux/moduleparam.h"
324struct kparam_string;
325#line 49
326struct kparam_array;
327#line 49 "include/linux/moduleparam.h"
328union __anonunion_ldv_13363_134 {
329 void *arg ;
330 struct kparam_string const *str ;
331 struct kparam_array const *arr ;
332};
333#line 49 "include/linux/moduleparam.h"
334struct kernel_param {
335 char const *name ;
336 struct kernel_param_ops const *ops ;
337 u16 perm ;
338 s16 level ;
339 union __anonunion_ldv_13363_134 ldv_13363 ;
340};
341#line 61 "include/linux/moduleparam.h"
342struct kparam_string {
343 unsigned int maxlen ;
344 char *string ;
345};
346#line 67 "include/linux/moduleparam.h"
347struct kparam_array {
348 unsigned int max ;
349 unsigned int elemsize ;
350 unsigned int *num ;
351 struct kernel_param_ops const *ops ;
352 void *elem ;
353};
354#line 458 "include/linux/moduleparam.h"
355struct static_key {
356 atomic_t enabled ;
357};
358#line 225 "include/linux/jump_label.h"
359struct tracepoint;
360#line 225
361struct tracepoint;
362#line 226 "include/linux/jump_label.h"
363struct tracepoint_func {
364 void *func ;
365 void *data ;
366};
367#line 29 "include/linux/tracepoint.h"
368struct tracepoint {
369 char const *name ;
370 struct static_key key ;
371 void (*regfunc)(void) ;
372 void (*unregfunc)(void) ;
373 struct tracepoint_func *funcs ;
374};
375#line 86 "include/linux/tracepoint.h"
376struct kernel_symbol {
377 unsigned long value ;
378 char const *name ;
379};
380#line 27 "include/linux/export.h"
381struct mod_arch_specific {
382
383};
384#line 34 "include/linux/module.h"
385struct module_param_attrs;
386#line 34 "include/linux/module.h"
387struct module_kobject {
388 struct kobject kobj ;
389 struct module *mod ;
390 struct kobject *drivers_dir ;
391 struct module_param_attrs *mp ;
392};
393#line 43 "include/linux/module.h"
394struct module_attribute {
395 struct attribute attr ;
396 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
397 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
398 size_t ) ;
399 void (*setup)(struct module * , char const * ) ;
400 int (*test)(struct module * ) ;
401 void (*free)(struct module * ) ;
402};
403#line 69
404struct exception_table_entry;
405#line 69
406struct exception_table_entry;
407#line 198
408enum module_state {
409 MODULE_STATE_LIVE = 0,
410 MODULE_STATE_COMING = 1,
411 MODULE_STATE_GOING = 2
412} ;
413#line 204 "include/linux/module.h"
414struct module_ref {
415 unsigned long incs ;
416 unsigned long decs ;
417};
418#line 219
419struct module_sect_attrs;
420#line 219
421struct module_notes_attrs;
422#line 219
423struct ftrace_event_call;
424#line 219 "include/linux/module.h"
425struct module {
426 enum module_state state ;
427 struct list_head list ;
428 char name[56U] ;
429 struct module_kobject mkobj ;
430 struct module_attribute *modinfo_attrs ;
431 char const *version ;
432 char const *srcversion ;
433 struct kobject *holders_dir ;
434 struct kernel_symbol const *syms ;
435 unsigned long const *crcs ;
436 unsigned int num_syms ;
437 struct kernel_param *kp ;
438 unsigned int num_kp ;
439 unsigned int num_gpl_syms ;
440 struct kernel_symbol const *gpl_syms ;
441 unsigned long const *gpl_crcs ;
442 struct kernel_symbol const *unused_syms ;
443 unsigned long const *unused_crcs ;
444 unsigned int num_unused_syms ;
445 unsigned int num_unused_gpl_syms ;
446 struct kernel_symbol const *unused_gpl_syms ;
447 unsigned long const *unused_gpl_crcs ;
448 struct kernel_symbol const *gpl_future_syms ;
449 unsigned long const *gpl_future_crcs ;
450 unsigned int num_gpl_future_syms ;
451 unsigned int num_exentries ;
452 struct exception_table_entry *extable ;
453 int (*init)(void) ;
454 void *module_init ;
455 void *module_core ;
456 unsigned int init_size ;
457 unsigned int core_size ;
458 unsigned int init_text_size ;
459 unsigned int core_text_size ;
460 unsigned int init_ro_size ;
461 unsigned int core_ro_size ;
462 struct mod_arch_specific arch ;
463 unsigned int taints ;
464 unsigned int num_bugs ;
465 struct list_head bug_list ;
466 struct bug_entry *bug_table ;
467 Elf64_Sym *symtab ;
468 Elf64_Sym *core_symtab ;
469 unsigned int num_symtab ;
470 unsigned int core_num_syms ;
471 char *strtab ;
472 char *core_strtab ;
473 struct module_sect_attrs *sect_attrs ;
474 struct module_notes_attrs *notes_attrs ;
475 char *args ;
476 void *percpu ;
477 unsigned int percpu_size ;
478 unsigned int num_tracepoints ;
479 struct tracepoint * const *tracepoints_ptrs ;
480 unsigned int num_trace_bprintk_fmt ;
481 char const **trace_bprintk_fmt_start ;
482 struct ftrace_event_call **trace_events ;
483 unsigned int num_trace_events ;
484 struct list_head source_list ;
485 struct list_head target_list ;
486 struct task_struct *waiter ;
487 void (*exit)(void) ;
488 struct module_ref *refptr ;
489 ctor_fn_t (**ctors)(void) ;
490 unsigned int num_ctors ;
491};
492#line 88 "include/linux/kmemleak.h"
493struct kmem_cache_cpu {
494 void **freelist ;
495 unsigned long tid ;
496 struct page *page ;
497 struct page *partial ;
498 int node ;
499 unsigned int stat[26U] ;
500};
501#line 55 "include/linux/slub_def.h"
502struct kmem_cache_node {
503 spinlock_t list_lock ;
504 unsigned long nr_partial ;
505 struct list_head partial ;
506 atomic_long_t nr_slabs ;
507 atomic_long_t total_objects ;
508 struct list_head full ;
509};
510#line 66 "include/linux/slub_def.h"
511struct kmem_cache_order_objects {
512 unsigned long x ;
513};
514#line 76 "include/linux/slub_def.h"
515struct kmem_cache {
516 struct kmem_cache_cpu *cpu_slab ;
517 unsigned long flags ;
518 unsigned long min_partial ;
519 int size ;
520 int objsize ;
521 int offset ;
522 int cpu_partial ;
523 struct kmem_cache_order_objects oo ;
524 struct kmem_cache_order_objects max ;
525 struct kmem_cache_order_objects min ;
526 gfp_t allocflags ;
527 int refcount ;
528 void (*ctor)(void * ) ;
529 int inuse ;
530 int align ;
531 int reserved ;
532 char const *name ;
533 struct list_head list ;
534 struct kobject kobj ;
535 int remote_node_defrag_ratio ;
536 struct kmem_cache_node *node[1024U] ;
537};
538#line 63 "include/linux/miscdevice.h"
539struct watchdog_info {
540 __u32 options ;
541 __u32 firmware_version ;
542 __u8 identity[32U] ;
543};
544#line 22 "include/linux/watchdog.h"
545struct watchdog_ops;
546#line 22
547struct watchdog_ops;
548#line 23
549struct watchdog_device;
550#line 23
551struct watchdog_device;
552#line 24 "include/linux/watchdog.h"
553struct watchdog_ops {
554 struct module *owner ;
555 int (*start)(struct watchdog_device * ) ;
556 int (*stop)(struct watchdog_device * ) ;
557 int (*ping)(struct watchdog_device * ) ;
558 unsigned int (*status)(struct watchdog_device * ) ;
559 int (*set_timeout)(struct watchdog_device * , unsigned int ) ;
560 unsigned int (*get_timeleft)(struct watchdog_device * ) ;
561 long (*ioctl)(struct watchdog_device * , unsigned int , unsigned long ) ;
562};
563#line 89 "include/linux/watchdog.h"
564struct watchdog_device {
565 struct watchdog_info const *info ;
566 struct watchdog_ops const *ops ;
567 unsigned int bootstatus ;
568 unsigned int timeout ;
569 unsigned int min_timeout ;
570 unsigned int max_timeout ;
571 void *driver_data ;
572 unsigned long status ;
573};
574#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
575void ldv_spin_lock(void) ;
576#line 3
577void ldv_spin_unlock(void) ;
578#line 4
579int ldv_spin_trylock(void) ;
580#line 60 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
581__inline static void set_bit(unsigned int nr , unsigned long volatile *addr )
582{ long volatile *__cil_tmp3 ;
583
584 {
585#line 68
586 __cil_tmp3 = (long volatile *)addr;
587#line 68
588 __asm__ volatile (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; bts %1,%0": "+m" (*__cil_tmp3): "Ir" (nr): "memory");
589#line 70
590 return;
591}
592}
593#line 101 "include/linux/printk.h"
594extern int printk(char const * , ...) ;
595#line 203 "include/linux/kernel.h"
596extern void panic(char const * , ...) ;
597#line 82 "include/linux/jiffies.h"
598extern unsigned long volatile jiffies ;
599#line 36 "include/linux/timer.h"
600extern struct tvec_base boot_tvec_bases ;
601#line 210
602extern int del_timer(struct timer_list * ) ;
603#line 211
604extern int mod_timer(struct timer_list * , unsigned long ) ;
605#line 26 "include/linux/export.h"
606extern struct module __this_module ;
607#line 220 "include/linux/slub_def.h"
608extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
609#line 223
610void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
611#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
612void ldv_check_alloc_flags(gfp_t flags ) ;
613#line 12
614void ldv_check_alloc_nonatomic(void) ;
615#line 14
616struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
617#line 132 "include/linux/watchdog.h"
618__inline static void watchdog_set_nowayout(struct watchdog_device *wdd , bool nowayout )
619{ unsigned long __cil_tmp3 ;
620 unsigned long __cil_tmp4 ;
621 unsigned long *__cil_tmp5 ;
622 unsigned long volatile *__cil_tmp6 ;
623
624 {
625#line 134
626 if ((int )nowayout) {
627 {
628#line 135
629 __cil_tmp3 = (unsigned long )wdd;
630#line 135
631 __cil_tmp4 = __cil_tmp3 + 40;
632#line 135
633 __cil_tmp5 = (unsigned long *)__cil_tmp4;
634#line 135
635 __cil_tmp6 = (unsigned long volatile *)__cil_tmp5;
636#line 135
637 set_bit(3U, __cil_tmp6);
638 }
639 } else {
640
641 }
642#line 136
643 return;
644}
645}
646#line 150
647extern int watchdog_register_device(struct watchdog_device * ) ;
648#line 151
649extern void watchdog_unregister_device(struct watchdog_device * ) ;
650#line 47 "include/linux/reboot.h"
651extern int register_reboot_notifier(struct notifier_block * ) ;
652#line 48
653extern int unregister_reboot_notifier(struct notifier_block * ) ;
654#line 84
655extern void emergency_restart(void) ;
656#line 69 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
657static unsigned int soft_margin = 60U;
658#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
659static bool nowayout = (bool )1;
660#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
661static int soft_noboot = 0;
662#line 86 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
663static int soft_panic ;
664#line 95
665static void watchdog_fire(unsigned long data ) ;
666#line 97 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
667static struct timer_list watchdog_ticktock =
668#line 97
669 {{(struct list_head *)0, (struct list_head *)1953723489}, 0UL, & boot_tvec_bases,
670 & watchdog_fire, 0UL, -1, 0, (void *)0, {(char)0, (char)0, (char)0, (char)0, (char)0,
671 (char)0, (char)0, (char)0, (char)0, (char)0,
672 (char)0, (char)0, (char)0, (char)0, (char)0,
673 (char)0}, {(struct lock_class_key *)"/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p:98",
674 {(struct lock_class *)0, (struct lock_class *)0},
675 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p:98",
676 0, 0UL}};
677#line 104 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
678static void watchdog_fire(unsigned long data )
679{ int *__cil_tmp2 ;
680 int __cil_tmp3 ;
681 int *__cil_tmp4 ;
682 int __cil_tmp5 ;
683
684 {
685 {
686#line 106
687 __cil_tmp2 = & soft_noboot;
688#line 106
689 __cil_tmp3 = *__cil_tmp2;
690#line 106
691 if (__cil_tmp3 != 0) {
692 {
693#line 107
694 printk("<2>softdog: Triggered - Reboot ignored\n");
695 }
696 } else {
697 {
698#line 108
699 __cil_tmp4 = & soft_panic;
700#line 108
701 __cil_tmp5 = *__cil_tmp4;
702#line 108
703 if (__cil_tmp5 != 0) {
704 {
705#line 109
706 printk("<2>softdog: Initiating panic\n");
707#line 110
708 panic("Software Watchdog Timer expired");
709 }
710 } else {
711 {
712#line 112
713 printk("<2>softdog: Initiating system reboot\n");
714#line 113
715 emergency_restart();
716#line 114
717 printk("<2>softdog: Reboot didn\'t ?????\n");
718 }
719 }
720 }
721 }
722 }
723#line 116
724 return;
725}
726}
727#line 122 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
728static int softdog_ping(struct watchdog_device *w )
729{ unsigned long __cil_tmp2 ;
730 unsigned long __cil_tmp3 ;
731 unsigned long __cil_tmp4 ;
732 unsigned int __cil_tmp5 ;
733 unsigned int __cil_tmp6 ;
734 unsigned long __cil_tmp7 ;
735 unsigned long __cil_tmp8 ;
736
737 {
738 {
739#line 124
740 __cil_tmp2 = (unsigned long )jiffies;
741#line 124
742 __cil_tmp3 = (unsigned long )w;
743#line 124
744 __cil_tmp4 = __cil_tmp3 + 20;
745#line 124
746 __cil_tmp5 = *((unsigned int *)__cil_tmp4);
747#line 124
748 __cil_tmp6 = __cil_tmp5 * 250U;
749#line 124
750 __cil_tmp7 = (unsigned long )__cil_tmp6;
751#line 124
752 __cil_tmp8 = __cil_tmp7 + __cil_tmp2;
753#line 124
754 mod_timer(& watchdog_ticktock, __cil_tmp8);
755 }
756#line 125
757 return (0);
758}
759}
760#line 128 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
761static int softdog_stop(struct watchdog_device *w )
762{
763
764 {
765 {
766#line 130
767 del_timer(& watchdog_ticktock);
768 }
769#line 131
770 return (0);
771}
772}
773#line 134 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
774static int softdog_set_timeout(struct watchdog_device *w , unsigned int t )
775{ unsigned long __cil_tmp3 ;
776 unsigned long __cil_tmp4 ;
777
778 {
779#line 136
780 __cil_tmp3 = (unsigned long )w;
781#line 136
782 __cil_tmp4 = __cil_tmp3 + 20;
783#line 136
784 *((unsigned int *)__cil_tmp4) = t;
785#line 137
786 return (0);
787}
788}
789#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
790static int softdog_notify_sys(struct notifier_block *this , unsigned long code , void *unused )
791{ struct watchdog_device *__cil_tmp4 ;
792 struct watchdog_device *__cil_tmp5 ;
793
794 {
795#line 147
796 if (code == 1UL) {
797 {
798#line 149
799 __cil_tmp4 = (struct watchdog_device *)0;
800#line 149
801 softdog_stop(__cil_tmp4);
802 }
803 } else
804#line 147
805 if (code == 2UL) {
806 {
807#line 149
808 __cil_tmp5 = (struct watchdog_device *)0;
809#line 149
810 softdog_stop(__cil_tmp5);
811 }
812 } else {
813
814 }
815#line 150
816 return (0);
817}
818}
819#line 157 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
820static struct notifier_block softdog_notifier = {& softdog_notify_sys, (struct notifier_block *)0, 0};
821#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
822static struct watchdog_info softdog_info = {33152U, 0U, {(__u8 )'S', (__u8 )'o', (__u8 )'f', (__u8 )'t', (__u8 )'w', (__u8 )'a',
823 (__u8 )'r', (__u8 )'e', (__u8 )' ', (__u8 )'W', (__u8 )'a', (__u8 )'t',
824 (__u8 )'c', (__u8 )'h', (__u8 )'d', (__u8 )'o', (__u8 )'g', (__u8 )'\000',
825 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
826 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
827 (unsigned char)0, (unsigned char)0, (unsigned char)0, (unsigned char)0,
828 (unsigned char)0, (unsigned char)0}};
829#line 166 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
830static struct watchdog_ops softdog_ops =
831#line 166
832 {& __this_module, & softdog_ping, & softdog_stop, & softdog_ping, (unsigned int (*)(struct watchdog_device * ))0,
833 & softdog_set_timeout, (unsigned int (*)(struct watchdog_device * ))0, (long (*)(struct watchdog_device * ,
834 unsigned int ,
835 unsigned long ))0};
836#line 174 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
837static struct watchdog_device softdog_dev =
838#line 174
839 {(struct watchdog_info const *)(& softdog_info), (struct watchdog_ops const *)(& softdog_ops),
840 0U, 0U, 1U, 65535U, (void *)0, 0UL};
841#line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
842static int watchdog_init(void)
843{ int ret ;
844 unsigned int *__cil_tmp2 ;
845 unsigned int __cil_tmp3 ;
846 unsigned int *__cil_tmp4 ;
847 unsigned int __cil_tmp5 ;
848 unsigned long __cil_tmp6 ;
849 unsigned int *__cil_tmp7 ;
850 bool *__cil_tmp8 ;
851 bool __cil_tmp9 ;
852 int __cil_tmp10 ;
853 bool __cil_tmp11 ;
854 int *__cil_tmp12 ;
855 int __cil_tmp13 ;
856 unsigned int *__cil_tmp14 ;
857 unsigned int __cil_tmp15 ;
858 int *__cil_tmp16 ;
859 int __cil_tmp17 ;
860 bool *__cil_tmp18 ;
861 bool __cil_tmp19 ;
862 int __cil_tmp20 ;
863
864 {
865 {
866#line 187
867 __cil_tmp2 = & soft_margin;
868#line 187
869 __cil_tmp3 = *__cil_tmp2;
870#line 187
871 if (__cil_tmp3 == 0U) {
872 {
873#line 188
874 printk("<6>softdog: soft_margin must be 0 < soft_margin < 65536, using %d\n",
875 60);
876 }
877#line 190
878 return (-22);
879 } else {
880 {
881#line 187
882 __cil_tmp4 = & soft_margin;
883#line 187
884 __cil_tmp5 = *__cil_tmp4;
885#line 187
886 if (__cil_tmp5 > 65535U) {
887 {
888#line 188
889 printk("<6>softdog: soft_margin must be 0 < soft_margin < 65536, using %d\n",
890 60);
891 }
892#line 190
893 return (-22);
894 } else {
895
896 }
897 }
898 }
899 }
900 {
901#line 192
902 __cil_tmp6 = (unsigned long )(& softdog_dev) + 20;
903#line 192
904 __cil_tmp7 = & soft_margin;
905#line 192
906 *((unsigned int *)__cil_tmp6) = *__cil_tmp7;
907#line 194
908 __cil_tmp8 = & nowayout;
909#line 194
910 __cil_tmp9 = *__cil_tmp8;
911#line 194
912 __cil_tmp10 = (int )__cil_tmp9;
913#line 194
914 __cil_tmp11 = (bool )__cil_tmp10;
915#line 194
916 watchdog_set_nowayout(& softdog_dev, __cil_tmp11);
917#line 196
918 ret = register_reboot_notifier(& softdog_notifier);
919 }
920#line 197
921 if (ret != 0) {
922 {
923#line 198
924 printk("<3>softdog: cannot register reboot notifier (err=%d)\n", ret);
925 }
926#line 199
927 return (ret);
928 } else {
929
930 }
931 {
932#line 202
933 ret = watchdog_register_device(& softdog_dev);
934 }
935#line 203
936 if (ret != 0) {
937 {
938#line 204
939 unregister_reboot_notifier(& softdog_notifier);
940 }
941#line 205
942 return (ret);
943 } else {
944
945 }
946 {
947#line 208
948 __cil_tmp12 = & soft_noboot;
949#line 208
950 __cil_tmp13 = *__cil_tmp12;
951#line 208
952 __cil_tmp14 = & soft_margin;
953#line 208
954 __cil_tmp15 = *__cil_tmp14;
955#line 208
956 __cil_tmp16 = & soft_panic;
957#line 208
958 __cil_tmp17 = *__cil_tmp16;
959#line 208
960 __cil_tmp18 = & nowayout;
961#line 208
962 __cil_tmp19 = *__cil_tmp18;
963#line 208
964 __cil_tmp20 = (int )__cil_tmp19;
965#line 208
966 printk("<6>softdog: Software Watchdog Timer: 0.08 initialized. soft_noboot=%d soft_margin=%d sec soft_panic=%d (nowayout=%d)\n",
967 __cil_tmp13, __cil_tmp15, __cil_tmp17, __cil_tmp20);
968 }
969#line 211
970 return (0);
971}
972}
973#line 214 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
974static void watchdog_exit(void)
975{
976
977 {
978 {
979#line 216
980 watchdog_unregister_device(& softdog_dev);
981#line 217
982 unregister_reboot_notifier(& softdog_notifier);
983 }
984#line 218
985 return;
986}
987}
988#line 244
989extern void ldv_check_final_state(void) ;
990#line 250
991extern void ldv_initialize(void) ;
992#line 253
993extern int __VERIFIER_nondet_int(void) ;
994#line 256 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
995int LDV_IN_INTERRUPT ;
996#line 259 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
997void main(void)
998{ struct notifier_block *var_group1 ;
999 unsigned long var_softdog_notify_sys_4_p1 ;
1000 void *var_softdog_notify_sys_4_p2 ;
1001 struct watchdog_device *var_group2 ;
1002 unsigned int var_softdog_set_timeout_3_p1 ;
1003 int tmp ;
1004 int tmp___0 ;
1005 int tmp___1 ;
1006
1007 {
1008 {
1009#line 305
1010 LDV_IN_INTERRUPT = 1;
1011#line 314
1012 ldv_initialize();
1013#line 323
1014 tmp = watchdog_init();
1015 }
1016#line 323
1017 if (tmp != 0) {
1018#line 324
1019 goto ldv_final;
1020 } else {
1021
1022 }
1023#line 330
1024 goto ldv_14378;
1025 ldv_14377:
1026 {
1027#line 333
1028 tmp___0 = __VERIFIER_nondet_int();
1029 }
1030#line 335
1031 if (tmp___0 == 0) {
1032#line 335
1033 goto case_0;
1034 } else
1035#line 354
1036 if (tmp___0 == 1) {
1037#line 354
1038 goto case_1;
1039 } else
1040#line 373
1041 if (tmp___0 == 2) {
1042#line 373
1043 goto case_2;
1044 } else
1045#line 392
1046 if (tmp___0 == 3) {
1047#line 392
1048 goto case_3;
1049 } else {
1050 {
1051#line 411
1052 goto switch_default;
1053#line 333
1054 if (0) {
1055 case_0:
1056 {
1057#line 346
1058 softdog_notify_sys(var_group1, var_softdog_notify_sys_4_p1, var_softdog_notify_sys_4_p2);
1059 }
1060#line 353
1061 goto ldv_14372;
1062 case_1:
1063 {
1064#line 365
1065 softdog_ping(var_group2);
1066 }
1067#line 372
1068 goto ldv_14372;
1069 case_2:
1070 {
1071#line 384
1072 softdog_stop(var_group2);
1073 }
1074#line 391
1075 goto ldv_14372;
1076 case_3:
1077 {
1078#line 403
1079 softdog_set_timeout(var_group2, var_softdog_set_timeout_3_p1);
1080 }
1081#line 410
1082 goto ldv_14372;
1083 switch_default: ;
1084#line 411
1085 goto ldv_14372;
1086 } else {
1087 switch_break: ;
1088 }
1089 }
1090 }
1091 ldv_14372: ;
1092 ldv_14378:
1093 {
1094#line 330
1095 tmp___1 = __VERIFIER_nondet_int();
1096 }
1097#line 330
1098 if (tmp___1 != 0) {
1099#line 331
1100 goto ldv_14377;
1101 } else {
1102#line 333
1103 goto ldv_14379;
1104 }
1105 ldv_14379: ;
1106 {
1107#line 426
1108 watchdog_exit();
1109 }
1110 ldv_final:
1111 {
1112#line 429
1113 ldv_check_final_state();
1114 }
1115#line 432
1116 return;
1117}
1118}
1119#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1120void ldv_blast_assert(void)
1121{
1122
1123 {
1124 ERROR: ;
1125#line 6
1126 goto ERROR;
1127}
1128}
1129#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1130extern int __VERIFIER_nondet_int(void) ;
1131#line 453 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
1132int ldv_spin = 0;
1133#line 457 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
1134void ldv_check_alloc_flags(gfp_t flags )
1135{
1136
1137 {
1138#line 460
1139 if (ldv_spin != 0) {
1140#line 460
1141 if (flags != 32U) {
1142 {
1143#line 460
1144 ldv_blast_assert();
1145 }
1146 } else {
1147
1148 }
1149 } else {
1150
1151 }
1152#line 463
1153 return;
1154}
1155}
1156#line 463
1157extern struct page *ldv_some_page(void) ;
1158#line 466 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
1159struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1160{ struct page *tmp ;
1161
1162 {
1163#line 469
1164 if (ldv_spin != 0) {
1165#line 469
1166 if (flags != 32U) {
1167 {
1168#line 469
1169 ldv_blast_assert();
1170 }
1171 } else {
1172
1173 }
1174 } else {
1175
1176 }
1177 {
1178#line 471
1179 tmp = ldv_some_page();
1180 }
1181#line 471
1182 return (tmp);
1183}
1184}
1185#line 475 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
1186void ldv_check_alloc_nonatomic(void)
1187{
1188
1189 {
1190#line 478
1191 if (ldv_spin != 0) {
1192 {
1193#line 478
1194 ldv_blast_assert();
1195 }
1196 } else {
1197
1198 }
1199#line 481
1200 return;
1201}
1202}
1203#line 482 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
1204void ldv_spin_lock(void)
1205{
1206
1207 {
1208#line 485
1209 ldv_spin = 1;
1210#line 486
1211 return;
1212}
1213}
1214#line 489 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
1215void ldv_spin_unlock(void)
1216{
1217
1218 {
1219#line 492
1220 ldv_spin = 0;
1221#line 493
1222 return;
1223}
1224}
1225#line 496 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
1226int ldv_spin_trylock(void)
1227{ int is_lock ;
1228
1229 {
1230 {
1231#line 501
1232 is_lock = __VERIFIER_nondet_int();
1233 }
1234#line 503
1235 if (is_lock != 0) {
1236#line 506
1237 return (0);
1238 } else {
1239#line 511
1240 ldv_spin = 1;
1241#line 513
1242 return (1);
1243 }
1244}
1245}
1246#line 680 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17364/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/softdog.c.p"
1247void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1248{
1249
1250 {
1251 {
1252#line 686
1253 ldv_check_alloc_flags(ldv_func_arg2);
1254#line 688
1255 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1256 }
1257#line 689
1258 return ((void *)0);
1259}
1260}