Showing error 1321

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--watchdog--sc520_wdt.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 3152
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

   1/* Generated by CIL v. 1.3.7 */
   2/* print_CIL_Input is true */
   3
   4#line 19 "include/asm-generic/int-ll64.h"
   5typedef signed char __s8;
   6#line 20 "include/asm-generic/int-ll64.h"
   7typedef unsigned char __u8;
   8#line 22 "include/asm-generic/int-ll64.h"
   9typedef short __s16;
  10#line 23 "include/asm-generic/int-ll64.h"
  11typedef unsigned short __u16;
  12#line 25 "include/asm-generic/int-ll64.h"
  13typedef int __s32;
  14#line 26 "include/asm-generic/int-ll64.h"
  15typedef unsigned int __u32;
  16#line 30 "include/asm-generic/int-ll64.h"
  17typedef unsigned long long __u64;
  18#line 43 "include/asm-generic/int-ll64.h"
  19typedef unsigned char u8;
  20#line 45 "include/asm-generic/int-ll64.h"
  21typedef short s16;
  22#line 46 "include/asm-generic/int-ll64.h"
  23typedef unsigned short u16;
  24#line 48 "include/asm-generic/int-ll64.h"
  25typedef int s32;
  26#line 49 "include/asm-generic/int-ll64.h"
  27typedef unsigned int u32;
  28#line 51 "include/asm-generic/int-ll64.h"
  29typedef long long s64;
  30#line 52 "include/asm-generic/int-ll64.h"
  31typedef unsigned long long u64;
  32#line 14 "include/asm-generic/posix_types.h"
  33typedef long __kernel_long_t;
  34#line 15 "include/asm-generic/posix_types.h"
  35typedef unsigned long __kernel_ulong_t;
  36#line 52 "include/asm-generic/posix_types.h"
  37typedef unsigned int __kernel_uid32_t;
  38#line 53 "include/asm-generic/posix_types.h"
  39typedef unsigned int __kernel_gid32_t;
  40#line 75 "include/asm-generic/posix_types.h"
  41typedef __kernel_ulong_t __kernel_size_t;
  42#line 76 "include/asm-generic/posix_types.h"
  43typedef __kernel_long_t __kernel_ssize_t;
  44#line 91 "include/asm-generic/posix_types.h"
  45typedef long long __kernel_loff_t;
  46#line 92 "include/asm-generic/posix_types.h"
  47typedef __kernel_long_t __kernel_time_t;
  48#line 21 "include/linux/types.h"
  49typedef __u32 __kernel_dev_t;
  50#line 24 "include/linux/types.h"
  51typedef __kernel_dev_t dev_t;
  52#line 27 "include/linux/types.h"
  53typedef unsigned short umode_t;
  54#line 38 "include/linux/types.h"
  55typedef _Bool bool;
  56#line 40 "include/linux/types.h"
  57typedef __kernel_uid32_t uid_t;
  58#line 41 "include/linux/types.h"
  59typedef __kernel_gid32_t gid_t;
  60#line 54 "include/linux/types.h"
  61typedef __kernel_loff_t loff_t;
  62#line 63 "include/linux/types.h"
  63typedef __kernel_size_t size_t;
  64#line 68 "include/linux/types.h"
  65typedef __kernel_ssize_t ssize_t;
  66#line 78 "include/linux/types.h"
  67typedef __kernel_time_t time_t;
  68#line 142 "include/linux/types.h"
  69typedef unsigned long sector_t;
  70#line 143 "include/linux/types.h"
  71typedef unsigned long blkcnt_t;
  72#line 202 "include/linux/types.h"
  73typedef unsigned int gfp_t;
  74#line 203 "include/linux/types.h"
  75typedef unsigned int fmode_t;
  76#line 206 "include/linux/types.h"
  77typedef u64 phys_addr_t;
  78#line 211 "include/linux/types.h"
  79typedef phys_addr_t resource_size_t;
  80#line 221 "include/linux/types.h"
  81struct __anonstruct_atomic_t_6 {
  82   int counter ;
  83};
  84#line 221 "include/linux/types.h"
  85typedef struct __anonstruct_atomic_t_6 atomic_t;
  86#line 226 "include/linux/types.h"
  87struct __anonstruct_atomic64_t_7 {
  88   long counter ;
  89};
  90#line 226 "include/linux/types.h"
  91typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  92#line 227 "include/linux/types.h"
  93struct list_head {
  94   struct list_head *next ;
  95   struct list_head *prev ;
  96};
  97#line 232
  98struct hlist_node;
  99#line 232 "include/linux/types.h"
 100struct hlist_head {
 101   struct hlist_node *first ;
 102};
 103#line 236 "include/linux/types.h"
 104struct hlist_node {
 105   struct hlist_node *next ;
 106   struct hlist_node **pprev ;
 107};
 108#line 247 "include/linux/types.h"
 109struct rcu_head {
 110   struct rcu_head *next ;
 111   void (*func)(struct rcu_head * ) ;
 112};
 113#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
 114struct module;
 115#line 55
 116struct module;
 117#line 146 "include/linux/init.h"
 118typedef void (*ctor_fn_t)(void);
 119#line 46 "include/linux/dynamic_debug.h"
 120struct device;
 121#line 46
 122struct device;
 123#line 348 "include/linux/kernel.h"
 124struct pid;
 125#line 348
 126struct pid;
 127#line 112 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/stat.h"
 128struct timespec;
 129#line 112
 130struct timespec;
 131#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
 132struct page;
 133#line 58
 134struct page;
 135#line 26 "include/asm-generic/getorder.h"
 136struct task_struct;
 137#line 26
 138struct task_struct;
 139#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 140struct file;
 141#line 290
 142struct file;
 143#line 305
 144struct seq_file;
 145#line 305
 146struct seq_file;
 147#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 148struct arch_spinlock;
 149#line 327
 150struct arch_spinlock;
 151#line 306 "include/linux/bitmap.h"
 152struct bug_entry {
 153   int bug_addr_disp ;
 154   int file_disp ;
 155   unsigned short line ;
 156   unsigned short flags ;
 157};
 158#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 159struct static_key;
 160#line 234
 161struct static_key;
 162#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 163struct kmem_cache;
 164#line 23 "include/asm-generic/atomic-long.h"
 165typedef atomic64_t atomic_long_t;
 166#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 167typedef u16 __ticket_t;
 168#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 169typedef u32 __ticketpair_t;
 170#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 171struct __raw_tickets {
 172   __ticket_t head ;
 173   __ticket_t tail ;
 174};
 175#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 176union __anonunion_ldv_5907_29 {
 177   __ticketpair_t head_tail ;
 178   struct __raw_tickets tickets ;
 179};
 180#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 181struct arch_spinlock {
 182   union __anonunion_ldv_5907_29 ldv_5907 ;
 183};
 184#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 185typedef struct arch_spinlock arch_spinlock_t;
 186#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 187struct __anonstruct_ldv_5914_31 {
 188   u32 read ;
 189   s32 write ;
 190};
 191#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 192union __anonunion_arch_rwlock_t_30 {
 193   s64 lock ;
 194   struct __anonstruct_ldv_5914_31 ldv_5914 ;
 195};
 196#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 197typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
 198#line 34
 199struct lockdep_map;
 200#line 34
 201struct lockdep_map;
 202#line 55 "include/linux/debug_locks.h"
 203struct stack_trace {
 204   unsigned int nr_entries ;
 205   unsigned int max_entries ;
 206   unsigned long *entries ;
 207   int skip ;
 208};
 209#line 26 "include/linux/stacktrace.h"
 210struct lockdep_subclass_key {
 211   char __one_byte ;
 212};
 213#line 53 "include/linux/lockdep.h"
 214struct lock_class_key {
 215   struct lockdep_subclass_key subkeys[8U] ;
 216};
 217#line 59 "include/linux/lockdep.h"
 218struct lock_class {
 219   struct list_head hash_entry ;
 220   struct list_head lock_entry ;
 221   struct lockdep_subclass_key *key ;
 222   unsigned int subclass ;
 223   unsigned int dep_gen_id ;
 224   unsigned long usage_mask ;
 225   struct stack_trace usage_traces[13U] ;
 226   struct list_head locks_after ;
 227   struct list_head locks_before ;
 228   unsigned int version ;
 229   unsigned long ops ;
 230   char const   *name ;
 231   int name_version ;
 232   unsigned long contention_point[4U] ;
 233   unsigned long contending_point[4U] ;
 234};
 235#line 144 "include/linux/lockdep.h"
 236struct lockdep_map {
 237   struct lock_class_key *key ;
 238   struct lock_class *class_cache[2U] ;
 239   char const   *name ;
 240   int cpu ;
 241   unsigned long ip ;
 242};
 243#line 556 "include/linux/lockdep.h"
 244struct raw_spinlock {
 245   arch_spinlock_t raw_lock ;
 246   unsigned int magic ;
 247   unsigned int owner_cpu ;
 248   void *owner ;
 249   struct lockdep_map dep_map ;
 250};
 251#line 32 "include/linux/spinlock_types.h"
 252typedef struct raw_spinlock raw_spinlock_t;
 253#line 33 "include/linux/spinlock_types.h"
 254struct __anonstruct_ldv_6122_33 {
 255   u8 __padding[24U] ;
 256   struct lockdep_map dep_map ;
 257};
 258#line 33 "include/linux/spinlock_types.h"
 259union __anonunion_ldv_6123_32 {
 260   struct raw_spinlock rlock ;
 261   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 262};
 263#line 33 "include/linux/spinlock_types.h"
 264struct spinlock {
 265   union __anonunion_ldv_6123_32 ldv_6123 ;
 266};
 267#line 76 "include/linux/spinlock_types.h"
 268typedef struct spinlock spinlock_t;
 269#line 23 "include/linux/rwlock_types.h"
 270struct __anonstruct_rwlock_t_34 {
 271   arch_rwlock_t raw_lock ;
 272   unsigned int magic ;
 273   unsigned int owner_cpu ;
 274   void *owner ;
 275   struct lockdep_map dep_map ;
 276};
 277#line 23 "include/linux/rwlock_types.h"
 278typedef struct __anonstruct_rwlock_t_34 rwlock_t;
 279#line 110 "include/linux/seqlock.h"
 280struct seqcount {
 281   unsigned int sequence ;
 282};
 283#line 121 "include/linux/seqlock.h"
 284typedef struct seqcount seqcount_t;
 285#line 254 "include/linux/seqlock.h"
 286struct timespec {
 287   __kernel_time_t tv_sec ;
 288   long tv_nsec ;
 289};
 290#line 286 "include/linux/time.h"
 291struct kstat {
 292   u64 ino ;
 293   dev_t dev ;
 294   umode_t mode ;
 295   unsigned int nlink ;
 296   uid_t uid ;
 297   gid_t gid ;
 298   dev_t rdev ;
 299   loff_t size ;
 300   struct timespec atime ;
 301   struct timespec mtime ;
 302   struct timespec ctime ;
 303   unsigned long blksize ;
 304   unsigned long long blocks ;
 305};
 306#line 48 "include/linux/wait.h"
 307struct __wait_queue_head {
 308   spinlock_t lock ;
 309   struct list_head task_list ;
 310};
 311#line 53 "include/linux/wait.h"
 312typedef struct __wait_queue_head wait_queue_head_t;
 313#line 670 "include/linux/mmzone.h"
 314struct mutex {
 315   atomic_t count ;
 316   spinlock_t wait_lock ;
 317   struct list_head wait_list ;
 318   struct task_struct *owner ;
 319   char const   *name ;
 320   void *magic ;
 321   struct lockdep_map dep_map ;
 322};
 323#line 171 "include/linux/mutex.h"
 324struct rw_semaphore;
 325#line 171
 326struct rw_semaphore;
 327#line 172 "include/linux/mutex.h"
 328struct rw_semaphore {
 329   long count ;
 330   raw_spinlock_t wait_lock ;
 331   struct list_head wait_list ;
 332   struct lockdep_map dep_map ;
 333};
 334#line 188 "include/linux/rcupdate.h"
 335struct notifier_block;
 336#line 188
 337struct notifier_block;
 338#line 239 "include/linux/srcu.h"
 339struct notifier_block {
 340   int (*notifier_call)(struct notifier_block * , unsigned long  , void * ) ;
 341   struct notifier_block *next ;
 342   int priority ;
 343};
 344#line 341 "include/linux/ktime.h"
 345struct tvec_base;
 346#line 341
 347struct tvec_base;
 348#line 342 "include/linux/ktime.h"
 349struct timer_list {
 350   struct list_head entry ;
 351   unsigned long expires ;
 352   struct tvec_base *base ;
 353   void (*function)(unsigned long  ) ;
 354   unsigned long data ;
 355   int slack ;
 356   int start_pid ;
 357   void *start_site ;
 358   char start_comm[16U] ;
 359   struct lockdep_map lockdep_map ;
 360};
 361#line 18 "include/asm-generic/pci_iomap.h"
 362struct vm_area_struct;
 363#line 18
 364struct vm_area_struct;
 365#line 37 "include/linux/kmod.h"
 366struct cred;
 367#line 37
 368struct cred;
 369#line 18 "include/linux/elf.h"
 370typedef __u64 Elf64_Addr;
 371#line 19 "include/linux/elf.h"
 372typedef __u16 Elf64_Half;
 373#line 23 "include/linux/elf.h"
 374typedef __u32 Elf64_Word;
 375#line 24 "include/linux/elf.h"
 376typedef __u64 Elf64_Xword;
 377#line 193 "include/linux/elf.h"
 378struct elf64_sym {
 379   Elf64_Word st_name ;
 380   unsigned char st_info ;
 381   unsigned char st_other ;
 382   Elf64_Half st_shndx ;
 383   Elf64_Addr st_value ;
 384   Elf64_Xword st_size ;
 385};
 386#line 201 "include/linux/elf.h"
 387typedef struct elf64_sym Elf64_Sym;
 388#line 445
 389struct sock;
 390#line 445
 391struct sock;
 392#line 446
 393struct kobject;
 394#line 446
 395struct kobject;
 396#line 447
 397enum kobj_ns_type {
 398    KOBJ_NS_TYPE_NONE = 0,
 399    KOBJ_NS_TYPE_NET = 1,
 400    KOBJ_NS_TYPES = 2
 401} ;
 402#line 453 "include/linux/elf.h"
 403struct kobj_ns_type_operations {
 404   enum kobj_ns_type type ;
 405   void *(*grab_current_ns)(void) ;
 406   void const   *(*netlink_ns)(struct sock * ) ;
 407   void const   *(*initial_ns)(void) ;
 408   void (*drop_ns)(void * ) ;
 409};
 410#line 57 "include/linux/kobject_ns.h"
 411struct attribute {
 412   char const   *name ;
 413   umode_t mode ;
 414   struct lock_class_key *key ;
 415   struct lock_class_key skey ;
 416};
 417#line 98 "include/linux/sysfs.h"
 418struct sysfs_ops {
 419   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 420   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 421   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 422};
 423#line 117
 424struct sysfs_dirent;
 425#line 117
 426struct sysfs_dirent;
 427#line 182 "include/linux/sysfs.h"
 428struct kref {
 429   atomic_t refcount ;
 430};
 431#line 49 "include/linux/kobject.h"
 432struct kset;
 433#line 49
 434struct kobj_type;
 435#line 49 "include/linux/kobject.h"
 436struct kobject {
 437   char const   *name ;
 438   struct list_head entry ;
 439   struct kobject *parent ;
 440   struct kset *kset ;
 441   struct kobj_type *ktype ;
 442   struct sysfs_dirent *sd ;
 443   struct kref kref ;
 444   unsigned char state_initialized : 1 ;
 445   unsigned char state_in_sysfs : 1 ;
 446   unsigned char state_add_uevent_sent : 1 ;
 447   unsigned char state_remove_uevent_sent : 1 ;
 448   unsigned char uevent_suppress : 1 ;
 449};
 450#line 107 "include/linux/kobject.h"
 451struct kobj_type {
 452   void (*release)(struct kobject * ) ;
 453   struct sysfs_ops  const  *sysfs_ops ;
 454   struct attribute **default_attrs ;
 455   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 456   void const   *(*namespace)(struct kobject * ) ;
 457};
 458#line 115 "include/linux/kobject.h"
 459struct kobj_uevent_env {
 460   char *envp[32U] ;
 461   int envp_idx ;
 462   char buf[2048U] ;
 463   int buflen ;
 464};
 465#line 122 "include/linux/kobject.h"
 466struct kset_uevent_ops {
 467   int (* const  filter)(struct kset * , struct kobject * ) ;
 468   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 469   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 470};
 471#line 139 "include/linux/kobject.h"
 472struct kset {
 473   struct list_head list ;
 474   spinlock_t list_lock ;
 475   struct kobject kobj ;
 476   struct kset_uevent_ops  const  *uevent_ops ;
 477};
 478#line 215
 479struct kernel_param;
 480#line 215
 481struct kernel_param;
 482#line 216 "include/linux/kobject.h"
 483struct kernel_param_ops {
 484   int (*set)(char const   * , struct kernel_param  const  * ) ;
 485   int (*get)(char * , struct kernel_param  const  * ) ;
 486   void (*free)(void * ) ;
 487};
 488#line 49 "include/linux/moduleparam.h"
 489struct kparam_string;
 490#line 49
 491struct kparam_array;
 492#line 49 "include/linux/moduleparam.h"
 493union __anonunion_ldv_13363_134 {
 494   void *arg ;
 495   struct kparam_string  const  *str ;
 496   struct kparam_array  const  *arr ;
 497};
 498#line 49 "include/linux/moduleparam.h"
 499struct kernel_param {
 500   char const   *name ;
 501   struct kernel_param_ops  const  *ops ;
 502   u16 perm ;
 503   s16 level ;
 504   union __anonunion_ldv_13363_134 ldv_13363 ;
 505};
 506#line 61 "include/linux/moduleparam.h"
 507struct kparam_string {
 508   unsigned int maxlen ;
 509   char *string ;
 510};
 511#line 67 "include/linux/moduleparam.h"
 512struct kparam_array {
 513   unsigned int max ;
 514   unsigned int elemsize ;
 515   unsigned int *num ;
 516   struct kernel_param_ops  const  *ops ;
 517   void *elem ;
 518};
 519#line 458 "include/linux/moduleparam.h"
 520struct static_key {
 521   atomic_t enabled ;
 522};
 523#line 225 "include/linux/jump_label.h"
 524struct tracepoint;
 525#line 225
 526struct tracepoint;
 527#line 226 "include/linux/jump_label.h"
 528struct tracepoint_func {
 529   void *func ;
 530   void *data ;
 531};
 532#line 29 "include/linux/tracepoint.h"
 533struct tracepoint {
 534   char const   *name ;
 535   struct static_key key ;
 536   void (*regfunc)(void) ;
 537   void (*unregfunc)(void) ;
 538   struct tracepoint_func *funcs ;
 539};
 540#line 86 "include/linux/tracepoint.h"
 541struct kernel_symbol {
 542   unsigned long value ;
 543   char const   *name ;
 544};
 545#line 27 "include/linux/export.h"
 546struct mod_arch_specific {
 547
 548};
 549#line 34 "include/linux/module.h"
 550struct module_param_attrs;
 551#line 34 "include/linux/module.h"
 552struct module_kobject {
 553   struct kobject kobj ;
 554   struct module *mod ;
 555   struct kobject *drivers_dir ;
 556   struct module_param_attrs *mp ;
 557};
 558#line 43 "include/linux/module.h"
 559struct module_attribute {
 560   struct attribute attr ;
 561   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 562   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 563                    size_t  ) ;
 564   void (*setup)(struct module * , char const   * ) ;
 565   int (*test)(struct module * ) ;
 566   void (*free)(struct module * ) ;
 567};
 568#line 69
 569struct exception_table_entry;
 570#line 69
 571struct exception_table_entry;
 572#line 198
 573enum module_state {
 574    MODULE_STATE_LIVE = 0,
 575    MODULE_STATE_COMING = 1,
 576    MODULE_STATE_GOING = 2
 577} ;
 578#line 204 "include/linux/module.h"
 579struct module_ref {
 580   unsigned long incs ;
 581   unsigned long decs ;
 582};
 583#line 219
 584struct module_sect_attrs;
 585#line 219
 586struct module_notes_attrs;
 587#line 219
 588struct ftrace_event_call;
 589#line 219 "include/linux/module.h"
 590struct module {
 591   enum module_state state ;
 592   struct list_head list ;
 593   char name[56U] ;
 594   struct module_kobject mkobj ;
 595   struct module_attribute *modinfo_attrs ;
 596   char const   *version ;
 597   char const   *srcversion ;
 598   struct kobject *holders_dir ;
 599   struct kernel_symbol  const  *syms ;
 600   unsigned long const   *crcs ;
 601   unsigned int num_syms ;
 602   struct kernel_param *kp ;
 603   unsigned int num_kp ;
 604   unsigned int num_gpl_syms ;
 605   struct kernel_symbol  const  *gpl_syms ;
 606   unsigned long const   *gpl_crcs ;
 607   struct kernel_symbol  const  *unused_syms ;
 608   unsigned long const   *unused_crcs ;
 609   unsigned int num_unused_syms ;
 610   unsigned int num_unused_gpl_syms ;
 611   struct kernel_symbol  const  *unused_gpl_syms ;
 612   unsigned long const   *unused_gpl_crcs ;
 613   struct kernel_symbol  const  *gpl_future_syms ;
 614   unsigned long const   *gpl_future_crcs ;
 615   unsigned int num_gpl_future_syms ;
 616   unsigned int num_exentries ;
 617   struct exception_table_entry *extable ;
 618   int (*init)(void) ;
 619   void *module_init ;
 620   void *module_core ;
 621   unsigned int init_size ;
 622   unsigned int core_size ;
 623   unsigned int init_text_size ;
 624   unsigned int core_text_size ;
 625   unsigned int init_ro_size ;
 626   unsigned int core_ro_size ;
 627   struct mod_arch_specific arch ;
 628   unsigned int taints ;
 629   unsigned int num_bugs ;
 630   struct list_head bug_list ;
 631   struct bug_entry *bug_table ;
 632   Elf64_Sym *symtab ;
 633   Elf64_Sym *core_symtab ;
 634   unsigned int num_symtab ;
 635   unsigned int core_num_syms ;
 636   char *strtab ;
 637   char *core_strtab ;
 638   struct module_sect_attrs *sect_attrs ;
 639   struct module_notes_attrs *notes_attrs ;
 640   char *args ;
 641   void *percpu ;
 642   unsigned int percpu_size ;
 643   unsigned int num_tracepoints ;
 644   struct tracepoint * const  *tracepoints_ptrs ;
 645   unsigned int num_trace_bprintk_fmt ;
 646   char const   **trace_bprintk_fmt_start ;
 647   struct ftrace_event_call **trace_events ;
 648   unsigned int num_trace_events ;
 649   struct list_head source_list ;
 650   struct list_head target_list ;
 651   struct task_struct *waiter ;
 652   void (*exit)(void) ;
 653   struct module_ref *refptr ;
 654   ctor_fn_t (**ctors)(void) ;
 655   unsigned int num_ctors ;
 656};
 657#line 88 "include/linux/kmemleak.h"
 658struct kmem_cache_cpu {
 659   void **freelist ;
 660   unsigned long tid ;
 661   struct page *page ;
 662   struct page *partial ;
 663   int node ;
 664   unsigned int stat[26U] ;
 665};
 666#line 55 "include/linux/slub_def.h"
 667struct kmem_cache_node {
 668   spinlock_t list_lock ;
 669   unsigned long nr_partial ;
 670   struct list_head partial ;
 671   atomic_long_t nr_slabs ;
 672   atomic_long_t total_objects ;
 673   struct list_head full ;
 674};
 675#line 66 "include/linux/slub_def.h"
 676struct kmem_cache_order_objects {
 677   unsigned long x ;
 678};
 679#line 76 "include/linux/slub_def.h"
 680struct kmem_cache {
 681   struct kmem_cache_cpu *cpu_slab ;
 682   unsigned long flags ;
 683   unsigned long min_partial ;
 684   int size ;
 685   int objsize ;
 686   int offset ;
 687   int cpu_partial ;
 688   struct kmem_cache_order_objects oo ;
 689   struct kmem_cache_order_objects max ;
 690   struct kmem_cache_order_objects min ;
 691   gfp_t allocflags ;
 692   int refcount ;
 693   void (*ctor)(void * ) ;
 694   int inuse ;
 695   int align ;
 696   int reserved ;
 697   char const   *name ;
 698   struct list_head list ;
 699   struct kobject kobj ;
 700   int remote_node_defrag_ratio ;
 701   struct kmem_cache_node *node[1024U] ;
 702};
 703#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
 704struct file_operations;
 705#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
 706struct miscdevice {
 707   int minor ;
 708   char const   *name ;
 709   struct file_operations  const  *fops ;
 710   struct list_head list ;
 711   struct device *parent ;
 712   struct device *this_device ;
 713   char const   *nodename ;
 714   umode_t mode ;
 715};
 716#line 63 "include/linux/miscdevice.h"
 717struct watchdog_info {
 718   __u32 options ;
 719   __u32 firmware_version ;
 720   __u8 identity[32U] ;
 721};
 722#line 155 "include/linux/watchdog.h"
 723struct block_device;
 724#line 155
 725struct block_device;
 726#line 93 "include/linux/bit_spinlock.h"
 727struct hlist_bl_node;
 728#line 93 "include/linux/bit_spinlock.h"
 729struct hlist_bl_head {
 730   struct hlist_bl_node *first ;
 731};
 732#line 36 "include/linux/list_bl.h"
 733struct hlist_bl_node {
 734   struct hlist_bl_node *next ;
 735   struct hlist_bl_node **pprev ;
 736};
 737#line 114 "include/linux/rculist_bl.h"
 738struct nameidata;
 739#line 114
 740struct nameidata;
 741#line 115
 742struct path;
 743#line 115
 744struct path;
 745#line 116
 746struct vfsmount;
 747#line 116
 748struct vfsmount;
 749#line 117 "include/linux/rculist_bl.h"
 750struct qstr {
 751   unsigned int hash ;
 752   unsigned int len ;
 753   unsigned char const   *name ;
 754};
 755#line 72 "include/linux/dcache.h"
 756struct inode;
 757#line 72
 758struct dentry_operations;
 759#line 72
 760struct super_block;
 761#line 72 "include/linux/dcache.h"
 762union __anonunion_d_u_135 {
 763   struct list_head d_child ;
 764   struct rcu_head d_rcu ;
 765};
 766#line 72 "include/linux/dcache.h"
 767struct dentry {
 768   unsigned int d_flags ;
 769   seqcount_t d_seq ;
 770   struct hlist_bl_node d_hash ;
 771   struct dentry *d_parent ;
 772   struct qstr d_name ;
 773   struct inode *d_inode ;
 774   unsigned char d_iname[32U] ;
 775   unsigned int d_count ;
 776   spinlock_t d_lock ;
 777   struct dentry_operations  const  *d_op ;
 778   struct super_block *d_sb ;
 779   unsigned long d_time ;
 780   void *d_fsdata ;
 781   struct list_head d_lru ;
 782   union __anonunion_d_u_135 d_u ;
 783   struct list_head d_subdirs ;
 784   struct list_head d_alias ;
 785};
 786#line 123 "include/linux/dcache.h"
 787struct dentry_operations {
 788   int (*d_revalidate)(struct dentry * , struct nameidata * ) ;
 789   int (*d_hash)(struct dentry  const  * , struct inode  const  * , struct qstr * ) ;
 790   int (*d_compare)(struct dentry  const  * , struct inode  const  * , struct dentry  const  * ,
 791                    struct inode  const  * , unsigned int  , char const   * , struct qstr  const  * ) ;
 792   int (*d_delete)(struct dentry  const  * ) ;
 793   void (*d_release)(struct dentry * ) ;
 794   void (*d_prune)(struct dentry * ) ;
 795   void (*d_iput)(struct dentry * , struct inode * ) ;
 796   char *(*d_dname)(struct dentry * , char * , int  ) ;
 797   struct vfsmount *(*d_automount)(struct path * ) ;
 798   int (*d_manage)(struct dentry * , bool  ) ;
 799};
 800#line 402 "include/linux/dcache.h"
 801struct path {
 802   struct vfsmount *mnt ;
 803   struct dentry *dentry ;
 804};
 805#line 58 "include/linux/radix-tree.h"
 806struct radix_tree_node;
 807#line 58 "include/linux/radix-tree.h"
 808struct radix_tree_root {
 809   unsigned int height ;
 810   gfp_t gfp_mask ;
 811   struct radix_tree_node *rnode ;
 812};
 813#line 377
 814struct prio_tree_node;
 815#line 19 "include/linux/prio_tree.h"
 816struct prio_tree_node {
 817   struct prio_tree_node *left ;
 818   struct prio_tree_node *right ;
 819   struct prio_tree_node *parent ;
 820   unsigned long start ;
 821   unsigned long last ;
 822};
 823#line 27 "include/linux/prio_tree.h"
 824struct prio_tree_root {
 825   struct prio_tree_node *prio_tree_node ;
 826   unsigned short index_bits ;
 827   unsigned short raw ;
 828};
 829#line 111
 830enum pid_type {
 831    PIDTYPE_PID = 0,
 832    PIDTYPE_PGID = 1,
 833    PIDTYPE_SID = 2,
 834    PIDTYPE_MAX = 3
 835} ;
 836#line 118
 837struct pid_namespace;
 838#line 118 "include/linux/prio_tree.h"
 839struct upid {
 840   int nr ;
 841   struct pid_namespace *ns ;
 842   struct hlist_node pid_chain ;
 843};
 844#line 56 "include/linux/pid.h"
 845struct pid {
 846   atomic_t count ;
 847   unsigned int level ;
 848   struct hlist_head tasks[3U] ;
 849   struct rcu_head rcu ;
 850   struct upid numbers[1U] ;
 851};
 852#line 45 "include/linux/semaphore.h"
 853struct fiemap_extent {
 854   __u64 fe_logical ;
 855   __u64 fe_physical ;
 856   __u64 fe_length ;
 857   __u64 fe_reserved64[2U] ;
 858   __u32 fe_flags ;
 859   __u32 fe_reserved[3U] ;
 860};
 861#line 38 "include/linux/fiemap.h"
 862struct shrink_control {
 863   gfp_t gfp_mask ;
 864   unsigned long nr_to_scan ;
 865};
 866#line 14 "include/linux/shrinker.h"
 867struct shrinker {
 868   int (*shrink)(struct shrinker * , struct shrink_control * ) ;
 869   int seeks ;
 870   long batch ;
 871   struct list_head list ;
 872   atomic_long_t nr_in_batch ;
 873};
 874#line 43
 875enum migrate_mode {
 876    MIGRATE_ASYNC = 0,
 877    MIGRATE_SYNC_LIGHT = 1,
 878    MIGRATE_SYNC = 2
 879} ;
 880#line 49
 881struct export_operations;
 882#line 49
 883struct export_operations;
 884#line 51
 885struct iovec;
 886#line 51
 887struct iovec;
 888#line 52
 889struct kiocb;
 890#line 52
 891struct kiocb;
 892#line 53
 893struct pipe_inode_info;
 894#line 53
 895struct pipe_inode_info;
 896#line 54
 897struct poll_table_struct;
 898#line 54
 899struct poll_table_struct;
 900#line 55
 901struct kstatfs;
 902#line 55
 903struct kstatfs;
 904#line 435 "include/linux/fs.h"
 905struct iattr {
 906   unsigned int ia_valid ;
 907   umode_t ia_mode ;
 908   uid_t ia_uid ;
 909   gid_t ia_gid ;
 910   loff_t ia_size ;
 911   struct timespec ia_atime ;
 912   struct timespec ia_mtime ;
 913   struct timespec ia_ctime ;
 914   struct file *ia_file ;
 915};
 916#line 119 "include/linux/quota.h"
 917struct if_dqinfo {
 918   __u64 dqi_bgrace ;
 919   __u64 dqi_igrace ;
 920   __u32 dqi_flags ;
 921   __u32 dqi_valid ;
 922};
 923#line 176 "include/linux/percpu_counter.h"
 924struct fs_disk_quota {
 925   __s8 d_version ;
 926   __s8 d_flags ;
 927   __u16 d_fieldmask ;
 928   __u32 d_id ;
 929   __u64 d_blk_hardlimit ;
 930   __u64 d_blk_softlimit ;
 931   __u64 d_ino_hardlimit ;
 932   __u64 d_ino_softlimit ;
 933   __u64 d_bcount ;
 934   __u64 d_icount ;
 935   __s32 d_itimer ;
 936   __s32 d_btimer ;
 937   __u16 d_iwarns ;
 938   __u16 d_bwarns ;
 939   __s32 d_padding2 ;
 940   __u64 d_rtb_hardlimit ;
 941   __u64 d_rtb_softlimit ;
 942   __u64 d_rtbcount ;
 943   __s32 d_rtbtimer ;
 944   __u16 d_rtbwarns ;
 945   __s16 d_padding3 ;
 946   char d_padding4[8U] ;
 947};
 948#line 75 "include/linux/dqblk_xfs.h"
 949struct fs_qfilestat {
 950   __u64 qfs_ino ;
 951   __u64 qfs_nblks ;
 952   __u32 qfs_nextents ;
 953};
 954#line 150 "include/linux/dqblk_xfs.h"
 955typedef struct fs_qfilestat fs_qfilestat_t;
 956#line 151 "include/linux/dqblk_xfs.h"
 957struct fs_quota_stat {
 958   __s8 qs_version ;
 959   __u16 qs_flags ;
 960   __s8 qs_pad ;
 961   fs_qfilestat_t qs_uquota ;
 962   fs_qfilestat_t qs_gquota ;
 963   __u32 qs_incoredqs ;
 964   __s32 qs_btimelimit ;
 965   __s32 qs_itimelimit ;
 966   __s32 qs_rtbtimelimit ;
 967   __u16 qs_bwarnlimit ;
 968   __u16 qs_iwarnlimit ;
 969};
 970#line 165
 971struct dquot;
 972#line 165
 973struct dquot;
 974#line 185 "include/linux/quota.h"
 975typedef __kernel_uid32_t qid_t;
 976#line 186 "include/linux/quota.h"
 977typedef long long qsize_t;
 978#line 189 "include/linux/quota.h"
 979struct mem_dqblk {
 980   qsize_t dqb_bhardlimit ;
 981   qsize_t dqb_bsoftlimit ;
 982   qsize_t dqb_curspace ;
 983   qsize_t dqb_rsvspace ;
 984   qsize_t dqb_ihardlimit ;
 985   qsize_t dqb_isoftlimit ;
 986   qsize_t dqb_curinodes ;
 987   time_t dqb_btime ;
 988   time_t dqb_itime ;
 989};
 990#line 211
 991struct quota_format_type;
 992#line 211
 993struct quota_format_type;
 994#line 212 "include/linux/quota.h"
 995struct mem_dqinfo {
 996   struct quota_format_type *dqi_format ;
 997   int dqi_fmt_id ;
 998   struct list_head dqi_dirty_list ;
 999   unsigned long dqi_flags ;
1000   unsigned int dqi_bgrace ;
1001   unsigned int dqi_igrace ;
1002   qsize_t dqi_maxblimit ;
1003   qsize_t dqi_maxilimit ;
1004   void *dqi_priv ;
1005};
1006#line 275 "include/linux/quota.h"
1007struct dquot {
1008   struct hlist_node dq_hash ;
1009   struct list_head dq_inuse ;
1010   struct list_head dq_free ;
1011   struct list_head dq_dirty ;
1012   struct mutex dq_lock ;
1013   atomic_t dq_count ;
1014   wait_queue_head_t dq_wait_unused ;
1015   struct super_block *dq_sb ;
1016   unsigned int dq_id ;
1017   loff_t dq_off ;
1018   unsigned long dq_flags ;
1019   short dq_type ;
1020   struct mem_dqblk dq_dqb ;
1021};
1022#line 303 "include/linux/quota.h"
1023struct quota_format_ops {
1024   int (*check_quota_file)(struct super_block * , int  ) ;
1025   int (*read_file_info)(struct super_block * , int  ) ;
1026   int (*write_file_info)(struct super_block * , int  ) ;
1027   int (*free_file_info)(struct super_block * , int  ) ;
1028   int (*read_dqblk)(struct dquot * ) ;
1029   int (*commit_dqblk)(struct dquot * ) ;
1030   int (*release_dqblk)(struct dquot * ) ;
1031};
1032#line 314 "include/linux/quota.h"
1033struct dquot_operations {
1034   int (*write_dquot)(struct dquot * ) ;
1035   struct dquot *(*alloc_dquot)(struct super_block * , int  ) ;
1036   void (*destroy_dquot)(struct dquot * ) ;
1037   int (*acquire_dquot)(struct dquot * ) ;
1038   int (*release_dquot)(struct dquot * ) ;
1039   int (*mark_dirty)(struct dquot * ) ;
1040   int (*write_info)(struct super_block * , int  ) ;
1041   qsize_t *(*get_reserved_space)(struct inode * ) ;
1042};
1043#line 328 "include/linux/quota.h"
1044struct quotactl_ops {
1045   int (*quota_on)(struct super_block * , int  , int  , struct path * ) ;
1046   int (*quota_on_meta)(struct super_block * , int  , int  ) ;
1047   int (*quota_off)(struct super_block * , int  ) ;
1048   int (*quota_sync)(struct super_block * , int  , int  ) ;
1049   int (*get_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1050   int (*set_info)(struct super_block * , int  , struct if_dqinfo * ) ;
1051   int (*get_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1052   int (*set_dqblk)(struct super_block * , int  , qid_t  , struct fs_disk_quota * ) ;
1053   int (*get_xstate)(struct super_block * , struct fs_quota_stat * ) ;
1054   int (*set_xstate)(struct super_block * , unsigned int  , int  ) ;
1055};
1056#line 344 "include/linux/quota.h"
1057struct quota_format_type {
1058   int qf_fmt_id ;
1059   struct quota_format_ops  const  *qf_ops ;
1060   struct module *qf_owner ;
1061   struct quota_format_type *qf_next ;
1062};
1063#line 390 "include/linux/quota.h"
1064struct quota_info {
1065   unsigned int flags ;
1066   struct mutex dqio_mutex ;
1067   struct mutex dqonoff_mutex ;
1068   struct rw_semaphore dqptr_sem ;
1069   struct inode *files[2U] ;
1070   struct mem_dqinfo info[2U] ;
1071   struct quota_format_ops  const  *ops[2U] ;
1072};
1073#line 421
1074struct address_space;
1075#line 421
1076struct address_space;
1077#line 422
1078struct writeback_control;
1079#line 422
1080struct writeback_control;
1081#line 585 "include/linux/fs.h"
1082union __anonunion_arg_138 {
1083   char *buf ;
1084   void *data ;
1085};
1086#line 585 "include/linux/fs.h"
1087struct __anonstruct_read_descriptor_t_137 {
1088   size_t written ;
1089   size_t count ;
1090   union __anonunion_arg_138 arg ;
1091   int error ;
1092};
1093#line 585 "include/linux/fs.h"
1094typedef struct __anonstruct_read_descriptor_t_137 read_descriptor_t;
1095#line 588 "include/linux/fs.h"
1096struct address_space_operations {
1097   int (*writepage)(struct page * , struct writeback_control * ) ;
1098   int (*readpage)(struct file * , struct page * ) ;
1099   int (*writepages)(struct address_space * , struct writeback_control * ) ;
1100   int (*set_page_dirty)(struct page * ) ;
1101   int (*readpages)(struct file * , struct address_space * , struct list_head * ,
1102                    unsigned int  ) ;
1103   int (*write_begin)(struct file * , struct address_space * , loff_t  , unsigned int  ,
1104                      unsigned int  , struct page ** , void ** ) ;
1105   int (*write_end)(struct file * , struct address_space * , loff_t  , unsigned int  ,
1106                    unsigned int  , struct page * , void * ) ;
1107   sector_t (*bmap)(struct address_space * , sector_t  ) ;
1108   void (*invalidatepage)(struct page * , unsigned long  ) ;
1109   int (*releasepage)(struct page * , gfp_t  ) ;
1110   void (*freepage)(struct page * ) ;
1111   ssize_t (*direct_IO)(int  , struct kiocb * , struct iovec  const  * , loff_t  ,
1112                        unsigned long  ) ;
1113   int (*get_xip_mem)(struct address_space * , unsigned long  , int  , void ** , unsigned long * ) ;
1114   int (*migratepage)(struct address_space * , struct page * , struct page * , enum migrate_mode  ) ;
1115   int (*launder_page)(struct page * ) ;
1116   int (*is_partially_uptodate)(struct page * , read_descriptor_t * , unsigned long  ) ;
1117   int (*error_remove_page)(struct address_space * , struct page * ) ;
1118};
1119#line 642
1120struct backing_dev_info;
1121#line 642
1122struct backing_dev_info;
1123#line 643 "include/linux/fs.h"
1124struct address_space {
1125   struct inode *host ;
1126   struct radix_tree_root page_tree ;
1127   spinlock_t tree_lock ;
1128   unsigned int i_mmap_writable ;
1129   struct prio_tree_root i_mmap ;
1130   struct list_head i_mmap_nonlinear ;
1131   struct mutex i_mmap_mutex ;
1132   unsigned long nrpages ;
1133   unsigned long writeback_index ;
1134   struct address_space_operations  const  *a_ops ;
1135   unsigned long flags ;
1136   struct backing_dev_info *backing_dev_info ;
1137   spinlock_t private_lock ;
1138   struct list_head private_list ;
1139   struct address_space *assoc_mapping ;
1140};
1141#line 664
1142struct request_queue;
1143#line 664
1144struct request_queue;
1145#line 665
1146struct hd_struct;
1147#line 665
1148struct gendisk;
1149#line 665 "include/linux/fs.h"
1150struct block_device {
1151   dev_t bd_dev ;
1152   int bd_openers ;
1153   struct inode *bd_inode ;
1154   struct super_block *bd_super ;
1155   struct mutex bd_mutex ;
1156   struct list_head bd_inodes ;
1157   void *bd_claiming ;
1158   void *bd_holder ;
1159   int bd_holders ;
1160   bool bd_write_holder ;
1161   struct list_head bd_holder_disks ;
1162   struct block_device *bd_contains ;
1163   unsigned int bd_block_size ;
1164   struct hd_struct *bd_part ;
1165   unsigned int bd_part_count ;
1166   int bd_invalidated ;
1167   struct gendisk *bd_disk ;
1168   struct request_queue *bd_queue ;
1169   struct list_head bd_list ;
1170   unsigned long bd_private ;
1171   int bd_fsfreeze_count ;
1172   struct mutex bd_fsfreeze_mutex ;
1173};
1174#line 737
1175struct posix_acl;
1176#line 737
1177struct posix_acl;
1178#line 738
1179struct inode_operations;
1180#line 738 "include/linux/fs.h"
1181union __anonunion_ldv_15809_139 {
1182   unsigned int const   i_nlink ;
1183   unsigned int __i_nlink ;
1184};
1185#line 738 "include/linux/fs.h"
1186union __anonunion_ldv_15828_140 {
1187   struct list_head i_dentry ;
1188   struct rcu_head i_rcu ;
1189};
1190#line 738
1191struct file_lock;
1192#line 738
1193struct cdev;
1194#line 738 "include/linux/fs.h"
1195union __anonunion_ldv_15845_141 {
1196   struct pipe_inode_info *i_pipe ;
1197   struct block_device *i_bdev ;
1198   struct cdev *i_cdev ;
1199};
1200#line 738 "include/linux/fs.h"
1201struct inode {
1202   umode_t i_mode ;
1203   unsigned short i_opflags ;
1204   uid_t i_uid ;
1205   gid_t i_gid ;
1206   unsigned int i_flags ;
1207   struct posix_acl *i_acl ;
1208   struct posix_acl *i_default_acl ;
1209   struct inode_operations  const  *i_op ;
1210   struct super_block *i_sb ;
1211   struct address_space *i_mapping ;
1212   void *i_security ;
1213   unsigned long i_ino ;
1214   union __anonunion_ldv_15809_139 ldv_15809 ;
1215   dev_t i_rdev ;
1216   struct timespec i_atime ;
1217   struct timespec i_mtime ;
1218   struct timespec i_ctime ;
1219   spinlock_t i_lock ;
1220   unsigned short i_bytes ;
1221   blkcnt_t i_blocks ;
1222   loff_t i_size ;
1223   unsigned long i_state ;
1224   struct mutex i_mutex ;
1225   unsigned long dirtied_when ;
1226   struct hlist_node i_hash ;
1227   struct list_head i_wb_list ;
1228   struct list_head i_lru ;
1229   struct list_head i_sb_list ;
1230   union __anonunion_ldv_15828_140 ldv_15828 ;
1231   atomic_t i_count ;
1232   unsigned int i_blkbits ;
1233   u64 i_version ;
1234   atomic_t i_dio_count ;
1235   atomic_t i_writecount ;
1236   struct file_operations  const  *i_fop ;
1237   struct file_lock *i_flock ;
1238   struct address_space i_data ;
1239   struct dquot *i_dquot[2U] ;
1240   struct list_head i_devices ;
1241   union __anonunion_ldv_15845_141 ldv_15845 ;
1242   __u32 i_generation ;
1243   __u32 i_fsnotify_mask ;
1244   struct hlist_head i_fsnotify_marks ;
1245   atomic_t i_readcount ;
1246   void *i_private ;
1247};
1248#line 941 "include/linux/fs.h"
1249struct fown_struct {
1250   rwlock_t lock ;
1251   struct pid *pid ;
1252   enum pid_type pid_type ;
1253   uid_t uid ;
1254   uid_t euid ;
1255   int signum ;
1256};
1257#line 949 "include/linux/fs.h"
1258struct file_ra_state {
1259   unsigned long start ;
1260   unsigned int size ;
1261   unsigned int async_size ;
1262   unsigned int ra_pages ;
1263   unsigned int mmap_miss ;
1264   loff_t prev_pos ;
1265};
1266#line 972 "include/linux/fs.h"
1267union __anonunion_f_u_142 {
1268   struct list_head fu_list ;
1269   struct rcu_head fu_rcuhead ;
1270};
1271#line 972 "include/linux/fs.h"
1272struct file {
1273   union __anonunion_f_u_142 f_u ;
1274   struct path f_path ;
1275   struct file_operations  const  *f_op ;
1276   spinlock_t f_lock ;
1277   int f_sb_list_cpu ;
1278   atomic_long_t f_count ;
1279   unsigned int f_flags ;
1280   fmode_t f_mode ;
1281   loff_t f_pos ;
1282   struct fown_struct f_owner ;
1283   struct cred  const  *f_cred ;
1284   struct file_ra_state f_ra ;
1285   u64 f_version ;
1286   void *f_security ;
1287   void *private_data ;
1288   struct list_head f_ep_links ;
1289   struct list_head f_tfile_llink ;
1290   struct address_space *f_mapping ;
1291   unsigned long f_mnt_write_state ;
1292};
1293#line 1111
1294struct files_struct;
1295#line 1111 "include/linux/fs.h"
1296typedef struct files_struct *fl_owner_t;
1297#line 1112 "include/linux/fs.h"
1298struct file_lock_operations {
1299   void (*fl_copy_lock)(struct file_lock * , struct file_lock * ) ;
1300   void (*fl_release_private)(struct file_lock * ) ;
1301};
1302#line 1117 "include/linux/fs.h"
1303struct lock_manager_operations {
1304   int (*lm_compare_owner)(struct file_lock * , struct file_lock * ) ;
1305   void (*lm_notify)(struct file_lock * ) ;
1306   int (*lm_grant)(struct file_lock * , struct file_lock * , int  ) ;
1307   void (*lm_release_private)(struct file_lock * ) ;
1308   void (*lm_break)(struct file_lock * ) ;
1309   int (*lm_change)(struct file_lock ** , int  ) ;
1310};
1311#line 1134
1312struct nlm_lockowner;
1313#line 1134
1314struct nlm_lockowner;
1315#line 1135 "include/linux/fs.h"
1316struct nfs_lock_info {
1317   u32 state ;
1318   struct nlm_lockowner *owner ;
1319   struct list_head list ;
1320};
1321#line 14 "include/linux/nfs_fs_i.h"
1322struct nfs4_lock_state;
1323#line 14
1324struct nfs4_lock_state;
1325#line 15 "include/linux/nfs_fs_i.h"
1326struct nfs4_lock_info {
1327   struct nfs4_lock_state *owner ;
1328};
1329#line 19
1330struct fasync_struct;
1331#line 19 "include/linux/nfs_fs_i.h"
1332struct __anonstruct_afs_144 {
1333   struct list_head link ;
1334   int state ;
1335};
1336#line 19 "include/linux/nfs_fs_i.h"
1337union __anonunion_fl_u_143 {
1338   struct nfs_lock_info nfs_fl ;
1339   struct nfs4_lock_info nfs4_fl ;
1340   struct __anonstruct_afs_144 afs ;
1341};
1342#line 19 "include/linux/nfs_fs_i.h"
1343struct file_lock {
1344   struct file_lock *fl_next ;
1345   struct list_head fl_link ;
1346   struct list_head fl_block ;
1347   fl_owner_t fl_owner ;
1348   unsigned int fl_flags ;
1349   unsigned char fl_type ;
1350   unsigned int fl_pid ;
1351   struct pid *fl_nspid ;
1352   wait_queue_head_t fl_wait ;
1353   struct file *fl_file ;
1354   loff_t fl_start ;
1355   loff_t fl_end ;
1356   struct fasync_struct *fl_fasync ;
1357   unsigned long fl_break_time ;
1358   unsigned long fl_downgrade_time ;
1359   struct file_lock_operations  const  *fl_ops ;
1360   struct lock_manager_operations  const  *fl_lmops ;
1361   union __anonunion_fl_u_143 fl_u ;
1362};
1363#line 1221 "include/linux/fs.h"
1364struct fasync_struct {
1365   spinlock_t fa_lock ;
1366   int magic ;
1367   int fa_fd ;
1368   struct fasync_struct *fa_next ;
1369   struct file *fa_file ;
1370   struct rcu_head fa_rcu ;
1371};
1372#line 1417
1373struct file_system_type;
1374#line 1417
1375struct super_operations;
1376#line 1417
1377struct xattr_handler;
1378#line 1417
1379struct mtd_info;
1380#line 1417 "include/linux/fs.h"
1381struct super_block {
1382   struct list_head s_list ;
1383   dev_t s_dev ;
1384   unsigned char s_dirt ;
1385   unsigned char s_blocksize_bits ;
1386   unsigned long s_blocksize ;
1387   loff_t s_maxbytes ;
1388   struct file_system_type *s_type ;
1389   struct super_operations  const  *s_op ;
1390   struct dquot_operations  const  *dq_op ;
1391   struct quotactl_ops  const  *s_qcop ;
1392   struct export_operations  const  *s_export_op ;
1393   unsigned long s_flags ;
1394   unsigned long s_magic ;
1395   struct dentry *s_root ;
1396   struct rw_semaphore s_umount ;
1397   struct mutex s_lock ;
1398   int s_count ;
1399   atomic_t s_active ;
1400   void *s_security ;
1401   struct xattr_handler  const  **s_xattr ;
1402   struct list_head s_inodes ;
1403   struct hlist_bl_head s_anon ;
1404   struct list_head *s_files ;
1405   struct list_head s_mounts ;
1406   struct list_head s_dentry_lru ;
1407   int s_nr_dentry_unused ;
1408   spinlock_t s_inode_lru_lock ;
1409   struct list_head s_inode_lru ;
1410   int s_nr_inodes_unused ;
1411   struct block_device *s_bdev ;
1412   struct backing_dev_info *s_bdi ;
1413   struct mtd_info *s_mtd ;
1414   struct hlist_node s_instances ;
1415   struct quota_info s_dquot ;
1416   int s_frozen ;
1417   wait_queue_head_t s_wait_unfrozen ;
1418   char s_id[32U] ;
1419   u8 s_uuid[16U] ;
1420   void *s_fs_info ;
1421   unsigned int s_max_links ;
1422   fmode_t s_mode ;
1423   u32 s_time_gran ;
1424   struct mutex s_vfs_rename_mutex ;
1425   char *s_subtype ;
1426   char *s_options ;
1427   struct dentry_operations  const  *s_d_op ;
1428   int cleancache_poolid ;
1429   struct shrinker s_shrink ;
1430   atomic_long_t s_remove_count ;
1431   int s_readonly_remount ;
1432};
1433#line 1563 "include/linux/fs.h"
1434struct fiemap_extent_info {
1435   unsigned int fi_flags ;
1436   unsigned int fi_extents_mapped ;
1437   unsigned int fi_extents_max ;
1438   struct fiemap_extent *fi_extents_start ;
1439};
1440#line 1602 "include/linux/fs.h"
1441struct file_operations {
1442   struct module *owner ;
1443   loff_t (*llseek)(struct file * , loff_t  , int  ) ;
1444   ssize_t (*read)(struct file * , char * , size_t  , loff_t * ) ;
1445   ssize_t (*write)(struct file * , char const   * , size_t  , loff_t * ) ;
1446   ssize_t (*aio_read)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1447                       loff_t  ) ;
1448   ssize_t (*aio_write)(struct kiocb * , struct iovec  const  * , unsigned long  ,
1449                        loff_t  ) ;
1450   int (*readdir)(struct file * , void * , int (*)(void * , char const   * , int  ,
1451                                                   loff_t  , u64  , unsigned int  ) ) ;
1452   unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
1453   long (*unlocked_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1454   long (*compat_ioctl)(struct file * , unsigned int  , unsigned long  ) ;
1455   int (*mmap)(struct file * , struct vm_area_struct * ) ;
1456   int (*open)(struct inode * , struct file * ) ;
1457   int (*flush)(struct file * , fl_owner_t  ) ;
1458   int (*release)(struct inode * , struct file * ) ;
1459   int (*fsync)(struct file * , loff_t  , loff_t  , int  ) ;
1460   int (*aio_fsync)(struct kiocb * , int  ) ;
1461   int (*fasync)(int  , struct file * , int  ) ;
1462   int (*lock)(struct file * , int  , struct file_lock * ) ;
1463   ssize_t (*sendpage)(struct file * , struct page * , int  , size_t  , loff_t * ,
1464                       int  ) ;
1465   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1466                                      unsigned long  , unsigned long  ) ;
1467   int (*check_flags)(int  ) ;
1468   int (*flock)(struct file * , int  , struct file_lock * ) ;
1469   ssize_t (*splice_write)(struct pipe_inode_info * , struct file * , loff_t * , size_t  ,
1470                           unsigned int  ) ;
1471   ssize_t (*splice_read)(struct file * , loff_t * , struct pipe_inode_info * , size_t  ,
1472                          unsigned int  ) ;
1473   int (*setlease)(struct file * , long  , struct file_lock ** ) ;
1474   long (*fallocate)(struct file * , int  , loff_t  , loff_t  ) ;
1475};
1476#line 1637 "include/linux/fs.h"
1477struct inode_operations {
1478   struct dentry *(*lookup)(struct inode * , struct dentry * , struct nameidata * ) ;
1479   void *(*follow_link)(struct dentry * , struct nameidata * ) ;
1480   int (*permission)(struct inode * , int  ) ;
1481   struct posix_acl *(*get_acl)(struct inode * , int  ) ;
1482   int (*readlink)(struct dentry * , char * , int  ) ;
1483   void (*put_link)(struct dentry * , struct nameidata * , void * ) ;
1484   int (*create)(struct inode * , struct dentry * , umode_t  , struct nameidata * ) ;
1485   int (*link)(struct dentry * , struct inode * , struct dentry * ) ;
1486   int (*unlink)(struct inode * , struct dentry * ) ;
1487   int (*symlink)(struct inode * , struct dentry * , char const   * ) ;
1488   int (*mkdir)(struct inode * , struct dentry * , umode_t  ) ;
1489   int (*rmdir)(struct inode * , struct dentry * ) ;
1490   int (*mknod)(struct inode * , struct dentry * , umode_t  , dev_t  ) ;
1491   int (*rename)(struct inode * , struct dentry * , struct inode * , struct dentry * ) ;
1492   void (*truncate)(struct inode * ) ;
1493   int (*setattr)(struct dentry * , struct iattr * ) ;
1494   int (*getattr)(struct vfsmount * , struct dentry * , struct kstat * ) ;
1495   int (*setxattr)(struct dentry * , char const   * , void const   * , size_t  , int  ) ;
1496   ssize_t (*getxattr)(struct dentry * , char const   * , void * , size_t  ) ;
1497   ssize_t (*listxattr)(struct dentry * , char * , size_t  ) ;
1498   int (*removexattr)(struct dentry * , char const   * ) ;
1499   void (*truncate_range)(struct inode * , loff_t  , loff_t  ) ;
1500   int (*fiemap)(struct inode * , struct fiemap_extent_info * , u64  , u64  ) ;
1501};
1502#line 1682 "include/linux/fs.h"
1503struct super_operations {
1504   struct inode *(*alloc_inode)(struct super_block * ) ;
1505   void (*destroy_inode)(struct inode * ) ;
1506   void (*dirty_inode)(struct inode * , int  ) ;
1507   int (*write_inode)(struct inode * , struct writeback_control * ) ;
1508   int (*drop_inode)(struct inode * ) ;
1509   void (*evict_inode)(struct inode * ) ;
1510   void (*put_super)(struct super_block * ) ;
1511   void (*write_super)(struct super_block * ) ;
1512   int (*sync_fs)(struct super_block * , int  ) ;
1513   int (*freeze_fs)(struct super_block * ) ;
1514   int (*unfreeze_fs)(struct super_block * ) ;
1515   int (*statfs)(struct dentry * , struct kstatfs * ) ;
1516   int (*remount_fs)(struct super_block * , int * , char * ) ;
1517   void (*umount_begin)(struct super_block * ) ;
1518   int (*show_options)(struct seq_file * , struct dentry * ) ;
1519   int (*show_devname)(struct seq_file * , struct dentry * ) ;
1520   int (*show_path)(struct seq_file * , struct dentry * ) ;
1521   int (*show_stats)(struct seq_file * , struct dentry * ) ;
1522   ssize_t (*quota_read)(struct super_block * , int  , char * , size_t  , loff_t  ) ;
1523   ssize_t (*quota_write)(struct super_block * , int  , char const   * , size_t  ,
1524                          loff_t  ) ;
1525   int (*bdev_try_to_free_page)(struct super_block * , struct page * , gfp_t  ) ;
1526   int (*nr_cached_objects)(struct super_block * ) ;
1527   void (*free_cached_objects)(struct super_block * , int  ) ;
1528};
1529#line 1834 "include/linux/fs.h"
1530struct file_system_type {
1531   char const   *name ;
1532   int fs_flags ;
1533   struct dentry *(*mount)(struct file_system_type * , int  , char const   * , void * ) ;
1534   void (*kill_sb)(struct super_block * ) ;
1535   struct module *owner ;
1536   struct file_system_type *next ;
1537   struct hlist_head fs_supers ;
1538   struct lock_class_key s_lock_key ;
1539   struct lock_class_key s_umount_key ;
1540   struct lock_class_key s_vfs_rename_key ;
1541   struct lock_class_key i_lock_key ;
1542   struct lock_class_key i_mutex_key ;
1543   struct lock_class_key i_mutex_dir_key ;
1544};
1545#line 69 "include/linux/io.h"
1546struct exception_table_entry {
1547   unsigned long insn ;
1548   unsigned long fixup ;
1549};
1550#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1551void ldv_spin_lock(void) ;
1552#line 3
1553void ldv_spin_unlock(void) ;
1554#line 4
1555int ldv_spin_trylock(void) ;
1556#line 98 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1557__inline static void clear_bit(int nr , unsigned long volatile   *addr ) 
1558{ long volatile   *__cil_tmp3 ;
1559
1560  {
1561#line 105
1562  __cil_tmp3 = (long volatile   *)addr;
1563#line 105
1564  __asm__  volatile   (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; btr %1,%0": "+m" (*__cil_tmp3): "Ir" (nr));
1565#line 107
1566  return;
1567}
1568}
1569#line 195 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1570__inline static int test_and_set_bit(int nr , unsigned long volatile   *addr ) 
1571{ int oldbit ;
1572  long volatile   *__cil_tmp4 ;
1573
1574  {
1575#line 199
1576  __cil_tmp4 = (long volatile   *)addr;
1577#line 199
1578  __asm__  volatile   (".section .smp_locks,\"a\"\n.balign 4\n.long 671f - .\n.previous\n671:\n\tlock; bts %2,%1\n\tsbb %0,%0": "=r" (oldbit),
1579                       "+m" (*__cil_tmp4): "Ir" (nr): "memory");
1580#line 202
1581  return (oldbit);
1582}
1583}
1584#line 101 "include/linux/printk.h"
1585extern int printk(char const   *  , ...) ;
1586#line 192 "include/linux/kernel.h"
1587extern void might_fault(void) ;
1588#line 22 "include/linux/spinlock_api_smp.h"
1589extern void _raw_spin_lock(raw_spinlock_t * ) ;
1590#line 39
1591extern void _raw_spin_unlock(raw_spinlock_t * ) ;
1592#line 43
1593extern void _raw_spin_unlock_irqrestore(raw_spinlock_t * , unsigned long  ) ;
1594#line 283 "include/linux/spinlock.h"
1595__inline static void ldv_spin_lock_1(spinlock_t *lock ) 
1596{ struct raw_spinlock *__cil_tmp2 ;
1597
1598  {
1599  {
1600#line 285
1601  __cil_tmp2 = (struct raw_spinlock *)lock;
1602#line 285
1603  _raw_spin_lock(__cil_tmp2);
1604  }
1605#line 286
1606  return;
1607}
1608}
1609#line 283
1610__inline static void spin_lock(spinlock_t *lock ) ;
1611#line 323 "include/linux/spinlock.h"
1612__inline static void ldv_spin_unlock_5(spinlock_t *lock ) 
1613{ struct raw_spinlock *__cil_tmp2 ;
1614
1615  {
1616  {
1617#line 325
1618  __cil_tmp2 = (struct raw_spinlock *)lock;
1619#line 325
1620  _raw_spin_unlock(__cil_tmp2);
1621  }
1622#line 326
1623  return;
1624}
1625}
1626#line 323
1627__inline static void spin_unlock(spinlock_t *lock ) ;
1628#line 350 "include/linux/spinlock.h"
1629__inline static void ldv_spin_unlock_irqrestore_8(spinlock_t *lock , unsigned long flags ) 
1630{ struct raw_spinlock *__cil_tmp5 ;
1631
1632  {
1633  {
1634#line 352
1635  __cil_tmp5 = (struct raw_spinlock *)lock;
1636#line 352
1637  _raw_spin_unlock_irqrestore(__cil_tmp5, flags);
1638  }
1639#line 353
1640  return;
1641}
1642}
1643#line 350
1644__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) ;
1645#line 82 "include/linux/jiffies.h"
1646extern unsigned long volatile   jiffies ;
1647#line 36 "include/linux/timer.h"
1648extern struct tvec_base boot_tvec_bases ;
1649#line 210
1650extern int del_timer(struct timer_list * ) ;
1651#line 211
1652extern int mod_timer(struct timer_list * , unsigned long  ) ;
1653#line 54 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1654__inline static unsigned short readw(void const volatile   *addr ) 
1655{ unsigned short ret ;
1656  unsigned short volatile   *__cil_tmp3 ;
1657
1658  {
1659#line 54
1660  __cil_tmp3 = (unsigned short volatile   *)addr;
1661#line 54
1662  __asm__  volatile   ("movw %1,%0": "=r" (ret): "m" (*__cil_tmp3): "memory");
1663#line 54
1664  return (ret);
1665}
1666}
1667#line 62 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1668__inline static void writew(unsigned short val , void volatile   *addr ) 
1669{ unsigned short volatile   *__cil_tmp3 ;
1670
1671  {
1672#line 62
1673  __cil_tmp3 = (unsigned short volatile   *)addr;
1674#line 62
1675  __asm__  volatile   ("movw %0,%1": : "r" (val), "m" (*__cil_tmp3): "memory");
1676#line 63
1677  return;
1678}
1679}
1680#line 174
1681extern void *ioremap_nocache(resource_size_t  , unsigned long  ) ;
1682#line 182 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1683__inline static void *ioremap(resource_size_t offset , unsigned long size ) 
1684{ void *tmp ;
1685
1686  {
1687  {
1688#line 184
1689  tmp = ioremap_nocache(offset, size);
1690  }
1691#line 184
1692  return (tmp);
1693}
1694}
1695#line 187
1696extern void iounmap(void volatile   * ) ;
1697#line 26 "include/linux/export.h"
1698extern struct module __this_module ;
1699#line 453 "include/linux/module.h"
1700extern void __module_get(struct module * ) ;
1701#line 220 "include/linux/slub_def.h"
1702extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1703#line 223
1704void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1705#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1706void ldv_check_alloc_flags(gfp_t flags ) ;
1707#line 12
1708void ldv_check_alloc_nonatomic(void) ;
1709#line 14
1710struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1711#line 61 "include/linux/miscdevice.h"
1712extern int misc_register(struct miscdevice * ) ;
1713#line 62
1714extern int misc_deregister(struct miscdevice * ) ;
1715#line 2402 "include/linux/fs.h"
1716extern loff_t no_llseek(struct file * , loff_t  , int  ) ;
1717#line 2407
1718extern int nonseekable_open(struct inode * , struct file * ) ;
1719#line 47 "include/linux/reboot.h"
1720extern int register_reboot_notifier(struct notifier_block * ) ;
1721#line 48
1722extern int unregister_reboot_notifier(struct notifier_block * ) ;
1723#line 40 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess_64.h"
1724extern unsigned long _copy_to_user(void * , void const   * , unsigned int  ) ;
1725#line 63 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/uaccess_64.h"
1726__inline static int copy_to_user(void *dst , void const   *src , unsigned int size ) 
1727{ unsigned long tmp ;
1728
1729  {
1730  {
1731#line 65
1732  might_fault();
1733#line 67
1734  tmp = _copy_to_user(dst, src, size);
1735  }
1736#line 67
1737  return ((int )tmp);
1738}
1739}
1740#line 108 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1741static int timeout  =    30;
1742#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1743static bool nowayout  =    (bool )1;
1744#line 139 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1745static __u16 *wdtmrctl  ;
1746#line 141
1747static void wdt_timer_ping(unsigned long data ) ;
1748#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1749static struct timer_list timer  = 
1750#line 142
1751     {{(struct list_head *)0, (struct list_head *)1953723489}, 0UL, & boot_tvec_bases,
1752    & wdt_timer_ping, 0UL, -1, 0, (void *)0, {(char)0, (char)0, (char)0, (char)0,
1753                                              (char)0, (char)0, (char)0, (char)0,
1754                                              (char)0, (char)0, (char)0, (char)0,
1755                                              (char)0, (char)0, (char)0, (char)0},
1756    {(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/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p:142",
1757     {(struct lock_class *)0, (struct lock_class *)0}, "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p:142",
1758     0, 0UL}};
1759#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1760static unsigned long next_heartbeat  ;
1761#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1762static unsigned long wdt_is_open  ;
1763#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1764static char wdt_expect_close  ;
1765#line 146 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1766static spinlock_t wdt_spinlock  =    {{{{{0U}}, 3735899821U, 4294967295U, (void *)0xffffffffffffffffUL, {(struct lock_class_key *)0,
1767                                                                       {(struct lock_class *)0,
1768                                                                        (struct lock_class *)0},
1769                                                                       "wdt_spinlock",
1770                                                                       0, 0UL}}}};
1771#line 152 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1772static void wdt_timer_ping(unsigned long data ) 
1773{ long __cil_tmp6 ;
1774  long __cil_tmp7 ;
1775  long __cil_tmp8 ;
1776  void volatile   *__cil_tmp9 ;
1777  void volatile   *__cil_tmp10 ;
1778  unsigned long __cil_tmp11 ;
1779  unsigned long __cil_tmp12 ;
1780
1781  {
1782  {
1783#line 157
1784  __cil_tmp6 = (long )next_heartbeat;
1785#line 157
1786  __cil_tmp7 = (long )jiffies;
1787#line 157
1788  __cil_tmp8 = __cil_tmp7 - __cil_tmp6;
1789#line 157
1790  if (__cil_tmp8 < 0L) {
1791    {
1792#line 159
1793    spin_lock(& wdt_spinlock);
1794#line 160
1795    __cil_tmp9 = (void volatile   *)wdtmrctl;
1796#line 160
1797    writew((unsigned short)43690, __cil_tmp9);
1798#line 161
1799    __cil_tmp10 = (void volatile   *)wdtmrctl;
1800#line 161
1801    writew((unsigned short)21845, __cil_tmp10);
1802#line 162
1803    spin_unlock(& wdt_spinlock);
1804#line 165
1805    __cil_tmp11 = (unsigned long )jiffies;
1806#line 165
1807    __cil_tmp12 = __cil_tmp11 + 63UL;
1808#line 165
1809    mod_timer(& timer, __cil_tmp12);
1810    }
1811  } else {
1812    {
1813#line 167
1814    printk("<4>sc520_wdt: Heartbeat lost! Will not ping the watchdog\n");
1815    }
1816  }
1817  }
1818#line 168
1819  return;
1820}
1821}
1822#line 174 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1823static void wdt_config(int writeval ) 
1824{ __u16 dummy ;
1825  unsigned long flags ;
1826  void const volatile   *__cil_tmp4 ;
1827  void volatile   *__cil_tmp5 ;
1828  void volatile   *__cil_tmp6 ;
1829  void volatile   *__cil_tmp7 ;
1830  void volatile   *__cil_tmp8 ;
1831  unsigned short __cil_tmp9 ;
1832  int __cil_tmp10 ;
1833  unsigned short __cil_tmp11 ;
1834  void volatile   *__cil_tmp12 ;
1835
1836  {
1837  {
1838#line 180
1839  ldv_spin_lock();
1840#line 181
1841  __cil_tmp4 = (void const volatile   *)wdtmrctl;
1842#line 181
1843  dummy = readw(__cil_tmp4);
1844#line 182
1845  __cil_tmp5 = (void volatile   *)wdtmrctl;
1846#line 182
1847  writew((unsigned short)43690, __cil_tmp5);
1848#line 183
1849  __cil_tmp6 = (void volatile   *)wdtmrctl;
1850#line 183
1851  writew((unsigned short)21845, __cil_tmp6);
1852#line 185
1853  __cil_tmp7 = (void volatile   *)wdtmrctl;
1854#line 185
1855  writew((unsigned short)13107, __cil_tmp7);
1856#line 186
1857  __cil_tmp8 = (void volatile   *)wdtmrctl;
1858#line 186
1859  writew((unsigned short)52428, __cil_tmp8);
1860#line 188
1861  __cil_tmp9 = (unsigned short )writeval;
1862#line 188
1863  __cil_tmp10 = (int )__cil_tmp9;
1864#line 188
1865  __cil_tmp11 = (unsigned short )__cil_tmp10;
1866#line 188
1867  __cil_tmp12 = (void volatile   *)wdtmrctl;
1868#line 188
1869  writew(__cil_tmp11, __cil_tmp12);
1870#line 189
1871  spin_unlock_irqrestore(& wdt_spinlock, flags);
1872  }
1873#line 190
1874  return;
1875}
1876}
1877#line 192 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1878static int wdt_startup(void) 
1879{ unsigned long __cil_tmp1 ;
1880  int *__cil_tmp2 ;
1881  int __cil_tmp3 ;
1882  int __cil_tmp4 ;
1883  unsigned long __cil_tmp5 ;
1884  unsigned long __cil_tmp6 ;
1885  unsigned long __cil_tmp7 ;
1886
1887  {
1888  {
1889#line 194
1890  __cil_tmp1 = (unsigned long )jiffies;
1891#line 194
1892  __cil_tmp2 = & timeout;
1893#line 194
1894  __cil_tmp3 = *__cil_tmp2;
1895#line 194
1896  __cil_tmp4 = __cil_tmp3 * 250;
1897#line 194
1898  __cil_tmp5 = (unsigned long )__cil_tmp4;
1899#line 194
1900  next_heartbeat = __cil_tmp5 + __cil_tmp1;
1901#line 197
1902  __cil_tmp6 = (unsigned long )jiffies;
1903#line 197
1904  __cil_tmp7 = __cil_tmp6 + 63UL;
1905#line 197
1906  mod_timer(& timer, __cil_tmp7);
1907#line 200
1908  wdt_config(49160);
1909#line 202
1910  printk("<6>sc520_wdt: Watchdog timer is now enabled\n");
1911  }
1912#line 203
1913  return (0);
1914}
1915}
1916#line 206 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1917static int wdt_turnoff(void) 
1918{ 
1919
1920  {
1921  {
1922#line 209
1923  del_timer(& timer);
1924#line 212
1925  wdt_config(0);
1926#line 214
1927  printk("<6>sc520_wdt: Watchdog timer is now disabled...\n");
1928  }
1929#line 215
1930  return (0);
1931}
1932}
1933#line 218 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1934static int wdt_keepalive(void) 
1935{ unsigned long __cil_tmp1 ;
1936  int *__cil_tmp2 ;
1937  int __cil_tmp3 ;
1938  int __cil_tmp4 ;
1939  unsigned long __cil_tmp5 ;
1940
1941  {
1942#line 221
1943  __cil_tmp1 = (unsigned long )jiffies;
1944#line 221
1945  __cil_tmp2 = & timeout;
1946#line 221
1947  __cil_tmp3 = *__cil_tmp2;
1948#line 221
1949  __cil_tmp4 = __cil_tmp3 * 250;
1950#line 221
1951  __cil_tmp5 = (unsigned long )__cil_tmp4;
1952#line 221
1953  next_heartbeat = __cil_tmp5 + __cil_tmp1;
1954#line 222
1955  return (0);
1956}
1957}
1958#line 225 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1959static int wdt_set_heartbeat(int t ) 
1960{ int *__cil_tmp2 ;
1961
1962  {
1963#line 227
1964  if (t <= 0) {
1965#line 228
1966    return (-22);
1967  } else
1968#line 227
1969  if (t > 3600) {
1970#line 228
1971    return (-22);
1972  } else {
1973
1974  }
1975#line 230
1976  __cil_tmp2 = & timeout;
1977#line 230
1978  *__cil_tmp2 = t;
1979#line 231
1980  return (0);
1981}
1982}
1983#line 238 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
1984static ssize_t fop_write(struct file *file , char const   *buf , size_t count , loff_t *ppos ) 
1985{ size_t ofs ;
1986  char c ;
1987  int __ret_gu ;
1988  unsigned long __val_gu ;
1989  bool *__cil_tmp9 ;
1990  bool __cil_tmp10 ;
1991  signed char __cil_tmp11 ;
1992  int __cil_tmp12 ;
1993
1994  {
1995#line 242
1996  if (count != 0UL) {
1997    {
1998#line 243
1999    __cil_tmp9 = & nowayout;
2000#line 243
2001    __cil_tmp10 = *__cil_tmp9;
2002#line 243
2003    if (! __cil_tmp10) {
2004#line 248
2005      wdt_expect_close = (char)0;
2006#line 251
2007      ofs = 0UL;
2008#line 251
2009      goto ldv_18070;
2010      ldv_18069: 
2011      {
2012#line 253
2013      might_fault();
2014      }
2015#line 253
2016      if (1 == 1) {
2017#line 253
2018        goto case_1;
2019      } else
2020#line 253
2021      if (1 == 2) {
2022#line 253
2023        goto case_2;
2024      } else
2025#line 253
2026      if (1 == 4) {
2027#line 253
2028        goto case_4;
2029      } else
2030#line 253
2031      if (1 == 8) {
2032#line 253
2033        goto case_8;
2034      } else {
2035        {
2036#line 253
2037        goto switch_default;
2038#line 253
2039        if (0) {
2040          case_1: /* CIL Label */ 
2041#line 253
2042          __asm__  volatile   ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + ofs));
2043#line 253
2044          goto ldv_18063;
2045          case_2: /* CIL Label */ 
2046#line 253
2047          __asm__  volatile   ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + ofs));
2048#line 253
2049          goto ldv_18063;
2050          case_4: /* CIL Label */ 
2051#line 253
2052          __asm__  volatile   ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + ofs));
2053#line 253
2054          goto ldv_18063;
2055          case_8: /* CIL Label */ 
2056#line 253
2057          __asm__  volatile   ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + ofs));
2058#line 253
2059          goto ldv_18063;
2060          switch_default: /* CIL Label */ 
2061#line 253
2062          __asm__  volatile   ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (buf + ofs));
2063#line 253
2064          goto ldv_18063;
2065        } else {
2066          switch_break: /* CIL Label */ ;
2067        }
2068        }
2069      }
2070      ldv_18063: 
2071#line 253
2072      c = (char )__val_gu;
2073#line 253
2074      if (__ret_gu != 0) {
2075#line 254
2076        return (-14L);
2077      } else {
2078
2079      }
2080      {
2081#line 255
2082      __cil_tmp11 = (signed char )c;
2083#line 255
2084      __cil_tmp12 = (int )__cil_tmp11;
2085#line 255
2086      if (__cil_tmp12 == 86) {
2087#line 256
2088        wdt_expect_close = (char)42;
2089      } else {
2090
2091      }
2092      }
2093#line 251
2094      ofs = ofs + 1UL;
2095      ldv_18070: ;
2096#line 251
2097      if (ofs != count) {
2098#line 252
2099        goto ldv_18069;
2100      } else {
2101#line 254
2102        goto ldv_18071;
2103      }
2104      ldv_18071: ;
2105    } else {
2106
2107    }
2108    }
2109    {
2110#line 262
2111    wdt_keepalive();
2112    }
2113  } else {
2114
2115  }
2116#line 264
2117  return ((ssize_t )count);
2118}
2119}
2120#line 267 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2121static int fop_open(struct inode *inode , struct file *file ) 
2122{ int tmp ;
2123  int tmp___0 ;
2124  unsigned long volatile   *__cil_tmp5 ;
2125  bool *__cil_tmp6 ;
2126  bool __cil_tmp7 ;
2127
2128  {
2129  {
2130#line 270
2131  __cil_tmp5 = (unsigned long volatile   *)(& wdt_is_open);
2132#line 270
2133  tmp = test_and_set_bit(0, __cil_tmp5);
2134  }
2135#line 270
2136  if (tmp != 0) {
2137#line 271
2138    return (-16);
2139  } else {
2140
2141  }
2142  {
2143#line 272
2144  __cil_tmp6 = & nowayout;
2145#line 272
2146  __cil_tmp7 = *__cil_tmp6;
2147#line 272
2148  if ((int )__cil_tmp7) {
2149    {
2150#line 273
2151    __module_get(& __this_module);
2152    }
2153  } else {
2154
2155  }
2156  }
2157  {
2158#line 276
2159  wdt_startup();
2160#line 277
2161  tmp___0 = nonseekable_open(inode, file);
2162  }
2163#line 277
2164  return (tmp___0);
2165}
2166}
2167#line 280 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2168static int fop_close(struct inode *inode , struct file *file ) 
2169{ signed char __cil_tmp3 ;
2170  int __cil_tmp4 ;
2171  unsigned long volatile   *__cil_tmp5 ;
2172
2173  {
2174  {
2175#line 282
2176  __cil_tmp3 = (signed char )wdt_expect_close;
2177#line 282
2178  __cil_tmp4 = (int )__cil_tmp3;
2179#line 282
2180  if (__cil_tmp4 == 42) {
2181    {
2182#line 283
2183    wdt_turnoff();
2184    }
2185  } else {
2186    {
2187#line 285
2188    printk("<2>sc520_wdt: Unexpected close, not stopping watchdog!\n");
2189#line 286
2190    wdt_keepalive();
2191    }
2192  }
2193  }
2194  {
2195#line 288
2196  __cil_tmp5 = (unsigned long volatile   *)(& wdt_is_open);
2197#line 288
2198  clear_bit(0, __cil_tmp5);
2199#line 289
2200  wdt_expect_close = (char)0;
2201  }
2202#line 290
2203  return (0);
2204}
2205}
2206#line 293 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2207static long fop_ioctl(struct file *file , unsigned int cmd , unsigned long arg ) 
2208{ void *argp ;
2209  int *p ;
2210  struct watchdog_info ident ;
2211  long tmp___0 ;
2212  int tmp___1 ;
2213  int __ret_pu ;
2214  int __pu_val ;
2215  int new_options ;
2216  int retval ;
2217  int __ret_gu ;
2218  unsigned long __val_gu ;
2219  int new_timeout ;
2220  int __ret_gu___0 ;
2221  unsigned long __val_gu___0 ;
2222  int tmp___2 ;
2223  int __ret_pu___0 ;
2224  int __pu_val___0 ;
2225  struct watchdog_info *__cil_tmp22 ;
2226  unsigned long __cil_tmp23 ;
2227  unsigned long __cil_tmp24 ;
2228  unsigned long __cil_tmp25 ;
2229  unsigned long __cil_tmp26 ;
2230  unsigned long __cil_tmp27 ;
2231  unsigned long __cil_tmp28 ;
2232  unsigned long __cil_tmp29 ;
2233  unsigned long __cil_tmp30 ;
2234  unsigned long __cil_tmp31 ;
2235  unsigned long __cil_tmp32 ;
2236  unsigned long __cil_tmp33 ;
2237  unsigned long __cil_tmp34 ;
2238  unsigned long __cil_tmp35 ;
2239  unsigned long __cil_tmp36 ;
2240  unsigned long __cil_tmp37 ;
2241  unsigned long __cil_tmp38 ;
2242  unsigned long __cil_tmp39 ;
2243  unsigned long __cil_tmp40 ;
2244  unsigned long __cil_tmp41 ;
2245  void const   *__cil_tmp42 ;
2246  int __cil_tmp43 ;
2247  int *__cil_tmp44 ;
2248
2249  {
2250#line 295
2251  argp = (void *)arg;
2252#line 296
2253  p = (int *)argp;
2254#line 297
2255  __cil_tmp22 = & ident;
2256#line 297
2257  *((__u32 *)__cil_tmp22) = 33152U;
2258#line 297
2259  __cil_tmp23 = (unsigned long )(& ident) + 4;
2260#line 297
2261  *((__u32 *)__cil_tmp23) = 1U;
2262#line 297
2263  __cil_tmp24 = 0 * 1UL;
2264#line 297
2265  __cil_tmp25 = 8 + __cil_tmp24;
2266#line 297
2267  __cil_tmp26 = (unsigned long )(& ident) + __cil_tmp25;
2268#line 297
2269  *((__u8 *)__cil_tmp26) = (__u8 )'S';
2270#line 297
2271  __cil_tmp27 = 1 * 1UL;
2272#line 297
2273  __cil_tmp28 = 8 + __cil_tmp27;
2274#line 297
2275  __cil_tmp29 = (unsigned long )(& ident) + __cil_tmp28;
2276#line 297
2277  *((__u8 *)__cil_tmp29) = (__u8 )'C';
2278#line 297
2279  __cil_tmp30 = 2 * 1UL;
2280#line 297
2281  __cil_tmp31 = 8 + __cil_tmp30;
2282#line 297
2283  __cil_tmp32 = (unsigned long )(& ident) + __cil_tmp31;
2284#line 297
2285  *((__u8 *)__cil_tmp32) = (__u8 )'5';
2286#line 297
2287  __cil_tmp33 = 3 * 1UL;
2288#line 297
2289  __cil_tmp34 = 8 + __cil_tmp33;
2290#line 297
2291  __cil_tmp35 = (unsigned long )(& ident) + __cil_tmp34;
2292#line 297
2293  *((__u8 *)__cil_tmp35) = (__u8 )'2';
2294#line 297
2295  __cil_tmp36 = 4 * 1UL;
2296#line 297
2297  __cil_tmp37 = 8 + __cil_tmp36;
2298#line 297
2299  __cil_tmp38 = (unsigned long )(& ident) + __cil_tmp37;
2300#line 297
2301  *((__u8 *)__cil_tmp38) = (__u8 )'0';
2302#line 297
2303  __cil_tmp39 = 5 * 1UL;
2304#line 297
2305  __cil_tmp40 = 8 + __cil_tmp39;
2306#line 297
2307  __cil_tmp41 = (unsigned long )(& ident) + __cil_tmp40;
2308#line 297
2309  *((__u8 *)__cil_tmp41) = (__u8 )'\000';
2310#line 305
2311  if ((int )cmd == -2144839936) {
2312#line 305
2313    goto case_neg_2144839936;
2314  } else
2315#line 307
2316  if ((int )cmd == -2147199231) {
2317#line 307
2318    goto case_neg_2147199231;
2319  } else
2320#line 308
2321  if ((int )cmd == -2147199230) {
2322#line 308
2323    goto case_neg_2147199230;
2324  } else
2325#line 310
2326  if ((int )cmd == -2147199228) {
2327#line 310
2328    goto case_neg_2147199228;
2329  } else
2330#line 329
2331  if ((int )cmd == -2147199227) {
2332#line 329
2333    goto case_neg_2147199227;
2334  } else
2335#line 332
2336  if ((int )cmd == -1073457402) {
2337#line 332
2338    goto case_neg_1073457402;
2339  } else
2340#line 345
2341  if ((int )cmd == -2147199225) {
2342#line 345
2343    goto case_neg_2147199225;
2344  } else {
2345    {
2346#line 347
2347    goto switch_default___3;
2348#line 304
2349    if (0) {
2350      case_neg_2144839936: /* CIL Label */ 
2351      {
2352#line 306
2353      __cil_tmp42 = (void const   *)(& ident);
2354#line 306
2355      tmp___1 = copy_to_user(argp, __cil_tmp42, 40U);
2356      }
2357#line 306
2358      if (tmp___1 != 0) {
2359#line 306
2360        tmp___0 = -14L;
2361      } else {
2362#line 306
2363        tmp___0 = 0L;
2364      }
2365#line 306
2366      return (tmp___0);
2367      case_neg_2147199231: /* CIL Label */ ;
2368      case_neg_2147199230: /* CIL Label */ 
2369      {
2370#line 309
2371      might_fault();
2372#line 309
2373      __pu_val = 0;
2374      }
2375#line 309
2376      if (4 == 1) {
2377#line 309
2378        goto case_1;
2379      } else
2380#line 309
2381      if (4 == 2) {
2382#line 309
2383        goto case_2;
2384      } else
2385#line 309
2386      if (4 == 4) {
2387#line 309
2388        goto case_4;
2389      } else
2390#line 309
2391      if (4 == 8) {
2392#line 309
2393        goto case_8;
2394      } else {
2395        {
2396#line 309
2397        goto switch_default;
2398#line 309
2399        if (0) {
2400          case_1: /* CIL Label */ 
2401#line 309
2402          __asm__  volatile   ("call __put_user_1": "=a" (__ret_pu): "0" (__pu_val),
2403                               "c" (p): "ebx");
2404#line 309
2405          goto ldv_18094;
2406          case_2: /* CIL Label */ 
2407#line 309
2408          __asm__  volatile   ("call __put_user_2": "=a" (__ret_pu): "0" (__pu_val),
2409                               "c" (p): "ebx");
2410#line 309
2411          goto ldv_18094;
2412          case_4: /* CIL Label */ 
2413#line 309
2414          __asm__  volatile   ("call __put_user_4": "=a" (__ret_pu): "0" (__pu_val),
2415                               "c" (p): "ebx");
2416#line 309
2417          goto ldv_18094;
2418          case_8: /* CIL Label */ 
2419#line 309
2420          __asm__  volatile   ("call __put_user_8": "=a" (__ret_pu): "0" (__pu_val),
2421                               "c" (p): "ebx");
2422#line 309
2423          goto ldv_18094;
2424          switch_default: /* CIL Label */ 
2425#line 309
2426          __asm__  volatile   ("call __put_user_X": "=a" (__ret_pu): "0" (__pu_val),
2427                               "c" (p): "ebx");
2428#line 309
2429          goto ldv_18094;
2430        } else {
2431          switch_break___0: /* CIL Label */ ;
2432        }
2433        }
2434      }
2435      ldv_18094: ;
2436#line 309
2437      return ((long )__ret_pu);
2438      case_neg_2147199228: /* CIL Label */ 
2439      {
2440#line 312
2441      retval = -22;
2442#line 314
2443      might_fault();
2444      }
2445#line 314
2446      if (4 == 1) {
2447#line 314
2448        goto case_1___0;
2449      } else
2450#line 314
2451      if (4 == 2) {
2452#line 314
2453        goto case_2___0;
2454      } else
2455#line 314
2456      if (4 == 4) {
2457#line 314
2458        goto case_4___0;
2459      } else
2460#line 314
2461      if (4 == 8) {
2462#line 314
2463        goto case_8___0;
2464      } else {
2465        {
2466#line 314
2467        goto switch_default___0;
2468#line 314
2469        if (0) {
2470          case_1___0: /* CIL Label */ 
2471#line 314
2472          __asm__  volatile   ("call __get_user_1": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
2473#line 314
2474          goto ldv_18106;
2475          case_2___0: /* CIL Label */ 
2476#line 314
2477          __asm__  volatile   ("call __get_user_2": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
2478#line 314
2479          goto ldv_18106;
2480          case_4___0: /* CIL Label */ 
2481#line 314
2482          __asm__  volatile   ("call __get_user_4": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
2483#line 314
2484          goto ldv_18106;
2485          case_8___0: /* CIL Label */ 
2486#line 314
2487          __asm__  volatile   ("call __get_user_8": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
2488#line 314
2489          goto ldv_18106;
2490          switch_default___0: /* CIL Label */ 
2491#line 314
2492          __asm__  volatile   ("call __get_user_X": "=a" (__ret_gu), "=d" (__val_gu): "0" (p));
2493#line 314
2494          goto ldv_18106;
2495        } else {
2496          switch_break___1: /* CIL Label */ ;
2497        }
2498        }
2499      }
2500      ldv_18106: 
2501#line 314
2502      new_options = (int )__val_gu;
2503#line 314
2504      if (__ret_gu != 0) {
2505#line 315
2506        return (-14L);
2507      } else {
2508
2509      }
2510#line 317
2511      if (new_options & 1) {
2512        {
2513#line 318
2514        wdt_turnoff();
2515#line 319
2516        retval = 0;
2517        }
2518      } else {
2519
2520      }
2521      {
2522#line 322
2523      __cil_tmp43 = new_options & 2;
2524#line 322
2525      if (__cil_tmp43 != 0) {
2526        {
2527#line 323
2528        wdt_startup();
2529#line 324
2530        retval = 0;
2531        }
2532      } else {
2533
2534      }
2535      }
2536#line 327
2537      return ((long )retval);
2538      case_neg_2147199227: /* CIL Label */ 
2539      {
2540#line 330
2541      wdt_keepalive();
2542      }
2543#line 331
2544      return (0L);
2545      case_neg_1073457402: /* CIL Label */ 
2546      {
2547#line 336
2548      might_fault();
2549      }
2550#line 336
2551      if (4 == 1) {
2552#line 336
2553        goto case_1___1;
2554      } else
2555#line 336
2556      if (4 == 2) {
2557#line 336
2558        goto case_2___1;
2559      } else
2560#line 336
2561      if (4 == 4) {
2562#line 336
2563        goto case_4___1;
2564      } else
2565#line 336
2566      if (4 == 8) {
2567#line 336
2568        goto case_8___1;
2569      } else {
2570        {
2571#line 336
2572        goto switch_default___1;
2573#line 336
2574        if (0) {
2575          case_1___1: /* CIL Label */ 
2576#line 336
2577          __asm__  volatile   ("call __get_user_1": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (p));
2578#line 336
2579          goto ldv_18118;
2580          case_2___1: /* CIL Label */ 
2581#line 336
2582          __asm__  volatile   ("call __get_user_2": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (p));
2583#line 336
2584          goto ldv_18118;
2585          case_4___1: /* CIL Label */ 
2586#line 336
2587          __asm__  volatile   ("call __get_user_4": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (p));
2588#line 336
2589          goto ldv_18118;
2590          case_8___1: /* CIL Label */ 
2591#line 336
2592          __asm__  volatile   ("call __get_user_8": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (p));
2593#line 336
2594          goto ldv_18118;
2595          switch_default___1: /* CIL Label */ 
2596#line 336
2597          __asm__  volatile   ("call __get_user_X": "=a" (__ret_gu___0), "=d" (__val_gu___0): "0" (p));
2598#line 336
2599          goto ldv_18118;
2600        } else {
2601          switch_break___2: /* CIL Label */ ;
2602        }
2603        }
2604      }
2605      ldv_18118: 
2606#line 336
2607      new_timeout = (int )__val_gu___0;
2608#line 336
2609      if (__ret_gu___0 != 0) {
2610#line 337
2611        return (-14L);
2612      } else {
2613
2614      }
2615      {
2616#line 339
2617      tmp___2 = wdt_set_heartbeat(new_timeout);
2618      }
2619#line 339
2620      if (tmp___2 != 0) {
2621#line 340
2622        return (-22L);
2623      } else {
2624
2625      }
2626      {
2627#line 342
2628      wdt_keepalive();
2629      }
2630      case_neg_2147199225: /* CIL Label */ 
2631      {
2632#line 346
2633      might_fault();
2634#line 346
2635      __cil_tmp44 = & timeout;
2636#line 346
2637      __pu_val___0 = *__cil_tmp44;
2638      }
2639#line 346
2640      if (4 == 1) {
2641#line 346
2642        goto case_1___2;
2643      } else
2644#line 346
2645      if (4 == 2) {
2646#line 346
2647        goto case_2___2;
2648      } else
2649#line 346
2650      if (4 == 4) {
2651#line 346
2652        goto case_4___2;
2653      } else
2654#line 346
2655      if (4 == 8) {
2656#line 346
2657        goto case_8___2;
2658      } else {
2659        {
2660#line 346
2661        goto switch_default___2;
2662#line 346
2663        if (0) {
2664          case_1___2: /* CIL Label */ 
2665#line 346
2666          __asm__  volatile   ("call __put_user_1": "=a" (__ret_pu___0): "0" (__pu_val___0),
2667                               "c" (p): "ebx");
2668#line 346
2669          goto ldv_18128;
2670          case_2___2: /* CIL Label */ 
2671#line 346
2672          __asm__  volatile   ("call __put_user_2": "=a" (__ret_pu___0): "0" (__pu_val___0),
2673                               "c" (p): "ebx");
2674#line 346
2675          goto ldv_18128;
2676          case_4___2: /* CIL Label */ 
2677#line 346
2678          __asm__  volatile   ("call __put_user_4": "=a" (__ret_pu___0): "0" (__pu_val___0),
2679                               "c" (p): "ebx");
2680#line 346
2681          goto ldv_18128;
2682          case_8___2: /* CIL Label */ 
2683#line 346
2684          __asm__  volatile   ("call __put_user_8": "=a" (__ret_pu___0): "0" (__pu_val___0),
2685                               "c" (p): "ebx");
2686#line 346
2687          goto ldv_18128;
2688          switch_default___2: /* CIL Label */ 
2689#line 346
2690          __asm__  volatile   ("call __put_user_X": "=a" (__ret_pu___0): "0" (__pu_val___0),
2691                               "c" (p): "ebx");
2692#line 346
2693          goto ldv_18128;
2694        } else {
2695          switch_break___3: /* CIL Label */ ;
2696        }
2697        }
2698      }
2699      ldv_18128: ;
2700#line 346
2701      return ((long )__ret_pu___0);
2702      switch_default___3: /* CIL Label */ ;
2703#line 348
2704      return (-25L);
2705    } else {
2706      switch_break: /* CIL Label */ ;
2707    }
2708    }
2709  }
2710}
2711}
2712#line 352 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2713static struct file_operations  const  wdt_fops  = 
2714#line 352
2715     {& __this_module, & no_llseek, (ssize_t (*)(struct file * , char * , size_t  ,
2716                                               loff_t * ))0, & fop_write, (ssize_t (*)(struct kiocb * ,
2717                                                                                       struct iovec  const  * ,
2718                                                                                       unsigned long  ,
2719                                                                                       loff_t  ))0,
2720    (ssize_t (*)(struct kiocb * , struct iovec  const  * , unsigned long  , loff_t  ))0,
2721    (int (*)(struct file * , void * , int (*)(void * , char const   * , int  , loff_t  ,
2722                                              u64  , unsigned int  ) ))0, (unsigned int (*)(struct file * ,
2723                                                                                            struct poll_table_struct * ))0,
2724    & fop_ioctl, (long (*)(struct file * , unsigned int  , unsigned long  ))0, (int (*)(struct file * ,
2725                                                                                        struct vm_area_struct * ))0,
2726    & fop_open, (int (*)(struct file * , fl_owner_t  ))0, & fop_close, (int (*)(struct file * ,
2727                                                                                loff_t  ,
2728                                                                                loff_t  ,
2729                                                                                int  ))0,
2730    (int (*)(struct kiocb * , int  ))0, (int (*)(int  , struct file * , int  ))0,
2731    (int (*)(struct file * , int  , struct file_lock * ))0, (ssize_t (*)(struct file * ,
2732                                                                         struct page * ,
2733                                                                         int  , size_t  ,
2734                                                                         loff_t * ,
2735                                                                         int  ))0,
2736    (unsigned long (*)(struct file * , unsigned long  , unsigned long  , unsigned long  ,
2737                       unsigned long  ))0, (int (*)(int  ))0, (int (*)(struct file * ,
2738                                                                       int  , struct file_lock * ))0,
2739    (ssize_t (*)(struct pipe_inode_info * , struct file * , loff_t * , size_t  , unsigned int  ))0,
2740    (ssize_t (*)(struct file * , loff_t * , struct pipe_inode_info * , size_t  , unsigned int  ))0,
2741    (int (*)(struct file * , long  , struct file_lock ** ))0, (long (*)(struct file * ,
2742                                                                        int  , loff_t  ,
2743                                                                        loff_t  ))0};
2744#line 361 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2745static struct miscdevice wdt_miscdev  = 
2746#line 361
2747     {130, "watchdog", & wdt_fops, {(struct list_head *)0, (struct list_head *)0}, (struct device *)0,
2748    (struct device *)0, (char const   *)0, (unsigned short)0};
2749#line 371 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2750static int wdt_notify_sys(struct notifier_block *this , unsigned long code , void *unused ) 
2751{ 
2752
2753  {
2754#line 374
2755  if (code == 1UL) {
2756    {
2757#line 375
2758    wdt_turnoff();
2759    }
2760  } else
2761#line 374
2762  if (code == 2UL) {
2763    {
2764#line 375
2765    wdt_turnoff();
2766    }
2767  } else {
2768
2769  }
2770#line 376
2771  return (0);
2772}
2773}
2774#line 384 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2775static struct notifier_block wdt_notifier  =    {& wdt_notify_sys, (struct notifier_block *)0, 0};
2776#line 388 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2777static void sc520_wdt_unload(void) 
2778{ bool *__cil_tmp1 ;
2779  bool __cil_tmp2 ;
2780  void volatile   *__cil_tmp3 ;
2781
2782  {
2783  {
2784#line 390
2785  __cil_tmp1 = & nowayout;
2786#line 390
2787  __cil_tmp2 = *__cil_tmp1;
2788#line 390
2789  if (! __cil_tmp2) {
2790    {
2791#line 391
2792    wdt_turnoff();
2793    }
2794  } else {
2795
2796  }
2797  }
2798  {
2799#line 394
2800  misc_deregister(& wdt_miscdev);
2801#line 395
2802  unregister_reboot_notifier(& wdt_notifier);
2803#line 396
2804  __cil_tmp3 = (void volatile   *)wdtmrctl;
2805#line 396
2806  iounmap(__cil_tmp3);
2807  }
2808#line 397
2809  return;
2810}
2811}
2812#line 399 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2813static int sc520_wdt_init(void) 
2814{ int rc ;
2815  int tmp ;
2816  void *tmp___0 ;
2817  int *__cil_tmp4 ;
2818  int __cil_tmp5 ;
2819  __u16 *__cil_tmp6 ;
2820  unsigned long __cil_tmp7 ;
2821  unsigned long __cil_tmp8 ;
2822  int *__cil_tmp9 ;
2823  int __cil_tmp10 ;
2824  bool *__cil_tmp11 ;
2825  bool __cil_tmp12 ;
2826  int __cil_tmp13 ;
2827  void volatile   *__cil_tmp14 ;
2828
2829  {
2830  {
2831#line 401
2832  rc = -16;
2833#line 405
2834  __cil_tmp4 = & timeout;
2835#line 405
2836  __cil_tmp5 = *__cil_tmp4;
2837#line 405
2838  tmp = wdt_set_heartbeat(__cil_tmp5);
2839  }
2840#line 405
2841  if (tmp != 0) {
2842    {
2843#line 406
2844    wdt_set_heartbeat(30);
2845#line 407
2846    printk("<6>sc520_wdt: timeout value must be 1 <= timeout <= 3600, using %d\n",
2847           30);
2848    }
2849  } else {
2850
2851  }
2852  {
2853#line 411
2854  tmp___0 = ioremap(4294900912ULL, 2UL);
2855#line 411
2856  wdtmrctl = (__u16 *)tmp___0;
2857  }
2858  {
2859#line 412
2860  __cil_tmp6 = (__u16 *)0;
2861#line 412
2862  __cil_tmp7 = (unsigned long )__cil_tmp6;
2863#line 412
2864  __cil_tmp8 = (unsigned long )wdtmrctl;
2865#line 412
2866  if (__cil_tmp8 == __cil_tmp7) {
2867    {
2868#line 413
2869    printk("<3>sc520_wdt: Unable to remap memory\n");
2870#line 414
2871    rc = -12;
2872    }
2873#line 415
2874    goto err_out_region2;
2875  } else {
2876
2877  }
2878  }
2879  {
2880#line 418
2881  rc = register_reboot_notifier(& wdt_notifier);
2882  }
2883#line 419
2884  if (rc != 0) {
2885    {
2886#line 420
2887    printk("<3>sc520_wdt: cannot register reboot notifier (err=%d)\n", rc);
2888    }
2889#line 421
2890    goto err_out_ioremap;
2891  } else {
2892
2893  }
2894  {
2895#line 424
2896  rc = misc_register(& wdt_miscdev);
2897  }
2898#line 425
2899  if (rc != 0) {
2900    {
2901#line 426
2902    printk("<3>sc520_wdt: cannot register miscdev on minor=%d (err=%d)\n", 130, rc);
2903    }
2904#line 428
2905    goto err_out_notifier;
2906  } else {
2907
2908  }
2909  {
2910#line 431
2911  __cil_tmp9 = & timeout;
2912#line 431
2913  __cil_tmp10 = *__cil_tmp9;
2914#line 431
2915  __cil_tmp11 = & nowayout;
2916#line 431
2917  __cil_tmp12 = *__cil_tmp11;
2918#line 431
2919  __cil_tmp13 = (int )__cil_tmp12;
2920#line 431
2921  printk("<6>sc520_wdt: WDT driver for SC520 initialised. timeout=%d sec (nowayout=%d)\n",
2922         __cil_tmp10, __cil_tmp13);
2923  }
2924#line 434
2925  return (0);
2926  err_out_notifier: 
2927  {
2928#line 437
2929  unregister_reboot_notifier(& wdt_notifier);
2930  }
2931  err_out_ioremap: 
2932  {
2933#line 439
2934  __cil_tmp14 = (void volatile   *)wdtmrctl;
2935#line 439
2936  iounmap(__cil_tmp14);
2937  }
2938  err_out_region2: ;
2939#line 441
2940  return (rc);
2941}
2942}
2943#line 469
2944extern void ldv_check_final_state(void) ;
2945#line 472
2946extern void ldv_check_return_value(int  ) ;
2947#line 475
2948extern void ldv_initialize(void) ;
2949#line 478
2950extern int __VERIFIER_nondet_int(void) ;
2951#line 481 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2952int LDV_IN_INTERRUPT  ;
2953#line 484 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
2954void main(void) 
2955{ struct file *var_group1 ;
2956  char const   *var_fop_write_6_p1 ;
2957  size_t var_fop_write_6_p2 ;
2958  loff_t *var_fop_write_6_p3 ;
2959  ssize_t res_fop_write_6 ;
2960  struct inode *var_group2 ;
2961  int res_fop_open_7 ;
2962  unsigned int var_fop_ioctl_9_p1 ;
2963  unsigned long var_fop_ioctl_9_p2 ;
2964  struct notifier_block *var_group3 ;
2965  unsigned long var_wdt_notify_sys_10_p1 ;
2966  void *var_wdt_notify_sys_10_p2 ;
2967  int ldv_s_wdt_fops_file_operations ;
2968  int tmp ;
2969  int tmp___0 ;
2970  int tmp___1 ;
2971  int __cil_tmp17 ;
2972
2973  {
2974  {
2975#line 653
2976  ldv_s_wdt_fops_file_operations = 0;
2977#line 619
2978  LDV_IN_INTERRUPT = 1;
2979#line 628
2980  ldv_initialize();
2981#line 651
2982  tmp = sc520_wdt_init();
2983  }
2984#line 651
2985  if (tmp != 0) {
2986#line 652
2987    goto ldv_final;
2988  } else {
2989
2990  }
2991#line 659
2992  goto ldv_18202;
2993  ldv_18201: 
2994  {
2995#line 663
2996  tmp___0 = __VERIFIER_nondet_int();
2997  }
2998#line 665
2999  if (tmp___0 == 0) {
3000#line 665
3001    goto case_0;
3002  } else
3003#line 701
3004  if (tmp___0 == 1) {
3005#line 701
3006    goto case_1;
3007  } else
3008#line 737
3009  if (tmp___0 == 2) {
3010#line 737
3011    goto case_2;
3012  } else
3013#line 770
3014  if (tmp___0 == 3) {
3015#line 770
3016    goto case_3;
3017  } else
3018#line 803
3019  if (tmp___0 == 4) {
3020#line 803
3021    goto case_4;
3022  } else {
3023    {
3024#line 836
3025    goto switch_default;
3026#line 663
3027    if (0) {
3028      case_0: /* CIL Label */ ;
3029#line 668
3030      if (ldv_s_wdt_fops_file_operations == 0) {
3031        {
3032#line 690
3033        res_fop_open_7 = fop_open(var_group2, var_group1);
3034#line 691
3035        ldv_check_return_value(res_fop_open_7);
3036        }
3037#line 692
3038        if (res_fop_open_7 != 0) {
3039#line 693
3040          goto ldv_module_exit;
3041        } else {
3042
3043        }
3044#line 694
3045        ldv_s_wdt_fops_file_operations = ldv_s_wdt_fops_file_operations + 1;
3046      } else {
3047
3048      }
3049#line 700
3050      goto ldv_18195;
3051      case_1: /* CIL Label */ ;
3052#line 704
3053      if (ldv_s_wdt_fops_file_operations == 1) {
3054        {
3055#line 726
3056        res_fop_write_6 = fop_write(var_group1, var_fop_write_6_p1, var_fop_write_6_p2,
3057                                    var_fop_write_6_p3);
3058#line 727
3059        __cil_tmp17 = (int )res_fop_write_6;
3060#line 727
3061        ldv_check_return_value(__cil_tmp17);
3062        }
3063#line 728
3064        if (res_fop_write_6 < 0L) {
3065#line 729
3066          goto ldv_module_exit;
3067        } else {
3068
3069        }
3070#line 730
3071        ldv_s_wdt_fops_file_operations = ldv_s_wdt_fops_file_operations + 1;
3072      } else {
3073
3074      }
3075#line 736
3076      goto ldv_18195;
3077      case_2: /* CIL Label */ ;
3078#line 740
3079      if (ldv_s_wdt_fops_file_operations == 2) {
3080        {
3081#line 762
3082        fop_close(var_group2, var_group1);
3083#line 763
3084        ldv_s_wdt_fops_file_operations = 0;
3085        }
3086      } else {
3087
3088      }
3089#line 769
3090      goto ldv_18195;
3091      case_3: /* CIL Label */ 
3092      {
3093#line 795
3094      fop_ioctl(var_group1, var_fop_ioctl_9_p1, var_fop_ioctl_9_p2);
3095      }
3096#line 802
3097      goto ldv_18195;
3098      case_4: /* CIL Label */ 
3099      {
3100#line 828
3101      wdt_notify_sys(var_group3, var_wdt_notify_sys_10_p1, var_wdt_notify_sys_10_p2);
3102      }
3103#line 835
3104      goto ldv_18195;
3105      switch_default: /* CIL Label */ ;
3106#line 836
3107      goto ldv_18195;
3108    } else {
3109      switch_break: /* CIL Label */ ;
3110    }
3111    }
3112  }
3113  ldv_18195: ;
3114  ldv_18202: 
3115  {
3116#line 659
3117  tmp___1 = __VERIFIER_nondet_int();
3118  }
3119#line 659
3120  if (tmp___1 != 0) {
3121#line 661
3122    goto ldv_18201;
3123  } else
3124#line 659
3125  if (ldv_s_wdt_fops_file_operations != 0) {
3126#line 661
3127    goto ldv_18201;
3128  } else {
3129#line 663
3130    goto ldv_18203;
3131  }
3132  ldv_18203: ;
3133  ldv_module_exit: 
3134  {
3135#line 865
3136  sc520_wdt_unload();
3137  }
3138  ldv_final: 
3139  {
3140#line 868
3141  ldv_check_final_state();
3142  }
3143#line 871
3144  return;
3145}
3146}
3147#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
3148void ldv_blast_assert(void) 
3149{ 
3150
3151  {
3152  ERROR: ;
3153#line 6
3154  goto ERROR;
3155}
3156}
3157#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
3158extern int __VERIFIER_nondet_int(void) ;
3159#line 892 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3160int ldv_spin  =    0;
3161#line 896 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3162void ldv_check_alloc_flags(gfp_t flags ) 
3163{ 
3164
3165  {
3166#line 899
3167  if (ldv_spin != 0) {
3168#line 899
3169    if (flags != 32U) {
3170      {
3171#line 899
3172      ldv_blast_assert();
3173      }
3174    } else {
3175
3176    }
3177  } else {
3178
3179  }
3180#line 902
3181  return;
3182}
3183}
3184#line 902
3185extern struct page *ldv_some_page(void) ;
3186#line 905 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3187struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
3188{ struct page *tmp ;
3189
3190  {
3191#line 908
3192  if (ldv_spin != 0) {
3193#line 908
3194    if (flags != 32U) {
3195      {
3196#line 908
3197      ldv_blast_assert();
3198      }
3199    } else {
3200
3201    }
3202  } else {
3203
3204  }
3205  {
3206#line 910
3207  tmp = ldv_some_page();
3208  }
3209#line 910
3210  return (tmp);
3211}
3212}
3213#line 914 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3214void ldv_check_alloc_nonatomic(void) 
3215{ 
3216
3217  {
3218#line 917
3219  if (ldv_spin != 0) {
3220    {
3221#line 917
3222    ldv_blast_assert();
3223    }
3224  } else {
3225
3226  }
3227#line 920
3228  return;
3229}
3230}
3231#line 921 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3232void ldv_spin_lock(void) 
3233{ 
3234
3235  {
3236#line 924
3237  ldv_spin = 1;
3238#line 925
3239  return;
3240}
3241}
3242#line 928 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3243void ldv_spin_unlock(void) 
3244{ 
3245
3246  {
3247#line 931
3248  ldv_spin = 0;
3249#line 932
3250  return;
3251}
3252}
3253#line 935 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3254int ldv_spin_trylock(void) 
3255{ int is_lock ;
3256
3257  {
3258  {
3259#line 940
3260  is_lock = __VERIFIER_nondet_int();
3261  }
3262#line 942
3263  if (is_lock != 0) {
3264#line 945
3265    return (0);
3266  } else {
3267#line 950
3268    ldv_spin = 1;
3269#line 952
3270    return (1);
3271  }
3272}
3273}
3274#line 956 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3275__inline static void spin_lock(spinlock_t *lock ) 
3276{ 
3277
3278  {
3279  {
3280#line 961
3281  ldv_spin_lock();
3282#line 963
3283  ldv_spin_lock_1(lock);
3284  }
3285#line 964
3286  return;
3287}
3288}
3289#line 998 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3290__inline static void spin_unlock(spinlock_t *lock ) 
3291{ 
3292
3293  {
3294  {
3295#line 1003
3296  ldv_spin_unlock();
3297#line 1005
3298  ldv_spin_unlock_5(lock);
3299  }
3300#line 1006
3301  return;
3302}
3303}
3304#line 1028 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3305__inline static void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) 
3306{ 
3307
3308  {
3309  {
3310#line 1034
3311  ldv_spin_unlock();
3312#line 1036
3313  ldv_spin_unlock_irqrestore_8(lock, flags);
3314  }
3315#line 1037
3316  return;
3317}
3318}
3319#line 1119 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/17361/dscv_tempdir/dscv/ri/43_1a/drivers/watchdog/sc520_wdt.c.p"
3320void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
3321{ 
3322
3323  {
3324  {
3325#line 1125
3326  ldv_check_alloc_flags(ldv_func_arg2);
3327#line 1127
3328  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
3329  }
3330#line 1128
3331  return ((void *)0);
3332}
3333}