Showing error 824

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--char--ramoops.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 2240
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 23 "include/asm-generic/int-ll64.h"
   5typedef unsigned short __u16;
   6#line 26 "include/asm-generic/int-ll64.h"
   7typedef unsigned int __u32;
   8#line 30 "include/asm-generic/int-ll64.h"
   9typedef unsigned long long __u64;
  10#line 43 "include/asm-generic/int-ll64.h"
  11typedef unsigned char u8;
  12#line 45 "include/asm-generic/int-ll64.h"
  13typedef short s16;
  14#line 46 "include/asm-generic/int-ll64.h"
  15typedef unsigned short u16;
  16#line 49 "include/asm-generic/int-ll64.h"
  17typedef unsigned int u32;
  18#line 51 "include/asm-generic/int-ll64.h"
  19typedef long long s64;
  20#line 52 "include/asm-generic/int-ll64.h"
  21typedef unsigned long long u64;
  22#line 14 "include/asm-generic/posix_types.h"
  23typedef long __kernel_long_t;
  24#line 15 "include/asm-generic/posix_types.h"
  25typedef unsigned long __kernel_ulong_t;
  26#line 44 "include/asm-generic/posix_types.h"
  27typedef __kernel_long_t __kernel_suseconds_t;
  28#line 75 "include/asm-generic/posix_types.h"
  29typedef __kernel_ulong_t __kernel_size_t;
  30#line 76 "include/asm-generic/posix_types.h"
  31typedef __kernel_long_t __kernel_ssize_t;
  32#line 91 "include/asm-generic/posix_types.h"
  33typedef long long __kernel_loff_t;
  34#line 92 "include/asm-generic/posix_types.h"
  35typedef __kernel_long_t __kernel_time_t;
  36#line 21 "include/linux/types.h"
  37typedef __u32 __kernel_dev_t;
  38#line 24 "include/linux/types.h"
  39typedef __kernel_dev_t dev_t;
  40#line 27 "include/linux/types.h"
  41typedef unsigned short umode_t;
  42#line 38 "include/linux/types.h"
  43typedef _Bool bool;
  44#line 54 "include/linux/types.h"
  45typedef __kernel_loff_t loff_t;
  46#line 63 "include/linux/types.h"
  47typedef __kernel_size_t size_t;
  48#line 68 "include/linux/types.h"
  49typedef __kernel_ssize_t ssize_t;
  50#line 101 "include/linux/types.h"
  51typedef unsigned long ulong;
  52#line 202 "include/linux/types.h"
  53typedef unsigned int gfp_t;
  54#line 206 "include/linux/types.h"
  55typedef u64 phys_addr_t;
  56#line 211 "include/linux/types.h"
  57typedef phys_addr_t resource_size_t;
  58#line 221 "include/linux/types.h"
  59struct __anonstruct_atomic_t_6 {
  60   int counter ;
  61};
  62#line 221 "include/linux/types.h"
  63typedef struct __anonstruct_atomic_t_6 atomic_t;
  64#line 226 "include/linux/types.h"
  65struct __anonstruct_atomic64_t_7 {
  66   long counter ;
  67};
  68#line 226 "include/linux/types.h"
  69typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  70#line 227 "include/linux/types.h"
  71struct list_head {
  72   struct list_head *next ;
  73   struct list_head *prev ;
  74};
  75#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  76struct module;
  77#line 55
  78struct module;
  79#line 146 "include/linux/init.h"
  80typedef void (*ctor_fn_t)(void);
  81#line 46 "include/linux/dynamic_debug.h"
  82struct device;
  83#line 46
  84struct device;
  85#line 57
  86struct completion;
  87#line 57
  88struct completion;
  89#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  90struct page;
  91#line 58
  92struct page;
  93#line 26 "include/asm-generic/getorder.h"
  94struct task_struct;
  95#line 26
  96struct task_struct;
  97#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
  98struct file;
  99#line 290
 100struct file;
 101#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 102struct arch_spinlock;
 103#line 327
 104struct arch_spinlock;
 105#line 306 "include/linux/bitmap.h"
 106struct bug_entry {
 107   int bug_addr_disp ;
 108   int file_disp ;
 109   unsigned short line ;
 110   unsigned short flags ;
 111};
 112#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 113struct static_key;
 114#line 234
 115struct static_key;
 116#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 117struct kmem_cache;
 118#line 23 "include/asm-generic/atomic-long.h"
 119typedef atomic64_t atomic_long_t;
 120#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 121typedef u16 __ticket_t;
 122#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 123typedef u32 __ticketpair_t;
 124#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 125struct __raw_tickets {
 126   __ticket_t head ;
 127   __ticket_t tail ;
 128};
 129#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 130union __anonunion_ldv_5907_29 {
 131   __ticketpair_t head_tail ;
 132   struct __raw_tickets tickets ;
 133};
 134#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 135struct arch_spinlock {
 136   union __anonunion_ldv_5907_29 ldv_5907 ;
 137};
 138#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 139typedef struct arch_spinlock arch_spinlock_t;
 140#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 141struct lockdep_map;
 142#line 34
 143struct lockdep_map;
 144#line 55 "include/linux/debug_locks.h"
 145struct stack_trace {
 146   unsigned int nr_entries ;
 147   unsigned int max_entries ;
 148   unsigned long *entries ;
 149   int skip ;
 150};
 151#line 26 "include/linux/stacktrace.h"
 152struct lockdep_subclass_key {
 153   char __one_byte ;
 154};
 155#line 53 "include/linux/lockdep.h"
 156struct lock_class_key {
 157   struct lockdep_subclass_key subkeys[8U] ;
 158};
 159#line 59 "include/linux/lockdep.h"
 160struct lock_class {
 161   struct list_head hash_entry ;
 162   struct list_head lock_entry ;
 163   struct lockdep_subclass_key *key ;
 164   unsigned int subclass ;
 165   unsigned int dep_gen_id ;
 166   unsigned long usage_mask ;
 167   struct stack_trace usage_traces[13U] ;
 168   struct list_head locks_after ;
 169   struct list_head locks_before ;
 170   unsigned int version ;
 171   unsigned long ops ;
 172   char const   *name ;
 173   int name_version ;
 174   unsigned long contention_point[4U] ;
 175   unsigned long contending_point[4U] ;
 176};
 177#line 144 "include/linux/lockdep.h"
 178struct lockdep_map {
 179   struct lock_class_key *key ;
 180   struct lock_class *class_cache[2U] ;
 181   char const   *name ;
 182   int cpu ;
 183   unsigned long ip ;
 184};
 185#line 556 "include/linux/lockdep.h"
 186struct raw_spinlock {
 187   arch_spinlock_t raw_lock ;
 188   unsigned int magic ;
 189   unsigned int owner_cpu ;
 190   void *owner ;
 191   struct lockdep_map dep_map ;
 192};
 193#line 33 "include/linux/spinlock_types.h"
 194struct __anonstruct_ldv_6122_33 {
 195   u8 __padding[24U] ;
 196   struct lockdep_map dep_map ;
 197};
 198#line 33 "include/linux/spinlock_types.h"
 199union __anonunion_ldv_6123_32 {
 200   struct raw_spinlock rlock ;
 201   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 202};
 203#line 33 "include/linux/spinlock_types.h"
 204struct spinlock {
 205   union __anonunion_ldv_6123_32 ldv_6123 ;
 206};
 207#line 76 "include/linux/spinlock_types.h"
 208typedef struct spinlock spinlock_t;
 209#line 18 "include/linux/time.h"
 210struct timeval {
 211   __kernel_time_t tv_sec ;
 212   __kernel_suseconds_t tv_usec ;
 213};
 214#line 48 "include/linux/wait.h"
 215struct __wait_queue_head {
 216   spinlock_t lock ;
 217   struct list_head task_list ;
 218};
 219#line 53 "include/linux/wait.h"
 220typedef struct __wait_queue_head wait_queue_head_t;
 221#line 670 "include/linux/mmzone.h"
 222struct mutex {
 223   atomic_t count ;
 224   spinlock_t wait_lock ;
 225   struct list_head wait_list ;
 226   struct task_struct *owner ;
 227   char const   *name ;
 228   void *magic ;
 229   struct lockdep_map dep_map ;
 230};
 231#line 128 "include/linux/rwsem.h"
 232struct completion {
 233   unsigned int done ;
 234   wait_queue_head_t wait ;
 235};
 236#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
 237struct resource {
 238   resource_size_t start ;
 239   resource_size_t end ;
 240   char const   *name ;
 241   unsigned long flags ;
 242   struct resource *parent ;
 243   struct resource *sibling ;
 244   struct resource *child ;
 245};
 246#line 312 "include/linux/jiffies.h"
 247union ktime {
 248   s64 tv64 ;
 249};
 250#line 59 "include/linux/ktime.h"
 251typedef union ktime ktime_t;
 252#line 341
 253struct tvec_base;
 254#line 341
 255struct tvec_base;
 256#line 342 "include/linux/ktime.h"
 257struct timer_list {
 258   struct list_head entry ;
 259   unsigned long expires ;
 260   struct tvec_base *base ;
 261   void (*function)(unsigned long  ) ;
 262   unsigned long data ;
 263   int slack ;
 264   int start_pid ;
 265   void *start_site ;
 266   char start_comm[16U] ;
 267   struct lockdep_map lockdep_map ;
 268};
 269#line 302 "include/linux/timer.h"
 270struct work_struct;
 271#line 302
 272struct work_struct;
 273#line 45 "include/linux/workqueue.h"
 274struct work_struct {
 275   atomic_long_t data ;
 276   struct list_head entry ;
 277   void (*func)(struct work_struct * ) ;
 278   struct lockdep_map lockdep_map ;
 279};
 280#line 46 "include/linux/pm.h"
 281struct pm_message {
 282   int event ;
 283};
 284#line 52 "include/linux/pm.h"
 285typedef struct pm_message pm_message_t;
 286#line 53 "include/linux/pm.h"
 287struct dev_pm_ops {
 288   int (*prepare)(struct device * ) ;
 289   void (*complete)(struct device * ) ;
 290   int (*suspend)(struct device * ) ;
 291   int (*resume)(struct device * ) ;
 292   int (*freeze)(struct device * ) ;
 293   int (*thaw)(struct device * ) ;
 294   int (*poweroff)(struct device * ) ;
 295   int (*restore)(struct device * ) ;
 296   int (*suspend_late)(struct device * ) ;
 297   int (*resume_early)(struct device * ) ;
 298   int (*freeze_late)(struct device * ) ;
 299   int (*thaw_early)(struct device * ) ;
 300   int (*poweroff_late)(struct device * ) ;
 301   int (*restore_early)(struct device * ) ;
 302   int (*suspend_noirq)(struct device * ) ;
 303   int (*resume_noirq)(struct device * ) ;
 304   int (*freeze_noirq)(struct device * ) ;
 305   int (*thaw_noirq)(struct device * ) ;
 306   int (*poweroff_noirq)(struct device * ) ;
 307   int (*restore_noirq)(struct device * ) ;
 308   int (*runtime_suspend)(struct device * ) ;
 309   int (*runtime_resume)(struct device * ) ;
 310   int (*runtime_idle)(struct device * ) ;
 311};
 312#line 289
 313enum rpm_status {
 314    RPM_ACTIVE = 0,
 315    RPM_RESUMING = 1,
 316    RPM_SUSPENDED = 2,
 317    RPM_SUSPENDING = 3
 318} ;
 319#line 296
 320enum rpm_request {
 321    RPM_REQ_NONE = 0,
 322    RPM_REQ_IDLE = 1,
 323    RPM_REQ_SUSPEND = 2,
 324    RPM_REQ_AUTOSUSPEND = 3,
 325    RPM_REQ_RESUME = 4
 326} ;
 327#line 304
 328struct wakeup_source;
 329#line 304
 330struct wakeup_source;
 331#line 494 "include/linux/pm.h"
 332struct pm_subsys_data {
 333   spinlock_t lock ;
 334   unsigned int refcount ;
 335};
 336#line 499
 337struct dev_pm_qos_request;
 338#line 499
 339struct pm_qos_constraints;
 340#line 499 "include/linux/pm.h"
 341struct dev_pm_info {
 342   pm_message_t power_state ;
 343   unsigned char can_wakeup : 1 ;
 344   unsigned char async_suspend : 1 ;
 345   bool is_prepared ;
 346   bool is_suspended ;
 347   bool ignore_children ;
 348   spinlock_t lock ;
 349   struct list_head entry ;
 350   struct completion completion ;
 351   struct wakeup_source *wakeup ;
 352   bool wakeup_path ;
 353   struct timer_list suspend_timer ;
 354   unsigned long timer_expires ;
 355   struct work_struct work ;
 356   wait_queue_head_t wait_queue ;
 357   atomic_t usage_count ;
 358   atomic_t child_count ;
 359   unsigned char disable_depth : 3 ;
 360   unsigned char idle_notification : 1 ;
 361   unsigned char request_pending : 1 ;
 362   unsigned char deferred_resume : 1 ;
 363   unsigned char run_wake : 1 ;
 364   unsigned char runtime_auto : 1 ;
 365   unsigned char no_callbacks : 1 ;
 366   unsigned char irq_safe : 1 ;
 367   unsigned char use_autosuspend : 1 ;
 368   unsigned char timer_autosuspends : 1 ;
 369   enum rpm_request request ;
 370   enum rpm_status runtime_status ;
 371   int runtime_error ;
 372   int autosuspend_delay ;
 373   unsigned long last_busy ;
 374   unsigned long active_jiffies ;
 375   unsigned long suspended_jiffies ;
 376   unsigned long accounting_timestamp ;
 377   ktime_t suspend_time ;
 378   s64 max_time_suspended_ns ;
 379   struct dev_pm_qos_request *pq_req ;
 380   struct pm_subsys_data *subsys_data ;
 381   struct pm_qos_constraints *constraints ;
 382};
 383#line 558 "include/linux/pm.h"
 384struct dev_pm_domain {
 385   struct dev_pm_ops ops ;
 386};
 387#line 18 "include/asm-generic/pci_iomap.h"
 388struct vm_area_struct;
 389#line 18
 390struct vm_area_struct;
 391#line 18 "include/linux/elf.h"
 392typedef __u64 Elf64_Addr;
 393#line 19 "include/linux/elf.h"
 394typedef __u16 Elf64_Half;
 395#line 23 "include/linux/elf.h"
 396typedef __u32 Elf64_Word;
 397#line 24 "include/linux/elf.h"
 398typedef __u64 Elf64_Xword;
 399#line 193 "include/linux/elf.h"
 400struct elf64_sym {
 401   Elf64_Word st_name ;
 402   unsigned char st_info ;
 403   unsigned char st_other ;
 404   Elf64_Half st_shndx ;
 405   Elf64_Addr st_value ;
 406   Elf64_Xword st_size ;
 407};
 408#line 201 "include/linux/elf.h"
 409typedef struct elf64_sym Elf64_Sym;
 410#line 445
 411struct sock;
 412#line 445
 413struct sock;
 414#line 446
 415struct kobject;
 416#line 446
 417struct kobject;
 418#line 447
 419enum kobj_ns_type {
 420    KOBJ_NS_TYPE_NONE = 0,
 421    KOBJ_NS_TYPE_NET = 1,
 422    KOBJ_NS_TYPES = 2
 423} ;
 424#line 453 "include/linux/elf.h"
 425struct kobj_ns_type_operations {
 426   enum kobj_ns_type type ;
 427   void *(*grab_current_ns)(void) ;
 428   void const   *(*netlink_ns)(struct sock * ) ;
 429   void const   *(*initial_ns)(void) ;
 430   void (*drop_ns)(void * ) ;
 431};
 432#line 57 "include/linux/kobject_ns.h"
 433struct attribute {
 434   char const   *name ;
 435   umode_t mode ;
 436   struct lock_class_key *key ;
 437   struct lock_class_key skey ;
 438};
 439#line 33 "include/linux/sysfs.h"
 440struct attribute_group {
 441   char const   *name ;
 442   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 443   struct attribute **attrs ;
 444};
 445#line 62 "include/linux/sysfs.h"
 446struct bin_attribute {
 447   struct attribute attr ;
 448   size_t size ;
 449   void *private ;
 450   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 451                   loff_t  , size_t  ) ;
 452   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 453                    loff_t  , size_t  ) ;
 454   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
 455};
 456#line 98 "include/linux/sysfs.h"
 457struct sysfs_ops {
 458   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 459   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 460   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 461};
 462#line 117
 463struct sysfs_dirent;
 464#line 117
 465struct sysfs_dirent;
 466#line 182 "include/linux/sysfs.h"
 467struct kref {
 468   atomic_t refcount ;
 469};
 470#line 49 "include/linux/kobject.h"
 471struct kset;
 472#line 49
 473struct kobj_type;
 474#line 49 "include/linux/kobject.h"
 475struct kobject {
 476   char const   *name ;
 477   struct list_head entry ;
 478   struct kobject *parent ;
 479   struct kset *kset ;
 480   struct kobj_type *ktype ;
 481   struct sysfs_dirent *sd ;
 482   struct kref kref ;
 483   unsigned char state_initialized : 1 ;
 484   unsigned char state_in_sysfs : 1 ;
 485   unsigned char state_add_uevent_sent : 1 ;
 486   unsigned char state_remove_uevent_sent : 1 ;
 487   unsigned char uevent_suppress : 1 ;
 488};
 489#line 107 "include/linux/kobject.h"
 490struct kobj_type {
 491   void (*release)(struct kobject * ) ;
 492   struct sysfs_ops  const  *sysfs_ops ;
 493   struct attribute **default_attrs ;
 494   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 495   void const   *(*namespace)(struct kobject * ) ;
 496};
 497#line 115 "include/linux/kobject.h"
 498struct kobj_uevent_env {
 499   char *envp[32U] ;
 500   int envp_idx ;
 501   char buf[2048U] ;
 502   int buflen ;
 503};
 504#line 122 "include/linux/kobject.h"
 505struct kset_uevent_ops {
 506   int (* const  filter)(struct kset * , struct kobject * ) ;
 507   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 508   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 509};
 510#line 139 "include/linux/kobject.h"
 511struct kset {
 512   struct list_head list ;
 513   spinlock_t list_lock ;
 514   struct kobject kobj ;
 515   struct kset_uevent_ops  const  *uevent_ops ;
 516};
 517#line 215
 518struct kernel_param;
 519#line 215
 520struct kernel_param;
 521#line 216 "include/linux/kobject.h"
 522struct kernel_param_ops {
 523   int (*set)(char const   * , struct kernel_param  const  * ) ;
 524   int (*get)(char * , struct kernel_param  const  * ) ;
 525   void (*free)(void * ) ;
 526};
 527#line 49 "include/linux/moduleparam.h"
 528struct kparam_string;
 529#line 49
 530struct kparam_array;
 531#line 49 "include/linux/moduleparam.h"
 532union __anonunion_ldv_13363_134 {
 533   void *arg ;
 534   struct kparam_string  const  *str ;
 535   struct kparam_array  const  *arr ;
 536};
 537#line 49 "include/linux/moduleparam.h"
 538struct kernel_param {
 539   char const   *name ;
 540   struct kernel_param_ops  const  *ops ;
 541   u16 perm ;
 542   s16 level ;
 543   union __anonunion_ldv_13363_134 ldv_13363 ;
 544};
 545#line 61 "include/linux/moduleparam.h"
 546struct kparam_string {
 547   unsigned int maxlen ;
 548   char *string ;
 549};
 550#line 67 "include/linux/moduleparam.h"
 551struct kparam_array {
 552   unsigned int max ;
 553   unsigned int elemsize ;
 554   unsigned int *num ;
 555   struct kernel_param_ops  const  *ops ;
 556   void *elem ;
 557};
 558#line 458 "include/linux/moduleparam.h"
 559struct static_key {
 560   atomic_t enabled ;
 561};
 562#line 225 "include/linux/jump_label.h"
 563struct tracepoint;
 564#line 225
 565struct tracepoint;
 566#line 226 "include/linux/jump_label.h"
 567struct tracepoint_func {
 568   void *func ;
 569   void *data ;
 570};
 571#line 29 "include/linux/tracepoint.h"
 572struct tracepoint {
 573   char const   *name ;
 574   struct static_key key ;
 575   void (*regfunc)(void) ;
 576   void (*unregfunc)(void) ;
 577   struct tracepoint_func *funcs ;
 578};
 579#line 86 "include/linux/tracepoint.h"
 580struct kernel_symbol {
 581   unsigned long value ;
 582   char const   *name ;
 583};
 584#line 27 "include/linux/export.h"
 585struct mod_arch_specific {
 586
 587};
 588#line 34 "include/linux/module.h"
 589struct module_param_attrs;
 590#line 34 "include/linux/module.h"
 591struct module_kobject {
 592   struct kobject kobj ;
 593   struct module *mod ;
 594   struct kobject *drivers_dir ;
 595   struct module_param_attrs *mp ;
 596};
 597#line 43 "include/linux/module.h"
 598struct module_attribute {
 599   struct attribute attr ;
 600   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 601   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 602                    size_t  ) ;
 603   void (*setup)(struct module * , char const   * ) ;
 604   int (*test)(struct module * ) ;
 605   void (*free)(struct module * ) ;
 606};
 607#line 69
 608struct exception_table_entry;
 609#line 69
 610struct exception_table_entry;
 611#line 198
 612enum module_state {
 613    MODULE_STATE_LIVE = 0,
 614    MODULE_STATE_COMING = 1,
 615    MODULE_STATE_GOING = 2
 616} ;
 617#line 204 "include/linux/module.h"
 618struct module_ref {
 619   unsigned long incs ;
 620   unsigned long decs ;
 621};
 622#line 219
 623struct module_sect_attrs;
 624#line 219
 625struct module_notes_attrs;
 626#line 219
 627struct ftrace_event_call;
 628#line 219 "include/linux/module.h"
 629struct module {
 630   enum module_state state ;
 631   struct list_head list ;
 632   char name[56U] ;
 633   struct module_kobject mkobj ;
 634   struct module_attribute *modinfo_attrs ;
 635   char const   *version ;
 636   char const   *srcversion ;
 637   struct kobject *holders_dir ;
 638   struct kernel_symbol  const  *syms ;
 639   unsigned long const   *crcs ;
 640   unsigned int num_syms ;
 641   struct kernel_param *kp ;
 642   unsigned int num_kp ;
 643   unsigned int num_gpl_syms ;
 644   struct kernel_symbol  const  *gpl_syms ;
 645   unsigned long const   *gpl_crcs ;
 646   struct kernel_symbol  const  *unused_syms ;
 647   unsigned long const   *unused_crcs ;
 648   unsigned int num_unused_syms ;
 649   unsigned int num_unused_gpl_syms ;
 650   struct kernel_symbol  const  *unused_gpl_syms ;
 651   unsigned long const   *unused_gpl_crcs ;
 652   struct kernel_symbol  const  *gpl_future_syms ;
 653   unsigned long const   *gpl_future_crcs ;
 654   unsigned int num_gpl_future_syms ;
 655   unsigned int num_exentries ;
 656   struct exception_table_entry *extable ;
 657   int (*init)(void) ;
 658   void *module_init ;
 659   void *module_core ;
 660   unsigned int init_size ;
 661   unsigned int core_size ;
 662   unsigned int init_text_size ;
 663   unsigned int core_text_size ;
 664   unsigned int init_ro_size ;
 665   unsigned int core_ro_size ;
 666   struct mod_arch_specific arch ;
 667   unsigned int taints ;
 668   unsigned int num_bugs ;
 669   struct list_head bug_list ;
 670   struct bug_entry *bug_table ;
 671   Elf64_Sym *symtab ;
 672   Elf64_Sym *core_symtab ;
 673   unsigned int num_symtab ;
 674   unsigned int core_num_syms ;
 675   char *strtab ;
 676   char *core_strtab ;
 677   struct module_sect_attrs *sect_attrs ;
 678   struct module_notes_attrs *notes_attrs ;
 679   char *args ;
 680   void *percpu ;
 681   unsigned int percpu_size ;
 682   unsigned int num_tracepoints ;
 683   struct tracepoint * const  *tracepoints_ptrs ;
 684   unsigned int num_trace_bprintk_fmt ;
 685   char const   **trace_bprintk_fmt_start ;
 686   struct ftrace_event_call **trace_events ;
 687   unsigned int num_trace_events ;
 688   struct list_head source_list ;
 689   struct list_head target_list ;
 690   struct task_struct *waiter ;
 691   void (*exit)(void) ;
 692   struct module_ref *refptr ;
 693   ctor_fn_t (**ctors)(void) ;
 694   unsigned int num_ctors ;
 695};
 696#line 88 "include/linux/kmemleak.h"
 697struct kmem_cache_cpu {
 698   void **freelist ;
 699   unsigned long tid ;
 700   struct page *page ;
 701   struct page *partial ;
 702   int node ;
 703   unsigned int stat[26U] ;
 704};
 705#line 55 "include/linux/slub_def.h"
 706struct kmem_cache_node {
 707   spinlock_t list_lock ;
 708   unsigned long nr_partial ;
 709   struct list_head partial ;
 710   atomic_long_t nr_slabs ;
 711   atomic_long_t total_objects ;
 712   struct list_head full ;
 713};
 714#line 66 "include/linux/slub_def.h"
 715struct kmem_cache_order_objects {
 716   unsigned long x ;
 717};
 718#line 76 "include/linux/slub_def.h"
 719struct kmem_cache {
 720   struct kmem_cache_cpu *cpu_slab ;
 721   unsigned long flags ;
 722   unsigned long min_partial ;
 723   int size ;
 724   int objsize ;
 725   int offset ;
 726   int cpu_partial ;
 727   struct kmem_cache_order_objects oo ;
 728   struct kmem_cache_order_objects max ;
 729   struct kmem_cache_order_objects min ;
 730   gfp_t allocflags ;
 731   int refcount ;
 732   void (*ctor)(void * ) ;
 733   int inuse ;
 734   int align ;
 735   int reserved ;
 736   char const   *name ;
 737   struct list_head list ;
 738   struct kobject kobj ;
 739   int remote_node_defrag_ratio ;
 740   struct kmem_cache_node *node[1024U] ;
 741};
 742#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
 743enum kmsg_dump_reason {
 744    KMSG_DUMP_PANIC = 0,
 745    KMSG_DUMP_OOPS = 1,
 746    KMSG_DUMP_EMERG = 2,
 747    KMSG_DUMP_RESTART = 3,
 748    KMSG_DUMP_HALT = 4,
 749    KMSG_DUMP_POWEROFF = 5
 750} ;
 751#line 24 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
 752struct kmsg_dumper {
 753   void (*dump)(struct kmsg_dumper * , enum kmsg_dump_reason  , char const   * , unsigned long  ,
 754                char const   * , unsigned long  ) ;
 755   struct list_head list ;
 756   int registered ;
 757};
 758#line 69 "include/linux/io.h"
 759struct klist_node;
 760#line 69
 761struct klist_node;
 762#line 37 "include/linux/klist.h"
 763struct klist_node {
 764   void *n_klist ;
 765   struct list_head n_node ;
 766   struct kref n_ref ;
 767};
 768#line 67
 769struct dma_map_ops;
 770#line 67 "include/linux/klist.h"
 771struct dev_archdata {
 772   void *acpi_handle ;
 773   struct dma_map_ops *dma_ops ;
 774   void *iommu ;
 775};
 776#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 777struct pdev_archdata {
 778
 779};
 780#line 17
 781struct device_private;
 782#line 17
 783struct device_private;
 784#line 18
 785struct device_driver;
 786#line 18
 787struct device_driver;
 788#line 19
 789struct driver_private;
 790#line 19
 791struct driver_private;
 792#line 20
 793struct class;
 794#line 20
 795struct class;
 796#line 21
 797struct subsys_private;
 798#line 21
 799struct subsys_private;
 800#line 22
 801struct bus_type;
 802#line 22
 803struct bus_type;
 804#line 23
 805struct device_node;
 806#line 23
 807struct device_node;
 808#line 24
 809struct iommu_ops;
 810#line 24
 811struct iommu_ops;
 812#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 813struct bus_attribute {
 814   struct attribute attr ;
 815   ssize_t (*show)(struct bus_type * , char * ) ;
 816   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
 817};
 818#line 51 "include/linux/device.h"
 819struct device_attribute;
 820#line 51
 821struct driver_attribute;
 822#line 51 "include/linux/device.h"
 823struct bus_type {
 824   char const   *name ;
 825   char const   *dev_name ;
 826   struct device *dev_root ;
 827   struct bus_attribute *bus_attrs ;
 828   struct device_attribute *dev_attrs ;
 829   struct driver_attribute *drv_attrs ;
 830   int (*match)(struct device * , struct device_driver * ) ;
 831   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 832   int (*probe)(struct device * ) ;
 833   int (*remove)(struct device * ) ;
 834   void (*shutdown)(struct device * ) ;
 835   int (*suspend)(struct device * , pm_message_t  ) ;
 836   int (*resume)(struct device * ) ;
 837   struct dev_pm_ops  const  *pm ;
 838   struct iommu_ops *iommu_ops ;
 839   struct subsys_private *p ;
 840};
 841#line 125
 842struct device_type;
 843#line 182
 844struct of_device_id;
 845#line 182 "include/linux/device.h"
 846struct device_driver {
 847   char const   *name ;
 848   struct bus_type *bus ;
 849   struct module *owner ;
 850   char const   *mod_name ;
 851   bool suppress_bind_attrs ;
 852   struct of_device_id  const  *of_match_table ;
 853   int (*probe)(struct device * ) ;
 854   int (*remove)(struct device * ) ;
 855   void (*shutdown)(struct device * ) ;
 856   int (*suspend)(struct device * , pm_message_t  ) ;
 857   int (*resume)(struct device * ) ;
 858   struct attribute_group  const  **groups ;
 859   struct dev_pm_ops  const  *pm ;
 860   struct driver_private *p ;
 861};
 862#line 245 "include/linux/device.h"
 863struct driver_attribute {
 864   struct attribute attr ;
 865   ssize_t (*show)(struct device_driver * , char * ) ;
 866   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
 867};
 868#line 299
 869struct class_attribute;
 870#line 299 "include/linux/device.h"
 871struct class {
 872   char const   *name ;
 873   struct module *owner ;
 874   struct class_attribute *class_attrs ;
 875   struct device_attribute *dev_attrs ;
 876   struct bin_attribute *dev_bin_attrs ;
 877   struct kobject *dev_kobj ;
 878   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
 879   char *(*devnode)(struct device * , umode_t * ) ;
 880   void (*class_release)(struct class * ) ;
 881   void (*dev_release)(struct device * ) ;
 882   int (*suspend)(struct device * , pm_message_t  ) ;
 883   int (*resume)(struct device * ) ;
 884   struct kobj_ns_type_operations  const  *ns_type ;
 885   void const   *(*namespace)(struct device * ) ;
 886   struct dev_pm_ops  const  *pm ;
 887   struct subsys_private *p ;
 888};
 889#line 394 "include/linux/device.h"
 890struct class_attribute {
 891   struct attribute attr ;
 892   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
 893   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
 894   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
 895};
 896#line 447 "include/linux/device.h"
 897struct device_type {
 898   char const   *name ;
 899   struct attribute_group  const  **groups ;
 900   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 901   char *(*devnode)(struct device * , umode_t * ) ;
 902   void (*release)(struct device * ) ;
 903   struct dev_pm_ops  const  *pm ;
 904};
 905#line 474 "include/linux/device.h"
 906struct device_attribute {
 907   struct attribute attr ;
 908   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
 909   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
 910                    size_t  ) ;
 911};
 912#line 557 "include/linux/device.h"
 913struct device_dma_parameters {
 914   unsigned int max_segment_size ;
 915   unsigned long segment_boundary_mask ;
 916};
 917#line 567
 918struct dma_coherent_mem;
 919#line 567 "include/linux/device.h"
 920struct device {
 921   struct device *parent ;
 922   struct device_private *p ;
 923   struct kobject kobj ;
 924   char const   *init_name ;
 925   struct device_type  const  *type ;
 926   struct mutex mutex ;
 927   struct bus_type *bus ;
 928   struct device_driver *driver ;
 929   void *platform_data ;
 930   struct dev_pm_info power ;
 931   struct dev_pm_domain *pm_domain ;
 932   int numa_node ;
 933   u64 *dma_mask ;
 934   u64 coherent_dma_mask ;
 935   struct device_dma_parameters *dma_parms ;
 936   struct list_head dma_pools ;
 937   struct dma_coherent_mem *dma_mem ;
 938   struct dev_archdata archdata ;
 939   struct device_node *of_node ;
 940   dev_t devt ;
 941   u32 id ;
 942   spinlock_t devres_lock ;
 943   struct list_head devres_head ;
 944   struct klist_node knode_class ;
 945   struct class *class ;
 946   struct attribute_group  const  **groups ;
 947   void (*release)(struct device * ) ;
 948};
 949#line 681 "include/linux/device.h"
 950struct wakeup_source {
 951   char const   *name ;
 952   struct list_head entry ;
 953   spinlock_t lock ;
 954   struct timer_list timer ;
 955   unsigned long timer_expires ;
 956   ktime_t total_time ;
 957   ktime_t max_time ;
 958   ktime_t last_time ;
 959   unsigned long event_count ;
 960   unsigned long active_count ;
 961   unsigned long relax_count ;
 962   unsigned long hit_count ;
 963   unsigned char active : 1 ;
 964};
 965#line 12 "include/linux/mod_devicetable.h"
 966typedef unsigned long kernel_ulong_t;
 967#line 215 "include/linux/mod_devicetable.h"
 968struct of_device_id {
 969   char name[32U] ;
 970   char type[32U] ;
 971   char compatible[128U] ;
 972   void *data ;
 973};
 974#line 492 "include/linux/mod_devicetable.h"
 975struct platform_device_id {
 976   char name[20U] ;
 977   kernel_ulong_t driver_data ;
 978};
 979#line 584
 980struct mfd_cell;
 981#line 584
 982struct mfd_cell;
 983#line 585 "include/linux/mod_devicetable.h"
 984struct platform_device {
 985   char const   *name ;
 986   int id ;
 987   struct device dev ;
 988   u32 num_resources ;
 989   struct resource *resource ;
 990   struct platform_device_id  const  *id_entry ;
 991   struct mfd_cell *mfd_cell ;
 992   struct pdev_archdata archdata ;
 993};
 994#line 163 "include/linux/platform_device.h"
 995struct platform_driver {
 996   int (*probe)(struct platform_device * ) ;
 997   int (*remove)(struct platform_device * ) ;
 998   void (*shutdown)(struct platform_device * ) ;
 999   int (*suspend)(struct platform_device * , pm_message_t  ) ;
1000   int (*resume)(struct platform_device * ) ;
1001   struct device_driver driver ;
1002   struct platform_device_id  const  *id_table ;
1003};
1004#line 272 "include/linux/platform_device.h"
1005struct ramoops_platform_data {
1006   unsigned long mem_size ;
1007   unsigned long mem_address ;
1008   unsigned long record_size ;
1009   int dump_oops ;
1010};
1011#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1012struct ramoops_context {
1013   struct kmsg_dumper dump ;
1014   void *virt_addr ;
1015   phys_addr_t phys_addr ;
1016   unsigned long size ;
1017   unsigned long record_size ;
1018   int dump_oops ;
1019   int count ;
1020   int max_count ;
1021};
1022#line 1 "<compiler builtins>"
1023
1024#line 1
1025long __builtin_expect(long  , long  ) ;
1026#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1027void ldv_spin_lock(void) ;
1028#line 3
1029void ldv_spin_unlock(void) ;
1030#line 4
1031int ldv_spin_trylock(void) ;
1032#line 482 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/bitops.h"
1033__inline static int fls64(__u64 x ) 
1034{ long bitpos ;
1035  unsigned int __cil_tmp3 ;
1036  unsigned int __cil_tmp4 ;
1037
1038  {
1039#line 484
1040  bitpos = -1L;
1041#line 490
1042  __asm__  ("bsrq %1,%0": "+r" (bitpos): "rm" (x));
1043  {
1044#line 493
1045  __cil_tmp3 = (unsigned int )bitpos;
1046#line 493
1047  __cil_tmp4 = __cil_tmp3 + 1U;
1048#line 493
1049  return ((int )__cil_tmp4);
1050  }
1051}
1052}
1053#line 160 "include/linux/bitops.h"
1054__inline static unsigned int fls_long(unsigned long l ) 
1055{ int tmp___0 ;
1056  __u64 __cil_tmp4 ;
1057
1058  {
1059  {
1060#line 164
1061  __cil_tmp4 = (__u64 )l;
1062#line 164
1063  tmp___0 = fls64(__cil_tmp4);
1064  }
1065#line 164
1066  return ((unsigned int )tmp___0);
1067}
1068}
1069#line 70 "include/linux/log2.h"
1070__inline static unsigned long __rounddown_pow_of_two(unsigned long n ) 
1071{ unsigned int tmp ;
1072  unsigned int __cil_tmp3 ;
1073  int __cil_tmp4 ;
1074
1075  {
1076  {
1077#line 72
1078  tmp = fls_long(n);
1079  }
1080  {
1081#line 72
1082  __cil_tmp3 = tmp - 1U;
1083#line 72
1084  __cil_tmp4 = (int )__cil_tmp3;
1085#line 72
1086  return (1UL << __cil_tmp4);
1087  }
1088}
1089}
1090#line 101 "include/linux/printk.h"
1091extern int printk(char const   *  , ...) ;
1092#line 320 "include/linux/kernel.h"
1093extern int sprintf(char * , char const   *  , ...) ;
1094#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
1095extern void *memset(void * , int  , size_t  ) ;
1096#line 27 "include/linux/err.h"
1097__inline static long PTR_ERR(void const   *ptr ) 
1098{ 
1099
1100  {
1101#line 29
1102  return ((long )ptr);
1103}
1104}
1105#line 32 "include/linux/err.h"
1106__inline static long IS_ERR(void const   *ptr ) 
1107{ long tmp ;
1108  unsigned long __cil_tmp3 ;
1109  int __cil_tmp4 ;
1110  long __cil_tmp5 ;
1111
1112  {
1113  {
1114#line 34
1115  __cil_tmp3 = (unsigned long )ptr;
1116#line 34
1117  __cil_tmp4 = __cil_tmp3 > 0xfffffffffffff000UL;
1118#line 34
1119  __cil_tmp5 = (long )__cil_tmp4;
1120#line 34
1121  tmp = __builtin_expect(__cil_tmp5, 0L);
1122  }
1123#line 34
1124  return (tmp);
1125}
1126}
1127#line 148 "include/linux/time.h"
1128extern void do_gettimeofday(struct timeval * ) ;
1129#line 138 "include/linux/ioport.h"
1130extern struct resource iomem_resource ;
1131#line 181
1132extern struct resource *__request_region(struct resource * , resource_size_t  , resource_size_t  ,
1133                                         char const   * , int  ) ;
1134#line 192
1135extern void __release_region(struct resource * , resource_size_t  , resource_size_t  ) ;
1136#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1137extern void *ioremap_nocache(resource_size_t  , unsigned long  ) ;
1138#line 182 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1139__inline static void *ioremap(resource_size_t offset , unsigned long size ) 
1140{ void *tmp ;
1141
1142  {
1143  {
1144#line 184
1145  tmp = ioremap_nocache(offset, size);
1146  }
1147#line 184
1148  return (tmp);
1149}
1150}
1151#line 187
1152extern void iounmap(void volatile   * ) ;
1153#line 26 "include/linux/export.h"
1154extern struct module __this_module ;
1155#line 161 "include/linux/slab.h"
1156extern void kfree(void const   * ) ;
1157#line 220 "include/linux/slub_def.h"
1158extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1159#line 223
1160void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1161#line 353 "include/linux/slab.h"
1162__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1163#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1164extern void *__VERIFIER_nondet_pointer(void) ;
1165#line 11
1166void ldv_check_alloc_flags(gfp_t flags ) ;
1167#line 12
1168void ldv_check_alloc_nonatomic(void) ;
1169#line 14
1170struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1171#line 51 "include/linux/kmsg_dump.h"
1172extern int kmsg_dump_register(struct kmsg_dumper * ) ;
1173#line 53
1174extern int kmsg_dump_unregister(struct kmsg_dumper * ) ;
1175#line 175 "include/linux/platform_device.h"
1176extern void platform_driver_unregister(struct platform_driver * ) ;
1177#line 180
1178extern int platform_driver_probe(struct platform_driver * , int (*)(struct platform_device * ) ) ;
1179#line 202
1180extern struct platform_device *platform_create_bundle(struct platform_driver * , int (*)(struct platform_device * ) ,
1181                                                      struct resource * , unsigned int  ,
1182                                                      void const   * , size_t  ) ;
1183#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1184static ulong record_size  =    4096UL;
1185#line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1186static ulong mem_address  ;
1187#line 63 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1188static ulong mem_size  ;
1189#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1190static int dump_oops  =    1;
1191#line 82 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1192static struct ramoops_context oops_cxt  ;
1193#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1194static struct platform_device *dummy  ;
1195#line 85 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1196static struct ramoops_platform_data *dummy_data  ;
1197#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1198static void ramoops_do_dump(struct kmsg_dumper *dumper , enum kmsg_dump_reason reason ,
1199                            char const   *s1 , unsigned long l1 , char const   *s2 ,
1200                            unsigned long l2 ) 
1201{ struct ramoops_context *cxt ;
1202  struct kmsg_dumper  const  *__mptr ;
1203  unsigned long s1_start ;
1204  unsigned long s2_start ;
1205  unsigned long l1_cpy ;
1206  unsigned long l2_cpy ;
1207  int res ;
1208  int hdr_size ;
1209  char *buf ;
1210  char *buf_orig ;
1211  struct timeval timestamp ;
1212  unsigned long _min1 ;
1213  unsigned long _min2 ;
1214  unsigned long tmp ;
1215  unsigned long _min1___0 ;
1216  unsigned long _min2___0 ;
1217  unsigned long tmp___0 ;
1218  size_t __len ;
1219  void *__ret ;
1220  size_t __len___0 ;
1221  void *__ret___0 ;
1222  unsigned int __cil_tmp28 ;
1223  unsigned int __cil_tmp29 ;
1224  unsigned int __cil_tmp30 ;
1225  unsigned long __cil_tmp31 ;
1226  unsigned long __cil_tmp32 ;
1227  int __cil_tmp33 ;
1228  unsigned long __cil_tmp34 ;
1229  unsigned long __cil_tmp35 ;
1230  unsigned long __cil_tmp36 ;
1231  unsigned long __cil_tmp37 ;
1232  unsigned long __cil_tmp38 ;
1233  int __cil_tmp39 ;
1234  unsigned long __cil_tmp40 ;
1235  unsigned long __cil_tmp41 ;
1236  unsigned long __cil_tmp42 ;
1237  unsigned long __cil_tmp43 ;
1238  void *__cil_tmp44 ;
1239  void *__cil_tmp45 ;
1240  void *__cil_tmp46 ;
1241  unsigned long __cil_tmp47 ;
1242  unsigned long __cil_tmp48 ;
1243  unsigned long __cil_tmp49 ;
1244  char *__cil_tmp50 ;
1245  unsigned long __cil_tmp51 ;
1246  struct timeval *__cil_tmp52 ;
1247  __kernel_time_t __cil_tmp53 ;
1248  unsigned long __cil_tmp54 ;
1249  __kernel_suseconds_t __cil_tmp55 ;
1250  unsigned long __cil_tmp56 ;
1251  long __cil_tmp57 ;
1252  unsigned int __cil_tmp58 ;
1253  long __cil_tmp59 ;
1254  unsigned int __cil_tmp60 ;
1255  unsigned int __cil_tmp61 ;
1256  unsigned long __cil_tmp62 ;
1257  unsigned long __cil_tmp63 ;
1258  unsigned long __cil_tmp64 ;
1259  unsigned long __cil_tmp65 ;
1260  unsigned long __cil_tmp66 ;
1261  unsigned long __cil_tmp67 ;
1262  unsigned long __cil_tmp68 ;
1263  unsigned long __cil_tmp69 ;
1264  unsigned long __cil_tmp70 ;
1265  void *__cil_tmp71 ;
1266  char const   *__cil_tmp72 ;
1267  void const   *__cil_tmp73 ;
1268  char *__cil_tmp74 ;
1269  void *__cil_tmp75 ;
1270  char const   *__cil_tmp76 ;
1271  void const   *__cil_tmp77 ;
1272  unsigned long __cil_tmp78 ;
1273  unsigned long __cil_tmp79 ;
1274  unsigned long __cil_tmp80 ;
1275  unsigned long __cil_tmp81 ;
1276  int __cil_tmp82 ;
1277  unsigned long __cil_tmp83 ;
1278  unsigned long __cil_tmp84 ;
1279  int __cil_tmp85 ;
1280  int __cil_tmp86 ;
1281
1282  {
1283#line 91
1284  __mptr = (struct kmsg_dumper  const  *)dumper;
1285#line 91
1286  cxt = (struct ramoops_context *)__mptr;
1287  {
1288#line 99
1289  __cil_tmp28 = (unsigned int )reason;
1290#line 99
1291  if (__cil_tmp28 != 1U) {
1292    {
1293#line 99
1294    __cil_tmp29 = (unsigned int )reason;
1295#line 99
1296    if (__cil_tmp29 != 0U) {
1297#line 101
1298      return;
1299    } else {
1300
1301    }
1302    }
1303  } else {
1304
1305  }
1306  }
1307  {
1308#line 104
1309  __cil_tmp30 = (unsigned int )reason;
1310#line 104
1311  if (__cil_tmp30 == 1U) {
1312    {
1313#line 104
1314    __cil_tmp31 = (unsigned long )cxt;
1315#line 104
1316    __cil_tmp32 = __cil_tmp31 + 64;
1317#line 104
1318    __cil_tmp33 = *((int *)__cil_tmp32);
1319#line 104
1320    if (__cil_tmp33 == 0) {
1321#line 105
1322      return;
1323    } else {
1324
1325    }
1326    }
1327  } else {
1328
1329  }
1330  }
1331  {
1332#line 107
1333  __cil_tmp34 = (unsigned long )cxt;
1334#line 107
1335  __cil_tmp35 = __cil_tmp34 + 56;
1336#line 107
1337  __cil_tmp36 = *((unsigned long *)__cil_tmp35);
1338#line 107
1339  __cil_tmp37 = (unsigned long )cxt;
1340#line 107
1341  __cil_tmp38 = __cil_tmp37 + 68;
1342#line 107
1343  __cil_tmp39 = *((int *)__cil_tmp38);
1344#line 107
1345  __cil_tmp40 = (unsigned long )__cil_tmp39;
1346#line 107
1347  __cil_tmp41 = __cil_tmp40 * __cil_tmp36;
1348#line 107
1349  __cil_tmp42 = (unsigned long )cxt;
1350#line 107
1351  __cil_tmp43 = __cil_tmp42 + 32;
1352#line 107
1353  __cil_tmp44 = *((void **)__cil_tmp43);
1354#line 107
1355  __cil_tmp45 = __cil_tmp44 + __cil_tmp41;
1356#line 107
1357  buf = (char *)__cil_tmp45;
1358#line 108
1359  buf_orig = buf;
1360#line 110
1361  __cil_tmp46 = (void *)buf;
1362#line 110
1363  __cil_tmp47 = (unsigned long )cxt;
1364#line 110
1365  __cil_tmp48 = __cil_tmp47 + 56;
1366#line 110
1367  __cil_tmp49 = *((unsigned long *)__cil_tmp48);
1368#line 110
1369  memset(__cil_tmp46, 0, __cil_tmp49);
1370#line 111
1371  __cil_tmp50 = (char *)"====";
1372#line 111
1373  res = sprintf(buf, "%s", __cil_tmp50);
1374#line 112
1375  __cil_tmp51 = (unsigned long )res;
1376#line 112
1377  buf = buf + __cil_tmp51;
1378#line 113
1379  do_gettimeofday(& timestamp);
1380#line 114
1381  __cil_tmp52 = & timestamp;
1382#line 114
1383  __cil_tmp53 = *((__kernel_time_t *)__cil_tmp52);
1384#line 114
1385  __cil_tmp54 = (unsigned long )(& timestamp) + 8;
1386#line 114
1387  __cil_tmp55 = *((__kernel_suseconds_t *)__cil_tmp54);
1388#line 114
1389  res = sprintf(buf, "%lu.%lu\n", __cil_tmp53, __cil_tmp55);
1390#line 115
1391  __cil_tmp56 = (unsigned long )res;
1392#line 115
1393  buf = buf + __cil_tmp56;
1394#line 117
1395  __cil_tmp57 = (long )buf_orig;
1396#line 117
1397  __cil_tmp58 = (unsigned int )__cil_tmp57;
1398#line 117
1399  __cil_tmp59 = (long )buf;
1400#line 117
1401  __cil_tmp60 = (unsigned int )__cil_tmp59;
1402#line 117
1403  __cil_tmp61 = __cil_tmp60 - __cil_tmp58;
1404#line 117
1405  hdr_size = (int )__cil_tmp61;
1406#line 118
1407  _min1 = l2;
1408#line 118
1409  __cil_tmp62 = (unsigned long )hdr_size;
1410#line 118
1411  __cil_tmp63 = (unsigned long )cxt;
1412#line 118
1413  __cil_tmp64 = __cil_tmp63 + 56;
1414#line 118
1415  __cil_tmp65 = *((unsigned long *)__cil_tmp64);
1416#line 118
1417  _min2 = __cil_tmp65 - __cil_tmp62;
1418  }
1419#line 118
1420  if (_min1 < _min2) {
1421#line 118
1422    tmp = _min1;
1423  } else {
1424#line 118
1425    tmp = _min2;
1426  }
1427#line 118
1428  l2_cpy = tmp;
1429#line 119
1430  _min1___0 = l1;
1431#line 119
1432  __cil_tmp66 = (unsigned long )hdr_size;
1433#line 119
1434  __cil_tmp67 = (unsigned long )cxt;
1435#line 119
1436  __cil_tmp68 = __cil_tmp67 + 56;
1437#line 119
1438  __cil_tmp69 = *((unsigned long *)__cil_tmp68);
1439#line 119
1440  __cil_tmp70 = __cil_tmp69 - __cil_tmp66;
1441#line 119
1442  _min2___0 = __cil_tmp70 - l2_cpy;
1443#line 119
1444  if (_min1___0 < _min2___0) {
1445#line 119
1446    tmp___0 = _min1___0;
1447  } else {
1448#line 119
1449    tmp___0 = _min2___0;
1450  }
1451  {
1452#line 119
1453  l1_cpy = tmp___0;
1454#line 121
1455  s2_start = l2 - l2_cpy;
1456#line 122
1457  s1_start = l1 - l1_cpy;
1458#line 124
1459  __len = l1_cpy;
1460#line 124
1461  __cil_tmp71 = (void *)buf;
1462#line 124
1463  __cil_tmp72 = s1 + s1_start;
1464#line 124
1465  __cil_tmp73 = (void const   *)__cil_tmp72;
1466#line 124
1467  __ret = __builtin_memcpy(__cil_tmp71, __cil_tmp73, __len);
1468#line 125
1469  __len___0 = l2_cpy;
1470#line 125
1471  __cil_tmp74 = buf + l1_cpy;
1472#line 125
1473  __cil_tmp75 = (void *)__cil_tmp74;
1474#line 125
1475  __cil_tmp76 = s2 + s2_start;
1476#line 125
1477  __cil_tmp77 = (void const   *)__cil_tmp76;
1478#line 125
1479  __ret___0 = __builtin_memcpy(__cil_tmp75, __cil_tmp77, __len___0);
1480#line 127
1481  __cil_tmp78 = (unsigned long )cxt;
1482#line 127
1483  __cil_tmp79 = __cil_tmp78 + 68;
1484#line 127
1485  __cil_tmp80 = (unsigned long )cxt;
1486#line 127
1487  __cil_tmp81 = __cil_tmp80 + 72;
1488#line 127
1489  __cil_tmp82 = *((int *)__cil_tmp81);
1490#line 127
1491  __cil_tmp83 = (unsigned long )cxt;
1492#line 127
1493  __cil_tmp84 = __cil_tmp83 + 68;
1494#line 127
1495  __cil_tmp85 = *((int *)__cil_tmp84);
1496#line 127
1497  __cil_tmp86 = __cil_tmp85 + 1;
1498#line 127
1499  *((int *)__cil_tmp79) = __cil_tmp86 % __cil_tmp82;
1500  }
1501#line 128
1502  return;
1503}
1504}
1505#line 130 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1506static int ramoops_probe(struct platform_device *pdev ) 
1507{ struct ramoops_platform_data *pdata ;
1508  struct ramoops_context *cxt ;
1509  int err ;
1510  struct resource *tmp ;
1511  unsigned long __cil_tmp6 ;
1512  unsigned long __cil_tmp7 ;
1513  unsigned long __cil_tmp8 ;
1514  void *__cil_tmp9 ;
1515  unsigned long __cil_tmp10 ;
1516  unsigned long __cil_tmp11 ;
1517  unsigned long __cil_tmp12 ;
1518  unsigned long __cil_tmp13 ;
1519  unsigned long __cil_tmp14 ;
1520  unsigned long __cil_tmp15 ;
1521  unsigned long __cil_tmp16 ;
1522  unsigned long __cil_tmp17 ;
1523  unsigned long __cil_tmp18 ;
1524  unsigned long __cil_tmp19 ;
1525  unsigned long __cil_tmp20 ;
1526  unsigned long __cil_tmp21 ;
1527  unsigned long __cil_tmp22 ;
1528  unsigned long __cil_tmp23 ;
1529  unsigned long __cil_tmp24 ;
1530  unsigned long __cil_tmp25 ;
1531  unsigned long __cil_tmp26 ;
1532  unsigned long __cil_tmp27 ;
1533  unsigned long __cil_tmp28 ;
1534  unsigned long __cil_tmp29 ;
1535  unsigned long __cil_tmp30 ;
1536  unsigned long __cil_tmp31 ;
1537  unsigned long __cil_tmp32 ;
1538  unsigned long __cil_tmp33 ;
1539  unsigned long __cil_tmp34 ;
1540  unsigned long __cil_tmp35 ;
1541  unsigned long __cil_tmp36 ;
1542  unsigned long __cil_tmp37 ;
1543  unsigned long __cil_tmp38 ;
1544  unsigned long __cil_tmp39 ;
1545  unsigned long __cil_tmp40 ;
1546  unsigned long __cil_tmp41 ;
1547  unsigned long __cil_tmp42 ;
1548  unsigned long __cil_tmp43 ;
1549  unsigned long __cil_tmp44 ;
1550  unsigned long __cil_tmp45 ;
1551  unsigned long __cil_tmp46 ;
1552  unsigned long __cil_tmp47 ;
1553  unsigned long __cil_tmp48 ;
1554  unsigned long __cil_tmp49 ;
1555  unsigned long __cil_tmp50 ;
1556  unsigned long __cil_tmp51 ;
1557  unsigned long __cil_tmp52 ;
1558  unsigned long __cil_tmp53 ;
1559  phys_addr_t __cil_tmp54 ;
1560  unsigned long __cil_tmp55 ;
1561  unsigned long __cil_tmp56 ;
1562  unsigned long __cil_tmp57 ;
1563  resource_size_t __cil_tmp58 ;
1564  struct resource *__cil_tmp59 ;
1565  unsigned long __cil_tmp60 ;
1566  unsigned long __cil_tmp61 ;
1567  unsigned long __cil_tmp62 ;
1568  unsigned long __cil_tmp63 ;
1569  unsigned long __cil_tmp64 ;
1570  unsigned long __cil_tmp65 ;
1571  phys_addr_t __cil_tmp66 ;
1572  unsigned long __cil_tmp67 ;
1573  unsigned long __cil_tmp68 ;
1574  unsigned long __cil_tmp69 ;
1575  void *__cil_tmp70 ;
1576  unsigned long __cil_tmp71 ;
1577  unsigned long __cil_tmp72 ;
1578  unsigned long __cil_tmp73 ;
1579  void *__cil_tmp74 ;
1580  unsigned long __cil_tmp75 ;
1581  struct kmsg_dumper *__cil_tmp76 ;
1582  ulong *__cil_tmp77 ;
1583  ulong *__cil_tmp78 ;
1584  unsigned long __cil_tmp79 ;
1585  unsigned long __cil_tmp80 ;
1586  ulong *__cil_tmp81 ;
1587  unsigned long __cil_tmp82 ;
1588  unsigned long __cil_tmp83 ;
1589  int *__cil_tmp84 ;
1590  unsigned long __cil_tmp85 ;
1591  unsigned long __cil_tmp86 ;
1592  unsigned long __cil_tmp87 ;
1593  unsigned long __cil_tmp88 ;
1594  void *__cil_tmp89 ;
1595  void volatile   *__cil_tmp90 ;
1596  unsigned long __cil_tmp91 ;
1597  unsigned long __cil_tmp92 ;
1598  phys_addr_t __cil_tmp93 ;
1599  unsigned long __cil_tmp94 ;
1600  unsigned long __cil_tmp95 ;
1601  unsigned long __cil_tmp96 ;
1602  resource_size_t __cil_tmp97 ;
1603
1604  {
1605#line 132
1606  __cil_tmp6 = 16 + 280;
1607#line 132
1608  __cil_tmp7 = (unsigned long )pdev;
1609#line 132
1610  __cil_tmp8 = __cil_tmp7 + __cil_tmp6;
1611#line 132
1612  __cil_tmp9 = *((void **)__cil_tmp8);
1613#line 132
1614  pdata = (struct ramoops_platform_data *)__cil_tmp9;
1615#line 133
1616  cxt = & oops_cxt;
1617#line 134
1618  err = -22;
1619  {
1620#line 136
1621  __cil_tmp10 = *((unsigned long *)pdata);
1622#line 136
1623  if (__cil_tmp10 == 0UL) {
1624    {
1625#line 137
1626    printk("<3>ramoops: The memory size and the record size must be non-zero\n");
1627    }
1628#line 139
1629    goto fail3;
1630  } else {
1631    {
1632#line 136
1633    __cil_tmp11 = (unsigned long )pdata;
1634#line 136
1635    __cil_tmp12 = __cil_tmp11 + 16;
1636#line 136
1637    __cil_tmp13 = *((unsigned long *)__cil_tmp12);
1638#line 136
1639    if (__cil_tmp13 == 0UL) {
1640      {
1641#line 137
1642      printk("<3>ramoops: The memory size and the record size must be non-zero\n");
1643      }
1644#line 139
1645      goto fail3;
1646    } else {
1647
1648    }
1649    }
1650  }
1651  }
1652  {
1653#line 142
1654  __cil_tmp14 = *((unsigned long *)pdata);
1655#line 142
1656  *((unsigned long *)pdata) = __rounddown_pow_of_two(__cil_tmp14);
1657#line 143
1658  __cil_tmp15 = (unsigned long )pdata;
1659#line 143
1660  __cil_tmp16 = __cil_tmp15 + 16;
1661#line 143
1662  __cil_tmp17 = (unsigned long )pdata;
1663#line 143
1664  __cil_tmp18 = __cil_tmp17 + 16;
1665#line 143
1666  __cil_tmp19 = *((unsigned long *)__cil_tmp18);
1667#line 143
1668  *((unsigned long *)__cil_tmp16) = __rounddown_pow_of_two(__cil_tmp19);
1669  }
1670  {
1671#line 146
1672  __cil_tmp20 = *((unsigned long *)pdata);
1673#line 146
1674  if (__cil_tmp20 <= 4095UL) {
1675    {
1676#line 146
1677    __cil_tmp21 = (unsigned long )pdata;
1678#line 146
1679    __cil_tmp22 = __cil_tmp21 + 16;
1680#line 146
1681    __cil_tmp23 = *((unsigned long *)__cil_tmp22);
1682#line 146
1683    if (__cil_tmp23 <= 4095UL) {
1684      {
1685#line 148
1686      printk("<3>ramoops: memory size too small, minium is %lu\n", 4096UL);
1687      }
1688#line 149
1689      goto fail3;
1690    } else {
1691
1692    }
1693    }
1694  } else {
1695
1696  }
1697  }
1698  {
1699#line 152
1700  __cil_tmp24 = (unsigned long )pdata;
1701#line 152
1702  __cil_tmp25 = __cil_tmp24 + 16;
1703#line 152
1704  __cil_tmp26 = *((unsigned long *)__cil_tmp25);
1705#line 152
1706  __cil_tmp27 = *((unsigned long *)pdata);
1707#line 152
1708  if (__cil_tmp27 < __cil_tmp26) {
1709    {
1710#line 153
1711    printk("<3>ramoops: The memory size must be larger than the records size\n");
1712    }
1713#line 155
1714    goto fail3;
1715  } else {
1716
1717  }
1718  }
1719  {
1720#line 158
1721  __cil_tmp28 = (unsigned long )cxt;
1722#line 158
1723  __cil_tmp29 = __cil_tmp28 + 72;
1724#line 158
1725  __cil_tmp30 = (unsigned long )pdata;
1726#line 158
1727  __cil_tmp31 = __cil_tmp30 + 16;
1728#line 158
1729  __cil_tmp32 = *((unsigned long *)__cil_tmp31);
1730#line 158
1731  __cil_tmp33 = *((unsigned long *)pdata);
1732#line 158
1733  __cil_tmp34 = __cil_tmp33 / __cil_tmp32;
1734#line 158
1735  *((int *)__cil_tmp29) = (int )__cil_tmp34;
1736#line 159
1737  __cil_tmp35 = (unsigned long )cxt;
1738#line 159
1739  __cil_tmp36 = __cil_tmp35 + 68;
1740#line 159
1741  *((int *)__cil_tmp36) = 0;
1742#line 160
1743  __cil_tmp37 = (unsigned long )cxt;
1744#line 160
1745  __cil_tmp38 = __cil_tmp37 + 48;
1746#line 160
1747  *((unsigned long *)__cil_tmp38) = *((unsigned long *)pdata);
1748#line 161
1749  __cil_tmp39 = (unsigned long )cxt;
1750#line 161
1751  __cil_tmp40 = __cil_tmp39 + 40;
1752#line 161
1753  __cil_tmp41 = (unsigned long )pdata;
1754#line 161
1755  __cil_tmp42 = __cil_tmp41 + 8;
1756#line 161
1757  __cil_tmp43 = *((unsigned long *)__cil_tmp42);
1758#line 161
1759  *((phys_addr_t *)__cil_tmp40) = (phys_addr_t )__cil_tmp43;
1760#line 162
1761  __cil_tmp44 = (unsigned long )cxt;
1762#line 162
1763  __cil_tmp45 = __cil_tmp44 + 56;
1764#line 162
1765  __cil_tmp46 = (unsigned long )pdata;
1766#line 162
1767  __cil_tmp47 = __cil_tmp46 + 16;
1768#line 162
1769  *((unsigned long *)__cil_tmp45) = *((unsigned long *)__cil_tmp47);
1770#line 163
1771  __cil_tmp48 = (unsigned long )cxt;
1772#line 163
1773  __cil_tmp49 = __cil_tmp48 + 64;
1774#line 163
1775  __cil_tmp50 = (unsigned long )pdata;
1776#line 163
1777  __cil_tmp51 = __cil_tmp50 + 24;
1778#line 163
1779  *((int *)__cil_tmp49) = *((int *)__cil_tmp51);
1780#line 165
1781  __cil_tmp52 = (unsigned long )cxt;
1782#line 165
1783  __cil_tmp53 = __cil_tmp52 + 40;
1784#line 165
1785  __cil_tmp54 = *((phys_addr_t *)__cil_tmp53);
1786#line 165
1787  __cil_tmp55 = (unsigned long )cxt;
1788#line 165
1789  __cil_tmp56 = __cil_tmp55 + 48;
1790#line 165
1791  __cil_tmp57 = *((unsigned long *)__cil_tmp56);
1792#line 165
1793  __cil_tmp58 = (resource_size_t )__cil_tmp57;
1794#line 165
1795  tmp = __request_region(& iomem_resource, __cil_tmp54, __cil_tmp58, "ramoops", 0);
1796  }
1797  {
1798#line 165
1799  __cil_tmp59 = (struct resource *)0;
1800#line 165
1801  __cil_tmp60 = (unsigned long )__cil_tmp59;
1802#line 165
1803  __cil_tmp61 = (unsigned long )tmp;
1804#line 165
1805  if (__cil_tmp61 == __cil_tmp60) {
1806    {
1807#line 166
1808    printk("<3>ramoops: request mem region failed\n");
1809#line 167
1810    err = -22;
1811    }
1812#line 168
1813    goto fail3;
1814  } else {
1815
1816  }
1817  }
1818  {
1819#line 171
1820  __cil_tmp62 = (unsigned long )cxt;
1821#line 171
1822  __cil_tmp63 = __cil_tmp62 + 32;
1823#line 171
1824  __cil_tmp64 = (unsigned long )cxt;
1825#line 171
1826  __cil_tmp65 = __cil_tmp64 + 40;
1827#line 171
1828  __cil_tmp66 = *((phys_addr_t *)__cil_tmp65);
1829#line 171
1830  __cil_tmp67 = (unsigned long )cxt;
1831#line 171
1832  __cil_tmp68 = __cil_tmp67 + 48;
1833#line 171
1834  __cil_tmp69 = *((unsigned long *)__cil_tmp68);
1835#line 171
1836  *((void **)__cil_tmp63) = ioremap(__cil_tmp66, __cil_tmp69);
1837  }
1838  {
1839#line 172
1840  __cil_tmp70 = (void *)0;
1841#line 172
1842  __cil_tmp71 = (unsigned long )__cil_tmp70;
1843#line 172
1844  __cil_tmp72 = (unsigned long )cxt;
1845#line 172
1846  __cil_tmp73 = __cil_tmp72 + 32;
1847#line 172
1848  __cil_tmp74 = *((void **)__cil_tmp73);
1849#line 172
1850  __cil_tmp75 = (unsigned long )__cil_tmp74;
1851#line 172
1852  if (__cil_tmp75 == __cil_tmp71) {
1853    {
1854#line 173
1855    printk("<3>ramoops: ioremap failed\n");
1856    }
1857#line 174
1858    goto fail2;
1859  } else {
1860
1861  }
1862  }
1863  {
1864#line 177
1865  *((void (**)(struct kmsg_dumper * , enum kmsg_dump_reason  , char const   * , unsigned long  ,
1866               char const   * , unsigned long  ))cxt) = & ramoops_do_dump;
1867#line 178
1868  __cil_tmp76 = (struct kmsg_dumper *)cxt;
1869#line 178
1870  err = kmsg_dump_register(__cil_tmp76);
1871  }
1872#line 179
1873  if (err != 0) {
1874    {
1875#line 180
1876    printk("<3>ramoops: registering kmsg dumper failed\n");
1877    }
1878#line 181
1879    goto fail1;
1880  } else {
1881
1882  }
1883#line 188
1884  __cil_tmp77 = & mem_size;
1885#line 188
1886  *__cil_tmp77 = *((unsigned long *)pdata);
1887#line 189
1888  __cil_tmp78 = & mem_address;
1889#line 189
1890  __cil_tmp79 = (unsigned long )pdata;
1891#line 189
1892  __cil_tmp80 = __cil_tmp79 + 8;
1893#line 189
1894  *__cil_tmp78 = *((unsigned long *)__cil_tmp80);
1895#line 190
1896  __cil_tmp81 = & record_size;
1897#line 190
1898  __cil_tmp82 = (unsigned long )pdata;
1899#line 190
1900  __cil_tmp83 = __cil_tmp82 + 16;
1901#line 190
1902  *__cil_tmp81 = *((unsigned long *)__cil_tmp83);
1903#line 191
1904  __cil_tmp84 = & dump_oops;
1905#line 191
1906  __cil_tmp85 = (unsigned long )pdata;
1907#line 191
1908  __cil_tmp86 = __cil_tmp85 + 24;
1909#line 191
1910  *__cil_tmp84 = *((int *)__cil_tmp86);
1911#line 193
1912  return (0);
1913  fail1: 
1914  {
1915#line 196
1916  __cil_tmp87 = (unsigned long )cxt;
1917#line 196
1918  __cil_tmp88 = __cil_tmp87 + 32;
1919#line 196
1920  __cil_tmp89 = *((void **)__cil_tmp88);
1921#line 196
1922  __cil_tmp90 = (void volatile   *)__cil_tmp89;
1923#line 196
1924  iounmap(__cil_tmp90);
1925  }
1926  fail2: 
1927  {
1928#line 198
1929  __cil_tmp91 = (unsigned long )cxt;
1930#line 198
1931  __cil_tmp92 = __cil_tmp91 + 40;
1932#line 198
1933  __cil_tmp93 = *((phys_addr_t *)__cil_tmp92);
1934#line 198
1935  __cil_tmp94 = (unsigned long )cxt;
1936#line 198
1937  __cil_tmp95 = __cil_tmp94 + 48;
1938#line 198
1939  __cil_tmp96 = *((unsigned long *)__cil_tmp95);
1940#line 198
1941  __cil_tmp97 = (resource_size_t )__cil_tmp96;
1942#line 198
1943  __release_region(& iomem_resource, __cil_tmp93, __cil_tmp97);
1944  }
1945  fail3: ;
1946#line 200
1947  return (err);
1948}
1949}
1950#line 203 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
1951static int ramoops_remove(struct platform_device *pdev ) 
1952{ struct ramoops_context *cxt ;
1953  int tmp ;
1954  struct kmsg_dumper *__cil_tmp4 ;
1955  unsigned long __cil_tmp5 ;
1956  unsigned long __cil_tmp6 ;
1957  void *__cil_tmp7 ;
1958  void volatile   *__cil_tmp8 ;
1959  unsigned long __cil_tmp9 ;
1960  unsigned long __cil_tmp10 ;
1961  phys_addr_t __cil_tmp11 ;
1962  unsigned long __cil_tmp12 ;
1963  unsigned long __cil_tmp13 ;
1964  unsigned long __cil_tmp14 ;
1965  resource_size_t __cil_tmp15 ;
1966
1967  {
1968  {
1969#line 205
1970  cxt = & oops_cxt;
1971#line 207
1972  __cil_tmp4 = (struct kmsg_dumper *)cxt;
1973#line 207
1974  tmp = kmsg_dump_unregister(__cil_tmp4);
1975  }
1976#line 207
1977  if (tmp < 0) {
1978    {
1979#line 208
1980    printk("<4>ramoops: could not unregister kmsg_dumper\n");
1981    }
1982  } else {
1983
1984  }
1985  {
1986#line 210
1987  __cil_tmp5 = (unsigned long )cxt;
1988#line 210
1989  __cil_tmp6 = __cil_tmp5 + 32;
1990#line 210
1991  __cil_tmp7 = *((void **)__cil_tmp6);
1992#line 210
1993  __cil_tmp8 = (void volatile   *)__cil_tmp7;
1994#line 210
1995  iounmap(__cil_tmp8);
1996#line 211
1997  __cil_tmp9 = (unsigned long )cxt;
1998#line 211
1999  __cil_tmp10 = __cil_tmp9 + 40;
2000#line 211
2001  __cil_tmp11 = *((phys_addr_t *)__cil_tmp10);
2002#line 211
2003  __cil_tmp12 = (unsigned long )cxt;
2004#line 211
2005  __cil_tmp13 = __cil_tmp12 + 48;
2006#line 211
2007  __cil_tmp14 = *((unsigned long *)__cil_tmp13);
2008#line 211
2009  __cil_tmp15 = (resource_size_t )__cil_tmp14;
2010#line 211
2011  __release_region(& iomem_resource, __cil_tmp11, __cil_tmp15);
2012  }
2013#line 212
2014  return (0);
2015}
2016}
2017#line 215 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2018static struct platform_driver ramoops_driver  =    {(int (*)(struct platform_device * ))0, & ramoops_remove, (void (*)(struct platform_device * ))0,
2019    (int (*)(struct platform_device * , pm_message_t  ))0, (int (*)(struct platform_device * ))0,
2020    {"ramoops", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
2021     (struct of_device_id  const  *)0, (int (*)(struct device * ))0, (int (*)(struct device * ))0,
2022     (void (*)(struct device * ))0, (int (*)(struct device * , pm_message_t  ))0,
2023     (int (*)(struct device * ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
2024     (struct driver_private *)0}, (struct platform_device_id  const  *)0};
2025#line 223 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2026static int ramoops_init(void) 
2027{ int ret ;
2028  void *tmp ;
2029  long tmp___0 ;
2030  long tmp___1 ;
2031  struct ramoops_platform_data *__cil_tmp5 ;
2032  unsigned long __cil_tmp6 ;
2033  unsigned long __cil_tmp7 ;
2034  ulong *__cil_tmp8 ;
2035  unsigned long __cil_tmp9 ;
2036  unsigned long __cil_tmp10 ;
2037  ulong *__cil_tmp11 ;
2038  unsigned long __cil_tmp12 ;
2039  unsigned long __cil_tmp13 ;
2040  ulong *__cil_tmp14 ;
2041  unsigned long __cil_tmp15 ;
2042  unsigned long __cil_tmp16 ;
2043  int *__cil_tmp17 ;
2044  struct resource *__cil_tmp18 ;
2045  void const   *__cil_tmp19 ;
2046  void const   *__cil_tmp20 ;
2047  void const   *__cil_tmp21 ;
2048
2049  {
2050  {
2051#line 226
2052  ret = platform_driver_probe(& ramoops_driver, & ramoops_probe);
2053  }
2054#line 227
2055  if (ret == -19) {
2056    {
2057#line 232
2058    printk("<6>ramoops: platform device not found, using module parameters\n");
2059#line 233
2060    tmp = kzalloc(32UL, 208U);
2061#line 233
2062    dummy_data = (struct ramoops_platform_data *)tmp;
2063    }
2064    {
2065#line 235
2066    __cil_tmp5 = (struct ramoops_platform_data *)0;
2067#line 235
2068    __cil_tmp6 = (unsigned long )__cil_tmp5;
2069#line 235
2070    __cil_tmp7 = (unsigned long )dummy_data;
2071#line 235
2072    if (__cil_tmp7 == __cil_tmp6) {
2073#line 236
2074      return (-12);
2075    } else {
2076
2077    }
2078    }
2079    {
2080#line 237
2081    __cil_tmp8 = & mem_size;
2082#line 237
2083    *((unsigned long *)dummy_data) = *__cil_tmp8;
2084#line 238
2085    __cil_tmp9 = (unsigned long )dummy_data;
2086#line 238
2087    __cil_tmp10 = __cil_tmp9 + 8;
2088#line 238
2089    __cil_tmp11 = & mem_address;
2090#line 238
2091    *((unsigned long *)__cil_tmp10) = *__cil_tmp11;
2092#line 239
2093    __cil_tmp12 = (unsigned long )dummy_data;
2094#line 239
2095    __cil_tmp13 = __cil_tmp12 + 16;
2096#line 239
2097    __cil_tmp14 = & record_size;
2098#line 239
2099    *((unsigned long *)__cil_tmp13) = *__cil_tmp14;
2100#line 240
2101    __cil_tmp15 = (unsigned long )dummy_data;
2102#line 240
2103    __cil_tmp16 = __cil_tmp15 + 24;
2104#line 240
2105    __cil_tmp17 = & dump_oops;
2106#line 240
2107    *((int *)__cil_tmp16) = *__cil_tmp17;
2108#line 241
2109    __cil_tmp18 = (struct resource *)0;
2110#line 241
2111    __cil_tmp19 = (void const   *)dummy_data;
2112#line 241
2113    dummy = platform_create_bundle(& ramoops_driver, & ramoops_probe, __cil_tmp18,
2114                                   0U, __cil_tmp19, 32UL);
2115#line 245
2116    __cil_tmp20 = (void const   *)dummy;
2117#line 245
2118    tmp___1 = IS_ERR(__cil_tmp20);
2119    }
2120#line 245
2121    if (tmp___1 != 0L) {
2122      {
2123#line 246
2124      __cil_tmp21 = (void const   *)dummy;
2125#line 246
2126      tmp___0 = PTR_ERR(__cil_tmp21);
2127#line 246
2128      ret = (int )tmp___0;
2129      }
2130    } else {
2131#line 248
2132      ret = 0;
2133    }
2134  } else {
2135
2136  }
2137#line 251
2138  return (ret);
2139}
2140}
2141#line 254 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2142static void ramoops_exit(void) 
2143{ void const   *__cil_tmp1 ;
2144
2145  {
2146  {
2147#line 256
2148  platform_driver_unregister(& ramoops_driver);
2149#line 257
2150  __cil_tmp1 = (void const   *)dummy_data;
2151#line 257
2152  kfree(__cil_tmp1);
2153  }
2154#line 258
2155  return;
2156}
2157}
2158#line 283
2159extern void ldv_check_final_state(void) ;
2160#line 289
2161extern void ldv_initialize(void) ;
2162#line 292
2163extern int __VERIFIER_nondet_int(void) ;
2164#line 295 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2165int LDV_IN_INTERRUPT  ;
2166#line 298 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2167void main(void) 
2168{ int tmp ;
2169  int tmp___0 ;
2170  int tmp___1 ;
2171
2172  {
2173  {
2174#line 310
2175  LDV_IN_INTERRUPT = 1;
2176#line 319
2177  ldv_initialize();
2178#line 329
2179  tmp = ramoops_init();
2180  }
2181#line 329
2182  if (tmp != 0) {
2183#line 330
2184    goto ldv_final;
2185  } else {
2186
2187  }
2188#line 332
2189  goto ldv_15479;
2190  ldv_15478: 
2191  {
2192#line 335
2193  tmp___0 = __VERIFIER_nondet_int();
2194  }
2195  {
2196#line 337
2197  goto switch_default;
2198#line 335
2199  if (0) {
2200    switch_default: /* CIL Label */ ;
2201#line 337
2202    goto ldv_15477;
2203  } else {
2204    switch_break: /* CIL Label */ ;
2205  }
2206  }
2207  ldv_15477: ;
2208  ldv_15479: 
2209  {
2210#line 332
2211  tmp___1 = __VERIFIER_nondet_int();
2212  }
2213#line 332
2214  if (tmp___1 != 0) {
2215#line 333
2216    goto ldv_15478;
2217  } else {
2218#line 335
2219    goto ldv_15480;
2220  }
2221  ldv_15480: ;
2222  {
2223#line 353
2224  ramoops_exit();
2225  }
2226  ldv_final: 
2227  {
2228#line 356
2229  ldv_check_final_state();
2230  }
2231#line 359
2232  return;
2233}
2234}
2235#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2236void ldv_blast_assert(void) 
2237{ 
2238
2239  {
2240  ERROR: ;
2241#line 6
2242  goto ERROR;
2243}
2244}
2245#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2246extern int __VERIFIER_nondet_int(void) ;
2247#line 380 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2248int ldv_spin  =    0;
2249#line 384 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2250void ldv_check_alloc_flags(gfp_t flags ) 
2251{ 
2252
2253  {
2254#line 387
2255  if (ldv_spin != 0) {
2256#line 387
2257    if (flags != 32U) {
2258      {
2259#line 387
2260      ldv_blast_assert();
2261      }
2262    } else {
2263
2264    }
2265  } else {
2266
2267  }
2268#line 390
2269  return;
2270}
2271}
2272#line 390
2273extern struct page *ldv_some_page(void) ;
2274#line 393 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2275struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
2276{ struct page *tmp ;
2277
2278  {
2279#line 396
2280  if (ldv_spin != 0) {
2281#line 396
2282    if (flags != 32U) {
2283      {
2284#line 396
2285      ldv_blast_assert();
2286      }
2287    } else {
2288
2289    }
2290  } else {
2291
2292  }
2293  {
2294#line 398
2295  tmp = ldv_some_page();
2296  }
2297#line 398
2298  return (tmp);
2299}
2300}
2301#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2302void ldv_check_alloc_nonatomic(void) 
2303{ 
2304
2305  {
2306#line 405
2307  if (ldv_spin != 0) {
2308    {
2309#line 405
2310    ldv_blast_assert();
2311    }
2312  } else {
2313
2314  }
2315#line 408
2316  return;
2317}
2318}
2319#line 409 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2320void ldv_spin_lock(void) 
2321{ 
2322
2323  {
2324#line 412
2325  ldv_spin = 1;
2326#line 413
2327  return;
2328}
2329}
2330#line 416 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2331void ldv_spin_unlock(void) 
2332{ 
2333
2334  {
2335#line 419
2336  ldv_spin = 0;
2337#line 420
2338  return;
2339}
2340}
2341#line 423 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2342int ldv_spin_trylock(void) 
2343{ int is_lock ;
2344
2345  {
2346  {
2347#line 428
2348  is_lock = __VERIFIER_nondet_int();
2349  }
2350#line 430
2351  if (is_lock != 0) {
2352#line 433
2353    return (0);
2354  } else {
2355#line 438
2356    ldv_spin = 1;
2357#line 440
2358    return (1);
2359  }
2360}
2361}
2362#line 607 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2363void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
2364{ 
2365
2366  {
2367  {
2368#line 613
2369  ldv_check_alloc_flags(ldv_func_arg2);
2370#line 615
2371  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2372  }
2373#line 616
2374  return ((void *)0);
2375}
2376}
2377#line 618 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11317/dscv_tempdir/dscv/ri/43_1a/drivers/char/ramoops.c.p"
2378__inline static void *kzalloc(size_t size , gfp_t flags ) 
2379{ void *tmp ;
2380
2381  {
2382  {
2383#line 624
2384  ldv_check_alloc_flags(flags);
2385#line 625
2386  tmp = __VERIFIER_nondet_pointer();
2387  }
2388#line 625
2389  return (tmp);
2390}
2391}