Showing error 512

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