Showing error 504

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/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--mtd--devices--mtdram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1914
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 20 "include/asm-generic/int-ll64.h"
   5typedef unsigned char __u8;
   6#line 23 "include/asm-generic/int-ll64.h"
   7typedef unsigned short __u16;
   8#line 26 "include/asm-generic/int-ll64.h"
   9typedef unsigned int __u32;
  10#line 30 "include/asm-generic/int-ll64.h"
  11typedef unsigned long long __u64;
  12#line 45 "include/asm-generic/int-ll64.h"
  13typedef short s16;
  14#line 46 "include/asm-generic/int-ll64.h"
  15typedef unsigned short u16;
  16#line 49 "include/asm-generic/int-ll64.h"
  17typedef unsigned int u32;
  18#line 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 75 "include/asm-generic/posix_types.h"
  27typedef __kernel_ulong_t __kernel_size_t;
  28#line 76 "include/asm-generic/posix_types.h"
  29typedef __kernel_long_t __kernel_ssize_t;
  30#line 91 "include/asm-generic/posix_types.h"
  31typedef long long __kernel_loff_t;
  32#line 21 "include/linux/types.h"
  33typedef __u32 __kernel_dev_t;
  34#line 24 "include/linux/types.h"
  35typedef __kernel_dev_t dev_t;
  36#line 27 "include/linux/types.h"
  37typedef unsigned short umode_t;
  38#line 38 "include/linux/types.h"
  39typedef _Bool bool;
  40#line 54 "include/linux/types.h"
  41typedef __kernel_loff_t loff_t;
  42#line 63 "include/linux/types.h"
  43typedef __kernel_size_t size_t;
  44#line 68 "include/linux/types.h"
  45typedef __kernel_ssize_t ssize_t;
  46#line 92 "include/linux/types.h"
  47typedef unsigned char u_char;
  48#line 95 "include/linux/types.h"
  49typedef unsigned long u_long;
  50#line 115 "include/linux/types.h"
  51typedef __u8 uint8_t;
  52#line 117 "include/linux/types.h"
  53typedef __u32 uint32_t;
  54#line 120 "include/linux/types.h"
  55typedef __u64 uint64_t;
  56#line 202 "include/linux/types.h"
  57typedef unsigned int gfp_t;
  58#line 206 "include/linux/types.h"
  59typedef u64 phys_addr_t;
  60#line 211 "include/linux/types.h"
  61typedef phys_addr_t resource_size_t;
  62#line 219 "include/linux/types.h"
  63struct __anonstruct_atomic_t_7 {
  64   int counter ;
  65};
  66#line 219 "include/linux/types.h"
  67typedef struct __anonstruct_atomic_t_7 atomic_t;
  68#line 224 "include/linux/types.h"
  69struct __anonstruct_atomic64_t_8 {
  70   long counter ;
  71};
  72#line 224 "include/linux/types.h"
  73typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  74#line 229 "include/linux/types.h"
  75struct list_head {
  76   struct list_head *next ;
  77   struct list_head *prev ;
  78};
  79#line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  80struct module;
  81#line 56
  82struct module;
  83#line 146 "include/linux/init.h"
  84typedef void (*ctor_fn_t)(void);
  85#line 47 "include/linux/dynamic_debug.h"
  86struct device;
  87#line 47
  88struct device;
  89#line 135 "include/linux/kernel.h"
  90struct completion;
  91#line 135
  92struct completion;
  93#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
  94struct page;
  95#line 18
  96struct page;
  97#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
  98struct task_struct;
  99#line 20
 100struct task_struct;
 101#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 102struct task_struct;
 103#line 295 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 104struct file;
 105#line 295
 106struct file;
 107#line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 108struct page;
 109#line 52
 110struct task_struct;
 111#line 329
 112struct arch_spinlock;
 113#line 329
 114struct arch_spinlock;
 115#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
 116struct task_struct;
 117#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
 118struct task_struct;
 119#line 10 "include/asm-generic/bug.h"
 120struct bug_entry {
 121   int bug_addr_disp ;
 122   int file_disp ;
 123   unsigned short line ;
 124   unsigned short flags ;
 125};
 126#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 127struct static_key;
 128#line 234
 129struct static_key;
 130#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 131struct kmem_cache;
 132#line 23 "include/asm-generic/atomic-long.h"
 133typedef atomic64_t atomic_long_t;
 134#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 135typedef u16 __ticket_t;
 136#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 137typedef u32 __ticketpair_t;
 138#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 139struct __raw_tickets {
 140   __ticket_t head ;
 141   __ticket_t tail ;
 142};
 143#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 144union __anonunion____missing_field_name_36 {
 145   __ticketpair_t head_tail ;
 146   struct __raw_tickets tickets ;
 147};
 148#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 149struct arch_spinlock {
 150   union __anonunion____missing_field_name_36 __annonCompField17 ;
 151};
 152#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 153typedef struct arch_spinlock arch_spinlock_t;
 154#line 12 "include/linux/lockdep.h"
 155struct task_struct;
 156#line 20 "include/linux/spinlock_types.h"
 157struct raw_spinlock {
 158   arch_spinlock_t raw_lock ;
 159   unsigned int magic ;
 160   unsigned int owner_cpu ;
 161   void *owner ;
 162};
 163#line 64 "include/linux/spinlock_types.h"
 164union __anonunion____missing_field_name_39 {
 165   struct raw_spinlock rlock ;
 166};
 167#line 64 "include/linux/spinlock_types.h"
 168struct spinlock {
 169   union __anonunion____missing_field_name_39 __annonCompField19 ;
 170};
 171#line 64 "include/linux/spinlock_types.h"
 172typedef struct spinlock spinlock_t;
 173#line 49 "include/linux/wait.h"
 174struct __wait_queue_head {
 175   spinlock_t lock ;
 176   struct list_head task_list ;
 177};
 178#line 53 "include/linux/wait.h"
 179typedef struct __wait_queue_head wait_queue_head_t;
 180#line 55
 181struct task_struct;
 182#line 60 "include/linux/pageblock-flags.h"
 183struct page;
 184#line 48 "include/linux/mutex.h"
 185struct mutex {
 186   atomic_t count ;
 187   spinlock_t wait_lock ;
 188   struct list_head wait_list ;
 189   struct task_struct *owner ;
 190   char const   *name ;
 191   void *magic ;
 192};
 193#line 25 "include/linux/completion.h"
 194struct completion {
 195   unsigned int done ;
 196   wait_queue_head_t wait ;
 197};
 198#line 188 "include/linux/rcupdate.h"
 199struct notifier_block;
 200#line 188
 201struct notifier_block;
 202#line 50 "include/linux/notifier.h"
 203struct notifier_block {
 204   int (*notifier_call)(struct notifier_block * , unsigned long  , void * ) ;
 205   struct notifier_block *next ;
 206   int priority ;
 207};
 208#line 9 "include/linux/memory_hotplug.h"
 209struct page;
 210#line 202 "include/linux/ioport.h"
 211struct device;
 212#line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 213struct device;
 214#line 46 "include/linux/ktime.h"
 215union ktime {
 216   s64 tv64 ;
 217};
 218#line 59 "include/linux/ktime.h"
 219typedef union ktime ktime_t;
 220#line 10 "include/linux/timer.h"
 221struct tvec_base;
 222#line 10
 223struct tvec_base;
 224#line 12 "include/linux/timer.h"
 225struct timer_list {
 226   struct list_head entry ;
 227   unsigned long expires ;
 228   struct tvec_base *base ;
 229   void (*function)(unsigned long  ) ;
 230   unsigned long data ;
 231   int slack ;
 232   int start_pid ;
 233   void *start_site ;
 234   char start_comm[16] ;
 235};
 236#line 17 "include/linux/workqueue.h"
 237struct work_struct;
 238#line 17
 239struct work_struct;
 240#line 79 "include/linux/workqueue.h"
 241struct work_struct {
 242   atomic_long_t data ;
 243   struct list_head entry ;
 244   void (*func)(struct work_struct *work ) ;
 245};
 246#line 42 "include/linux/pm.h"
 247struct device;
 248#line 50 "include/linux/pm.h"
 249struct pm_message {
 250   int event ;
 251};
 252#line 50 "include/linux/pm.h"
 253typedef struct pm_message pm_message_t;
 254#line 264 "include/linux/pm.h"
 255struct dev_pm_ops {
 256   int (*prepare)(struct device *dev ) ;
 257   void (*complete)(struct device *dev ) ;
 258   int (*suspend)(struct device *dev ) ;
 259   int (*resume)(struct device *dev ) ;
 260   int (*freeze)(struct device *dev ) ;
 261   int (*thaw)(struct device *dev ) ;
 262   int (*poweroff)(struct device *dev ) ;
 263   int (*restore)(struct device *dev ) ;
 264   int (*suspend_late)(struct device *dev ) ;
 265   int (*resume_early)(struct device *dev ) ;
 266   int (*freeze_late)(struct device *dev ) ;
 267   int (*thaw_early)(struct device *dev ) ;
 268   int (*poweroff_late)(struct device *dev ) ;
 269   int (*restore_early)(struct device *dev ) ;
 270   int (*suspend_noirq)(struct device *dev ) ;
 271   int (*resume_noirq)(struct device *dev ) ;
 272   int (*freeze_noirq)(struct device *dev ) ;
 273   int (*thaw_noirq)(struct device *dev ) ;
 274   int (*poweroff_noirq)(struct device *dev ) ;
 275   int (*restore_noirq)(struct device *dev ) ;
 276   int (*runtime_suspend)(struct device *dev ) ;
 277   int (*runtime_resume)(struct device *dev ) ;
 278   int (*runtime_idle)(struct device *dev ) ;
 279};
 280#line 458
 281enum rpm_status {
 282    RPM_ACTIVE = 0,
 283    RPM_RESUMING = 1,
 284    RPM_SUSPENDED = 2,
 285    RPM_SUSPENDING = 3
 286} ;
 287#line 480
 288enum rpm_request {
 289    RPM_REQ_NONE = 0,
 290    RPM_REQ_IDLE = 1,
 291    RPM_REQ_SUSPEND = 2,
 292    RPM_REQ_AUTOSUSPEND = 3,
 293    RPM_REQ_RESUME = 4
 294} ;
 295#line 488
 296struct wakeup_source;
 297#line 488
 298struct wakeup_source;
 299#line 495 "include/linux/pm.h"
 300struct pm_subsys_data {
 301   spinlock_t lock ;
 302   unsigned int refcount ;
 303};
 304#line 506
 305struct dev_pm_qos_request;
 306#line 506
 307struct pm_qos_constraints;
 308#line 506 "include/linux/pm.h"
 309struct dev_pm_info {
 310   pm_message_t power_state ;
 311   unsigned int can_wakeup : 1 ;
 312   unsigned int async_suspend : 1 ;
 313   bool is_prepared : 1 ;
 314   bool is_suspended : 1 ;
 315   bool ignore_children : 1 ;
 316   spinlock_t lock ;
 317   struct list_head entry ;
 318   struct completion completion ;
 319   struct wakeup_source *wakeup ;
 320   bool wakeup_path : 1 ;
 321   struct timer_list suspend_timer ;
 322   unsigned long timer_expires ;
 323   struct work_struct work ;
 324   wait_queue_head_t wait_queue ;
 325   atomic_t usage_count ;
 326   atomic_t child_count ;
 327   unsigned int disable_depth : 3 ;
 328   unsigned int idle_notification : 1 ;
 329   unsigned int request_pending : 1 ;
 330   unsigned int deferred_resume : 1 ;
 331   unsigned int run_wake : 1 ;
 332   unsigned int runtime_auto : 1 ;
 333   unsigned int no_callbacks : 1 ;
 334   unsigned int irq_safe : 1 ;
 335   unsigned int use_autosuspend : 1 ;
 336   unsigned int timer_autosuspends : 1 ;
 337   enum rpm_request request ;
 338   enum rpm_status runtime_status ;
 339   int runtime_error ;
 340   int autosuspend_delay ;
 341   unsigned long last_busy ;
 342   unsigned long active_jiffies ;
 343   unsigned long suspended_jiffies ;
 344   unsigned long accounting_timestamp ;
 345   ktime_t suspend_time ;
 346   s64 max_time_suspended_ns ;
 347   struct dev_pm_qos_request *pq_req ;
 348   struct pm_subsys_data *subsys_data ;
 349   struct pm_qos_constraints *constraints ;
 350};
 351#line 564 "include/linux/pm.h"
 352struct dev_pm_domain {
 353   struct dev_pm_ops ops ;
 354};
 355#line 8 "include/linux/vmalloc.h"
 356struct vm_area_struct;
 357#line 8
 358struct vm_area_struct;
 359#line 994 "include/linux/mmzone.h"
 360struct page;
 361#line 10 "include/linux/gfp.h"
 362struct vm_area_struct;
 363#line 29 "include/linux/sysctl.h"
 364struct completion;
 365#line 49 "include/linux/kmod.h"
 366struct file;
 367#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 368struct task_struct;
 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 194 "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 194 "include/linux/elf.h"
 387typedef struct elf64_sym Elf64_Sym;
 388#line 438
 389struct file;
 390#line 20 "include/linux/kobject_ns.h"
 391struct sock;
 392#line 20
 393struct sock;
 394#line 21
 395struct kobject;
 396#line 21
 397struct kobject;
 398#line 27
 399enum kobj_ns_type {
 400    KOBJ_NS_TYPE_NONE = 0,
 401    KOBJ_NS_TYPE_NET = 1,
 402    KOBJ_NS_TYPES = 2
 403} ;
 404#line 40 "include/linux/kobject_ns.h"
 405struct kobj_ns_type_operations {
 406   enum kobj_ns_type type ;
 407   void *(*grab_current_ns)(void) ;
 408   void const   *(*netlink_ns)(struct sock *sk ) ;
 409   void const   *(*initial_ns)(void) ;
 410   void (*drop_ns)(void * ) ;
 411};
 412#line 22 "include/linux/sysfs.h"
 413struct kobject;
 414#line 23
 415struct module;
 416#line 24
 417enum kobj_ns_type;
 418#line 26 "include/linux/sysfs.h"
 419struct attribute {
 420   char const   *name ;
 421   umode_t mode ;
 422};
 423#line 56 "include/linux/sysfs.h"
 424struct attribute_group {
 425   char const   *name ;
 426   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 427   struct attribute **attrs ;
 428};
 429#line 85
 430struct file;
 431#line 86
 432struct vm_area_struct;
 433#line 88 "include/linux/sysfs.h"
 434struct bin_attribute {
 435   struct attribute attr ;
 436   size_t size ;
 437   void *private ;
 438   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 439                   loff_t  , size_t  ) ;
 440   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 441                    loff_t  , size_t  ) ;
 442   int (*mmap)(struct file * , struct kobject * , struct bin_attribute *attr , struct vm_area_struct *vma ) ;
 443};
 444#line 112 "include/linux/sysfs.h"
 445struct sysfs_ops {
 446   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 447   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 448   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 449};
 450#line 118
 451struct sysfs_dirent;
 452#line 118
 453struct sysfs_dirent;
 454#line 22 "include/linux/kref.h"
 455struct kref {
 456   atomic_t refcount ;
 457};
 458#line 60 "include/linux/kobject.h"
 459struct kset;
 460#line 60
 461struct kobj_type;
 462#line 60 "include/linux/kobject.h"
 463struct kobject {
 464   char const   *name ;
 465   struct list_head entry ;
 466   struct kobject *parent ;
 467   struct kset *kset ;
 468   struct kobj_type *ktype ;
 469   struct sysfs_dirent *sd ;
 470   struct kref kref ;
 471   unsigned int state_initialized : 1 ;
 472   unsigned int state_in_sysfs : 1 ;
 473   unsigned int state_add_uevent_sent : 1 ;
 474   unsigned int state_remove_uevent_sent : 1 ;
 475   unsigned int uevent_suppress : 1 ;
 476};
 477#line 108 "include/linux/kobject.h"
 478struct kobj_type {
 479   void (*release)(struct kobject *kobj ) ;
 480   struct sysfs_ops  const  *sysfs_ops ;
 481   struct attribute **default_attrs ;
 482   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
 483   void const   *(*namespace)(struct kobject *kobj ) ;
 484};
 485#line 116 "include/linux/kobject.h"
 486struct kobj_uevent_env {
 487   char *envp[32] ;
 488   int envp_idx ;
 489   char buf[2048] ;
 490   int buflen ;
 491};
 492#line 123 "include/linux/kobject.h"
 493struct kset_uevent_ops {
 494   int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
 495   char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
 496   int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 497};
 498#line 140
 499struct sock;
 500#line 159 "include/linux/kobject.h"
 501struct kset {
 502   struct list_head list ;
 503   spinlock_t list_lock ;
 504   struct kobject kobj ;
 505   struct kset_uevent_ops  const  *uevent_ops ;
 506};
 507#line 39 "include/linux/moduleparam.h"
 508struct kernel_param;
 509#line 39
 510struct kernel_param;
 511#line 41 "include/linux/moduleparam.h"
 512struct kernel_param_ops {
 513   int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
 514   int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
 515   void (*free)(void *arg ) ;
 516};
 517#line 50
 518struct kparam_string;
 519#line 50
 520struct kparam_array;
 521#line 50 "include/linux/moduleparam.h"
 522union __anonunion____missing_field_name_199 {
 523   void *arg ;
 524   struct kparam_string  const  *str ;
 525   struct kparam_array  const  *arr ;
 526};
 527#line 50 "include/linux/moduleparam.h"
 528struct kernel_param {
 529   char const   *name ;
 530   struct kernel_param_ops  const  *ops ;
 531   u16 perm ;
 532   s16 level ;
 533   union __anonunion____missing_field_name_199 __annonCompField32 ;
 534};
 535#line 63 "include/linux/moduleparam.h"
 536struct kparam_string {
 537   unsigned int maxlen ;
 538   char *string ;
 539};
 540#line 69 "include/linux/moduleparam.h"
 541struct kparam_array {
 542   unsigned int max ;
 543   unsigned int elemsize ;
 544   unsigned int *num ;
 545   struct kernel_param_ops  const  *ops ;
 546   void *elem ;
 547};
 548#line 445
 549struct module;
 550#line 80 "include/linux/jump_label.h"
 551struct module;
 552#line 143 "include/linux/jump_label.h"
 553struct static_key {
 554   atomic_t enabled ;
 555};
 556#line 22 "include/linux/tracepoint.h"
 557struct module;
 558#line 23
 559struct tracepoint;
 560#line 23
 561struct tracepoint;
 562#line 25 "include/linux/tracepoint.h"
 563struct tracepoint_func {
 564   void *func ;
 565   void *data ;
 566};
 567#line 30 "include/linux/tracepoint.h"
 568struct tracepoint {
 569   char const   *name ;
 570   struct static_key key ;
 571   void (*regfunc)(void) ;
 572   void (*unregfunc)(void) ;
 573   struct tracepoint_func *funcs ;
 574};
 575#line 19 "include/linux/export.h"
 576struct kernel_symbol {
 577   unsigned long value ;
 578   char const   *name ;
 579};
 580#line 8 "include/asm-generic/module.h"
 581struct mod_arch_specific {
 582
 583};
 584#line 35 "include/linux/module.h"
 585struct module;
 586#line 37
 587struct module_param_attrs;
 588#line 37 "include/linux/module.h"
 589struct module_kobject {
 590   struct kobject kobj ;
 591   struct module *mod ;
 592   struct kobject *drivers_dir ;
 593   struct module_param_attrs *mp ;
 594};
 595#line 44 "include/linux/module.h"
 596struct module_attribute {
 597   struct attribute attr ;
 598   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 599   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 600                    size_t count ) ;
 601   void (*setup)(struct module * , char const   * ) ;
 602   int (*test)(struct module * ) ;
 603   void (*free)(struct module * ) ;
 604};
 605#line 71
 606struct exception_table_entry;
 607#line 71
 608struct exception_table_entry;
 609#line 182
 610struct notifier_block;
 611#line 199
 612enum module_state {
 613    MODULE_STATE_LIVE = 0,
 614    MODULE_STATE_COMING = 1,
 615    MODULE_STATE_GOING = 2
 616} ;
 617#line 215 "include/linux/module.h"
 618struct module_ref {
 619   unsigned long incs ;
 620   unsigned long decs ;
 621} __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 622#line 220
 623struct module_sect_attrs;
 624#line 220
 625struct module_notes_attrs;
 626#line 220
 627struct ftrace_event_call;
 628#line 220 "include/linux/module.h"
 629struct module {
 630   enum module_state state ;
 631   struct list_head list ;
 632   char name[64UL - sizeof(unsigned long )] ;
 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 ;
 694   unsigned int num_ctors ;
 695};
 696#line 46 "include/linux/slub_def.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[26] ;
 704};
 705#line 57 "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 73 "include/linux/slub_def.h"
 715struct kmem_cache_order_objects {
 716   unsigned long x ;
 717};
 718#line 80 "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[1 << 10] ;
 741};
 742#line 31 "include/linux/uio.h"
 743struct kvec {
 744   void *iov_base ;
 745   size_t iov_len ;
 746};
 747#line 19 "include/linux/klist.h"
 748struct klist_node;
 749#line 19
 750struct klist_node;
 751#line 39 "include/linux/klist.h"
 752struct klist_node {
 753   void *n_klist ;
 754   struct list_head n_node ;
 755   struct kref n_ref ;
 756};
 757#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 758struct dma_map_ops;
 759#line 4 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 760struct dev_archdata {
 761   void *acpi_handle ;
 762   struct dma_map_ops *dma_ops ;
 763   void *iommu ;
 764};
 765#line 28 "include/linux/device.h"
 766struct device;
 767#line 29
 768struct device_private;
 769#line 29
 770struct device_private;
 771#line 30
 772struct device_driver;
 773#line 30
 774struct device_driver;
 775#line 31
 776struct driver_private;
 777#line 31
 778struct driver_private;
 779#line 32
 780struct module;
 781#line 33
 782struct class;
 783#line 33
 784struct class;
 785#line 34
 786struct subsys_private;
 787#line 34
 788struct subsys_private;
 789#line 35
 790struct bus_type;
 791#line 35
 792struct bus_type;
 793#line 36
 794struct device_node;
 795#line 36
 796struct device_node;
 797#line 37
 798struct iommu_ops;
 799#line 37
 800struct iommu_ops;
 801#line 39 "include/linux/device.h"
 802struct bus_attribute {
 803   struct attribute attr ;
 804   ssize_t (*show)(struct bus_type *bus , char *buf ) ;
 805   ssize_t (*store)(struct bus_type *bus , char const   *buf , size_t count ) ;
 806};
 807#line 89
 808struct device_attribute;
 809#line 89
 810struct driver_attribute;
 811#line 89 "include/linux/device.h"
 812struct bus_type {
 813   char const   *name ;
 814   char const   *dev_name ;
 815   struct device *dev_root ;
 816   struct bus_attribute *bus_attrs ;
 817   struct device_attribute *dev_attrs ;
 818   struct driver_attribute *drv_attrs ;
 819   int (*match)(struct device *dev , struct device_driver *drv ) ;
 820   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 821   int (*probe)(struct device *dev ) ;
 822   int (*remove)(struct device *dev ) ;
 823   void (*shutdown)(struct device *dev ) ;
 824   int (*suspend)(struct device *dev , pm_message_t state ) ;
 825   int (*resume)(struct device *dev ) ;
 826   struct dev_pm_ops  const  *pm ;
 827   struct iommu_ops *iommu_ops ;
 828   struct subsys_private *p ;
 829};
 830#line 127
 831struct device_type;
 832#line 159
 833struct notifier_block;
 834#line 214
 835struct of_device_id;
 836#line 214 "include/linux/device.h"
 837struct device_driver {
 838   char const   *name ;
 839   struct bus_type *bus ;
 840   struct module *owner ;
 841   char const   *mod_name ;
 842   bool suppress_bind_attrs ;
 843   struct of_device_id  const  *of_match_table ;
 844   int (*probe)(struct device *dev ) ;
 845   int (*remove)(struct device *dev ) ;
 846   void (*shutdown)(struct device *dev ) ;
 847   int (*suspend)(struct device *dev , pm_message_t state ) ;
 848   int (*resume)(struct device *dev ) ;
 849   struct attribute_group  const  **groups ;
 850   struct dev_pm_ops  const  *pm ;
 851   struct driver_private *p ;
 852};
 853#line 249 "include/linux/device.h"
 854struct driver_attribute {
 855   struct attribute attr ;
 856   ssize_t (*show)(struct device_driver *driver , char *buf ) ;
 857   ssize_t (*store)(struct device_driver *driver , char const   *buf , size_t count ) ;
 858};
 859#line 330
 860struct class_attribute;
 861#line 330 "include/linux/device.h"
 862struct class {
 863   char const   *name ;
 864   struct module *owner ;
 865   struct class_attribute *class_attrs ;
 866   struct device_attribute *dev_attrs ;
 867   struct bin_attribute *dev_bin_attrs ;
 868   struct kobject *dev_kobj ;
 869   int (*dev_uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 870   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 871   void (*class_release)(struct class *class ) ;
 872   void (*dev_release)(struct device *dev ) ;
 873   int (*suspend)(struct device *dev , pm_message_t state ) ;
 874   int (*resume)(struct device *dev ) ;
 875   struct kobj_ns_type_operations  const  *ns_type ;
 876   void const   *(*namespace)(struct device *dev ) ;
 877   struct dev_pm_ops  const  *pm ;
 878   struct subsys_private *p ;
 879};
 880#line 397 "include/linux/device.h"
 881struct class_attribute {
 882   struct attribute attr ;
 883   ssize_t (*show)(struct class *class , struct class_attribute *attr , char *buf ) ;
 884   ssize_t (*store)(struct class *class , struct class_attribute *attr , char const   *buf ,
 885                    size_t count ) ;
 886   void const   *(*namespace)(struct class *class , struct class_attribute  const  *attr ) ;
 887};
 888#line 465 "include/linux/device.h"
 889struct device_type {
 890   char const   *name ;
 891   struct attribute_group  const  **groups ;
 892   int (*uevent)(struct device *dev , struct kobj_uevent_env *env ) ;
 893   char *(*devnode)(struct device *dev , umode_t *mode ) ;
 894   void (*release)(struct device *dev ) ;
 895   struct dev_pm_ops  const  *pm ;
 896};
 897#line 476 "include/linux/device.h"
 898struct device_attribute {
 899   struct attribute attr ;
 900   ssize_t (*show)(struct device *dev , struct device_attribute *attr , char *buf ) ;
 901   ssize_t (*store)(struct device *dev , struct device_attribute *attr , char const   *buf ,
 902                    size_t count ) ;
 903};
 904#line 559 "include/linux/device.h"
 905struct device_dma_parameters {
 906   unsigned int max_segment_size ;
 907   unsigned long segment_boundary_mask ;
 908};
 909#line 627
 910struct dma_coherent_mem;
 911#line 627 "include/linux/device.h"
 912struct device {
 913   struct device *parent ;
 914   struct device_private *p ;
 915   struct kobject kobj ;
 916   char const   *init_name ;
 917   struct device_type  const  *type ;
 918   struct mutex mutex ;
 919   struct bus_type *bus ;
 920   struct device_driver *driver ;
 921   void *platform_data ;
 922   struct dev_pm_info power ;
 923   struct dev_pm_domain *pm_domain ;
 924   int numa_node ;
 925   u64 *dma_mask ;
 926   u64 coherent_dma_mask ;
 927   struct device_dma_parameters *dma_parms ;
 928   struct list_head dma_pools ;
 929   struct dma_coherent_mem *dma_mem ;
 930   struct dev_archdata archdata ;
 931   struct device_node *of_node ;
 932   dev_t devt ;
 933   u32 id ;
 934   spinlock_t devres_lock ;
 935   struct list_head devres_head ;
 936   struct klist_node knode_class ;
 937   struct class *class ;
 938   struct attribute_group  const  **groups ;
 939   void (*release)(struct device *dev ) ;
 940};
 941#line 43 "include/linux/pm_wakeup.h"
 942struct wakeup_source {
 943   char const   *name ;
 944   struct list_head entry ;
 945   spinlock_t lock ;
 946   struct timer_list timer ;
 947   unsigned long timer_expires ;
 948   ktime_t total_time ;
 949   ktime_t max_time ;
 950   ktime_t last_time ;
 951   unsigned long event_count ;
 952   unsigned long active_count ;
 953   unsigned long relax_count ;
 954   unsigned long hit_count ;
 955   unsigned int active : 1 ;
 956};
 957#line 143 "include/mtd/mtd-abi.h"
 958struct otp_info {
 959   __u32 start ;
 960   __u32 length ;
 961   __u32 locked ;
 962};
 963#line 217 "include/mtd/mtd-abi.h"
 964struct nand_oobfree {
 965   __u32 offset ;
 966   __u32 length ;
 967};
 968#line 247 "include/mtd/mtd-abi.h"
 969struct mtd_ecc_stats {
 970   __u32 corrected ;
 971   __u32 failed ;
 972   __u32 badblocks ;
 973   __u32 bbtblocks ;
 974};
 975#line 48 "include/linux/mtd/mtd.h"
 976struct mtd_info;
 977#line 48 "include/linux/mtd/mtd.h"
 978struct erase_info {
 979   struct mtd_info *mtd ;
 980   uint64_t addr ;
 981   uint64_t len ;
 982   uint64_t fail_addr ;
 983   u_long time ;
 984   u_long retries ;
 985   unsigned int dev ;
 986   unsigned int cell ;
 987   void (*callback)(struct erase_info *self ) ;
 988   u_long priv ;
 989   u_char state ;
 990   struct erase_info *next ;
 991};
 992#line 63 "include/linux/mtd/mtd.h"
 993struct mtd_erase_region_info {
 994   uint64_t offset ;
 995   uint32_t erasesize ;
 996   uint32_t numblocks ;
 997   unsigned long *lockmap ;
 998};
 999#line 89 "include/linux/mtd/mtd.h"
1000struct mtd_oob_ops {
1001   unsigned int mode ;
1002   size_t len ;
1003   size_t retlen ;
1004   size_t ooblen ;
1005   size_t oobretlen ;
1006   uint32_t ooboffs ;
1007   uint8_t *datbuf ;
1008   uint8_t *oobbuf ;
1009};
1010#line 108 "include/linux/mtd/mtd.h"
1011struct nand_ecclayout {
1012   __u32 eccbytes ;
1013   __u32 eccpos[448] ;
1014   __u32 oobavail ;
1015   struct nand_oobfree oobfree[32] ;
1016};
1017#line 115
1018struct module;
1019#line 117
1020struct backing_dev_info;
1021#line 117 "include/linux/mtd/mtd.h"
1022struct mtd_info {
1023   u_char type ;
1024   uint32_t flags ;
1025   uint64_t size ;
1026   uint32_t erasesize ;
1027   uint32_t writesize ;
1028   uint32_t writebufsize ;
1029   uint32_t oobsize ;
1030   uint32_t oobavail ;
1031   unsigned int erasesize_shift ;
1032   unsigned int writesize_shift ;
1033   unsigned int erasesize_mask ;
1034   unsigned int writesize_mask ;
1035   char const   *name ;
1036   int index ;
1037   struct nand_ecclayout *ecclayout ;
1038   unsigned int ecc_strength ;
1039   int numeraseregions ;
1040   struct mtd_erase_region_info *eraseregions ;
1041   int (*_erase)(struct mtd_info *mtd , struct erase_info *instr ) ;
1042   int (*_point)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1043                 void **virt , resource_size_t *phys ) ;
1044   int (*_unpoint)(struct mtd_info *mtd , loff_t from , size_t len ) ;
1045   unsigned long (*_get_unmapped_area)(struct mtd_info *mtd , unsigned long len ,
1046                                       unsigned long offset , unsigned long flags ) ;
1047   int (*_read)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1048                u_char *buf ) ;
1049   int (*_write)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1050                 u_char const   *buf ) ;
1051   int (*_panic_write)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1052                       u_char const   *buf ) ;
1053   int (*_read_oob)(struct mtd_info *mtd , loff_t from , struct mtd_oob_ops *ops ) ;
1054   int (*_write_oob)(struct mtd_info *mtd , loff_t to , struct mtd_oob_ops *ops ) ;
1055   int (*_get_fact_prot_info)(struct mtd_info *mtd , struct otp_info *buf , size_t len ) ;
1056   int (*_read_fact_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1057                              u_char *buf ) ;
1058   int (*_get_user_prot_info)(struct mtd_info *mtd , struct otp_info *buf , size_t len ) ;
1059   int (*_read_user_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1060                              u_char *buf ) ;
1061   int (*_write_user_prot_reg)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1062                               u_char *buf ) ;
1063   int (*_lock_user_prot_reg)(struct mtd_info *mtd , loff_t from , size_t len ) ;
1064   int (*_writev)(struct mtd_info *mtd , struct kvec  const  *vecs , unsigned long count ,
1065                  loff_t to , size_t *retlen ) ;
1066   void (*_sync)(struct mtd_info *mtd ) ;
1067   int (*_lock)(struct mtd_info *mtd , loff_t ofs , uint64_t len ) ;
1068   int (*_unlock)(struct mtd_info *mtd , loff_t ofs , uint64_t len ) ;
1069   int (*_is_locked)(struct mtd_info *mtd , loff_t ofs , uint64_t len ) ;
1070   int (*_block_isbad)(struct mtd_info *mtd , loff_t ofs ) ;
1071   int (*_block_markbad)(struct mtd_info *mtd , loff_t ofs ) ;
1072   int (*_suspend)(struct mtd_info *mtd ) ;
1073   void (*_resume)(struct mtd_info *mtd ) ;
1074   int (*_get_device)(struct mtd_info *mtd ) ;
1075   void (*_put_device)(struct mtd_info *mtd ) ;
1076   struct backing_dev_info *backing_dev_info ;
1077   struct notifier_block reboot_notifier ;
1078   struct mtd_ecc_stats ecc_stats ;
1079   int subpage_sft ;
1080   void *priv ;
1081   struct module *owner ;
1082   struct device dev ;
1083   int usecount ;
1084};
1085#line 359
1086struct mtd_partition;
1087#line 359
1088struct mtd_partition;
1089#line 360
1090struct mtd_part_parser_data;
1091#line 360
1092struct mtd_part_parser_data;
1093#line 1 "<compiler builtins>"
1094
1095#line 1
1096long __builtin_expect(long val , long res ) ;
1097#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
1098extern void *memset(void *s , int c , size_t n ) ;
1099#line 152 "include/linux/mutex.h"
1100void mutex_lock(struct mutex *lock ) ;
1101#line 153
1102int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
1103#line 154
1104int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
1105#line 168
1106int mutex_trylock(struct mutex *lock ) ;
1107#line 169
1108void mutex_unlock(struct mutex *lock ) ;
1109#line 170
1110int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
1111#line 54 "include/linux/vmalloc.h"
1112extern void *vmalloc(unsigned long size ) ;
1113#line 66
1114extern void vfree(void const   *addr ) ;
1115#line 371 "include/linux/moduleparam.h"
1116extern struct kernel_param_ops param_ops_ulong ;
1117#line 26 "include/linux/export.h"
1118extern struct module __this_module ;
1119#line 67 "include/linux/module.h"
1120int init_module(void) ;
1121#line 68
1122void cleanup_module(void) ;
1123#line 161 "include/linux/slab.h"
1124extern void kfree(void const   * ) ;
1125#line 221 "include/linux/slub_def.h"
1126extern void *__kmalloc(size_t size , gfp_t flags ) ;
1127#line 268
1128__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1129                                                                    gfp_t flags )  __attribute__((__no_instrument_function__)) ;
1130#line 268 "include/linux/slub_def.h"
1131__inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
1132                                                                    gfp_t flags ) 
1133{ void *tmp___2 ;
1134
1135  {
1136  {
1137#line 283
1138  tmp___2 = __kmalloc(size, flags);
1139  }
1140#line 283
1141  return (tmp___2);
1142}
1143}
1144#line 362 "include/linux/mtd/mtd.h"
1145extern int mtd_device_parse_register(struct mtd_info *mtd , char const   **part_probe_types ,
1146                                     struct mtd_part_parser_data *parser_data , struct mtd_partition  const  *defparts ,
1147                                     int defnr_parts ) ;
1148#line 369
1149extern int mtd_device_unregister(struct mtd_info *master ) ;
1150#line 388
1151extern void mtd_erase_callback(struct erase_info *instr ) ;
1152#line 5 "include/linux/mtd/mtdram.h"
1153int mtdram_init_device(struct mtd_info *mtd , void *mapped_address , unsigned long size ,
1154                       char *name ) ;
1155#line 21 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1156static unsigned long total_size  =    4096UL;
1157#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1158static unsigned long erase_size  =    128UL;
1159#line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1160static char const   __param_str_total_size[11]  = 
1161#line 27
1162  {      (char const   )'t',      (char const   )'o',      (char const   )'t',      (char const   )'a', 
1163        (char const   )'l',      (char const   )'_',      (char const   )'s',      (char const   )'i', 
1164        (char const   )'z',      (char const   )'e',      (char const   )'\000'};
1165#line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1166static struct kernel_param  const  __param_total_size  __attribute__((__used__, __unused__,
1167__section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_total_size, (struct kernel_param_ops  const  *)(& param_ops_ulong),
1168    (u16 )0, (s16 )0, {(void *)(& total_size)}};
1169#line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1170static char const   __mod_total_sizetype27[26]  __attribute__((__used__, __unused__,
1171__section__(".modinfo"), __aligned__(1)))  = 
1172#line 27
1173  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
1174        (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
1175        (char const   )'=',      (char const   )'t',      (char const   )'o',      (char const   )'t', 
1176        (char const   )'a',      (char const   )'l',      (char const   )'_',      (char const   )'s', 
1177        (char const   )'i',      (char const   )'z',      (char const   )'e',      (char const   )':', 
1178        (char const   )'u',      (char const   )'l',      (char const   )'o',      (char const   )'n', 
1179        (char const   )'g',      (char const   )'\000'};
1180#line 28 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1181static char const   __mod_total_size28[41]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1182__aligned__(1)))  = 
1183#line 28
1184  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
1185        (char const   )'=',      (char const   )'t',      (char const   )'o',      (char const   )'t', 
1186        (char const   )'a',      (char const   )'l',      (char const   )'_',      (char const   )'s', 
1187        (char const   )'i',      (char const   )'z',      (char const   )'e',      (char const   )':', 
1188        (char const   )'T',      (char const   )'o',      (char const   )'t',      (char const   )'a', 
1189        (char const   )'l',      (char const   )' ',      (char const   )'d',      (char const   )'e', 
1190        (char const   )'v',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
1191        (char const   )' ',      (char const   )'s',      (char const   )'i',      (char const   )'z', 
1192        (char const   )'e',      (char const   )' ',      (char const   )'i',      (char const   )'n', 
1193        (char const   )' ',      (char const   )'K',      (char const   )'i',      (char const   )'B', 
1194        (char const   )'\000'};
1195#line 29 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1196static char const   __param_str_erase_size[11]  = 
1197#line 29
1198  {      (char const   )'e',      (char const   )'r',      (char const   )'a',      (char const   )'s', 
1199        (char const   )'e',      (char const   )'_',      (char const   )'s',      (char const   )'i', 
1200        (char const   )'z',      (char const   )'e',      (char const   )'\000'};
1201#line 29 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1202static struct kernel_param  const  __param_erase_size  __attribute__((__used__, __unused__,
1203__section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_erase_size, (struct kernel_param_ops  const  *)(& param_ops_ulong),
1204    (u16 )0, (s16 )0, {(void *)(& erase_size)}};
1205#line 29 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1206static char const   __mod_erase_sizetype29[26]  __attribute__((__used__, __unused__,
1207__section__(".modinfo"), __aligned__(1)))  = 
1208#line 29
1209  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
1210        (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
1211        (char const   )'=',      (char const   )'e',      (char const   )'r',      (char const   )'a', 
1212        (char const   )'s',      (char const   )'e',      (char const   )'_',      (char const   )'s', 
1213        (char const   )'i',      (char const   )'z',      (char const   )'e',      (char const   )':', 
1214        (char const   )'u',      (char const   )'l',      (char const   )'o',      (char const   )'n', 
1215        (char const   )'g',      (char const   )'\000'};
1216#line 30 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1217static char const   __mod_erase_size30[47]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1218__aligned__(1)))  = 
1219#line 30
1220  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
1221        (char const   )'=',      (char const   )'e',      (char const   )'r',      (char const   )'a', 
1222        (char const   )'s',      (char const   )'e',      (char const   )'_',      (char const   )'s', 
1223        (char const   )'i',      (char const   )'z',      (char const   )'e',      (char const   )':', 
1224        (char const   )'D',      (char const   )'e',      (char const   )'v',      (char const   )'i', 
1225        (char const   )'c',      (char const   )'e',      (char const   )' ',      (char const   )'e', 
1226        (char const   )'r',      (char const   )'a',      (char const   )'s',      (char const   )'e', 
1227        (char const   )' ',      (char const   )'b',      (char const   )'l',      (char const   )'o', 
1228        (char const   )'c',      (char const   )'k',      (char const   )' ',      (char const   )'s', 
1229        (char const   )'i',      (char const   )'z',      (char const   )'e',      (char const   )' ', 
1230        (char const   )'i',      (char const   )'n',      (char const   )' ',      (char const   )'K', 
1231        (char const   )'i',      (char const   )'B',      (char const   )'\000'};
1232#line 34 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1233static struct mtd_info *mtd_info  ;
1234#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1235static int ram_erase(struct mtd_info *mtd , struct erase_info *instr ) 
1236{ unsigned long __cil_tmp3 ;
1237  unsigned long __cil_tmp4 ;
1238  uint64_t __cil_tmp5 ;
1239  unsigned long __cil_tmp6 ;
1240  unsigned long __cil_tmp7 ;
1241  void *__cil_tmp8 ;
1242  char *__cil_tmp9 ;
1243  char *__cil_tmp10 ;
1244  void *__cil_tmp11 ;
1245  unsigned long __cil_tmp12 ;
1246  unsigned long __cil_tmp13 ;
1247  uint64_t __cil_tmp14 ;
1248  size_t __cil_tmp15 ;
1249  unsigned long __cil_tmp16 ;
1250  unsigned long __cil_tmp17 ;
1251
1252  {
1253  {
1254#line 38
1255  __cil_tmp3 = (unsigned long )instr;
1256#line 38
1257  __cil_tmp4 = __cil_tmp3 + 8;
1258#line 38
1259  __cil_tmp5 = *((uint64_t *)__cil_tmp4);
1260#line 38
1261  __cil_tmp6 = (unsigned long )mtd;
1262#line 38
1263  __cil_tmp7 = __cil_tmp6 + 360;
1264#line 38
1265  __cil_tmp8 = *((void **)__cil_tmp7);
1266#line 38
1267  __cil_tmp9 = (char *)__cil_tmp8;
1268#line 38
1269  __cil_tmp10 = __cil_tmp9 + __cil_tmp5;
1270#line 38
1271  __cil_tmp11 = (void *)__cil_tmp10;
1272#line 38
1273  __cil_tmp12 = (unsigned long )instr;
1274#line 38
1275  __cil_tmp13 = __cil_tmp12 + 16;
1276#line 38
1277  __cil_tmp14 = *((uint64_t *)__cil_tmp13);
1278#line 38
1279  __cil_tmp15 = (size_t )__cil_tmp14;
1280#line 38
1281  memset(__cil_tmp11, 255, __cil_tmp15);
1282#line 39
1283  __cil_tmp16 = (unsigned long )instr;
1284#line 39
1285  __cil_tmp17 = __cil_tmp16 + 72;
1286#line 39
1287  *((u_char *)__cil_tmp17) = (u_char )8;
1288#line 40
1289  mtd_erase_callback(instr);
1290  }
1291#line 41
1292  return (0);
1293}
1294}
1295#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1296static int ram_point(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1297                     void **virt , resource_size_t *phys ) 
1298{ unsigned long __cil_tmp7 ;
1299  unsigned long __cil_tmp8 ;
1300  void *__cil_tmp9 ;
1301
1302  {
1303#line 47
1304  __cil_tmp7 = (unsigned long )mtd;
1305#line 47
1306  __cil_tmp8 = __cil_tmp7 + 360;
1307#line 47
1308  __cil_tmp9 = *((void **)__cil_tmp8);
1309#line 47
1310  *virt = __cil_tmp9 + from;
1311#line 48
1312  *retlen = len;
1313#line 49
1314  return (0);
1315}
1316}
1317#line 52 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1318static int ram_unpoint(struct mtd_info *mtd , loff_t from , size_t len ) 
1319{ 
1320
1321  {
1322#line 54
1323  return (0);
1324}
1325}
1326#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1327static unsigned long ram_get_unmapped_area(struct mtd_info *mtd , unsigned long len ,
1328                                           unsigned long offset , unsigned long flags ) 
1329{ unsigned long __cil_tmp5 ;
1330  unsigned long __cil_tmp6 ;
1331  void *__cil_tmp7 ;
1332  unsigned long __cil_tmp8 ;
1333
1334  {
1335  {
1336#line 67
1337  __cil_tmp5 = (unsigned long )mtd;
1338#line 67
1339  __cil_tmp6 = __cil_tmp5 + 360;
1340#line 67
1341  __cil_tmp7 = *((void **)__cil_tmp6);
1342#line 67
1343  __cil_tmp8 = (unsigned long )__cil_tmp7;
1344#line 67
1345  return (__cil_tmp8 + offset);
1346  }
1347}
1348}
1349#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1350static int ram_read(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1351                    u_char *buf ) 
1352{ size_t __len ;
1353  void *__ret ;
1354  void *__cil_tmp8 ;
1355  unsigned long __cil_tmp9 ;
1356  unsigned long __cil_tmp10 ;
1357  void *__cil_tmp11 ;
1358  void *__cil_tmp12 ;
1359  void const   *__cil_tmp13 ;
1360
1361  {
1362  {
1363#line 73
1364  __len = len;
1365#line 73
1366  __cil_tmp8 = (void *)buf;
1367#line 73
1368  __cil_tmp9 = (unsigned long )mtd;
1369#line 73
1370  __cil_tmp10 = __cil_tmp9 + 360;
1371#line 73
1372  __cil_tmp11 = *((void **)__cil_tmp10);
1373#line 73
1374  __cil_tmp12 = __cil_tmp11 + from;
1375#line 73
1376  __cil_tmp13 = (void const   *)__cil_tmp12;
1377#line 73
1378  __ret = __builtin_memcpy(__cil_tmp8, __cil_tmp13, __len);
1379#line 74
1380  *retlen = len;
1381  }
1382#line 75
1383  return (0);
1384}
1385}
1386#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1387static int ram_write(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1388                     u_char const   *buf ) 
1389{ size_t __len ;
1390  void *__ret ;
1391  unsigned long __cil_tmp8 ;
1392  unsigned long __cil_tmp9 ;
1393  void *__cil_tmp10 ;
1394  char *__cil_tmp11 ;
1395  char *__cil_tmp12 ;
1396  void *__cil_tmp13 ;
1397  void const   *__cil_tmp14 ;
1398
1399  {
1400  {
1401#line 81
1402  __len = len;
1403#line 81
1404  __cil_tmp8 = (unsigned long )mtd;
1405#line 81
1406  __cil_tmp9 = __cil_tmp8 + 360;
1407#line 81
1408  __cil_tmp10 = *((void **)__cil_tmp9);
1409#line 81
1410  __cil_tmp11 = (char *)__cil_tmp10;
1411#line 81
1412  __cil_tmp12 = __cil_tmp11 + to;
1413#line 81
1414  __cil_tmp13 = (void *)__cil_tmp12;
1415#line 81
1416  __cil_tmp14 = (void const   *)buf;
1417#line 81
1418  __ret = __builtin_memcpy(__cil_tmp13, __cil_tmp14, __len);
1419#line 82
1420  *retlen = len;
1421  }
1422#line 83
1423  return (0);
1424}
1425}
1426#line 86
1427static void cleanup_mtdram(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
1428#line 86 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1429static void cleanup_mtdram(void) 
1430{ unsigned long __cil_tmp1 ;
1431  unsigned long __cil_tmp2 ;
1432  void *__cil_tmp3 ;
1433  void const   *__cil_tmp4 ;
1434  void const   *__cil_tmp5 ;
1435
1436  {
1437#line 88
1438  if (mtd_info) {
1439    {
1440#line 89
1441    mtd_device_unregister(mtd_info);
1442#line 90
1443    __cil_tmp1 = (unsigned long )mtd_info;
1444#line 90
1445    __cil_tmp2 = __cil_tmp1 + 360;
1446#line 90
1447    __cil_tmp3 = *((void **)__cil_tmp2);
1448#line 90
1449    __cil_tmp4 = (void const   *)__cil_tmp3;
1450#line 90
1451    vfree(__cil_tmp4);
1452#line 91
1453    __cil_tmp5 = (void const   *)mtd_info;
1454#line 91
1455    kfree(__cil_tmp5);
1456    }
1457  } else {
1458
1459  }
1460#line 93
1461  return;
1462}
1463}
1464#line 95 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1465int mtdram_init_device(struct mtd_info *mtd , void *mapped_address , unsigned long size ,
1466                       char *name ) 
1467{ int tmp ;
1468  void *__cil_tmp6 ;
1469  unsigned long __cil_tmp7 ;
1470  unsigned long __cil_tmp8 ;
1471  unsigned long __cil_tmp9 ;
1472  unsigned long __cil_tmp10 ;
1473  unsigned long __cil_tmp11 ;
1474  unsigned long __cil_tmp12 ;
1475  unsigned long __cil_tmp13 ;
1476  unsigned long __cil_tmp14 ;
1477  unsigned long __cil_tmp15 ;
1478  unsigned long __cil_tmp16 ;
1479  unsigned long __cil_tmp17 ;
1480  unsigned long __cil_tmp18 ;
1481  unsigned long *__cil_tmp19 ;
1482  unsigned long __cil_tmp20 ;
1483  unsigned long __cil_tmp21 ;
1484  unsigned long __cil_tmp22 ;
1485  unsigned long __cil_tmp23 ;
1486  unsigned long __cil_tmp24 ;
1487  unsigned long __cil_tmp25 ;
1488  unsigned long __cil_tmp26 ;
1489  unsigned long __cil_tmp27 ;
1490  unsigned long __cil_tmp28 ;
1491  unsigned long __cil_tmp29 ;
1492  unsigned long __cil_tmp30 ;
1493  unsigned long __cil_tmp31 ;
1494  unsigned long __cil_tmp32 ;
1495  unsigned long __cil_tmp33 ;
1496  unsigned long __cil_tmp34 ;
1497  unsigned long __cil_tmp35 ;
1498  unsigned long __cil_tmp36 ;
1499  unsigned long __cil_tmp37 ;
1500  void *__cil_tmp38 ;
1501  char const   **__cil_tmp39 ;
1502  void *__cil_tmp40 ;
1503  struct mtd_part_parser_data *__cil_tmp41 ;
1504  void *__cil_tmp42 ;
1505  struct mtd_partition  const  *__cil_tmp43 ;
1506
1507  {
1508  {
1509#line 98
1510  __cil_tmp6 = (void *)mtd;
1511#line 98
1512  memset(__cil_tmp6, 0, 1152UL);
1513#line 101
1514  __cil_tmp7 = (unsigned long )mtd;
1515#line 101
1516  __cil_tmp8 = __cil_tmp7 + 56;
1517#line 101
1518  *((char const   **)__cil_tmp8) = (char const   *)name;
1519#line 102
1520  *((u_char *)mtd) = (u_char )1;
1521#line 103
1522  __cil_tmp9 = (unsigned long )mtd;
1523#line 103
1524  __cil_tmp10 = __cil_tmp9 + 4;
1525#line 103
1526  *((uint32_t *)__cil_tmp10) = (uint32_t )7168;
1527#line 104
1528  __cil_tmp11 = (unsigned long )mtd;
1529#line 104
1530  __cil_tmp12 = __cil_tmp11 + 8;
1531#line 104
1532  *((uint64_t *)__cil_tmp12) = (uint64_t )size;
1533#line 105
1534  __cil_tmp13 = (unsigned long )mtd;
1535#line 105
1536  __cil_tmp14 = __cil_tmp13 + 20;
1537#line 105
1538  *((uint32_t *)__cil_tmp14) = (uint32_t )1;
1539#line 106
1540  __cil_tmp15 = (unsigned long )mtd;
1541#line 106
1542  __cil_tmp16 = __cil_tmp15 + 24;
1543#line 106
1544  *((uint32_t *)__cil_tmp16) = (uint32_t )64;
1545#line 107
1546  __cil_tmp17 = (unsigned long )mtd;
1547#line 107
1548  __cil_tmp18 = __cil_tmp17 + 16;
1549#line 107
1550  __cil_tmp19 = & erase_size;
1551#line 107
1552  __cil_tmp20 = *__cil_tmp19;
1553#line 107
1554  __cil_tmp21 = __cil_tmp20 * 1024UL;
1555#line 107
1556  *((uint32_t *)__cil_tmp18) = (uint32_t )__cil_tmp21;
1557#line 108
1558  __cil_tmp22 = (unsigned long )mtd;
1559#line 108
1560  __cil_tmp23 = __cil_tmp22 + 360;
1561#line 108
1562  *((void **)__cil_tmp23) = mapped_address;
1563#line 110
1564  __cil_tmp24 = (unsigned long )mtd;
1565#line 110
1566  __cil_tmp25 = __cil_tmp24 + 368;
1567#line 110
1568  *((struct module **)__cil_tmp25) = & __this_module;
1569#line 111
1570  __cil_tmp26 = (unsigned long )mtd;
1571#line 111
1572  __cil_tmp27 = __cil_tmp26 + 96;
1573#line 111
1574  *((int (**)(struct mtd_info *mtd , struct erase_info *instr ))__cil_tmp27) = & ram_erase;
1575#line 112
1576  __cil_tmp28 = (unsigned long )mtd;
1577#line 112
1578  __cil_tmp29 = __cil_tmp28 + 104;
1579#line 112
1580  *((int (**)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen , void **virt ,
1581              resource_size_t *phys ))__cil_tmp29) = & ram_point;
1582#line 113
1583  __cil_tmp30 = (unsigned long )mtd;
1584#line 113
1585  __cil_tmp31 = __cil_tmp30 + 112;
1586#line 113
1587  *((int (**)(struct mtd_info *mtd , loff_t from , size_t len ))__cil_tmp31) = & ram_unpoint;
1588#line 114
1589  __cil_tmp32 = (unsigned long )mtd;
1590#line 114
1591  __cil_tmp33 = __cil_tmp32 + 120;
1592#line 114
1593  *((unsigned long (**)(struct mtd_info *mtd , unsigned long len , unsigned long offset ,
1594                        unsigned long flags ))__cil_tmp33) = & ram_get_unmapped_area;
1595#line 115
1596  __cil_tmp34 = (unsigned long )mtd;
1597#line 115
1598  __cil_tmp35 = __cil_tmp34 + 128;
1599#line 115
1600  *((int (**)(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen , u_char *buf ))__cil_tmp35) = & ram_read;
1601#line 116
1602  __cil_tmp36 = (unsigned long )mtd;
1603#line 116
1604  __cil_tmp37 = __cil_tmp36 + 136;
1605#line 116
1606  *((int (**)(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen , u_char const   *buf ))__cil_tmp37) = & ram_write;
1607#line 118
1608  __cil_tmp38 = (void *)0;
1609#line 118
1610  __cil_tmp39 = (char const   **)__cil_tmp38;
1611#line 118
1612  __cil_tmp40 = (void *)0;
1613#line 118
1614  __cil_tmp41 = (struct mtd_part_parser_data *)__cil_tmp40;
1615#line 118
1616  __cil_tmp42 = (void *)0;
1617#line 118
1618  __cil_tmp43 = (struct mtd_partition  const  *)__cil_tmp42;
1619#line 118
1620  tmp = mtd_device_parse_register(mtd, __cil_tmp39, __cil_tmp41, __cil_tmp43, 0);
1621  }
1622#line 118
1623  if (tmp) {
1624#line 119
1625    return (-5);
1626  } else {
1627
1628  }
1629#line 121
1630  return (0);
1631}
1632}
1633#line 124
1634static int init_mtdram(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
1635#line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1636static int init_mtdram(void) 
1637{ void *addr ;
1638  int err ;
1639  void *tmp ;
1640  unsigned long *__cil_tmp4 ;
1641  unsigned long __cil_tmp5 ;
1642  unsigned long *__cil_tmp6 ;
1643  unsigned long __cil_tmp7 ;
1644  unsigned long __cil_tmp8 ;
1645  void const   *__cil_tmp9 ;
1646  void *__cil_tmp10 ;
1647  unsigned long *__cil_tmp11 ;
1648  unsigned long __cil_tmp12 ;
1649  unsigned long __cil_tmp13 ;
1650  char *__cil_tmp14 ;
1651  void const   *__cil_tmp15 ;
1652  void const   *__cil_tmp16 ;
1653  void *__cil_tmp17 ;
1654  unsigned long __cil_tmp18 ;
1655  unsigned long __cil_tmp19 ;
1656  void *__cil_tmp20 ;
1657  unsigned long *__cil_tmp21 ;
1658  unsigned long __cil_tmp22 ;
1659  unsigned long __cil_tmp23 ;
1660
1661  {
1662  {
1663#line 129
1664  __cil_tmp4 = & total_size;
1665#line 129
1666  __cil_tmp5 = *__cil_tmp4;
1667#line 129
1668  if (! __cil_tmp5) {
1669#line 130
1670    return (-22);
1671  } else {
1672
1673  }
1674  }
1675  {
1676#line 133
1677  tmp = kmalloc(1152UL, 208U);
1678#line 133
1679  mtd_info = (struct mtd_info *)tmp;
1680  }
1681#line 134
1682  if (! mtd_info) {
1683#line 135
1684    return (-12);
1685  } else {
1686
1687  }
1688  {
1689#line 137
1690  __cil_tmp6 = & total_size;
1691#line 137
1692  __cil_tmp7 = *__cil_tmp6;
1693#line 137
1694  __cil_tmp8 = __cil_tmp7 * 1024UL;
1695#line 137
1696  addr = vmalloc(__cil_tmp8);
1697  }
1698#line 138
1699  if (! addr) {
1700    {
1701#line 139
1702    __cil_tmp9 = (void const   *)mtd_info;
1703#line 139
1704    kfree(__cil_tmp9);
1705#line 140
1706    __cil_tmp10 = (void *)0;
1707#line 140
1708    mtd_info = (struct mtd_info *)__cil_tmp10;
1709    }
1710#line 141
1711    return (-12);
1712  } else {
1713
1714  }
1715  {
1716#line 143
1717  __cil_tmp11 = & total_size;
1718#line 143
1719  __cil_tmp12 = *__cil_tmp11;
1720#line 143
1721  __cil_tmp13 = __cil_tmp12 * 1024UL;
1722#line 143
1723  __cil_tmp14 = (char *)"mtdram test device";
1724#line 143
1725  err = mtdram_init_device(mtd_info, addr, __cil_tmp13, __cil_tmp14);
1726  }
1727#line 144
1728  if (err) {
1729    {
1730#line 145
1731    __cil_tmp15 = (void const   *)addr;
1732#line 145
1733    vfree(__cil_tmp15);
1734#line 146
1735    __cil_tmp16 = (void const   *)mtd_info;
1736#line 146
1737    kfree(__cil_tmp16);
1738#line 147
1739    __cil_tmp17 = (void *)0;
1740#line 147
1741    mtd_info = (struct mtd_info *)__cil_tmp17;
1742    }
1743#line 148
1744    return (err);
1745  } else {
1746
1747  }
1748  {
1749#line 150
1750  __cil_tmp18 = (unsigned long )mtd_info;
1751#line 150
1752  __cil_tmp19 = __cil_tmp18 + 360;
1753#line 150
1754  __cil_tmp20 = *((void **)__cil_tmp19);
1755#line 150
1756  __cil_tmp21 = & total_size;
1757#line 150
1758  __cil_tmp22 = *__cil_tmp21;
1759#line 150
1760  __cil_tmp23 = __cil_tmp22 * 1024UL;
1761#line 150
1762  memset(__cil_tmp20, 255, __cil_tmp23);
1763  }
1764#line 151
1765  return (err);
1766}
1767}
1768#line 154 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1769int init_module(void) 
1770{ int tmp ;
1771
1772  {
1773  {
1774#line 154
1775  tmp = init_mtdram();
1776  }
1777#line 154
1778  return (tmp);
1779}
1780}
1781#line 155 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1782void cleanup_module(void) 
1783{ 
1784
1785  {
1786  {
1787#line 155
1788  cleanup_mtdram();
1789  }
1790#line 155
1791  return;
1792}
1793}
1794#line 157 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1795static char const   __mod_license157[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1796__aligned__(1)))  = 
1797#line 157
1798  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
1799        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
1800        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
1801#line 158 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1802static char const   __mod_author158[44]  __attribute__((__used__, __unused__, __section__(".modinfo"),
1803__aligned__(1)))  = 
1804#line 158
1805  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
1806        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'A', 
1807        (char const   )'l',      (char const   )'e',      (char const   )'x',      (char const   )'a', 
1808        (char const   )'n',      (char const   )'d',      (char const   )'e',      (char const   )'r', 
1809        (char const   )' ',      (char const   )'L',      (char const   )'a',      (char const   )'r', 
1810        (char const   )'s',      (char const   )'s',      (char const   )'o',      (char const   )'n', 
1811        (char const   )' ',      (char const   )'<',      (char const   )'a',      (char const   )'l', 
1812        (char const   )'e',      (char const   )'x',      (char const   )'l',      (char const   )'@', 
1813        (char const   )'r',      (char const   )'e',      (char const   )'d',      (char const   )'h', 
1814        (char const   )'a',      (char const   )'t',      (char const   )'.',      (char const   )'c', 
1815        (char const   )'o',      (char const   )'m',      (char const   )'>',      (char const   )'\000'};
1816#line 159 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1817static char const   __mod_description159[45]  __attribute__((__used__, __unused__,
1818__section__(".modinfo"), __aligned__(1)))  = 
1819#line 159
1820  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
1821        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
1822        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
1823        (char const   )'S',      (char const   )'i',      (char const   )'m',      (char const   )'u', 
1824        (char const   )'l',      (char const   )'a',      (char const   )'t',      (char const   )'e', 
1825        (char const   )'d',      (char const   )' ',      (char const   )'M',      (char const   )'T', 
1826        (char const   )'D',      (char const   )' ',      (char const   )'d',      (char const   )'r', 
1827        (char const   )'i',      (char const   )'v',      (char const   )'e',      (char const   )'r', 
1828        (char const   )' ',      (char const   )'f',      (char const   )'o',      (char const   )'r', 
1829        (char const   )' ',      (char const   )'t',      (char const   )'e',      (char const   )'s', 
1830        (char const   )'t',      (char const   )'i',      (char const   )'n',      (char const   )'g', 
1831        (char const   )'\000'};
1832#line 177
1833void ldv_check_final_state(void) ;
1834#line 183
1835extern void ldv_initialize(void) ;
1836#line 186
1837extern int __VERIFIER_nondet_int(void) ;
1838#line 189 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1839int LDV_IN_INTERRUPT  ;
1840#line 192 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
1841void main(void) 
1842{ int tmp ;
1843  int tmp___0 ;
1844  int tmp___1 ;
1845
1846  {
1847  {
1848#line 204
1849  LDV_IN_INTERRUPT = 1;
1850#line 213
1851  ldv_initialize();
1852#line 224
1853  tmp = init_mtdram();
1854  }
1855#line 224
1856  if (tmp) {
1857#line 225
1858    goto ldv_final;
1859  } else {
1860
1861  }
1862  {
1863#line 227
1864  while (1) {
1865    while_continue: /* CIL Label */ ;
1866    {
1867#line 227
1868    tmp___1 = __VERIFIER_nondet_int();
1869    }
1870#line 227
1871    if (tmp___1) {
1872
1873    } else {
1874#line 227
1875      goto while_break;
1876    }
1877    {
1878#line 230
1879    tmp___0 = __VERIFIER_nondet_int();
1880    }
1881    {
1882#line 232
1883    goto switch_default;
1884#line 230
1885    if (0) {
1886      switch_default: /* CIL Label */ 
1887#line 232
1888      goto switch_break;
1889    } else {
1890      switch_break: /* CIL Label */ ;
1891    }
1892    }
1893  }
1894  while_break: /* CIL Label */ ;
1895  }
1896  {
1897#line 249
1898  cleanup_mtdram();
1899  }
1900  ldv_final: 
1901  {
1902#line 252
1903  ldv_check_final_state();
1904  }
1905#line 255
1906  return;
1907}
1908}
1909#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1910void ldv_blast_assert(void) 
1911{ 
1912
1913  {
1914  ERROR: 
1915#line 6
1916  goto ERROR;
1917}
1918}
1919#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1920extern int __VERIFIER_nondet_int(void) ;
1921#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1922int ldv_mutex  =    1;
1923#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1924int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
1925{ int nondetermined ;
1926
1927  {
1928#line 29
1929  if (ldv_mutex == 1) {
1930
1931  } else {
1932    {
1933#line 29
1934    ldv_blast_assert();
1935    }
1936  }
1937  {
1938#line 32
1939  nondetermined = __VERIFIER_nondet_int();
1940  }
1941#line 35
1942  if (nondetermined) {
1943#line 38
1944    ldv_mutex = 2;
1945#line 40
1946    return (0);
1947  } else {
1948#line 45
1949    return (-4);
1950  }
1951}
1952}
1953#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1954int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
1955{ int nondetermined ;
1956
1957  {
1958#line 57
1959  if (ldv_mutex == 1) {
1960
1961  } else {
1962    {
1963#line 57
1964    ldv_blast_assert();
1965    }
1966  }
1967  {
1968#line 60
1969  nondetermined = __VERIFIER_nondet_int();
1970  }
1971#line 63
1972  if (nondetermined) {
1973#line 66
1974    ldv_mutex = 2;
1975#line 68
1976    return (0);
1977  } else {
1978#line 73
1979    return (-4);
1980  }
1981}
1982}
1983#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1984int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
1985{ int atomic_value_after_dec ;
1986
1987  {
1988#line 83
1989  if (ldv_mutex == 1) {
1990
1991  } else {
1992    {
1993#line 83
1994    ldv_blast_assert();
1995    }
1996  }
1997  {
1998#line 86
1999  atomic_value_after_dec = __VERIFIER_nondet_int();
2000  }
2001#line 89
2002  if (atomic_value_after_dec == 0) {
2003#line 92
2004    ldv_mutex = 2;
2005#line 94
2006    return (1);
2007  } else {
2008
2009  }
2010#line 98
2011  return (0);
2012}
2013}
2014#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2015void mutex_lock(struct mutex *lock ) 
2016{ 
2017
2018  {
2019#line 108
2020  if (ldv_mutex == 1) {
2021
2022  } else {
2023    {
2024#line 108
2025    ldv_blast_assert();
2026    }
2027  }
2028#line 110
2029  ldv_mutex = 2;
2030#line 111
2031  return;
2032}
2033}
2034#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2035int mutex_trylock(struct mutex *lock ) 
2036{ int nondetermined ;
2037
2038  {
2039#line 121
2040  if (ldv_mutex == 1) {
2041
2042  } else {
2043    {
2044#line 121
2045    ldv_blast_assert();
2046    }
2047  }
2048  {
2049#line 124
2050  nondetermined = __VERIFIER_nondet_int();
2051  }
2052#line 127
2053  if (nondetermined) {
2054#line 130
2055    ldv_mutex = 2;
2056#line 132
2057    return (1);
2058  } else {
2059#line 137
2060    return (0);
2061  }
2062}
2063}
2064#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2065void mutex_unlock(struct mutex *lock ) 
2066{ 
2067
2068  {
2069#line 147
2070  if (ldv_mutex == 2) {
2071
2072  } else {
2073    {
2074#line 147
2075    ldv_blast_assert();
2076    }
2077  }
2078#line 149
2079  ldv_mutex = 1;
2080#line 150
2081  return;
2082}
2083}
2084#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
2085void ldv_check_final_state(void) 
2086{ 
2087
2088  {
2089#line 156
2090  if (ldv_mutex == 1) {
2091
2092  } else {
2093    {
2094#line 156
2095    ldv_blast_assert();
2096    }
2097  }
2098#line 157
2099  return;
2100}
2101}
2102#line 264 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/5413/dscv_tempdir/dscv/ri/32_1/drivers/mtd/devices/mtdram.c.common.c"
2103long s__builtin_expect(long val , long res ) 
2104{ 
2105
2106  {
2107#line 265
2108  return (val);
2109}
2110}