Showing error 1091

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--devices--mtdram.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1770
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_13367_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_13367_134 ldv_13367 ;
 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 21 "include/linux/uio.h"
 744struct kvec {
 745   void *iov_base ;
 746   size_t iov_len ;
 747};
 748#line 54
 749struct klist_node;
 750#line 54
 751struct klist_node;
 752#line 37 "include/linux/klist.h"
 753struct klist_node {
 754   void *n_klist ;
 755   struct list_head n_node ;
 756   struct kref n_ref ;
 757};
 758#line 67
 759struct dma_map_ops;
 760#line 67 "include/linux/klist.h"
 761struct dev_archdata {
 762   void *acpi_handle ;
 763   struct dma_map_ops *dma_ops ;
 764   void *iommu ;
 765};
 766#line 17 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 767struct device_private;
 768#line 17
 769struct device_private;
 770#line 18
 771struct device_driver;
 772#line 18
 773struct device_driver;
 774#line 19
 775struct driver_private;
 776#line 19
 777struct driver_private;
 778#line 20
 779struct class;
 780#line 20
 781struct class;
 782#line 21
 783struct subsys_private;
 784#line 21
 785struct subsys_private;
 786#line 22
 787struct bus_type;
 788#line 22
 789struct bus_type;
 790#line 23
 791struct device_node;
 792#line 23
 793struct device_node;
 794#line 24
 795struct iommu_ops;
 796#line 24
 797struct iommu_ops;
 798#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 799struct bus_attribute {
 800   struct attribute attr ;
 801   ssize_t (*show)(struct bus_type * , char * ) ;
 802   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
 803};
 804#line 51 "include/linux/device.h"
 805struct device_attribute;
 806#line 51
 807struct driver_attribute;
 808#line 51 "include/linux/device.h"
 809struct bus_type {
 810   char const   *name ;
 811   char const   *dev_name ;
 812   struct device *dev_root ;
 813   struct bus_attribute *bus_attrs ;
 814   struct device_attribute *dev_attrs ;
 815   struct driver_attribute *drv_attrs ;
 816   int (*match)(struct device * , struct device_driver * ) ;
 817   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 818   int (*probe)(struct device * ) ;
 819   int (*remove)(struct device * ) ;
 820   void (*shutdown)(struct device * ) ;
 821   int (*suspend)(struct device * , pm_message_t  ) ;
 822   int (*resume)(struct device * ) ;
 823   struct dev_pm_ops  const  *pm ;
 824   struct iommu_ops *iommu_ops ;
 825   struct subsys_private *p ;
 826};
 827#line 125
 828struct device_type;
 829#line 182
 830struct of_device_id;
 831#line 182 "include/linux/device.h"
 832struct device_driver {
 833   char const   *name ;
 834   struct bus_type *bus ;
 835   struct module *owner ;
 836   char const   *mod_name ;
 837   bool suppress_bind_attrs ;
 838   struct of_device_id  const  *of_match_table ;
 839   int (*probe)(struct device * ) ;
 840   int (*remove)(struct device * ) ;
 841   void (*shutdown)(struct device * ) ;
 842   int (*suspend)(struct device * , pm_message_t  ) ;
 843   int (*resume)(struct device * ) ;
 844   struct attribute_group  const  **groups ;
 845   struct dev_pm_ops  const  *pm ;
 846   struct driver_private *p ;
 847};
 848#line 245 "include/linux/device.h"
 849struct driver_attribute {
 850   struct attribute attr ;
 851   ssize_t (*show)(struct device_driver * , char * ) ;
 852   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
 853};
 854#line 299
 855struct class_attribute;
 856#line 299 "include/linux/device.h"
 857struct class {
 858   char const   *name ;
 859   struct module *owner ;
 860   struct class_attribute *class_attrs ;
 861   struct device_attribute *dev_attrs ;
 862   struct bin_attribute *dev_bin_attrs ;
 863   struct kobject *dev_kobj ;
 864   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
 865   char *(*devnode)(struct device * , umode_t * ) ;
 866   void (*class_release)(struct class * ) ;
 867   void (*dev_release)(struct device * ) ;
 868   int (*suspend)(struct device * , pm_message_t  ) ;
 869   int (*resume)(struct device * ) ;
 870   struct kobj_ns_type_operations  const  *ns_type ;
 871   void const   *(*namespace)(struct device * ) ;
 872   struct dev_pm_ops  const  *pm ;
 873   struct subsys_private *p ;
 874};
 875#line 394 "include/linux/device.h"
 876struct class_attribute {
 877   struct attribute attr ;
 878   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
 879   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
 880   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
 881};
 882#line 447 "include/linux/device.h"
 883struct device_type {
 884   char const   *name ;
 885   struct attribute_group  const  **groups ;
 886   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 887   char *(*devnode)(struct device * , umode_t * ) ;
 888   void (*release)(struct device * ) ;
 889   struct dev_pm_ops  const  *pm ;
 890};
 891#line 474 "include/linux/device.h"
 892struct device_attribute {
 893   struct attribute attr ;
 894   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
 895   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
 896                    size_t  ) ;
 897};
 898#line 557 "include/linux/device.h"
 899struct device_dma_parameters {
 900   unsigned int max_segment_size ;
 901   unsigned long segment_boundary_mask ;
 902};
 903#line 567
 904struct dma_coherent_mem;
 905#line 567 "include/linux/device.h"
 906struct device {
 907   struct device *parent ;
 908   struct device_private *p ;
 909   struct kobject kobj ;
 910   char const   *init_name ;
 911   struct device_type  const  *type ;
 912   struct mutex mutex ;
 913   struct bus_type *bus ;
 914   struct device_driver *driver ;
 915   void *platform_data ;
 916   struct dev_pm_info power ;
 917   struct dev_pm_domain *pm_domain ;
 918   int numa_node ;
 919   u64 *dma_mask ;
 920   u64 coherent_dma_mask ;
 921   struct device_dma_parameters *dma_parms ;
 922   struct list_head dma_pools ;
 923   struct dma_coherent_mem *dma_mem ;
 924   struct dev_archdata archdata ;
 925   struct device_node *of_node ;
 926   dev_t devt ;
 927   u32 id ;
 928   spinlock_t devres_lock ;
 929   struct list_head devres_head ;
 930   struct klist_node knode_class ;
 931   struct class *class ;
 932   struct attribute_group  const  **groups ;
 933   void (*release)(struct device * ) ;
 934};
 935#line 681 "include/linux/device.h"
 936struct wakeup_source {
 937   char const   *name ;
 938   struct list_head entry ;
 939   spinlock_t lock ;
 940   struct timer_list timer ;
 941   unsigned long timer_expires ;
 942   ktime_t total_time ;
 943   ktime_t max_time ;
 944   ktime_t last_time ;
 945   unsigned long event_count ;
 946   unsigned long active_count ;
 947   unsigned long relax_count ;
 948   unsigned long hit_count ;
 949   unsigned char active : 1 ;
 950};
 951#line 142 "include/mtd/mtd-abi.h"
 952struct otp_info {
 953   __u32 start ;
 954   __u32 length ;
 955   __u32 locked ;
 956};
 957#line 216 "include/mtd/mtd-abi.h"
 958struct nand_oobfree {
 959   __u32 offset ;
 960   __u32 length ;
 961};
 962#line 238 "include/mtd/mtd-abi.h"
 963struct mtd_ecc_stats {
 964   __u32 corrected ;
 965   __u32 failed ;
 966   __u32 badblocks ;
 967   __u32 bbtblocks ;
 968};
 969#line 260
 970struct mtd_info;
 971#line 260 "include/mtd/mtd-abi.h"
 972struct erase_info {
 973   struct mtd_info *mtd ;
 974   uint64_t addr ;
 975   uint64_t len ;
 976   uint64_t fail_addr ;
 977   u_long time ;
 978   u_long retries ;
 979   unsigned int dev ;
 980   unsigned int cell ;
 981   void (*callback)(struct erase_info * ) ;
 982   u_long priv ;
 983   u_char state ;
 984   struct erase_info *next ;
 985};
 986#line 62 "include/linux/mtd/mtd.h"
 987struct mtd_erase_region_info {
 988   uint64_t offset ;
 989   uint32_t erasesize ;
 990   uint32_t numblocks ;
 991   unsigned long *lockmap ;
 992};
 993#line 69 "include/linux/mtd/mtd.h"
 994struct mtd_oob_ops {
 995   unsigned int mode ;
 996   size_t len ;
 997   size_t retlen ;
 998   size_t ooblen ;
 999   size_t oobretlen ;
1000   uint32_t ooboffs ;
1001   uint8_t *datbuf ;
1002   uint8_t *oobbuf ;
1003};
1004#line 99 "include/linux/mtd/mtd.h"
1005struct nand_ecclayout {
1006   __u32 eccbytes ;
1007   __u32 eccpos[448U] ;
1008   __u32 oobavail ;
1009   struct nand_oobfree oobfree[32U] ;
1010};
1011#line 114
1012struct backing_dev_info;
1013#line 114 "include/linux/mtd/mtd.h"
1014struct mtd_info {
1015   u_char type ;
1016   uint32_t flags ;
1017   uint64_t size ;
1018   uint32_t erasesize ;
1019   uint32_t writesize ;
1020   uint32_t writebufsize ;
1021   uint32_t oobsize ;
1022   uint32_t oobavail ;
1023   unsigned int erasesize_shift ;
1024   unsigned int writesize_shift ;
1025   unsigned int erasesize_mask ;
1026   unsigned int writesize_mask ;
1027   char const   *name ;
1028   int index ;
1029   struct nand_ecclayout *ecclayout ;
1030   unsigned int ecc_strength ;
1031   int numeraseregions ;
1032   struct mtd_erase_region_info *eraseregions ;
1033   int (*_erase)(struct mtd_info * , struct erase_info * ) ;
1034   int (*_point)(struct mtd_info * , loff_t  , size_t  , size_t * , void ** , resource_size_t * ) ;
1035   int (*_unpoint)(struct mtd_info * , loff_t  , size_t  ) ;
1036   unsigned long (*_get_unmapped_area)(struct mtd_info * , unsigned long  , unsigned long  ,
1037                                       unsigned long  ) ;
1038   int (*_read)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char * ) ;
1039   int (*_write)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char const   * ) ;
1040   int (*_panic_write)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char const   * ) ;
1041   int (*_read_oob)(struct mtd_info * , loff_t  , struct mtd_oob_ops * ) ;
1042   int (*_write_oob)(struct mtd_info * , loff_t  , struct mtd_oob_ops * ) ;
1043   int (*_get_fact_prot_info)(struct mtd_info * , struct otp_info * , size_t  ) ;
1044   int (*_read_fact_prot_reg)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char * ) ;
1045   int (*_get_user_prot_info)(struct mtd_info * , struct otp_info * , size_t  ) ;
1046   int (*_read_user_prot_reg)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char * ) ;
1047   int (*_write_user_prot_reg)(struct mtd_info * , loff_t  , size_t  , size_t * ,
1048                               u_char * ) ;
1049   int (*_lock_user_prot_reg)(struct mtd_info * , loff_t  , size_t  ) ;
1050   int (*_writev)(struct mtd_info * , struct kvec  const  * , unsigned long  , loff_t  ,
1051                  size_t * ) ;
1052   void (*_sync)(struct mtd_info * ) ;
1053   int (*_lock)(struct mtd_info * , loff_t  , uint64_t  ) ;
1054   int (*_unlock)(struct mtd_info * , loff_t  , uint64_t  ) ;
1055   int (*_is_locked)(struct mtd_info * , loff_t  , uint64_t  ) ;
1056   int (*_block_isbad)(struct mtd_info * , loff_t  ) ;
1057   int (*_block_markbad)(struct mtd_info * , loff_t  ) ;
1058   int (*_suspend)(struct mtd_info * ) ;
1059   void (*_resume)(struct mtd_info * ) ;
1060   int (*_get_device)(struct mtd_info * ) ;
1061   void (*_put_device)(struct mtd_info * ) ;
1062   struct backing_dev_info *backing_dev_info ;
1063   struct notifier_block reboot_notifier ;
1064   struct mtd_ecc_stats ecc_stats ;
1065   int subpage_sft ;
1066   void *priv ;
1067   struct module *owner ;
1068   struct device dev ;
1069   int usecount ;
1070};
1071#line 356
1072struct mtd_partition;
1073#line 356
1074struct mtd_partition;
1075#line 357
1076struct mtd_part_parser_data;
1077#line 357
1078struct mtd_part_parser_data;
1079#line 1 "<compiler builtins>"
1080
1081#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1082void ldv_spin_lock(void) ;
1083#line 3
1084void ldv_spin_unlock(void) ;
1085#line 4
1086int ldv_spin_trylock(void) ;
1087#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
1088extern void *memset(void * , int  , size_t  ) ;
1089#line 54 "include/linux/vmalloc.h"
1090extern void *vmalloc(unsigned long  ) ;
1091#line 57
1092void *ldv_vmalloc_19(unsigned long ldv_func_arg1 ) ;
1093#line 70
1094extern void vfree(void const   * ) ;
1095#line 26 "include/linux/export.h"
1096extern struct module __this_module ;
1097#line 161 "include/linux/slab.h"
1098extern void kfree(void const   * ) ;
1099#line 220 "include/linux/slub_def.h"
1100extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1101#line 223
1102void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1103#line 225
1104extern void *__kmalloc(size_t  , gfp_t  ) ;
1105#line 268 "include/linux/slub_def.h"
1106__inline static void *ldv_kmalloc_12(size_t size , gfp_t flags ) 
1107{ void *tmp___2 ;
1108
1109  {
1110  {
1111#line 283
1112  tmp___2 = __kmalloc(size, flags);
1113  }
1114#line 283
1115  return (tmp___2);
1116}
1117}
1118#line 268
1119__inline static void *kmalloc(size_t size , gfp_t flags ) ;
1120#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1121void ldv_check_alloc_flags(gfp_t flags ) ;
1122#line 12
1123void ldv_check_alloc_nonatomic(void) ;
1124#line 14
1125struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1126#line 362 "include/linux/mtd/mtd.h"
1127extern int mtd_device_parse_register(struct mtd_info * , char const   ** , struct mtd_part_parser_data * ,
1128                                     struct mtd_partition  const  * , int  ) ;
1129#line 369
1130extern int mtd_device_unregister(struct mtd_info * ) ;
1131#line 388
1132extern void mtd_erase_callback(struct erase_info * ) ;
1133#line 5 "include/linux/mtd/mtdram.h"
1134int mtdram_init_device(struct mtd_info *mtd , void *mapped_address , unsigned long size ,
1135                       char *name ) ;
1136#line 35 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1137static unsigned long total_size  =    4096UL;
1138#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1139static unsigned long erase_size  =    128UL;
1140#line 48 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1141static struct mtd_info *mtd_info  ;
1142#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1143static int ram_erase(struct mtd_info *mtd , struct erase_info *instr ) 
1144{ unsigned long __cil_tmp3 ;
1145  unsigned long __cil_tmp4 ;
1146  uint64_t __cil_tmp5 ;
1147  unsigned long __cil_tmp6 ;
1148  unsigned long __cil_tmp7 ;
1149  unsigned long __cil_tmp8 ;
1150  void *__cil_tmp9 ;
1151  void *__cil_tmp10 ;
1152  unsigned long __cil_tmp11 ;
1153  unsigned long __cil_tmp12 ;
1154  uint64_t __cil_tmp13 ;
1155  size_t __cil_tmp14 ;
1156  unsigned long __cil_tmp15 ;
1157  unsigned long __cil_tmp16 ;
1158
1159  {
1160  {
1161#line 52
1162  __cil_tmp3 = (unsigned long )instr;
1163#line 52
1164  __cil_tmp4 = __cil_tmp3 + 8;
1165#line 52
1166  __cil_tmp5 = *((uint64_t *)__cil_tmp4);
1167#line 52
1168  __cil_tmp6 = (unsigned long )__cil_tmp5;
1169#line 52
1170  __cil_tmp7 = (unsigned long )mtd;
1171#line 52
1172  __cil_tmp8 = __cil_tmp7 + 360;
1173#line 52
1174  __cil_tmp9 = *((void **)__cil_tmp8);
1175#line 52
1176  __cil_tmp10 = __cil_tmp9 + __cil_tmp6;
1177#line 52
1178  __cil_tmp11 = (unsigned long )instr;
1179#line 52
1180  __cil_tmp12 = __cil_tmp11 + 16;
1181#line 52
1182  __cil_tmp13 = *((uint64_t *)__cil_tmp12);
1183#line 52
1184  __cil_tmp14 = (size_t )__cil_tmp13;
1185#line 52
1186  memset(__cil_tmp10, 255, __cil_tmp14);
1187#line 53
1188  __cil_tmp15 = (unsigned long )instr;
1189#line 53
1190  __cil_tmp16 = __cil_tmp15 + 72;
1191#line 53
1192  *((u_char *)__cil_tmp16) = (u_char )8U;
1193#line 54
1194  mtd_erase_callback(instr);
1195  }
1196#line 55
1197  return (0);
1198}
1199}
1200#line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1201static int ram_point(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1202                     void **virt , resource_size_t *phys ) 
1203{ unsigned long __cil_tmp7 ;
1204  unsigned long __cil_tmp8 ;
1205  unsigned long __cil_tmp9 ;
1206  void *__cil_tmp10 ;
1207
1208  {
1209#line 61
1210  __cil_tmp7 = (unsigned long )from;
1211#line 61
1212  __cil_tmp8 = (unsigned long )mtd;
1213#line 61
1214  __cil_tmp9 = __cil_tmp8 + 360;
1215#line 61
1216  __cil_tmp10 = *((void **)__cil_tmp9);
1217#line 61
1218  *virt = __cil_tmp10 + __cil_tmp7;
1219#line 62
1220  *retlen = len;
1221#line 63
1222  return (0);
1223}
1224}
1225#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1226static int ram_unpoint(struct mtd_info *mtd , loff_t from , size_t len ) 
1227{ 
1228
1229  {
1230#line 68
1231  return (0);
1232}
1233}
1234#line 76 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1235static unsigned long ram_get_unmapped_area(struct mtd_info *mtd , unsigned long len ,
1236                                           unsigned long offset , unsigned long flags ) 
1237{ unsigned long __cil_tmp5 ;
1238  unsigned long __cil_tmp6 ;
1239  void *__cil_tmp7 ;
1240  unsigned long __cil_tmp8 ;
1241
1242  {
1243  {
1244#line 81
1245  __cil_tmp5 = (unsigned long )mtd;
1246#line 81
1247  __cil_tmp6 = __cil_tmp5 + 360;
1248#line 81
1249  __cil_tmp7 = *((void **)__cil_tmp6);
1250#line 81
1251  __cil_tmp8 = (unsigned long )__cil_tmp7;
1252#line 81
1253  return (__cil_tmp8 + offset);
1254  }
1255}
1256}
1257#line 84 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1258static int ram_read(struct mtd_info *mtd , loff_t from , size_t len , size_t *retlen ,
1259                    u_char *buf ) 
1260{ size_t __len ;
1261  void *__ret ;
1262  void *__cil_tmp8 ;
1263  unsigned long __cil_tmp9 ;
1264  unsigned long __cil_tmp10 ;
1265  unsigned long __cil_tmp11 ;
1266  void *__cil_tmp12 ;
1267  void const   *__cil_tmp13 ;
1268  void const   *__cil_tmp14 ;
1269
1270  {
1271  {
1272#line 87
1273  __len = len;
1274#line 87
1275  __cil_tmp8 = (void *)buf;
1276#line 87
1277  __cil_tmp9 = (unsigned long )from;
1278#line 87
1279  __cil_tmp10 = (unsigned long )mtd;
1280#line 87
1281  __cil_tmp11 = __cil_tmp10 + 360;
1282#line 87
1283  __cil_tmp12 = *((void **)__cil_tmp11);
1284#line 87
1285  __cil_tmp13 = (void const   *)__cil_tmp12;
1286#line 87
1287  __cil_tmp14 = __cil_tmp13 + __cil_tmp9;
1288#line 87
1289  __ret = __builtin_memcpy(__cil_tmp8, __cil_tmp14, __len);
1290#line 88
1291  *retlen = len;
1292  }
1293#line 89
1294  return (0);
1295}
1296}
1297#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1298static int ram_write(struct mtd_info *mtd , loff_t to , size_t len , size_t *retlen ,
1299                     u_char const   *buf ) 
1300{ size_t __len ;
1301  void *__ret ;
1302  unsigned long __cil_tmp8 ;
1303  unsigned long __cil_tmp9 ;
1304  unsigned long __cil_tmp10 ;
1305  void *__cil_tmp11 ;
1306  void *__cil_tmp12 ;
1307  void const   *__cil_tmp13 ;
1308
1309  {
1310  {
1311#line 95
1312  __len = len;
1313#line 95
1314  __cil_tmp8 = (unsigned long )to;
1315#line 95
1316  __cil_tmp9 = (unsigned long )mtd;
1317#line 95
1318  __cil_tmp10 = __cil_tmp9 + 360;
1319#line 95
1320  __cil_tmp11 = *((void **)__cil_tmp10);
1321#line 95
1322  __cil_tmp12 = __cil_tmp11 + __cil_tmp8;
1323#line 95
1324  __cil_tmp13 = (void const   *)buf;
1325#line 95
1326  __ret = __builtin_memcpy(__cil_tmp12, __cil_tmp13, __len);
1327#line 96
1328  *retlen = len;
1329  }
1330#line 97
1331  return (0);
1332}
1333}
1334#line 100 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1335static void cleanup_mtdram(void) 
1336{ struct mtd_info *__cil_tmp1 ;
1337  unsigned long __cil_tmp2 ;
1338  unsigned long __cil_tmp3 ;
1339  unsigned long __cil_tmp4 ;
1340  unsigned long __cil_tmp5 ;
1341  void *__cil_tmp6 ;
1342  void const   *__cil_tmp7 ;
1343  void const   *__cil_tmp8 ;
1344
1345  {
1346  {
1347#line 102
1348  __cil_tmp1 = (struct mtd_info *)0;
1349#line 102
1350  __cil_tmp2 = (unsigned long )__cil_tmp1;
1351#line 102
1352  __cil_tmp3 = (unsigned long )mtd_info;
1353#line 102
1354  if (__cil_tmp3 != __cil_tmp2) {
1355    {
1356#line 103
1357    mtd_device_unregister(mtd_info);
1358#line 104
1359    __cil_tmp4 = (unsigned long )mtd_info;
1360#line 104
1361    __cil_tmp5 = __cil_tmp4 + 360;
1362#line 104
1363    __cil_tmp6 = *((void **)__cil_tmp5);
1364#line 104
1365    __cil_tmp7 = (void const   *)__cil_tmp6;
1366#line 104
1367    vfree(__cil_tmp7);
1368#line 105
1369    __cil_tmp8 = (void const   *)mtd_info;
1370#line 105
1371    kfree(__cil_tmp8);
1372    }
1373  } else {
1374
1375  }
1376  }
1377#line 107
1378  return;
1379}
1380}
1381#line 109 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1382int mtdram_init_device(struct mtd_info *mtd , void *mapped_address , unsigned long size ,
1383                       char *name ) 
1384{ int tmp ;
1385  void *__cil_tmp6 ;
1386  unsigned long __cil_tmp7 ;
1387  unsigned long __cil_tmp8 ;
1388  unsigned long __cil_tmp9 ;
1389  unsigned long __cil_tmp10 ;
1390  unsigned long __cil_tmp11 ;
1391  unsigned long __cil_tmp12 ;
1392  unsigned long __cil_tmp13 ;
1393  unsigned long __cil_tmp14 ;
1394  unsigned long __cil_tmp15 ;
1395  unsigned long __cil_tmp16 ;
1396  unsigned long __cil_tmp17 ;
1397  unsigned long __cil_tmp18 ;
1398  unsigned long *__cil_tmp19 ;
1399  unsigned long __cil_tmp20 ;
1400  uint32_t __cil_tmp21 ;
1401  unsigned long __cil_tmp22 ;
1402  unsigned long __cil_tmp23 ;
1403  unsigned long __cil_tmp24 ;
1404  unsigned long __cil_tmp25 ;
1405  unsigned long __cil_tmp26 ;
1406  unsigned long __cil_tmp27 ;
1407  unsigned long __cil_tmp28 ;
1408  unsigned long __cil_tmp29 ;
1409  unsigned long __cil_tmp30 ;
1410  unsigned long __cil_tmp31 ;
1411  unsigned long __cil_tmp32 ;
1412  unsigned long __cil_tmp33 ;
1413  unsigned long __cil_tmp34 ;
1414  unsigned long __cil_tmp35 ;
1415  unsigned long __cil_tmp36 ;
1416  unsigned long __cil_tmp37 ;
1417  char const   **__cil_tmp38 ;
1418  struct mtd_part_parser_data *__cil_tmp39 ;
1419  struct mtd_partition  const  *__cil_tmp40 ;
1420
1421  {
1422  {
1423#line 112
1424  __cil_tmp6 = (void *)mtd;
1425#line 112
1426  memset(__cil_tmp6, 0, 1536UL);
1427#line 115
1428  __cil_tmp7 = (unsigned long )mtd;
1429#line 115
1430  __cil_tmp8 = __cil_tmp7 + 56;
1431#line 115
1432  *((char const   **)__cil_tmp8) = (char const   *)name;
1433#line 116
1434  *((u_char *)mtd) = (u_char )1U;
1435#line 117
1436  __cil_tmp9 = (unsigned long )mtd;
1437#line 117
1438  __cil_tmp10 = __cil_tmp9 + 4;
1439#line 117
1440  *((uint32_t *)__cil_tmp10) = 7168U;
1441#line 118
1442  __cil_tmp11 = (unsigned long )mtd;
1443#line 118
1444  __cil_tmp12 = __cil_tmp11 + 8;
1445#line 118
1446  *((uint64_t *)__cil_tmp12) = (uint64_t )size;
1447#line 119
1448  __cil_tmp13 = (unsigned long )mtd;
1449#line 119
1450  __cil_tmp14 = __cil_tmp13 + 20;
1451#line 119
1452  *((uint32_t *)__cil_tmp14) = 1U;
1453#line 120
1454  __cil_tmp15 = (unsigned long )mtd;
1455#line 120
1456  __cil_tmp16 = __cil_tmp15 + 24;
1457#line 120
1458  *((uint32_t *)__cil_tmp16) = 64U;
1459#line 121
1460  __cil_tmp17 = (unsigned long )mtd;
1461#line 121
1462  __cil_tmp18 = __cil_tmp17 + 16;
1463#line 121
1464  __cil_tmp19 = & erase_size;
1465#line 121
1466  __cil_tmp20 = *__cil_tmp19;
1467#line 121
1468  __cil_tmp21 = (uint32_t )__cil_tmp20;
1469#line 121
1470  *((uint32_t *)__cil_tmp18) = __cil_tmp21 * 1024U;
1471#line 122
1472  __cil_tmp22 = (unsigned long )mtd;
1473#line 122
1474  __cil_tmp23 = __cil_tmp22 + 360;
1475#line 122
1476  *((void **)__cil_tmp23) = mapped_address;
1477#line 124
1478  __cil_tmp24 = (unsigned long )mtd;
1479#line 124
1480  __cil_tmp25 = __cil_tmp24 + 368;
1481#line 124
1482  *((struct module **)__cil_tmp25) = & __this_module;
1483#line 125
1484  __cil_tmp26 = (unsigned long )mtd;
1485#line 125
1486  __cil_tmp27 = __cil_tmp26 + 96;
1487#line 125
1488  *((int (**)(struct mtd_info * , struct erase_info * ))__cil_tmp27) = & ram_erase;
1489#line 126
1490  __cil_tmp28 = (unsigned long )mtd;
1491#line 126
1492  __cil_tmp29 = __cil_tmp28 + 104;
1493#line 126
1494  *((int (**)(struct mtd_info * , loff_t  , size_t  , size_t * , void ** , resource_size_t * ))__cil_tmp29) = & ram_point;
1495#line 127
1496  __cil_tmp30 = (unsigned long )mtd;
1497#line 127
1498  __cil_tmp31 = __cil_tmp30 + 112;
1499#line 127
1500  *((int (**)(struct mtd_info * , loff_t  , size_t  ))__cil_tmp31) = & ram_unpoint;
1501#line 128
1502  __cil_tmp32 = (unsigned long )mtd;
1503#line 128
1504  __cil_tmp33 = __cil_tmp32 + 120;
1505#line 128
1506  *((unsigned long (**)(struct mtd_info * , unsigned long  , unsigned long  , unsigned long  ))__cil_tmp33) = & ram_get_unmapped_area;
1507#line 129
1508  __cil_tmp34 = (unsigned long )mtd;
1509#line 129
1510  __cil_tmp35 = __cil_tmp34 + 128;
1511#line 129
1512  *((int (**)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char * ))__cil_tmp35) = & ram_read;
1513#line 130
1514  __cil_tmp36 = (unsigned long )mtd;
1515#line 130
1516  __cil_tmp37 = __cil_tmp36 + 136;
1517#line 130
1518  *((int (**)(struct mtd_info * , loff_t  , size_t  , size_t * , u_char const   * ))__cil_tmp37) = & ram_write;
1519#line 132
1520  __cil_tmp38 = (char const   **)0;
1521#line 132
1522  __cil_tmp39 = (struct mtd_part_parser_data *)0;
1523#line 132
1524  __cil_tmp40 = (struct mtd_partition  const  *)0;
1525#line 132
1526  tmp = mtd_device_parse_register(mtd, __cil_tmp38, __cil_tmp39, __cil_tmp40, 0);
1527  }
1528#line 132
1529  if (tmp != 0) {
1530#line 133
1531    return (-5);
1532  } else {
1533
1534  }
1535#line 135
1536  return (0);
1537}
1538}
1539#line 138 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1540static int init_mtdram(void) 
1541{ void *addr ;
1542  int err ;
1543  void *tmp ;
1544  unsigned long *__cil_tmp4 ;
1545  unsigned long __cil_tmp5 ;
1546  struct mtd_info *__cil_tmp6 ;
1547  unsigned long __cil_tmp7 ;
1548  unsigned long __cil_tmp8 ;
1549  unsigned long *__cil_tmp9 ;
1550  unsigned long __cil_tmp10 ;
1551  unsigned long __cil_tmp11 ;
1552  void *__cil_tmp12 ;
1553  unsigned long __cil_tmp13 ;
1554  unsigned long __cil_tmp14 ;
1555  void const   *__cil_tmp15 ;
1556  unsigned long *__cil_tmp16 ;
1557  unsigned long __cil_tmp17 ;
1558  unsigned long __cil_tmp18 ;
1559  char *__cil_tmp19 ;
1560  void const   *__cil_tmp20 ;
1561  void const   *__cil_tmp21 ;
1562  unsigned long __cil_tmp22 ;
1563  unsigned long __cil_tmp23 ;
1564  void *__cil_tmp24 ;
1565  unsigned long *__cil_tmp25 ;
1566  unsigned long __cil_tmp26 ;
1567  unsigned long __cil_tmp27 ;
1568
1569  {
1570  {
1571#line 143
1572  __cil_tmp4 = & total_size;
1573#line 143
1574  __cil_tmp5 = *__cil_tmp4;
1575#line 143
1576  if (__cil_tmp5 == 0UL) {
1577#line 144
1578    return (-22);
1579  } else {
1580
1581  }
1582  }
1583  {
1584#line 147
1585  tmp = kmalloc(1536UL, 208U);
1586#line 147
1587  mtd_info = (struct mtd_info *)tmp;
1588  }
1589  {
1590#line 148
1591  __cil_tmp6 = (struct mtd_info *)0;
1592#line 148
1593  __cil_tmp7 = (unsigned long )__cil_tmp6;
1594#line 148
1595  __cil_tmp8 = (unsigned long )mtd_info;
1596#line 148
1597  if (__cil_tmp8 == __cil_tmp7) {
1598#line 149
1599    return (-12);
1600  } else {
1601
1602  }
1603  }
1604  {
1605#line 151
1606  __cil_tmp9 = & total_size;
1607#line 151
1608  __cil_tmp10 = *__cil_tmp9;
1609#line 151
1610  __cil_tmp11 = __cil_tmp10 * 1024UL;
1611#line 151
1612  addr = ldv_vmalloc_19(__cil_tmp11);
1613  }
1614  {
1615#line 152
1616  __cil_tmp12 = (void *)0;
1617#line 152
1618  __cil_tmp13 = (unsigned long )__cil_tmp12;
1619#line 152
1620  __cil_tmp14 = (unsigned long )addr;
1621#line 152
1622  if (__cil_tmp14 == __cil_tmp13) {
1623    {
1624#line 153
1625    __cil_tmp15 = (void const   *)mtd_info;
1626#line 153
1627    kfree(__cil_tmp15);
1628#line 154
1629    mtd_info = (struct mtd_info *)0;
1630    }
1631#line 155
1632    return (-12);
1633  } else {
1634
1635  }
1636  }
1637  {
1638#line 157
1639  __cil_tmp16 = & total_size;
1640#line 157
1641  __cil_tmp17 = *__cil_tmp16;
1642#line 157
1643  __cil_tmp18 = __cil_tmp17 * 1024UL;
1644#line 157
1645  __cil_tmp19 = (char *)"mtdram test device";
1646#line 157
1647  err = mtdram_init_device(mtd_info, addr, __cil_tmp18, __cil_tmp19);
1648  }
1649#line 158
1650  if (err != 0) {
1651    {
1652#line 159
1653    __cil_tmp20 = (void const   *)addr;
1654#line 159
1655    vfree(__cil_tmp20);
1656#line 160
1657    __cil_tmp21 = (void const   *)mtd_info;
1658#line 160
1659    kfree(__cil_tmp21);
1660#line 161
1661    mtd_info = (struct mtd_info *)0;
1662    }
1663#line 162
1664    return (err);
1665  } else {
1666
1667  }
1668  {
1669#line 164
1670  __cil_tmp22 = (unsigned long )mtd_info;
1671#line 164
1672  __cil_tmp23 = __cil_tmp22 + 360;
1673#line 164
1674  __cil_tmp24 = *((void **)__cil_tmp23);
1675#line 164
1676  __cil_tmp25 = & total_size;
1677#line 164
1678  __cil_tmp26 = *__cil_tmp25;
1679#line 164
1680  __cil_tmp27 = __cil_tmp26 * 1024UL;
1681#line 164
1682  memset(__cil_tmp24, 255, __cil_tmp27);
1683  }
1684#line 165
1685  return (err);
1686}
1687}
1688#line 191
1689extern void ldv_check_final_state(void) ;
1690#line 197
1691extern void ldv_initialize(void) ;
1692#line 200
1693extern int __VERIFIER_nondet_int(void) ;
1694#line 203 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1695int LDV_IN_INTERRUPT  ;
1696#line 206 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1697void main(void) 
1698{ int tmp ;
1699  int tmp___0 ;
1700  int tmp___1 ;
1701
1702  {
1703  {
1704#line 218
1705  LDV_IN_INTERRUPT = 1;
1706#line 227
1707  ldv_initialize();
1708#line 238
1709  tmp = init_mtdram();
1710  }
1711#line 238
1712  if (tmp != 0) {
1713#line 239
1714    goto ldv_final;
1715  } else {
1716
1717  }
1718#line 241
1719  goto ldv_15479;
1720  ldv_15478: 
1721  {
1722#line 244
1723  tmp___0 = __VERIFIER_nondet_int();
1724  }
1725  {
1726#line 246
1727  goto switch_default;
1728#line 244
1729  if (0) {
1730    switch_default: /* CIL Label */ ;
1731#line 246
1732    goto ldv_15477;
1733  } else {
1734    switch_break: /* CIL Label */ ;
1735  }
1736  }
1737  ldv_15477: ;
1738  ldv_15479: 
1739  {
1740#line 241
1741  tmp___1 = __VERIFIER_nondet_int();
1742  }
1743#line 241
1744  if (tmp___1 != 0) {
1745#line 242
1746    goto ldv_15478;
1747  } else {
1748#line 244
1749    goto ldv_15480;
1750  }
1751  ldv_15480: ;
1752  {
1753#line 263
1754  cleanup_mtdram();
1755  }
1756  ldv_final: 
1757  {
1758#line 266
1759  ldv_check_final_state();
1760  }
1761#line 269
1762  return;
1763}
1764}
1765#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1766void ldv_blast_assert(void) 
1767{ 
1768
1769  {
1770  ERROR: ;
1771#line 6
1772  goto ERROR;
1773}
1774}
1775#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1776extern int __VERIFIER_nondet_int(void) ;
1777#line 290 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1778int ldv_spin  =    0;
1779#line 294 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1780void ldv_check_alloc_flags(gfp_t flags ) 
1781{ 
1782
1783  {
1784#line 297
1785  if (ldv_spin != 0) {
1786#line 297
1787    if (flags != 32U) {
1788      {
1789#line 297
1790      ldv_blast_assert();
1791      }
1792    } else {
1793
1794    }
1795  } else {
1796
1797  }
1798#line 300
1799  return;
1800}
1801}
1802#line 300
1803extern struct page *ldv_some_page(void) ;
1804#line 303 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1805struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
1806{ struct page *tmp ;
1807
1808  {
1809#line 306
1810  if (ldv_spin != 0) {
1811#line 306
1812    if (flags != 32U) {
1813      {
1814#line 306
1815      ldv_blast_assert();
1816      }
1817    } else {
1818
1819    }
1820  } else {
1821
1822  }
1823  {
1824#line 308
1825  tmp = ldv_some_page();
1826  }
1827#line 308
1828  return (tmp);
1829}
1830}
1831#line 312 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1832void ldv_check_alloc_nonatomic(void) 
1833{ 
1834
1835  {
1836#line 315
1837  if (ldv_spin != 0) {
1838    {
1839#line 315
1840    ldv_blast_assert();
1841    }
1842  } else {
1843
1844  }
1845#line 318
1846  return;
1847}
1848}
1849#line 319 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1850void ldv_spin_lock(void) 
1851{ 
1852
1853  {
1854#line 322
1855  ldv_spin = 1;
1856#line 323
1857  return;
1858}
1859}
1860#line 326 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1861void ldv_spin_unlock(void) 
1862{ 
1863
1864  {
1865#line 329
1866  ldv_spin = 0;
1867#line 330
1868  return;
1869}
1870}
1871#line 333 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1872int ldv_spin_trylock(void) 
1873{ int is_lock ;
1874
1875  {
1876  {
1877#line 338
1878  is_lock = __VERIFIER_nondet_int();
1879  }
1880#line 340
1881  if (is_lock != 0) {
1882#line 343
1883    return (0);
1884  } else {
1885#line 348
1886    ldv_spin = 1;
1887#line 350
1888    return (1);
1889  }
1890}
1891}
1892#line 472 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1893__inline static void *kmalloc(size_t size , gfp_t flags ) 
1894{ 
1895
1896  {
1897  {
1898#line 478
1899  ldv_check_alloc_flags(flags);
1900#line 480
1901  ldv_kmalloc_12(size, flags);
1902  }
1903#line 481
1904  return ((void *)0);
1905}
1906}
1907#line 517 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1908void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
1909{ 
1910
1911  {
1912  {
1913#line 523
1914  ldv_check_alloc_flags(ldv_func_arg2);
1915#line 525
1916  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1917  }
1918#line 526
1919  return ((void *)0);
1920}
1921}
1922#line 549 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11719/dscv_tempdir/dscv/ri/43_1a/drivers/mtd/devices/mtdram.c.p"
1923void *ldv_vmalloc_19(unsigned long ldv_func_arg1 ) 
1924{ 
1925
1926  {
1927  {
1928#line 554
1929  ldv_check_alloc_nonatomic();
1930#line 556
1931  vmalloc(ldv_func_arg1);
1932  }
1933#line 557
1934  return ((void *)0);
1935}
1936}