Showing error 514

User: Jiri Slaby
Error type: Reachable Error Location
Error type description: A specified error location is reachable in some program path
File location: ldv-linux-3.4/32_1_cilled_safe_ok_nondet_linux-3.4-32_1-drivers--mtd--mtdblock_ro.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 1659
Project: SV-COMP 2013
Project version: 2.6.28
Tools: Manual Work
Entered: 2013-01-17 16:57:54 UTC


Source:

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