Showing error 501

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