Showing error 1100

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/43_1a_cilled_safe_ok_nondet_linux-43_1a-drivers--mtd--maps--ts5500_flash.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1478
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 221 "include/linux/types.h"
  65struct __anonstruct_atomic_t_6 {
  66   int counter ;
  67};
  68#line 221 "include/linux/types.h"
  69typedef struct __anonstruct_atomic_t_6 atomic_t;
  70#line 226 "include/linux/types.h"
  71struct __anonstruct_atomic64_t_7 {
  72   long counter ;
  73};
  74#line 226 "include/linux/types.h"
  75typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  76#line 227 "include/linux/types.h"
  77struct list_head {
  78   struct list_head *next ;
  79   struct list_head *prev ;
  80};
  81#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  82struct module;
  83#line 55
  84struct module;
  85#line 146 "include/linux/init.h"
  86typedef void (*ctor_fn_t)(void);
  87#line 46 "include/linux/dynamic_debug.h"
  88struct device;
  89#line 46
  90struct device;
  91#line 57
  92struct completion;
  93#line 57
  94struct completion;
  95#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  96struct page;
  97#line 58
  98struct page;
  99#line 26 "include/asm-generic/getorder.h"
 100struct task_struct;
 101#line 26
 102struct task_struct;
 103#line 290 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 104struct file;
 105#line 290
 106struct file;
 107#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 108struct arch_spinlock;
 109#line 327
 110struct arch_spinlock;
 111#line 306 "include/linux/bitmap.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 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 123struct kmem_cache;
 124#line 23 "include/asm-generic/atomic-long.h"
 125typedef atomic64_t atomic_long_t;
 126#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 127typedef u16 __ticket_t;
 128#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 129typedef u32 __ticketpair_t;
 130#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 131struct __raw_tickets {
 132   __ticket_t head ;
 133   __ticket_t tail ;
 134};
 135#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 136union __anonunion_ldv_5907_29 {
 137   __ticketpair_t head_tail ;
 138   struct __raw_tickets tickets ;
 139};
 140#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 141struct arch_spinlock {
 142   union __anonunion_ldv_5907_29 ldv_5907 ;
 143};
 144#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 145typedef struct arch_spinlock arch_spinlock_t;
 146#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 147struct lockdep_map;
 148#line 34
 149struct lockdep_map;
 150#line 55 "include/linux/debug_locks.h"
 151struct stack_trace {
 152   unsigned int nr_entries ;
 153   unsigned int max_entries ;
 154   unsigned long *entries ;
 155   int skip ;
 156};
 157#line 26 "include/linux/stacktrace.h"
 158struct lockdep_subclass_key {
 159   char __one_byte ;
 160};
 161#line 53 "include/linux/lockdep.h"
 162struct lock_class_key {
 163   struct lockdep_subclass_key subkeys[8U] ;
 164};
 165#line 59 "include/linux/lockdep.h"
 166struct lock_class {
 167   struct list_head hash_entry ;
 168   struct list_head lock_entry ;
 169   struct lockdep_subclass_key *key ;
 170   unsigned int subclass ;
 171   unsigned int dep_gen_id ;
 172   unsigned long usage_mask ;
 173   struct stack_trace usage_traces[13U] ;
 174   struct list_head locks_after ;
 175   struct list_head locks_before ;
 176   unsigned int version ;
 177   unsigned long ops ;
 178   char const   *name ;
 179   int name_version ;
 180   unsigned long contention_point[4U] ;
 181   unsigned long contending_point[4U] ;
 182};
 183#line 144 "include/linux/lockdep.h"
 184struct lockdep_map {
 185   struct lock_class_key *key ;
 186   struct lock_class *class_cache[2U] ;
 187   char const   *name ;
 188   int cpu ;
 189   unsigned long ip ;
 190};
 191#line 556 "include/linux/lockdep.h"
 192struct raw_spinlock {
 193   arch_spinlock_t raw_lock ;
 194   unsigned int magic ;
 195   unsigned int owner_cpu ;
 196   void *owner ;
 197   struct lockdep_map dep_map ;
 198};
 199#line 33 "include/linux/spinlock_types.h"
 200struct __anonstruct_ldv_6122_33 {
 201   u8 __padding[24U] ;
 202   struct lockdep_map dep_map ;
 203};
 204#line 33 "include/linux/spinlock_types.h"
 205union __anonunion_ldv_6123_32 {
 206   struct raw_spinlock rlock ;
 207   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 208};
 209#line 33 "include/linux/spinlock_types.h"
 210struct spinlock {
 211   union __anonunion_ldv_6123_32 ldv_6123 ;
 212};
 213#line 76 "include/linux/spinlock_types.h"
 214typedef struct spinlock spinlock_t;
 215#line 48 "include/linux/wait.h"
 216struct __wait_queue_head {
 217   spinlock_t lock ;
 218   struct list_head task_list ;
 219};
 220#line 53 "include/linux/wait.h"
 221typedef struct __wait_queue_head wait_queue_head_t;
 222#line 670 "include/linux/mmzone.h"
 223struct mutex {
 224   atomic_t count ;
 225   spinlock_t wait_lock ;
 226   struct list_head wait_list ;
 227   struct task_struct *owner ;
 228   char const   *name ;
 229   void *magic ;
 230   struct lockdep_map dep_map ;
 231};
 232#line 128 "include/linux/rwsem.h"
 233struct completion {
 234   unsigned int done ;
 235   wait_queue_head_t wait ;
 236};
 237#line 188 "include/linux/rcupdate.h"
 238struct notifier_block;
 239#line 188
 240struct notifier_block;
 241#line 239 "include/linux/srcu.h"
 242struct notifier_block {
 243   int (*notifier_call)(struct notifier_block * , unsigned long  , void * ) ;
 244   struct notifier_block *next ;
 245   int priority ;
 246};
 247#line 312 "include/linux/jiffies.h"
 248union ktime {
 249   s64 tv64 ;
 250};
 251#line 59 "include/linux/ktime.h"
 252typedef union ktime ktime_t;
 253#line 341
 254struct tvec_base;
 255#line 341
 256struct tvec_base;
 257#line 342 "include/linux/ktime.h"
 258struct timer_list {
 259   struct list_head entry ;
 260   unsigned long expires ;
 261   struct tvec_base *base ;
 262   void (*function)(unsigned long  ) ;
 263   unsigned long data ;
 264   int slack ;
 265   int start_pid ;
 266   void *start_site ;
 267   char start_comm[16U] ;
 268   struct lockdep_map lockdep_map ;
 269};
 270#line 302 "include/linux/timer.h"
 271struct work_struct;
 272#line 302
 273struct work_struct;
 274#line 45 "include/linux/workqueue.h"
 275struct work_struct {
 276   atomic_long_t data ;
 277   struct list_head entry ;
 278   void (*func)(struct work_struct * ) ;
 279   struct lockdep_map lockdep_map ;
 280};
 281#line 46 "include/linux/pm.h"
 282struct pm_message {
 283   int event ;
 284};
 285#line 52 "include/linux/pm.h"
 286typedef struct pm_message pm_message_t;
 287#line 53 "include/linux/pm.h"
 288struct dev_pm_ops {
 289   int (*prepare)(struct device * ) ;
 290   void (*complete)(struct device * ) ;
 291   int (*suspend)(struct device * ) ;
 292   int (*resume)(struct device * ) ;
 293   int (*freeze)(struct device * ) ;
 294   int (*thaw)(struct device * ) ;
 295   int (*poweroff)(struct device * ) ;
 296   int (*restore)(struct device * ) ;
 297   int (*suspend_late)(struct device * ) ;
 298   int (*resume_early)(struct device * ) ;
 299   int (*freeze_late)(struct device * ) ;
 300   int (*thaw_early)(struct device * ) ;
 301   int (*poweroff_late)(struct device * ) ;
 302   int (*restore_early)(struct device * ) ;
 303   int (*suspend_noirq)(struct device * ) ;
 304   int (*resume_noirq)(struct device * ) ;
 305   int (*freeze_noirq)(struct device * ) ;
 306   int (*thaw_noirq)(struct device * ) ;
 307   int (*poweroff_noirq)(struct device * ) ;
 308   int (*restore_noirq)(struct device * ) ;
 309   int (*runtime_suspend)(struct device * ) ;
 310   int (*runtime_resume)(struct device * ) ;
 311   int (*runtime_idle)(struct device * ) ;
 312};
 313#line 289
 314enum rpm_status {
 315    RPM_ACTIVE = 0,
 316    RPM_RESUMING = 1,
 317    RPM_SUSPENDED = 2,
 318    RPM_SUSPENDING = 3
 319} ;
 320#line 296
 321enum rpm_request {
 322    RPM_REQ_NONE = 0,
 323    RPM_REQ_IDLE = 1,
 324    RPM_REQ_SUSPEND = 2,
 325    RPM_REQ_AUTOSUSPEND = 3,
 326    RPM_REQ_RESUME = 4
 327} ;
 328#line 304
 329struct wakeup_source;
 330#line 304
 331struct wakeup_source;
 332#line 494 "include/linux/pm.h"
 333struct pm_subsys_data {
 334   spinlock_t lock ;
 335   unsigned int refcount ;
 336};
 337#line 499
 338struct dev_pm_qos_request;
 339#line 499
 340struct pm_qos_constraints;
 341#line 499 "include/linux/pm.h"
 342struct dev_pm_info {
 343   pm_message_t power_state ;
 344   unsigned char can_wakeup : 1 ;
 345   unsigned char async_suspend : 1 ;
 346   bool is_prepared ;
 347   bool is_suspended ;
 348   bool ignore_children ;
 349   spinlock_t lock ;
 350   struct list_head entry ;
 351   struct completion completion ;
 352   struct wakeup_source *wakeup ;
 353   bool wakeup_path ;
 354   struct timer_list suspend_timer ;
 355   unsigned long timer_expires ;
 356   struct work_struct work ;
 357   wait_queue_head_t wait_queue ;
 358   atomic_t usage_count ;
 359   atomic_t child_count ;
 360   unsigned char disable_depth : 3 ;
 361   unsigned char idle_notification : 1 ;
 362   unsigned char request_pending : 1 ;
 363   unsigned char deferred_resume : 1 ;
 364   unsigned char run_wake : 1 ;
 365   unsigned char runtime_auto : 1 ;
 366   unsigned char no_callbacks : 1 ;
 367   unsigned char irq_safe : 1 ;
 368   unsigned char use_autosuspend : 1 ;
 369   unsigned char timer_autosuspends : 1 ;
 370   enum rpm_request request ;
 371   enum rpm_status runtime_status ;
 372   int runtime_error ;
 373   int autosuspend_delay ;
 374   unsigned long last_busy ;
 375   unsigned long active_jiffies ;
 376   unsigned long suspended_jiffies ;
 377   unsigned long accounting_timestamp ;
 378   ktime_t suspend_time ;
 379   s64 max_time_suspended_ns ;
 380   struct dev_pm_qos_request *pq_req ;
 381   struct pm_subsys_data *subsys_data ;
 382   struct pm_qos_constraints *constraints ;
 383};
 384#line 558 "include/linux/pm.h"
 385struct dev_pm_domain {
 386   struct dev_pm_ops ops ;
 387};
 388#line 18 "include/asm-generic/pci_iomap.h"
 389struct vm_area_struct;
 390#line 18
 391struct vm_area_struct;
 392#line 18 "include/linux/elf.h"
 393typedef __u64 Elf64_Addr;
 394#line 19 "include/linux/elf.h"
 395typedef __u16 Elf64_Half;
 396#line 23 "include/linux/elf.h"
 397typedef __u32 Elf64_Word;
 398#line 24 "include/linux/elf.h"
 399typedef __u64 Elf64_Xword;
 400#line 193 "include/linux/elf.h"
 401struct elf64_sym {
 402   Elf64_Word st_name ;
 403   unsigned char st_info ;
 404   unsigned char st_other ;
 405   Elf64_Half st_shndx ;
 406   Elf64_Addr st_value ;
 407   Elf64_Xword st_size ;
 408};
 409#line 201 "include/linux/elf.h"
 410typedef struct elf64_sym Elf64_Sym;
 411#line 445
 412struct sock;
 413#line 445
 414struct sock;
 415#line 446
 416struct kobject;
 417#line 446
 418struct kobject;
 419#line 447
 420enum kobj_ns_type {
 421    KOBJ_NS_TYPE_NONE = 0,
 422    KOBJ_NS_TYPE_NET = 1,
 423    KOBJ_NS_TYPES = 2
 424} ;
 425#line 453 "include/linux/elf.h"
 426struct kobj_ns_type_operations {
 427   enum kobj_ns_type type ;
 428   void *(*grab_current_ns)(void) ;
 429   void const   *(*netlink_ns)(struct sock * ) ;
 430   void const   *(*initial_ns)(void) ;
 431   void (*drop_ns)(void * ) ;
 432};
 433#line 57 "include/linux/kobject_ns.h"
 434struct attribute {
 435   char const   *name ;
 436   umode_t mode ;
 437   struct lock_class_key *key ;
 438   struct lock_class_key skey ;
 439};
 440#line 33 "include/linux/sysfs.h"
 441struct attribute_group {
 442   char const   *name ;
 443   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 444   struct attribute **attrs ;
 445};
 446#line 62 "include/linux/sysfs.h"
 447struct bin_attribute {
 448   struct attribute attr ;
 449   size_t size ;
 450   void *private ;
 451   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 452                   loff_t  , size_t  ) ;
 453   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 454                    loff_t  , size_t  ) ;
 455   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
 456};
 457#line 98 "include/linux/sysfs.h"
 458struct sysfs_ops {
 459   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 460   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 461   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 462};
 463#line 117
 464struct sysfs_dirent;
 465#line 117
 466struct sysfs_dirent;
 467#line 182 "include/linux/sysfs.h"
 468struct kref {
 469   atomic_t refcount ;
 470};
 471#line 49 "include/linux/kobject.h"
 472struct kset;
 473#line 49
 474struct kobj_type;
 475#line 49 "include/linux/kobject.h"
 476struct kobject {
 477   char const   *name ;
 478   struct list_head entry ;
 479   struct kobject *parent ;
 480   struct kset *kset ;
 481   struct kobj_type *ktype ;
 482   struct sysfs_dirent *sd ;
 483   struct kref kref ;
 484   unsigned char state_initialized : 1 ;
 485   unsigned char state_in_sysfs : 1 ;
 486   unsigned char state_add_uevent_sent : 1 ;
 487   unsigned char state_remove_uevent_sent : 1 ;
 488   unsigned char uevent_suppress : 1 ;
 489};
 490#line 107 "include/linux/kobject.h"
 491struct kobj_type {
 492   void (*release)(struct kobject * ) ;
 493   struct sysfs_ops  const  *sysfs_ops ;
 494   struct attribute **default_attrs ;
 495   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 496   void const   *(*namespace)(struct kobject * ) ;
 497};
 498#line 115 "include/linux/kobject.h"
 499struct kobj_uevent_env {
 500   char *envp[32U] ;
 501   int envp_idx ;
 502   char buf[2048U] ;
 503   int buflen ;
 504};
 505#line 122 "include/linux/kobject.h"
 506struct kset_uevent_ops {
 507   int (* const  filter)(struct kset * , struct kobject * ) ;
 508   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 509   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 510};
 511#line 139 "include/linux/kobject.h"
 512struct kset {
 513   struct list_head list ;
 514   spinlock_t list_lock ;
 515   struct kobject kobj ;
 516   struct kset_uevent_ops  const  *uevent_ops ;
 517};
 518#line 215
 519struct kernel_param;
 520#line 215
 521struct kernel_param;
 522#line 216 "include/linux/kobject.h"
 523struct kernel_param_ops {
 524   int (*set)(char const   * , struct kernel_param  const  * ) ;
 525   int (*get)(char * , struct kernel_param  const  * ) ;
 526   void (*free)(void * ) ;
 527};
 528#line 49 "include/linux/moduleparam.h"
 529struct kparam_string;
 530#line 49
 531struct kparam_array;
 532#line 49 "include/linux/moduleparam.h"
 533union __anonunion_ldv_13363_134 {
 534   void *arg ;
 535   struct kparam_string  const  *str ;
 536   struct kparam_array  const  *arr ;
 537};
 538#line 49 "include/linux/moduleparam.h"
 539struct kernel_param {
 540   char const   *name ;
 541   struct kernel_param_ops  const  *ops ;
 542   u16 perm ;
 543   s16 level ;
 544   union __anonunion_ldv_13363_134 ldv_13363 ;
 545};
 546#line 61 "include/linux/moduleparam.h"
 547struct kparam_string {
 548   unsigned int maxlen ;
 549   char *string ;
 550};
 551#line 67 "include/linux/moduleparam.h"
 552struct kparam_array {
 553   unsigned int max ;
 554   unsigned int elemsize ;
 555   unsigned int *num ;
 556   struct kernel_param_ops  const  *ops ;
 557   void *elem ;
 558};
 559#line 458 "include/linux/moduleparam.h"
 560struct static_key {
 561   atomic_t enabled ;
 562};
 563#line 225 "include/linux/jump_label.h"
 564struct tracepoint;
 565#line 225
 566struct tracepoint;
 567#line 226 "include/linux/jump_label.h"
 568struct tracepoint_func {
 569   void *func ;
 570   void *data ;
 571};
 572#line 29 "include/linux/tracepoint.h"
 573struct tracepoint {
 574   char const   *name ;
 575   struct static_key key ;
 576   void (*regfunc)(void) ;
 577   void (*unregfunc)(void) ;
 578   struct tracepoint_func *funcs ;
 579};
 580#line 86 "include/linux/tracepoint.h"
 581struct kernel_symbol {
 582   unsigned long value ;
 583   char const   *name ;
 584};
 585#line 27 "include/linux/export.h"
 586struct mod_arch_specific {
 587
 588};
 589#line 34 "include/linux/module.h"
 590struct module_param_attrs;
 591#line 34 "include/linux/module.h"
 592struct module_kobject {
 593   struct kobject kobj ;
 594   struct module *mod ;
 595   struct kobject *drivers_dir ;
 596   struct module_param_attrs *mp ;
 597};
 598#line 43 "include/linux/module.h"
 599struct module_attribute {
 600   struct attribute attr ;
 601   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 602   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 603                    size_t  ) ;
 604   void (*setup)(struct module * , char const   * ) ;
 605   int (*test)(struct module * ) ;
 606   void (*free)(struct module * ) ;
 607};
 608#line 69
 609struct exception_table_entry;
 610#line 69
 611struct exception_table_entry;
 612#line 198
 613enum module_state {
 614    MODULE_STATE_LIVE = 0,
 615    MODULE_STATE_COMING = 1,
 616    MODULE_STATE_GOING = 2
 617} ;
 618#line 204 "include/linux/module.h"
 619struct module_ref {
 620   unsigned long incs ;
 621   unsigned long decs ;
 622};
 623#line 219
 624struct module_sect_attrs;
 625#line 219
 626struct module_notes_attrs;
 627#line 219
 628struct ftrace_event_call;
 629#line 219 "include/linux/module.h"
 630struct module {
 631   enum module_state state ;
 632   struct list_head list ;
 633   char name[56U] ;
 634   struct module_kobject mkobj ;
 635   struct module_attribute *modinfo_attrs ;
 636   char const   *version ;
 637   char const   *srcversion ;
 638   struct kobject *holders_dir ;
 639   struct kernel_symbol  const  *syms ;
 640   unsigned long const   *crcs ;
 641   unsigned int num_syms ;
 642   struct kernel_param *kp ;
 643   unsigned int num_kp ;
 644   unsigned int num_gpl_syms ;
 645   struct kernel_symbol  const  *gpl_syms ;
 646   unsigned long const   *gpl_crcs ;
 647   struct kernel_symbol  const  *unused_syms ;
 648   unsigned long const   *unused_crcs ;
 649   unsigned int num_unused_syms ;
 650   unsigned int num_unused_gpl_syms ;
 651   struct kernel_symbol  const  *unused_gpl_syms ;
 652   unsigned long const   *unused_gpl_crcs ;
 653   struct kernel_symbol  const  *gpl_future_syms ;
 654   unsigned long const   *gpl_future_crcs ;
 655   unsigned int num_gpl_future_syms ;
 656   unsigned int num_exentries ;
 657   struct exception_table_entry *extable ;
 658   int (*init)(void) ;
 659   void *module_init ;
 660   void *module_core ;
 661   unsigned int init_size ;
 662   unsigned int core_size ;
 663   unsigned int init_text_size ;
 664   unsigned int core_text_size ;
 665   unsigned int init_ro_size ;
 666   unsigned int core_ro_size ;
 667   struct mod_arch_specific arch ;
 668   unsigned int taints ;
 669   unsigned int num_bugs ;
 670   struct list_head bug_list ;
 671   struct bug_entry *bug_table ;
 672   Elf64_Sym *symtab ;
 673   Elf64_Sym *core_symtab ;
 674   unsigned int num_symtab ;
 675   unsigned int core_num_syms ;
 676   char *strtab ;
 677   char *core_strtab ;
 678   struct module_sect_attrs *sect_attrs ;
 679   struct module_notes_attrs *notes_attrs ;
 680   char *args ;
 681   void *percpu ;
 682   unsigned int percpu_size ;
 683   unsigned int num_tracepoints ;
 684   struct tracepoint * const  *tracepoints_ptrs ;
 685   unsigned int num_trace_bprintk_fmt ;
 686   char const   **trace_bprintk_fmt_start ;
 687   struct ftrace_event_call **trace_events ;
 688   unsigned int num_trace_events ;
 689   struct list_head source_list ;
 690   struct list_head target_list ;
 691   struct task_struct *waiter ;
 692   void (*exit)(void) ;
 693   struct module_ref *refptr ;
 694   ctor_fn_t (**ctors)(void) ;
 695   unsigned int num_ctors ;
 696};
 697#line 88 "include/linux/kmemleak.h"
 698struct kmem_cache_cpu {
 699   void **freelist ;
 700   unsigned long tid ;
 701   struct page *page ;
 702   struct page *partial ;
 703   int node ;
 704   unsigned int stat[26U] ;
 705};
 706#line 55 "include/linux/slub_def.h"
 707struct kmem_cache_node {
 708   spinlock_t list_lock ;
 709   unsigned long nr_partial ;
 710   struct list_head partial ;
 711   atomic_long_t nr_slabs ;
 712   atomic_long_t total_objects ;
 713   struct list_head full ;
 714};
 715#line 66 "include/linux/slub_def.h"
 716struct kmem_cache_order_objects {
 717   unsigned long x ;
 718};
 719#line 76 "include/linux/slub_def.h"
 720struct kmem_cache {
 721   struct kmem_cache_cpu *cpu_slab ;
 722   unsigned long flags ;
 723   unsigned long min_partial ;
 724   int size ;
 725   int objsize ;
 726   int offset ;
 727   int cpu_partial ;
 728   struct kmem_cache_order_objects oo ;
 729   struct kmem_cache_order_objects max ;
 730   struct kmem_cache_order_objects min ;
 731   gfp_t allocflags ;
 732   int refcount ;
 733   void (*ctor)(void * ) ;
 734   int inuse ;
 735   int align ;
 736   int reserved ;
 737   char const   *name ;
 738   struct list_head list ;
 739   struct kobject kobj ;
 740   int remote_node_defrag_ratio ;
 741   struct kmem_cache_node *node[1024U] ;
 742};
 743#line 188 "include/linux/mtd/map.h"
 744union __anonunion_map_word_135 {
 745   unsigned long x[4U] ;
 746};
 747#line 188 "include/linux/mtd/map.h"
 748typedef union __anonunion_map_word_135 map_word;
 749#line 189
 750struct mtd_chip_driver;
 751#line 189 "include/linux/mtd/map.h"
 752struct map_info {
 753   char const   *name ;
 754   unsigned long size ;
 755   resource_size_t phys ;
 756   void *virt ;
 757   void *cached ;
 758   int swap ;
 759   int bankwidth ;
 760   map_word (*read)(struct map_info * , unsigned long  ) ;
 761   void (*copy_from)(struct map_info * , void * , unsigned long  , ssize_t  ) ;
 762   void (*write)(struct map_info * , map_word const    , unsigned long  ) ;
 763   void (*copy_to)(struct map_info * , unsigned long  , void const   * , ssize_t  ) ;
 764   void (*inval_cache)(struct map_info * , unsigned long  , ssize_t  ) ;
 765   void (*set_vpp)(struct map_info * , int  ) ;
 766   unsigned long pfow_base ;
 767   unsigned long map_priv_1 ;
 768   unsigned long map_priv_2 ;
 769   void *fldrv_priv ;
 770   struct mtd_chip_driver *fldrv ;
 771};
 772#line 251
 773struct mtd_info;
 774#line 251 "include/linux/mtd/map.h"
 775struct mtd_chip_driver {
 776   struct mtd_info *(*probe)(struct map_info * ) ;
 777   void (*destroy)(struct mtd_info * ) ;
 778   struct module *module ;
 779   char *name ;
 780   struct list_head list ;
 781};
 782#line 21 "include/linux/uio.h"
 783struct kvec {
 784   void *iov_base ;
 785   size_t iov_len ;
 786};
 787#line 54
 788struct klist_node;
 789#line 54
 790struct klist_node;
 791#line 37 "include/linux/klist.h"
 792struct klist_node {
 793   void *n_klist ;
 794   struct list_head n_node ;
 795   struct kref n_ref ;
 796};
 797#line 67
 798struct dma_map_ops;
 799#line 67 "include/linux/klist.h"
 800struct dev_archdata {
 801   void *acpi_handle ;
 802   struct dma_map_ops *dma_ops ;
 803   void *iommu ;
 804};
 805#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 806struct device_private;
 807#line 17
 808struct device_private;
 809#line 18
 810struct device_driver;
 811#line 18
 812struct device_driver;
 813#line 19
 814struct driver_private;
 815#line 19
 816struct driver_private;
 817#line 20
 818struct class;
 819#line 20
 820struct class;
 821#line 21
 822struct subsys_private;
 823#line 21
 824struct subsys_private;
 825#line 22
 826struct bus_type;
 827#line 22
 828struct bus_type;
 829#line 23
 830struct device_node;
 831#line 23
 832struct device_node;
 833#line 24
 834struct iommu_ops;
 835#line 24
 836struct iommu_ops;
 837#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 838struct bus_attribute {
 839   struct attribute attr ;
 840   ssize_t (*show)(struct bus_type * , char * ) ;
 841   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
 842};
 843#line 51 "include/linux/device.h"
 844struct device_attribute;
 845#line 51
 846struct driver_attribute;
 847#line 51 "include/linux/device.h"
 848struct bus_type {
 849   char const   *name ;
 850   char const   *dev_name ;
 851   struct device *dev_root ;
 852   struct bus_attribute *bus_attrs ;
 853   struct device_attribute *dev_attrs ;
 854   struct driver_attribute *drv_attrs ;
 855   int (*match)(struct device * , struct device_driver * ) ;
 856   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 857   int (*probe)(struct device * ) ;
 858   int (*remove)(struct device * ) ;
 859   void (*shutdown)(struct device * ) ;
 860   int (*suspend)(struct device * , pm_message_t  ) ;
 861   int (*resume)(struct device * ) ;
 862   struct dev_pm_ops  const  *pm ;
 863   struct iommu_ops *iommu_ops ;
 864   struct subsys_private *p ;
 865};
 866#line 125
 867struct device_type;
 868#line 182
 869struct of_device_id;
 870#line 182 "include/linux/device.h"
 871struct device_driver {
 872   char const   *name ;
 873   struct bus_type *bus ;
 874   struct module *owner ;
 875   char const   *mod_name ;
 876   bool suppress_bind_attrs ;
 877   struct of_device_id  const  *of_match_table ;
 878   int (*probe)(struct device * ) ;
 879   int (*remove)(struct device * ) ;
 880   void (*shutdown)(struct device * ) ;
 881   int (*suspend)(struct device * , pm_message_t  ) ;
 882   int (*resume)(struct device * ) ;
 883   struct attribute_group  const  **groups ;
 884   struct dev_pm_ops  const  *pm ;
 885   struct driver_private *p ;
 886};
 887#line 245 "include/linux/device.h"
 888struct driver_attribute {
 889   struct attribute attr ;
 890   ssize_t (*show)(struct device_driver * , char * ) ;
 891   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
 892};
 893#line 299
 894struct class_attribute;
 895#line 299 "include/linux/device.h"
 896struct class {
 897   char const   *name ;
 898   struct module *owner ;
 899   struct class_attribute *class_attrs ;
 900   struct device_attribute *dev_attrs ;
 901   struct bin_attribute *dev_bin_attrs ;
 902   struct kobject *dev_kobj ;
 903   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
 904   char *(*devnode)(struct device * , umode_t * ) ;
 905   void (*class_release)(struct class * ) ;
 906   void (*dev_release)(struct device * ) ;
 907   int (*suspend)(struct device * , pm_message_t  ) ;
 908   int (*resume)(struct device * ) ;
 909   struct kobj_ns_type_operations  const  *ns_type ;
 910   void const   *(*namespace)(struct device * ) ;
 911   struct dev_pm_ops  const  *pm ;
 912   struct subsys_private *p ;
 913};
 914#line 394 "include/linux/device.h"
 915struct class_attribute {
 916   struct attribute attr ;
 917   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
 918   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
 919   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
 920};
 921#line 447 "include/linux/device.h"
 922struct device_type {
 923   char const   *name ;
 924   struct attribute_group  const  **groups ;
 925   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 926   char *(*devnode)(struct device * , umode_t * ) ;
 927   void (*release)(struct device * ) ;
 928   struct dev_pm_ops  const  *pm ;
 929};
 930#line 474 "include/linux/device.h"
 931struct device_attribute {
 932   struct attribute attr ;
 933   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
 934   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
 935                    size_t  ) ;
 936};
 937#line 557 "include/linux/device.h"
 938struct device_dma_parameters {
 939   unsigned int max_segment_size ;
 940   unsigned long segment_boundary_mask ;
 941};
 942#line 567
 943struct dma_coherent_mem;
 944#line 567 "include/linux/device.h"
 945struct device {
 946   struct device *parent ;
 947   struct device_private *p ;
 948   struct kobject kobj ;
 949   char const   *init_name ;
 950   struct device_type  const  *type ;
 951   struct mutex mutex ;
 952   struct bus_type *bus ;
 953   struct device_driver *driver ;
 954   void *platform_data ;
 955   struct dev_pm_info power ;
 956   struct dev_pm_domain *pm_domain ;
 957   int numa_node ;
 958   u64 *dma_mask ;
 959   u64 coherent_dma_mask ;
 960   struct device_dma_parameters *dma_parms ;
 961   struct list_head dma_pools ;
 962   struct dma_coherent_mem *dma_mem ;
 963   struct dev_archdata archdata ;
 964   struct device_node *of_node ;
 965   dev_t devt ;
 966   u32 id ;
 967   spinlock_t devres_lock ;
 968   struct list_head devres_head ;
 969   struct klist_node knode_class ;
 970   struct class *class ;
 971   struct attribute_group  const  **groups ;
 972   void (*release)(struct device * ) ;
 973};
 974#line 681 "include/linux/device.h"
 975struct wakeup_source {
 976   char const   *name ;
 977   struct list_head entry ;
 978   spinlock_t lock ;
 979   struct timer_list timer ;
 980   unsigned long timer_expires ;
 981   ktime_t total_time ;
 982   ktime_t max_time ;
 983   ktime_t last_time ;
 984   unsigned long event_count ;
 985   unsigned long active_count ;
 986   unsigned long relax_count ;
 987   unsigned long hit_count ;
 988   unsigned char active : 1 ;
 989};
 990#line 142 "include/mtd/mtd-abi.h"
 991struct otp_info {
 992   __u32 start ;
 993   __u32 length ;
 994   __u32 locked ;
 995};
 996#line 216 "include/mtd/mtd-abi.h"
 997struct nand_oobfree {
 998   __u32 offset ;
 999   __u32 length ;
1000};
1001#line 238 "include/mtd/mtd-abi.h"
1002struct mtd_ecc_stats {
1003   __u32 corrected ;
1004   __u32 failed ;
1005   __u32 badblocks ;
1006   __u32 bbtblocks ;
1007};
1008#line 260 "include/mtd/mtd-abi.h"
1009struct erase_info {
1010   struct mtd_info *mtd ;
1011   uint64_t addr ;
1012   uint64_t len ;
1013   uint64_t fail_addr ;
1014   u_long time ;
1015   u_long retries ;
1016   unsigned int dev ;
1017   unsigned int cell ;
1018   void (*callback)(struct erase_info * ) ;
1019   u_long priv ;
1020   u_char state ;
1021   struct erase_info *next ;
1022};
1023#line 62 "include/linux/mtd/mtd.h"
1024struct mtd_erase_region_info {
1025   uint64_t offset ;
1026   uint32_t erasesize ;
1027   uint32_t numblocks ;
1028   unsigned long *lockmap ;
1029};
1030#line 69 "include/linux/mtd/mtd.h"
1031struct mtd_oob_ops {
1032   unsigned int mode ;
1033   size_t len ;
1034   size_t retlen ;
1035   size_t ooblen ;
1036   size_t oobretlen ;
1037   uint32_t ooboffs ;
1038   uint8_t *datbuf ;
1039   uint8_t *oobbuf ;
1040};
1041#line 99 "include/linux/mtd/mtd.h"
1042struct nand_ecclayout {
1043   __u32 eccbytes ;
1044   __u32 eccpos[448U] ;
1045   __u32 oobavail ;
1046   struct nand_oobfree oobfree[32U] ;
1047};
1048#line 114
1049struct backing_dev_info;
1050#line 114 "include/linux/mtd/mtd.h"
1051struct mtd_info {
1052   u_char type ;
1053   uint32_t flags ;
1054   uint64_t size ;
1055   uint32_t erasesize ;
1056   uint32_t writesize ;
1057   uint32_t writebufsize ;
1058   uint32_t oobsize ;
1059   uint32_t oobavail ;
1060   unsigned int erasesize_shift ;
1061   unsigned int writesize_shift ;
1062   unsigned int erasesize_mask ;
1063   unsigned int writesize_mask ;
1064   char const   *name ;
1065   int index ;
1066   struct nand_ecclayout *ecclayout ;
1067   unsigned int ecc_strength ;
1068   int numeraseregions ;
1069   struct mtd_erase_region_info *eraseregions ;
1070   int (*_erase)(struct mtd_info * , struct erase_info * ) ;
1071   int (*_point)(struct mtd_info * , loff_t  , size_t  , size_t * , void ** , resource_size_t * ) ;
1072   int (*_unpoint)(struct mtd_info * , loff_t  , size_t  ) ;
1073   unsigned long (*_get_unmapped_area)(struct mtd_info * , unsigned long  , unsigned long  ,
1074                                       unsigned long  ) ;
1075   int (*_read)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char * ) ;
1076   int (*_write)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char const   * ) ;
1077   int (*_panic_write)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char const   * ) ;
1078   int (*_read_oob)(struct mtd_info * , loff_t  , struct mtd_oob_ops * ) ;
1079   int (*_write_oob)(struct mtd_info * , loff_t  , struct mtd_oob_ops * ) ;
1080   int (*_get_fact_prot_info)(struct mtd_info * , struct otp_info * , size_t  ) ;
1081   int (*_read_fact_prot_reg)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char * ) ;
1082   int (*_get_user_prot_info)(struct mtd_info * , struct otp_info * , size_t  ) ;
1083   int (*_read_user_prot_reg)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char * ) ;
1084   int (*_write_user_prot_reg)(struct mtd_info * , loff_t  , size_t  , size_t * ,
1085                               u_char * ) ;
1086   int (*_lock_user_prot_reg)(struct mtd_info * , loff_t  , size_t  ) ;
1087   int (*_writev)(struct mtd_info * , struct kvec  const  * , unsigned long  , loff_t  ,
1088                  size_t * ) ;
1089   void (*_sync)(struct mtd_info * ) ;
1090   int (*_lock)(struct mtd_info * , loff_t  , uint64_t  ) ;
1091   int (*_unlock)(struct mtd_info * , loff_t  , uint64_t  ) ;
1092   int (*_is_locked)(struct mtd_info * , loff_t  , uint64_t  ) ;
1093   int (*_block_isbad)(struct mtd_info * , loff_t  ) ;
1094   int (*_block_markbad)(struct mtd_info * , loff_t  ) ;
1095   int (*_suspend)(struct mtd_info * ) ;
1096   void (*_resume)(struct mtd_info * ) ;
1097   int (*_get_device)(struct mtd_info * ) ;
1098   void (*_put_device)(struct mtd_info * ) ;
1099   struct backing_dev_info *backing_dev_info ;
1100   struct notifier_block reboot_notifier ;
1101   struct mtd_ecc_stats ecc_stats ;
1102   int subpage_sft ;
1103   void *priv ;
1104   struct module *owner ;
1105   struct device dev ;
1106   int usecount ;
1107};
1108#line 356
1109struct mtd_partition;
1110#line 356
1111struct mtd_partition;
1112#line 357
1113struct mtd_part_parser_data;
1114#line 357
1115struct mtd_part_parser_data;
1116#line 401 "include/linux/mtd/mtd.h"
1117struct mtd_partition {
1118   char *name ;
1119   uint64_t size ;
1120   uint64_t offset ;
1121   uint32_t mask_flags ;
1122   struct nand_ecclayout *ecclayout ;
1123};
1124#line 46 "include/linux/mtd/partitions.h"
1125struct mtd_part_parser_data {
1126   unsigned long origin ;
1127   struct device_node *of_node ;
1128};
1129#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1130void ldv_spin_lock(void) ;
1131#line 3
1132void ldv_spin_unlock(void) ;
1133#line 4
1134int ldv_spin_trylock(void) ;
1135#line 101 "include/linux/printk.h"
1136extern int printk(char const   *  , ...) ;
1137#line 174 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
1138extern void *ioremap_nocache(resource_size_t  , unsigned long  ) ;
1139#line 187
1140extern void iounmap(void volatile   * ) ;
1141#line 26 "include/linux/export.h"
1142extern struct module __this_module ;
1143#line 220 "include/linux/slub_def.h"
1144extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1145#line 223
1146void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1147#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1148void ldv_check_alloc_flags(gfp_t flags ) ;
1149#line 12
1150void ldv_check_alloc_nonatomic(void) ;
1151#line 14
1152struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1153#line 263 "include/linux/mtd/map.h"
1154extern struct mtd_info *do_map_probe(char const   * , struct map_info * ) ;
1155#line 264
1156extern void map_destroy(struct mtd_info * ) ;
1157#line 450
1158extern void simple_map_init(struct map_info * ) ;
1159#line 362 "include/linux/mtd/mtd.h"
1160extern int mtd_device_parse_register(struct mtd_info * , char const   ** , struct mtd_part_parser_data * ,
1161                                     struct mtd_partition  const  * , int  ) ;
1162#line 369
1163extern int mtd_device_unregister(struct mtd_info * ) ;
1164#line 54 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1165static struct map_info ts5500_map  = 
1166#line 54 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1167     {"TS-5500 Flash", 2097152UL, 155189248ULL, (void *)0, (void *)0, 0, 1, (map_word (*)(struct map_info * ,
1168                                                                                        unsigned long  ))0,
1169    (void (*)(struct map_info * , void * , unsigned long  , ssize_t  ))0, (void (*)(struct map_info * ,
1170                                                                                    map_word const    ,
1171                                                                                    unsigned long  ))0,
1172    (void (*)(struct map_info * , unsigned long  , void const   * , ssize_t  ))0,
1173    (void (*)(struct map_info * , unsigned long  , ssize_t  ))0, (void (*)(struct map_info * ,
1174                                                                           int  ))0,
1175    0UL, 0UL, 0UL, (void *)0, (struct mtd_chip_driver *)0};
1176#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1177static struct mtd_partition ts5500_partitions[3U]  = {      {(char *)"Drive A", 917504ULL, 0ULL, 0U, (struct nand_ecclayout *)0}, 
1178        {(char *)"BIOS", 131072ULL, 917504ULL, 0U, (struct nand_ecclayout *)0}, 
1179        {(char *)"Drive B", 1048576ULL, 1048576ULL, 0U, (struct nand_ecclayout *)0}};
1180#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1181static struct mtd_info *mymtd  ;
1182#line 83 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1183static int init_ts5500_map(void) 
1184{ int rc ;
1185  unsigned long __cil_tmp2 ;
1186  unsigned long __cil_tmp3 ;
1187  resource_size_t __cil_tmp4 ;
1188  unsigned long __cil_tmp5 ;
1189  unsigned long __cil_tmp6 ;
1190  void *__cil_tmp7 ;
1191  unsigned long __cil_tmp8 ;
1192  unsigned long __cil_tmp9 ;
1193  void *__cil_tmp10 ;
1194  unsigned long __cil_tmp11 ;
1195  struct mtd_info *__cil_tmp12 ;
1196  unsigned long __cil_tmp13 ;
1197  unsigned long __cil_tmp14 ;
1198  struct mtd_info *__cil_tmp15 ;
1199  unsigned long __cil_tmp16 ;
1200  unsigned long __cil_tmp17 ;
1201  unsigned long __cil_tmp18 ;
1202  unsigned long __cil_tmp19 ;
1203  char const   **__cil_tmp20 ;
1204  struct mtd_part_parser_data *__cil_tmp21 ;
1205  struct mtd_partition  const  *__cil_tmp22 ;
1206  unsigned long __cil_tmp23 ;
1207  void *__cil_tmp24 ;
1208  void volatile   *__cil_tmp25 ;
1209
1210  {
1211  {
1212#line 85
1213  rc = 0;
1214#line 87
1215  __cil_tmp2 = (unsigned long )(& ts5500_map) + 24;
1216#line 87
1217  __cil_tmp3 = (unsigned long )(& ts5500_map) + 16;
1218#line 87
1219  __cil_tmp4 = *((resource_size_t *)__cil_tmp3);
1220#line 87
1221  __cil_tmp5 = (unsigned long )(& ts5500_map) + 8;
1222#line 87
1223  __cil_tmp6 = *((unsigned long *)__cil_tmp5);
1224#line 87
1225  *((void **)__cil_tmp2) = ioremap_nocache(__cil_tmp4, __cil_tmp6);
1226  }
1227  {
1228#line 89
1229  __cil_tmp7 = (void *)0;
1230#line 89
1231  __cil_tmp8 = (unsigned long )__cil_tmp7;
1232#line 89
1233  __cil_tmp9 = (unsigned long )(& ts5500_map) + 24;
1234#line 89
1235  __cil_tmp10 = *((void **)__cil_tmp9);
1236#line 89
1237  __cil_tmp11 = (unsigned long )__cil_tmp10;
1238#line 89
1239  if (__cil_tmp11 == __cil_tmp8) {
1240    {
1241#line 90
1242    printk("<3>Failed to ioremap_nocache\n");
1243#line 91
1244    rc = -5;
1245    }
1246#line 92
1247    goto err2;
1248  } else {
1249
1250  }
1251  }
1252  {
1253#line 95
1254  simple_map_init(& ts5500_map);
1255#line 97
1256  mymtd = do_map_probe("jedec_probe", & ts5500_map);
1257  }
1258  {
1259#line 98
1260  __cil_tmp12 = (struct mtd_info *)0;
1261#line 98
1262  __cil_tmp13 = (unsigned long )__cil_tmp12;
1263#line 98
1264  __cil_tmp14 = (unsigned long )mymtd;
1265#line 98
1266  if (__cil_tmp14 == __cil_tmp13) {
1267    {
1268#line 99
1269    mymtd = do_map_probe("map_rom", & ts5500_map);
1270    }
1271  } else {
1272
1273  }
1274  }
1275  {
1276#line 101
1277  __cil_tmp15 = (struct mtd_info *)0;
1278#line 101
1279  __cil_tmp16 = (unsigned long )__cil_tmp15;
1280#line 101
1281  __cil_tmp17 = (unsigned long )mymtd;
1282#line 101
1283  if (__cil_tmp17 == __cil_tmp16) {
1284#line 102
1285    rc = -6;
1286#line 103
1287    goto err1;
1288  } else {
1289
1290  }
1291  }
1292  {
1293#line 106
1294  __cil_tmp18 = (unsigned long )mymtd;
1295#line 106
1296  __cil_tmp19 = __cil_tmp18 + 368;
1297#line 106
1298  *((struct module **)__cil_tmp19) = & __this_module;
1299#line 107
1300  __cil_tmp20 = (char const   **)0;
1301#line 107
1302  __cil_tmp21 = (struct mtd_part_parser_data *)0;
1303#line 107
1304  __cil_tmp22 = (struct mtd_partition  const  *)(& ts5500_partitions);
1305#line 107
1306  mtd_device_parse_register(mymtd, __cil_tmp20, __cil_tmp21, __cil_tmp22, 3);
1307  }
1308#line 109
1309  return (0);
1310  err1: 
1311  {
1312#line 112
1313  __cil_tmp23 = (unsigned long )(& ts5500_map) + 24;
1314#line 112
1315  __cil_tmp24 = *((void **)__cil_tmp23);
1316#line 112
1317  __cil_tmp25 = (void volatile   *)__cil_tmp24;
1318#line 112
1319  iounmap(__cil_tmp25);
1320  }
1321  err2: ;
1322#line 114
1323  return (rc);
1324}
1325}
1326#line 117 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1327static void cleanup_ts5500_map(void) 
1328{ struct mtd_info *__cil_tmp1 ;
1329  unsigned long __cil_tmp2 ;
1330  unsigned long __cil_tmp3 ;
1331  void *__cil_tmp4 ;
1332  unsigned long __cil_tmp5 ;
1333  unsigned long __cil_tmp6 ;
1334  void *__cil_tmp7 ;
1335  unsigned long __cil_tmp8 ;
1336  unsigned long __cil_tmp9 ;
1337  void *__cil_tmp10 ;
1338  void volatile   *__cil_tmp11 ;
1339  unsigned long __cil_tmp12 ;
1340
1341  {
1342  {
1343#line 119
1344  __cil_tmp1 = (struct mtd_info *)0;
1345#line 119
1346  __cil_tmp2 = (unsigned long )__cil_tmp1;
1347#line 119
1348  __cil_tmp3 = (unsigned long )mymtd;
1349#line 119
1350  if (__cil_tmp3 != __cil_tmp2) {
1351    {
1352#line 120
1353    mtd_device_unregister(mymtd);
1354#line 121
1355    map_destroy(mymtd);
1356    }
1357  } else {
1358
1359  }
1360  }
1361  {
1362#line 124
1363  __cil_tmp4 = (void *)0;
1364#line 124
1365  __cil_tmp5 = (unsigned long )__cil_tmp4;
1366#line 124
1367  __cil_tmp6 = (unsigned long )(& ts5500_map) + 24;
1368#line 124
1369  __cil_tmp7 = *((void **)__cil_tmp6);
1370#line 124
1371  __cil_tmp8 = (unsigned long )__cil_tmp7;
1372#line 124
1373  if (__cil_tmp8 != __cil_tmp5) {
1374    {
1375#line 125
1376    __cil_tmp9 = (unsigned long )(& ts5500_map) + 24;
1377#line 125
1378    __cil_tmp10 = *((void **)__cil_tmp9);
1379#line 125
1380    __cil_tmp11 = (void volatile   *)__cil_tmp10;
1381#line 125
1382    iounmap(__cil_tmp11);
1383#line 126
1384    __cil_tmp12 = (unsigned long )(& ts5500_map) + 24;
1385#line 126
1386    *((void **)__cil_tmp12) = (void *)0;
1387    }
1388  } else {
1389
1390  }
1391  }
1392#line 128
1393  return;
1394}
1395}
1396#line 154
1397extern void ldv_check_final_state(void) ;
1398#line 160
1399extern void ldv_initialize(void) ;
1400#line 163
1401extern int __VERIFIER_nondet_int(void) ;
1402#line 166 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1403int LDV_IN_INTERRUPT  ;
1404#line 169 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1405void main(void) 
1406{ int tmp ;
1407  int tmp___0 ;
1408  int tmp___1 ;
1409
1410  {
1411  {
1412#line 181
1413  LDV_IN_INTERRUPT = 1;
1414#line 190
1415  ldv_initialize();
1416#line 200
1417  tmp = init_ts5500_map();
1418  }
1419#line 200
1420  if (tmp != 0) {
1421#line 201
1422    goto ldv_final;
1423  } else {
1424
1425  }
1426#line 203
1427  goto ldv_15649;
1428  ldv_15648: 
1429  {
1430#line 206
1431  tmp___0 = __VERIFIER_nondet_int();
1432  }
1433  {
1434#line 208
1435  goto switch_default;
1436#line 206
1437  if (0) {
1438    switch_default: /* CIL Label */ ;
1439#line 208
1440    goto ldv_15647;
1441  } else {
1442    switch_break: /* CIL Label */ ;
1443  }
1444  }
1445  ldv_15647: ;
1446  ldv_15649: 
1447  {
1448#line 203
1449  tmp___1 = __VERIFIER_nondet_int();
1450  }
1451#line 203
1452  if (tmp___1 != 0) {
1453#line 204
1454    goto ldv_15648;
1455  } else {
1456#line 206
1457    goto ldv_15650;
1458  }
1459  ldv_15650: ;
1460  {
1461#line 224
1462  cleanup_ts5500_map();
1463  }
1464  ldv_final: 
1465  {
1466#line 227
1467  ldv_check_final_state();
1468  }
1469#line 230
1470  return;
1471}
1472}
1473#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1474void ldv_blast_assert(void) 
1475{ 
1476
1477  {
1478  ERROR: ;
1479#line 6
1480  goto ERROR;
1481}
1482}
1483#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1484extern int __VERIFIER_nondet_int(void) ;
1485#line 251 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1486int ldv_spin  =    0;
1487#line 255 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1488void ldv_check_alloc_flags(gfp_t flags ) 
1489{ 
1490
1491  {
1492#line 258
1493  if (ldv_spin != 0) {
1494#line 258
1495    if (flags != 32U) {
1496      {
1497#line 258
1498      ldv_blast_assert();
1499      }
1500    } else {
1501
1502    }
1503  } else {
1504
1505  }
1506#line 261
1507  return;
1508}
1509}
1510#line 261
1511extern struct page *ldv_some_page(void) ;
1512#line 264 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1513struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
1514{ struct page *tmp ;
1515
1516  {
1517#line 267
1518  if (ldv_spin != 0) {
1519#line 267
1520    if (flags != 32U) {
1521      {
1522#line 267
1523      ldv_blast_assert();
1524      }
1525    } else {
1526
1527    }
1528  } else {
1529
1530  }
1531  {
1532#line 269
1533  tmp = ldv_some_page();
1534  }
1535#line 269
1536  return (tmp);
1537}
1538}
1539#line 273 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1540void ldv_check_alloc_nonatomic(void) 
1541{ 
1542
1543  {
1544#line 276
1545  if (ldv_spin != 0) {
1546    {
1547#line 276
1548    ldv_blast_assert();
1549    }
1550  } else {
1551
1552  }
1553#line 279
1554  return;
1555}
1556}
1557#line 280 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1558void ldv_spin_lock(void) 
1559{ 
1560
1561  {
1562#line 283
1563  ldv_spin = 1;
1564#line 284
1565  return;
1566}
1567}
1568#line 287 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1569void ldv_spin_unlock(void) 
1570{ 
1571
1572  {
1573#line 290
1574  ldv_spin = 0;
1575#line 291
1576  return;
1577}
1578}
1579#line 294 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1580int ldv_spin_trylock(void) 
1581{ int is_lock ;
1582
1583  {
1584  {
1585#line 299
1586  is_lock = __VERIFIER_nondet_int();
1587  }
1588#line 301
1589  if (is_lock != 0) {
1590#line 304
1591    return (0);
1592  } else {
1593#line 309
1594    ldv_spin = 1;
1595#line 311
1596    return (1);
1597  }
1598}
1599}
1600#line 478 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11647/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/maps/ts5500_flash.c.p"
1601void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
1602{ 
1603
1604  {
1605  {
1606#line 484
1607  ldv_check_alloc_flags(ldv_func_arg2);
1608#line 486
1609  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1610  }
1611#line 487
1612  return ((void *)0);
1613}
1614}