Showing error 1269

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--usb--otg--nop-usb-xceiv.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c
Line in file: 2339
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 23 "include/asm-generic/int-ll64.h"
   5typedef unsigned short __u16;
   6#line 26 "include/asm-generic/int-ll64.h"
   7typedef unsigned int __u32;
   8#line 30 "include/asm-generic/int-ll64.h"
   9typedef unsigned long long __u64;
  10#line 43 "include/asm-generic/int-ll64.h"
  11typedef unsigned char u8;
  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 155 "include/linux/types.h"
  47typedef u64 dma_addr_t;
  48#line 202 "include/linux/types.h"
  49typedef unsigned int gfp_t;
  50#line 206 "include/linux/types.h"
  51typedef u64 phys_addr_t;
  52#line 211 "include/linux/types.h"
  53typedef phys_addr_t resource_size_t;
  54#line 221 "include/linux/types.h"
  55struct __anonstruct_atomic_t_6 {
  56   int counter ;
  57};
  58#line 221 "include/linux/types.h"
  59typedef struct __anonstruct_atomic_t_6 atomic_t;
  60#line 226 "include/linux/types.h"
  61struct __anonstruct_atomic64_t_7 {
  62   long counter ;
  63};
  64#line 226 "include/linux/types.h"
  65typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  66#line 227 "include/linux/types.h"
  67struct list_head {
  68   struct list_head *next ;
  69   struct list_head *prev ;
  70};
  71#line 232
  72struct hlist_node;
  73#line 232 "include/linux/types.h"
  74struct hlist_head {
  75   struct hlist_node *first ;
  76};
  77#line 236 "include/linux/types.h"
  78struct hlist_node {
  79   struct hlist_node *next ;
  80   struct hlist_node **pprev ;
  81};
  82#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  83struct module;
  84#line 55
  85struct module;
  86#line 146 "include/linux/init.h"
  87typedef void (*ctor_fn_t)(void);
  88#line 46 "include/linux/dynamic_debug.h"
  89struct device;
  90#line 46
  91struct device;
  92#line 57
  93struct completion;
  94#line 57
  95struct completion;
  96#line 200 "include/linux/kernel.h"
  97struct atomic_notifier_head;
  98#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  99struct page;
 100#line 58
 101struct page;
 102#line 26 "include/asm-generic/getorder.h"
 103struct task_struct;
 104#line 26
 105struct task_struct;
 106#line 28
 107struct mm_struct;
 108#line 28
 109struct mm_struct;
 110#line 13 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 111typedef unsigned long pgdval_t;
 112#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 113typedef unsigned long pgprotval_t;
 114#line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_64_types.h"
 115struct pgprot {
 116   pgprotval_t pgprot ;
 117};
 118#line 192 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 119typedef struct pgprot pgprot_t;
 120#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 121struct __anonstruct_pgd_t_16 {
 122   pgdval_t pgd ;
 123};
 124#line 194 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 125typedef struct __anonstruct_pgd_t_16 pgd_t;
 126#line 282 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
 127typedef struct page *pgtable_t;
 128#line 290
 129struct file;
 130#line 290
 131struct file;
 132#line 339
 133struct cpumask;
 134#line 339
 135struct cpumask;
 136#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
 137struct arch_spinlock;
 138#line 327
 139struct arch_spinlock;
 140#line 306 "include/linux/bitmap.h"
 141struct bug_entry {
 142   int bug_addr_disp ;
 143   int file_disp ;
 144   unsigned short line ;
 145   unsigned short flags ;
 146};
 147#line 89 "include/linux/bug.h"
 148struct cpumask {
 149   unsigned long bits[64U] ;
 150};
 151#line 637 "include/linux/cpumask.h"
 152typedef struct cpumask *cpumask_var_t;
 153#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
 154struct static_key;
 155#line 234
 156struct static_key;
 157#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
 158struct kmem_cache;
 159#line 23 "include/asm-generic/atomic-long.h"
 160typedef atomic64_t atomic_long_t;
 161#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 162typedef u16 __ticket_t;
 163#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 164typedef u32 __ticketpair_t;
 165#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 166struct __raw_tickets {
 167   __ticket_t head ;
 168   __ticket_t tail ;
 169};
 170#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 171union __anonunion_ldv_5907_29 {
 172   __ticketpair_t head_tail ;
 173   struct __raw_tickets tickets ;
 174};
 175#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 176struct arch_spinlock {
 177   union __anonunion_ldv_5907_29 ldv_5907 ;
 178};
 179#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 180typedef struct arch_spinlock arch_spinlock_t;
 181#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 182struct lockdep_map;
 183#line 34
 184struct lockdep_map;
 185#line 55 "include/linux/debug_locks.h"
 186struct stack_trace {
 187   unsigned int nr_entries ;
 188   unsigned int max_entries ;
 189   unsigned long *entries ;
 190   int skip ;
 191};
 192#line 26 "include/linux/stacktrace.h"
 193struct lockdep_subclass_key {
 194   char __one_byte ;
 195};
 196#line 53 "include/linux/lockdep.h"
 197struct lock_class_key {
 198   struct lockdep_subclass_key subkeys[8U] ;
 199};
 200#line 59 "include/linux/lockdep.h"
 201struct lock_class {
 202   struct list_head hash_entry ;
 203   struct list_head lock_entry ;
 204   struct lockdep_subclass_key *key ;
 205   unsigned int subclass ;
 206   unsigned int dep_gen_id ;
 207   unsigned long usage_mask ;
 208   struct stack_trace usage_traces[13U] ;
 209   struct list_head locks_after ;
 210   struct list_head locks_before ;
 211   unsigned int version ;
 212   unsigned long ops ;
 213   char const   *name ;
 214   int name_version ;
 215   unsigned long contention_point[4U] ;
 216   unsigned long contending_point[4U] ;
 217};
 218#line 144 "include/linux/lockdep.h"
 219struct lockdep_map {
 220   struct lock_class_key *key ;
 221   struct lock_class *class_cache[2U] ;
 222   char const   *name ;
 223   int cpu ;
 224   unsigned long ip ;
 225};
 226#line 556 "include/linux/lockdep.h"
 227struct raw_spinlock {
 228   arch_spinlock_t raw_lock ;
 229   unsigned int magic ;
 230   unsigned int owner_cpu ;
 231   void *owner ;
 232   struct lockdep_map dep_map ;
 233};
 234#line 32 "include/linux/spinlock_types.h"
 235typedef struct raw_spinlock raw_spinlock_t;
 236#line 33 "include/linux/spinlock_types.h"
 237struct __anonstruct_ldv_6122_33 {
 238   u8 __padding[24U] ;
 239   struct lockdep_map dep_map ;
 240};
 241#line 33 "include/linux/spinlock_types.h"
 242union __anonunion_ldv_6123_32 {
 243   struct raw_spinlock rlock ;
 244   struct __anonstruct_ldv_6122_33 ldv_6122 ;
 245};
 246#line 33 "include/linux/spinlock_types.h"
 247struct spinlock {
 248   union __anonunion_ldv_6123_32 ldv_6123 ;
 249};
 250#line 76 "include/linux/spinlock_types.h"
 251typedef struct spinlock spinlock_t;
 252#line 48 "include/linux/wait.h"
 253struct __wait_queue_head {
 254   spinlock_t lock ;
 255   struct list_head task_list ;
 256};
 257#line 53 "include/linux/wait.h"
 258typedef struct __wait_queue_head wait_queue_head_t;
 259#line 98 "include/linux/nodemask.h"
 260struct __anonstruct_nodemask_t_36 {
 261   unsigned long bits[16U] ;
 262};
 263#line 98 "include/linux/nodemask.h"
 264typedef struct __anonstruct_nodemask_t_36 nodemask_t;
 265#line 670 "include/linux/mmzone.h"
 266struct mutex {
 267   atomic_t count ;
 268   spinlock_t wait_lock ;
 269   struct list_head wait_list ;
 270   struct task_struct *owner ;
 271   char const   *name ;
 272   void *magic ;
 273   struct lockdep_map dep_map ;
 274};
 275#line 171 "include/linux/mutex.h"
 276struct rw_semaphore;
 277#line 171
 278struct rw_semaphore;
 279#line 172 "include/linux/mutex.h"
 280struct rw_semaphore {
 281   long count ;
 282   raw_spinlock_t wait_lock ;
 283   struct list_head wait_list ;
 284   struct lockdep_map dep_map ;
 285};
 286#line 128 "include/linux/rwsem.h"
 287struct completion {
 288   unsigned int done ;
 289   wait_queue_head_t wait ;
 290};
 291#line 188 "include/linux/rcupdate.h"
 292struct notifier_block;
 293#line 188
 294struct notifier_block;
 295#line 239 "include/linux/srcu.h"
 296struct notifier_block {
 297   int (*notifier_call)(struct notifier_block * , unsigned long  , void * ) ;
 298   struct notifier_block *next ;
 299   int priority ;
 300};
 301#line 55 "include/linux/notifier.h"
 302struct atomic_notifier_head {
 303   spinlock_t lock ;
 304   struct notifier_block *head ;
 305};
 306#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/e820.h"
 307struct resource {
 308   resource_size_t start ;
 309   resource_size_t end ;
 310   char const   *name ;
 311   unsigned long flags ;
 312   struct resource *parent ;
 313   struct resource *sibling ;
 314   struct resource *child ;
 315};
 316#line 312 "include/linux/jiffies.h"
 317union ktime {
 318   s64 tv64 ;
 319};
 320#line 59 "include/linux/ktime.h"
 321typedef union ktime ktime_t;
 322#line 341
 323struct tvec_base;
 324#line 341
 325struct tvec_base;
 326#line 342 "include/linux/ktime.h"
 327struct timer_list {
 328   struct list_head entry ;
 329   unsigned long expires ;
 330   struct tvec_base *base ;
 331   void (*function)(unsigned long  ) ;
 332   unsigned long data ;
 333   int slack ;
 334   int start_pid ;
 335   void *start_site ;
 336   char start_comm[16U] ;
 337   struct lockdep_map lockdep_map ;
 338};
 339#line 302 "include/linux/timer.h"
 340struct work_struct;
 341#line 302
 342struct work_struct;
 343#line 45 "include/linux/workqueue.h"
 344struct work_struct {
 345   atomic_long_t data ;
 346   struct list_head entry ;
 347   void (*func)(struct work_struct * ) ;
 348   struct lockdep_map lockdep_map ;
 349};
 350#line 46 "include/linux/pm.h"
 351struct pm_message {
 352   int event ;
 353};
 354#line 52 "include/linux/pm.h"
 355typedef struct pm_message pm_message_t;
 356#line 53 "include/linux/pm.h"
 357struct dev_pm_ops {
 358   int (*prepare)(struct device * ) ;
 359   void (*complete)(struct device * ) ;
 360   int (*suspend)(struct device * ) ;
 361   int (*resume)(struct device * ) ;
 362   int (*freeze)(struct device * ) ;
 363   int (*thaw)(struct device * ) ;
 364   int (*poweroff)(struct device * ) ;
 365   int (*restore)(struct device * ) ;
 366   int (*suspend_late)(struct device * ) ;
 367   int (*resume_early)(struct device * ) ;
 368   int (*freeze_late)(struct device * ) ;
 369   int (*thaw_early)(struct device * ) ;
 370   int (*poweroff_late)(struct device * ) ;
 371   int (*restore_early)(struct device * ) ;
 372   int (*suspend_noirq)(struct device * ) ;
 373   int (*resume_noirq)(struct device * ) ;
 374   int (*freeze_noirq)(struct device * ) ;
 375   int (*thaw_noirq)(struct device * ) ;
 376   int (*poweroff_noirq)(struct device * ) ;
 377   int (*restore_noirq)(struct device * ) ;
 378   int (*runtime_suspend)(struct device * ) ;
 379   int (*runtime_resume)(struct device * ) ;
 380   int (*runtime_idle)(struct device * ) ;
 381};
 382#line 289
 383enum rpm_status {
 384    RPM_ACTIVE = 0,
 385    RPM_RESUMING = 1,
 386    RPM_SUSPENDED = 2,
 387    RPM_SUSPENDING = 3
 388} ;
 389#line 296
 390enum rpm_request {
 391    RPM_REQ_NONE = 0,
 392    RPM_REQ_IDLE = 1,
 393    RPM_REQ_SUSPEND = 2,
 394    RPM_REQ_AUTOSUSPEND = 3,
 395    RPM_REQ_RESUME = 4
 396} ;
 397#line 304
 398struct wakeup_source;
 399#line 304
 400struct wakeup_source;
 401#line 494 "include/linux/pm.h"
 402struct pm_subsys_data {
 403   spinlock_t lock ;
 404   unsigned int refcount ;
 405};
 406#line 499
 407struct dev_pm_qos_request;
 408#line 499
 409struct pm_qos_constraints;
 410#line 499 "include/linux/pm.h"
 411struct dev_pm_info {
 412   pm_message_t power_state ;
 413   unsigned char can_wakeup : 1 ;
 414   unsigned char async_suspend : 1 ;
 415   bool is_prepared ;
 416   bool is_suspended ;
 417   bool ignore_children ;
 418   spinlock_t lock ;
 419   struct list_head entry ;
 420   struct completion completion ;
 421   struct wakeup_source *wakeup ;
 422   bool wakeup_path ;
 423   struct timer_list suspend_timer ;
 424   unsigned long timer_expires ;
 425   struct work_struct work ;
 426   wait_queue_head_t wait_queue ;
 427   atomic_t usage_count ;
 428   atomic_t child_count ;
 429   unsigned char disable_depth : 3 ;
 430   unsigned char idle_notification : 1 ;
 431   unsigned char request_pending : 1 ;
 432   unsigned char deferred_resume : 1 ;
 433   unsigned char run_wake : 1 ;
 434   unsigned char runtime_auto : 1 ;
 435   unsigned char no_callbacks : 1 ;
 436   unsigned char irq_safe : 1 ;
 437   unsigned char use_autosuspend : 1 ;
 438   unsigned char timer_autosuspends : 1 ;
 439   enum rpm_request request ;
 440   enum rpm_status runtime_status ;
 441   int runtime_error ;
 442   int autosuspend_delay ;
 443   unsigned long last_busy ;
 444   unsigned long active_jiffies ;
 445   unsigned long suspended_jiffies ;
 446   unsigned long accounting_timestamp ;
 447   ktime_t suspend_time ;
 448   s64 max_time_suspended_ns ;
 449   struct dev_pm_qos_request *pq_req ;
 450   struct pm_subsys_data *subsys_data ;
 451   struct pm_qos_constraints *constraints ;
 452};
 453#line 558 "include/linux/pm.h"
 454struct dev_pm_domain {
 455   struct dev_pm_ops ops ;
 456};
 457#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 458struct __anonstruct_mm_context_t_101 {
 459   void *ldt ;
 460   int size ;
 461   unsigned short ia32_compat ;
 462   struct mutex lock ;
 463   void *vdso ;
 464};
 465#line 22 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mmu.h"
 466typedef struct __anonstruct_mm_context_t_101 mm_context_t;
 467#line 18 "include/asm-generic/pci_iomap.h"
 468struct vm_area_struct;
 469#line 18
 470struct vm_area_struct;
 471#line 835 "include/linux/sysctl.h"
 472struct rb_node {
 473   unsigned long rb_parent_color ;
 474   struct rb_node *rb_right ;
 475   struct rb_node *rb_left ;
 476};
 477#line 108 "include/linux/rbtree.h"
 478struct rb_root {
 479   struct rb_node *rb_node ;
 480};
 481#line 18 "include/linux/elf.h"
 482typedef __u64 Elf64_Addr;
 483#line 19 "include/linux/elf.h"
 484typedef __u16 Elf64_Half;
 485#line 23 "include/linux/elf.h"
 486typedef __u32 Elf64_Word;
 487#line 24 "include/linux/elf.h"
 488typedef __u64 Elf64_Xword;
 489#line 193 "include/linux/elf.h"
 490struct elf64_sym {
 491   Elf64_Word st_name ;
 492   unsigned char st_info ;
 493   unsigned char st_other ;
 494   Elf64_Half st_shndx ;
 495   Elf64_Addr st_value ;
 496   Elf64_Xword st_size ;
 497};
 498#line 201 "include/linux/elf.h"
 499typedef struct elf64_sym Elf64_Sym;
 500#line 445
 501struct sock;
 502#line 445
 503struct sock;
 504#line 446
 505struct kobject;
 506#line 446
 507struct kobject;
 508#line 447
 509enum kobj_ns_type {
 510    KOBJ_NS_TYPE_NONE = 0,
 511    KOBJ_NS_TYPE_NET = 1,
 512    KOBJ_NS_TYPES = 2
 513} ;
 514#line 453 "include/linux/elf.h"
 515struct kobj_ns_type_operations {
 516   enum kobj_ns_type type ;
 517   void *(*grab_current_ns)(void) ;
 518   void const   *(*netlink_ns)(struct sock * ) ;
 519   void const   *(*initial_ns)(void) ;
 520   void (*drop_ns)(void * ) ;
 521};
 522#line 57 "include/linux/kobject_ns.h"
 523struct attribute {
 524   char const   *name ;
 525   umode_t mode ;
 526   struct lock_class_key *key ;
 527   struct lock_class_key skey ;
 528};
 529#line 33 "include/linux/sysfs.h"
 530struct attribute_group {
 531   char const   *name ;
 532   umode_t (*is_visible)(struct kobject * , struct attribute * , int  ) ;
 533   struct attribute **attrs ;
 534};
 535#line 62 "include/linux/sysfs.h"
 536struct bin_attribute {
 537   struct attribute attr ;
 538   size_t size ;
 539   void *private ;
 540   ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 541                   loff_t  , size_t  ) ;
 542   ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
 543                    loff_t  , size_t  ) ;
 544   int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
 545};
 546#line 98 "include/linux/sysfs.h"
 547struct sysfs_ops {
 548   ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
 549   ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
 550   void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 551};
 552#line 117
 553struct sysfs_dirent;
 554#line 117
 555struct sysfs_dirent;
 556#line 182 "include/linux/sysfs.h"
 557struct kref {
 558   atomic_t refcount ;
 559};
 560#line 49 "include/linux/kobject.h"
 561struct kset;
 562#line 49
 563struct kobj_type;
 564#line 49 "include/linux/kobject.h"
 565struct kobject {
 566   char const   *name ;
 567   struct list_head entry ;
 568   struct kobject *parent ;
 569   struct kset *kset ;
 570   struct kobj_type *ktype ;
 571   struct sysfs_dirent *sd ;
 572   struct kref kref ;
 573   unsigned char state_initialized : 1 ;
 574   unsigned char state_in_sysfs : 1 ;
 575   unsigned char state_add_uevent_sent : 1 ;
 576   unsigned char state_remove_uevent_sent : 1 ;
 577   unsigned char uevent_suppress : 1 ;
 578};
 579#line 107 "include/linux/kobject.h"
 580struct kobj_type {
 581   void (*release)(struct kobject * ) ;
 582   struct sysfs_ops  const  *sysfs_ops ;
 583   struct attribute **default_attrs ;
 584   struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
 585   void const   *(*namespace)(struct kobject * ) ;
 586};
 587#line 115 "include/linux/kobject.h"
 588struct kobj_uevent_env {
 589   char *envp[32U] ;
 590   int envp_idx ;
 591   char buf[2048U] ;
 592   int buflen ;
 593};
 594#line 122 "include/linux/kobject.h"
 595struct kset_uevent_ops {
 596   int (* const  filter)(struct kset * , struct kobject * ) ;
 597   char const   *(* const  name)(struct kset * , struct kobject * ) ;
 598   int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 599};
 600#line 139 "include/linux/kobject.h"
 601struct kset {
 602   struct list_head list ;
 603   spinlock_t list_lock ;
 604   struct kobject kobj ;
 605   struct kset_uevent_ops  const  *uevent_ops ;
 606};
 607#line 215
 608struct kernel_param;
 609#line 215
 610struct kernel_param;
 611#line 216 "include/linux/kobject.h"
 612struct kernel_param_ops {
 613   int (*set)(char const   * , struct kernel_param  const  * ) ;
 614   int (*get)(char * , struct kernel_param  const  * ) ;
 615   void (*free)(void * ) ;
 616};
 617#line 49 "include/linux/moduleparam.h"
 618struct kparam_string;
 619#line 49
 620struct kparam_array;
 621#line 49 "include/linux/moduleparam.h"
 622union __anonunion_ldv_13363_134 {
 623   void *arg ;
 624   struct kparam_string  const  *str ;
 625   struct kparam_array  const  *arr ;
 626};
 627#line 49 "include/linux/moduleparam.h"
 628struct kernel_param {
 629   char const   *name ;
 630   struct kernel_param_ops  const  *ops ;
 631   u16 perm ;
 632   s16 level ;
 633   union __anonunion_ldv_13363_134 ldv_13363 ;
 634};
 635#line 61 "include/linux/moduleparam.h"
 636struct kparam_string {
 637   unsigned int maxlen ;
 638   char *string ;
 639};
 640#line 67 "include/linux/moduleparam.h"
 641struct kparam_array {
 642   unsigned int max ;
 643   unsigned int elemsize ;
 644   unsigned int *num ;
 645   struct kernel_param_ops  const  *ops ;
 646   void *elem ;
 647};
 648#line 458 "include/linux/moduleparam.h"
 649struct static_key {
 650   atomic_t enabled ;
 651};
 652#line 225 "include/linux/jump_label.h"
 653struct tracepoint;
 654#line 225
 655struct tracepoint;
 656#line 226 "include/linux/jump_label.h"
 657struct tracepoint_func {
 658   void *func ;
 659   void *data ;
 660};
 661#line 29 "include/linux/tracepoint.h"
 662struct tracepoint {
 663   char const   *name ;
 664   struct static_key key ;
 665   void (*regfunc)(void) ;
 666   void (*unregfunc)(void) ;
 667   struct tracepoint_func *funcs ;
 668};
 669#line 86 "include/linux/tracepoint.h"
 670struct kernel_symbol {
 671   unsigned long value ;
 672   char const   *name ;
 673};
 674#line 27 "include/linux/export.h"
 675struct mod_arch_specific {
 676
 677};
 678#line 34 "include/linux/module.h"
 679struct module_param_attrs;
 680#line 34 "include/linux/module.h"
 681struct module_kobject {
 682   struct kobject kobj ;
 683   struct module *mod ;
 684   struct kobject *drivers_dir ;
 685   struct module_param_attrs *mp ;
 686};
 687#line 43 "include/linux/module.h"
 688struct module_attribute {
 689   struct attribute attr ;
 690   ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
 691   ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
 692                    size_t  ) ;
 693   void (*setup)(struct module * , char const   * ) ;
 694   int (*test)(struct module * ) ;
 695   void (*free)(struct module * ) ;
 696};
 697#line 69
 698struct exception_table_entry;
 699#line 69
 700struct exception_table_entry;
 701#line 198
 702enum module_state {
 703    MODULE_STATE_LIVE = 0,
 704    MODULE_STATE_COMING = 1,
 705    MODULE_STATE_GOING = 2
 706} ;
 707#line 204 "include/linux/module.h"
 708struct module_ref {
 709   unsigned long incs ;
 710   unsigned long decs ;
 711};
 712#line 219
 713struct module_sect_attrs;
 714#line 219
 715struct module_notes_attrs;
 716#line 219
 717struct ftrace_event_call;
 718#line 219 "include/linux/module.h"
 719struct module {
 720   enum module_state state ;
 721   struct list_head list ;
 722   char name[56U] ;
 723   struct module_kobject mkobj ;
 724   struct module_attribute *modinfo_attrs ;
 725   char const   *version ;
 726   char const   *srcversion ;
 727   struct kobject *holders_dir ;
 728   struct kernel_symbol  const  *syms ;
 729   unsigned long const   *crcs ;
 730   unsigned int num_syms ;
 731   struct kernel_param *kp ;
 732   unsigned int num_kp ;
 733   unsigned int num_gpl_syms ;
 734   struct kernel_symbol  const  *gpl_syms ;
 735   unsigned long const   *gpl_crcs ;
 736   struct kernel_symbol  const  *unused_syms ;
 737   unsigned long const   *unused_crcs ;
 738   unsigned int num_unused_syms ;
 739   unsigned int num_unused_gpl_syms ;
 740   struct kernel_symbol  const  *unused_gpl_syms ;
 741   unsigned long const   *unused_gpl_crcs ;
 742   struct kernel_symbol  const  *gpl_future_syms ;
 743   unsigned long const   *gpl_future_crcs ;
 744   unsigned int num_gpl_future_syms ;
 745   unsigned int num_exentries ;
 746   struct exception_table_entry *extable ;
 747   int (*init)(void) ;
 748   void *module_init ;
 749   void *module_core ;
 750   unsigned int init_size ;
 751   unsigned int core_size ;
 752   unsigned int init_text_size ;
 753   unsigned int core_text_size ;
 754   unsigned int init_ro_size ;
 755   unsigned int core_ro_size ;
 756   struct mod_arch_specific arch ;
 757   unsigned int taints ;
 758   unsigned int num_bugs ;
 759   struct list_head bug_list ;
 760   struct bug_entry *bug_table ;
 761   Elf64_Sym *symtab ;
 762   Elf64_Sym *core_symtab ;
 763   unsigned int num_symtab ;
 764   unsigned int core_num_syms ;
 765   char *strtab ;
 766   char *core_strtab ;
 767   struct module_sect_attrs *sect_attrs ;
 768   struct module_notes_attrs *notes_attrs ;
 769   char *args ;
 770   void *percpu ;
 771   unsigned int percpu_size ;
 772   unsigned int num_tracepoints ;
 773   struct tracepoint * const  *tracepoints_ptrs ;
 774   unsigned int num_trace_bprintk_fmt ;
 775   char const   **trace_bprintk_fmt_start ;
 776   struct ftrace_event_call **trace_events ;
 777   unsigned int num_trace_events ;
 778   struct list_head source_list ;
 779   struct list_head target_list ;
 780   struct task_struct *waiter ;
 781   void (*exit)(void) ;
 782   struct module_ref *refptr ;
 783   ctor_fn_t (**ctors)(void) ;
 784   unsigned int num_ctors ;
 785};
 786#line 88 "include/linux/kmemleak.h"
 787struct kmem_cache_cpu {
 788   void **freelist ;
 789   unsigned long tid ;
 790   struct page *page ;
 791   struct page *partial ;
 792   int node ;
 793   unsigned int stat[26U] ;
 794};
 795#line 55 "include/linux/slub_def.h"
 796struct kmem_cache_node {
 797   spinlock_t list_lock ;
 798   unsigned long nr_partial ;
 799   struct list_head partial ;
 800   atomic_long_t nr_slabs ;
 801   atomic_long_t total_objects ;
 802   struct list_head full ;
 803};
 804#line 66 "include/linux/slub_def.h"
 805struct kmem_cache_order_objects {
 806   unsigned long x ;
 807};
 808#line 76 "include/linux/slub_def.h"
 809struct kmem_cache {
 810   struct kmem_cache_cpu *cpu_slab ;
 811   unsigned long flags ;
 812   unsigned long min_partial ;
 813   int size ;
 814   int objsize ;
 815   int offset ;
 816   int cpu_partial ;
 817   struct kmem_cache_order_objects oo ;
 818   struct kmem_cache_order_objects max ;
 819   struct kmem_cache_order_objects min ;
 820   gfp_t allocflags ;
 821   int refcount ;
 822   void (*ctor)(void * ) ;
 823   int inuse ;
 824   int align ;
 825   int reserved ;
 826   char const   *name ;
 827   struct list_head list ;
 828   struct kobject kobj ;
 829   int remote_node_defrag_ratio ;
 830   struct kmem_cache_node *node[1024U] ;
 831};
 832#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
 833struct klist_node;
 834#line 15
 835struct klist_node;
 836#line 37 "include/linux/klist.h"
 837struct klist_node {
 838   void *n_klist ;
 839   struct list_head n_node ;
 840   struct kref n_ref ;
 841};
 842#line 67
 843struct dma_map_ops;
 844#line 67 "include/linux/klist.h"
 845struct dev_archdata {
 846   void *acpi_handle ;
 847   struct dma_map_ops *dma_ops ;
 848   void *iommu ;
 849};
 850#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 851struct pdev_archdata {
 852
 853};
 854#line 17
 855struct device_private;
 856#line 17
 857struct device_private;
 858#line 18
 859struct device_driver;
 860#line 18
 861struct device_driver;
 862#line 19
 863struct driver_private;
 864#line 19
 865struct driver_private;
 866#line 20
 867struct class;
 868#line 20
 869struct class;
 870#line 21
 871struct subsys_private;
 872#line 21
 873struct subsys_private;
 874#line 22
 875struct bus_type;
 876#line 22
 877struct bus_type;
 878#line 23
 879struct device_node;
 880#line 23
 881struct device_node;
 882#line 24
 883struct iommu_ops;
 884#line 24
 885struct iommu_ops;
 886#line 25 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/device.h"
 887struct bus_attribute {
 888   struct attribute attr ;
 889   ssize_t (*show)(struct bus_type * , char * ) ;
 890   ssize_t (*store)(struct bus_type * , char const   * , size_t  ) ;
 891};
 892#line 51 "include/linux/device.h"
 893struct device_attribute;
 894#line 51
 895struct driver_attribute;
 896#line 51 "include/linux/device.h"
 897struct bus_type {
 898   char const   *name ;
 899   char const   *dev_name ;
 900   struct device *dev_root ;
 901   struct bus_attribute *bus_attrs ;
 902   struct device_attribute *dev_attrs ;
 903   struct driver_attribute *drv_attrs ;
 904   int (*match)(struct device * , struct device_driver * ) ;
 905   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 906   int (*probe)(struct device * ) ;
 907   int (*remove)(struct device * ) ;
 908   void (*shutdown)(struct device * ) ;
 909   int (*suspend)(struct device * , pm_message_t  ) ;
 910   int (*resume)(struct device * ) ;
 911   struct dev_pm_ops  const  *pm ;
 912   struct iommu_ops *iommu_ops ;
 913   struct subsys_private *p ;
 914};
 915#line 125
 916struct device_type;
 917#line 182
 918struct of_device_id;
 919#line 182 "include/linux/device.h"
 920struct device_driver {
 921   char const   *name ;
 922   struct bus_type *bus ;
 923   struct module *owner ;
 924   char const   *mod_name ;
 925   bool suppress_bind_attrs ;
 926   struct of_device_id  const  *of_match_table ;
 927   int (*probe)(struct device * ) ;
 928   int (*remove)(struct device * ) ;
 929   void (*shutdown)(struct device * ) ;
 930   int (*suspend)(struct device * , pm_message_t  ) ;
 931   int (*resume)(struct device * ) ;
 932   struct attribute_group  const  **groups ;
 933   struct dev_pm_ops  const  *pm ;
 934   struct driver_private *p ;
 935};
 936#line 245 "include/linux/device.h"
 937struct driver_attribute {
 938   struct attribute attr ;
 939   ssize_t (*show)(struct device_driver * , char * ) ;
 940   ssize_t (*store)(struct device_driver * , char const   * , size_t  ) ;
 941};
 942#line 299
 943struct class_attribute;
 944#line 299 "include/linux/device.h"
 945struct class {
 946   char const   *name ;
 947   struct module *owner ;
 948   struct class_attribute *class_attrs ;
 949   struct device_attribute *dev_attrs ;
 950   struct bin_attribute *dev_bin_attrs ;
 951   struct kobject *dev_kobj ;
 952   int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
 953   char *(*devnode)(struct device * , umode_t * ) ;
 954   void (*class_release)(struct class * ) ;
 955   void (*dev_release)(struct device * ) ;
 956   int (*suspend)(struct device * , pm_message_t  ) ;
 957   int (*resume)(struct device * ) ;
 958   struct kobj_ns_type_operations  const  *ns_type ;
 959   void const   *(*namespace)(struct device * ) ;
 960   struct dev_pm_ops  const  *pm ;
 961   struct subsys_private *p ;
 962};
 963#line 394 "include/linux/device.h"
 964struct class_attribute {
 965   struct attribute attr ;
 966   ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
 967   ssize_t (*store)(struct class * , struct class_attribute * , char const   * , size_t  ) ;
 968   void const   *(*namespace)(struct class * , struct class_attribute  const  * ) ;
 969};
 970#line 447 "include/linux/device.h"
 971struct device_type {
 972   char const   *name ;
 973   struct attribute_group  const  **groups ;
 974   int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
 975   char *(*devnode)(struct device * , umode_t * ) ;
 976   void (*release)(struct device * ) ;
 977   struct dev_pm_ops  const  *pm ;
 978};
 979#line 474 "include/linux/device.h"
 980struct device_attribute {
 981   struct attribute attr ;
 982   ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
 983   ssize_t (*store)(struct device * , struct device_attribute * , char const   * ,
 984                    size_t  ) ;
 985};
 986#line 557 "include/linux/device.h"
 987struct device_dma_parameters {
 988   unsigned int max_segment_size ;
 989   unsigned long segment_boundary_mask ;
 990};
 991#line 567
 992struct dma_coherent_mem;
 993#line 567 "include/linux/device.h"
 994struct device {
 995   struct device *parent ;
 996   struct device_private *p ;
 997   struct kobject kobj ;
 998   char const   *init_name ;
 999   struct device_type  const  *type ;
1000   struct mutex mutex ;
1001   struct bus_type *bus ;
1002   struct device_driver *driver ;
1003   void *platform_data ;
1004   struct dev_pm_info power ;
1005   struct dev_pm_domain *pm_domain ;
1006   int numa_node ;
1007   u64 *dma_mask ;
1008   u64 coherent_dma_mask ;
1009   struct device_dma_parameters *dma_parms ;
1010   struct list_head dma_pools ;
1011   struct dma_coherent_mem *dma_mem ;
1012   struct dev_archdata archdata ;
1013   struct device_node *of_node ;
1014   dev_t devt ;
1015   u32 id ;
1016   spinlock_t devres_lock ;
1017   struct list_head devres_head ;
1018   struct klist_node knode_class ;
1019   struct class *class ;
1020   struct attribute_group  const  **groups ;
1021   void (*release)(struct device * ) ;
1022};
1023#line 681 "include/linux/device.h"
1024struct wakeup_source {
1025   char const   *name ;
1026   struct list_head entry ;
1027   spinlock_t lock ;
1028   struct timer_list timer ;
1029   unsigned long timer_expires ;
1030   ktime_t total_time ;
1031   ktime_t max_time ;
1032   ktime_t last_time ;
1033   unsigned long event_count ;
1034   unsigned long active_count ;
1035   unsigned long relax_count ;
1036   unsigned long hit_count ;
1037   unsigned char active : 1 ;
1038};
1039#line 12 "include/linux/mod_devicetable.h"
1040typedef unsigned long kernel_ulong_t;
1041#line 215 "include/linux/mod_devicetable.h"
1042struct of_device_id {
1043   char name[32U] ;
1044   char type[32U] ;
1045   char compatible[128U] ;
1046   void *data ;
1047};
1048#line 492 "include/linux/mod_devicetable.h"
1049struct platform_device_id {
1050   char name[20U] ;
1051   kernel_ulong_t driver_data ;
1052};
1053#line 584
1054struct mfd_cell;
1055#line 584
1056struct mfd_cell;
1057#line 585 "include/linux/mod_devicetable.h"
1058struct platform_device {
1059   char const   *name ;
1060   int id ;
1061   struct device dev ;
1062   u32 num_resources ;
1063   struct resource *resource ;
1064   struct platform_device_id  const  *id_entry ;
1065   struct mfd_cell *mfd_cell ;
1066   struct pdev_archdata archdata ;
1067};
1068#line 51 "include/linux/platform_device.h"
1069struct platform_device_info {
1070   struct device *parent ;
1071   char const   *name ;
1072   int id ;
1073   struct resource  const  *res ;
1074   unsigned int num_res ;
1075   void const   *data ;
1076   size_t size_data ;
1077   u64 dma_mask ;
1078};
1079#line 163 "include/linux/platform_device.h"
1080struct platform_driver {
1081   int (*probe)(struct platform_device * ) ;
1082   int (*remove)(struct platform_device * ) ;
1083   void (*shutdown)(struct platform_device * ) ;
1084   int (*suspend)(struct platform_device * , pm_message_t  ) ;
1085   int (*resume)(struct platform_device * ) ;
1086   struct device_driver driver ;
1087   struct platform_device_id  const  *id_table ;
1088};
1089#line 280 "include/linux/platform_device.h"
1090struct dma_attrs {
1091   unsigned long flags[1U] ;
1092};
1093#line 67 "include/linux/dma-attrs.h"
1094enum dma_data_direction {
1095    DMA_BIDIRECTIONAL = 0,
1096    DMA_TO_DEVICE = 1,
1097    DMA_FROM_DEVICE = 2,
1098    DMA_NONE = 3
1099} ;
1100#line 74
1101struct prio_tree_node;
1102#line 74 "include/linux/dma-attrs.h"
1103struct raw_prio_tree_node {
1104   struct prio_tree_node *left ;
1105   struct prio_tree_node *right ;
1106   struct prio_tree_node *parent ;
1107};
1108#line 19 "include/linux/prio_tree.h"
1109struct prio_tree_node {
1110   struct prio_tree_node *left ;
1111   struct prio_tree_node *right ;
1112   struct prio_tree_node *parent ;
1113   unsigned long start ;
1114   unsigned long last ;
1115};
1116#line 116
1117struct address_space;
1118#line 116
1119struct address_space;
1120#line 117 "include/linux/prio_tree.h"
1121union __anonunion_ldv_15355_137 {
1122   unsigned long index ;
1123   void *freelist ;
1124};
1125#line 117 "include/linux/prio_tree.h"
1126struct __anonstruct_ldv_15365_141 {
1127   unsigned short inuse ;
1128   unsigned short objects : 15 ;
1129   unsigned char frozen : 1 ;
1130};
1131#line 117 "include/linux/prio_tree.h"
1132union __anonunion_ldv_15366_140 {
1133   atomic_t _mapcount ;
1134   struct __anonstruct_ldv_15365_141 ldv_15365 ;
1135};
1136#line 117 "include/linux/prio_tree.h"
1137struct __anonstruct_ldv_15368_139 {
1138   union __anonunion_ldv_15366_140 ldv_15366 ;
1139   atomic_t _count ;
1140};
1141#line 117 "include/linux/prio_tree.h"
1142union __anonunion_ldv_15369_138 {
1143   unsigned long counters ;
1144   struct __anonstruct_ldv_15368_139 ldv_15368 ;
1145};
1146#line 117 "include/linux/prio_tree.h"
1147struct __anonstruct_ldv_15370_136 {
1148   union __anonunion_ldv_15355_137 ldv_15355 ;
1149   union __anonunion_ldv_15369_138 ldv_15369 ;
1150};
1151#line 117 "include/linux/prio_tree.h"
1152struct __anonstruct_ldv_15377_143 {
1153   struct page *next ;
1154   int pages ;
1155   int pobjects ;
1156};
1157#line 117 "include/linux/prio_tree.h"
1158union __anonunion_ldv_15378_142 {
1159   struct list_head lru ;
1160   struct __anonstruct_ldv_15377_143 ldv_15377 ;
1161};
1162#line 117 "include/linux/prio_tree.h"
1163union __anonunion_ldv_15383_144 {
1164   unsigned long private ;
1165   struct kmem_cache *slab ;
1166   struct page *first_page ;
1167};
1168#line 117 "include/linux/prio_tree.h"
1169struct page {
1170   unsigned long flags ;
1171   struct address_space *mapping ;
1172   struct __anonstruct_ldv_15370_136 ldv_15370 ;
1173   union __anonunion_ldv_15378_142 ldv_15378 ;
1174   union __anonunion_ldv_15383_144 ldv_15383 ;
1175   unsigned long debug_flags ;
1176};
1177#line 192 "include/linux/mm_types.h"
1178struct __anonstruct_vm_set_146 {
1179   struct list_head list ;
1180   void *parent ;
1181   struct vm_area_struct *head ;
1182};
1183#line 192 "include/linux/mm_types.h"
1184union __anonunion_shared_145 {
1185   struct __anonstruct_vm_set_146 vm_set ;
1186   struct raw_prio_tree_node prio_tree_node ;
1187};
1188#line 192
1189struct anon_vma;
1190#line 192
1191struct vm_operations_struct;
1192#line 192
1193struct mempolicy;
1194#line 192 "include/linux/mm_types.h"
1195struct vm_area_struct {
1196   struct mm_struct *vm_mm ;
1197   unsigned long vm_start ;
1198   unsigned long vm_end ;
1199   struct vm_area_struct *vm_next ;
1200   struct vm_area_struct *vm_prev ;
1201   pgprot_t vm_page_prot ;
1202   unsigned long vm_flags ;
1203   struct rb_node vm_rb ;
1204   union __anonunion_shared_145 shared ;
1205   struct list_head anon_vma_chain ;
1206   struct anon_vma *anon_vma ;
1207   struct vm_operations_struct  const  *vm_ops ;
1208   unsigned long vm_pgoff ;
1209   struct file *vm_file ;
1210   void *vm_private_data ;
1211   struct mempolicy *vm_policy ;
1212};
1213#line 255 "include/linux/mm_types.h"
1214struct core_thread {
1215   struct task_struct *task ;
1216   struct core_thread *next ;
1217};
1218#line 261 "include/linux/mm_types.h"
1219struct core_state {
1220   atomic_t nr_threads ;
1221   struct core_thread dumper ;
1222   struct completion startup ;
1223};
1224#line 274 "include/linux/mm_types.h"
1225struct mm_rss_stat {
1226   atomic_long_t count[3U] ;
1227};
1228#line 287
1229struct linux_binfmt;
1230#line 287
1231struct mmu_notifier_mm;
1232#line 287 "include/linux/mm_types.h"
1233struct mm_struct {
1234   struct vm_area_struct *mmap ;
1235   struct rb_root mm_rb ;
1236   struct vm_area_struct *mmap_cache ;
1237   unsigned long (*get_unmapped_area)(struct file * , unsigned long  , unsigned long  ,
1238                                      unsigned long  , unsigned long  ) ;
1239   void (*unmap_area)(struct mm_struct * , unsigned long  ) ;
1240   unsigned long mmap_base ;
1241   unsigned long task_size ;
1242   unsigned long cached_hole_size ;
1243   unsigned long free_area_cache ;
1244   pgd_t *pgd ;
1245   atomic_t mm_users ;
1246   atomic_t mm_count ;
1247   int map_count ;
1248   spinlock_t page_table_lock ;
1249   struct rw_semaphore mmap_sem ;
1250   struct list_head mmlist ;
1251   unsigned long hiwater_rss ;
1252   unsigned long hiwater_vm ;
1253   unsigned long total_vm ;
1254   unsigned long locked_vm ;
1255   unsigned long pinned_vm ;
1256   unsigned long shared_vm ;
1257   unsigned long exec_vm ;
1258   unsigned long stack_vm ;
1259   unsigned long reserved_vm ;
1260   unsigned long def_flags ;
1261   unsigned long nr_ptes ;
1262   unsigned long start_code ;
1263   unsigned long end_code ;
1264   unsigned long start_data ;
1265   unsigned long end_data ;
1266   unsigned long start_brk ;
1267   unsigned long brk ;
1268   unsigned long start_stack ;
1269   unsigned long arg_start ;
1270   unsigned long arg_end ;
1271   unsigned long env_start ;
1272   unsigned long env_end ;
1273   unsigned long saved_auxv[44U] ;
1274   struct mm_rss_stat rss_stat ;
1275   struct linux_binfmt *binfmt ;
1276   cpumask_var_t cpu_vm_mask_var ;
1277   mm_context_t context ;
1278   unsigned int faultstamp ;
1279   unsigned int token_priority ;
1280   unsigned int last_interval ;
1281   unsigned long flags ;
1282   struct core_state *core_state ;
1283   spinlock_t ioctx_lock ;
1284   struct hlist_head ioctx_list ;
1285   struct task_struct *owner ;
1286   struct file *exe_file ;
1287   unsigned long num_exe_file_vmas ;
1288   struct mmu_notifier_mm *mmu_notifier_mm ;
1289   pgtable_t pmd_huge_pte ;
1290   struct cpumask cpumask_allocation ;
1291};
1292#line 178 "include/linux/mm.h"
1293struct vm_fault {
1294   unsigned int flags ;
1295   unsigned long pgoff ;
1296   void *virtual_address ;
1297   struct page *page ;
1298};
1299#line 195 "include/linux/mm.h"
1300struct vm_operations_struct {
1301   void (*open)(struct vm_area_struct * ) ;
1302   void (*close)(struct vm_area_struct * ) ;
1303   int (*fault)(struct vm_area_struct * , struct vm_fault * ) ;
1304   int (*page_mkwrite)(struct vm_area_struct * , struct vm_fault * ) ;
1305   int (*access)(struct vm_area_struct * , unsigned long  , void * , int  , int  ) ;
1306   int (*set_policy)(struct vm_area_struct * , struct mempolicy * ) ;
1307   struct mempolicy *(*get_policy)(struct vm_area_struct * , unsigned long  ) ;
1308   int (*migrate)(struct vm_area_struct * , nodemask_t const   * , nodemask_t const   * ,
1309                  unsigned long  ) ;
1310};
1311#line 1631 "include/linux/mm.h"
1312struct scatterlist {
1313   unsigned long sg_magic ;
1314   unsigned long page_link ;
1315   unsigned int offset ;
1316   unsigned int length ;
1317   dma_addr_t dma_address ;
1318   unsigned int dma_length ;
1319};
1320#line 268 "include/linux/scatterlist.h"
1321struct dma_map_ops {
1322   void *(*alloc)(struct device * , size_t  , dma_addr_t * , gfp_t  , struct dma_attrs * ) ;
1323   void (*free)(struct device * , size_t  , void * , dma_addr_t  , struct dma_attrs * ) ;
1324   int (*mmap)(struct device * , struct vm_area_struct * , void * , dma_addr_t  ,
1325               size_t  , struct dma_attrs * ) ;
1326   dma_addr_t (*map_page)(struct device * , struct page * , unsigned long  , size_t  ,
1327                          enum dma_data_direction  , struct dma_attrs * ) ;
1328   void (*unmap_page)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ,
1329                      struct dma_attrs * ) ;
1330   int (*map_sg)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ,
1331                 struct dma_attrs * ) ;
1332   void (*unmap_sg)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ,
1333                    struct dma_attrs * ) ;
1334   void (*sync_single_for_cpu)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ) ;
1335   void (*sync_single_for_device)(struct device * , dma_addr_t  , size_t  , enum dma_data_direction  ) ;
1336   void (*sync_sg_for_cpu)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ) ;
1337   void (*sync_sg_for_device)(struct device * , struct scatterlist * , int  , enum dma_data_direction  ) ;
1338   int (*mapping_error)(struct device * , dma_addr_t  ) ;
1339   int (*dma_supported)(struct device * , u64  ) ;
1340   int (*set_dma_mask)(struct device * , u64  ) ;
1341   int is_phys ;
1342};
1343#line 202 "include/linux/dma-mapping.h"
1344enum usb_otg_state {
1345    OTG_STATE_UNDEFINED = 0,
1346    OTG_STATE_B_IDLE = 1,
1347    OTG_STATE_B_SRP_INIT = 2,
1348    OTG_STATE_B_PERIPHERAL = 3,
1349    OTG_STATE_B_WAIT_ACON = 4,
1350    OTG_STATE_B_HOST = 5,
1351    OTG_STATE_A_IDLE = 6,
1352    OTG_STATE_A_WAIT_VRISE = 7,
1353    OTG_STATE_A_WAIT_BCON = 8,
1354    OTG_STATE_A_HOST = 9,
1355    OTG_STATE_A_SUSPEND = 10,
1356    OTG_STATE_A_PERIPHERAL = 11,
1357    OTG_STATE_A_WAIT_VFALL = 12,
1358    OTG_STATE_A_VBUS_ERR = 13
1359} ;
1360#line 219
1361enum usb_phy_events {
1362    USB_EVENT_NONE = 0,
1363    USB_EVENT_VBUS = 1,
1364    USB_EVENT_ID = 2,
1365    USB_EVENT_CHARGER = 3,
1366    USB_EVENT_ENUMERATED = 4
1367} ;
1368#line 227
1369struct usb_phy;
1370#line 227
1371struct usb_phy;
1372#line 228 "include/linux/dma-mapping.h"
1373struct usb_phy_io_ops {
1374   int (*read)(struct usb_phy * , u32  ) ;
1375   int (*write)(struct usb_phy * , u32  , u32  ) ;
1376};
1377#line 55 "include/linux/usb/otg.h"
1378struct usb_bus;
1379#line 55
1380struct usb_gadget;
1381#line 55 "include/linux/usb/otg.h"
1382struct usb_otg {
1383   u8 default_a ;
1384   struct usb_phy *phy ;
1385   struct usb_bus *host ;
1386   struct usb_gadget *gadget ;
1387   int (*set_host)(struct usb_otg * , struct usb_bus * ) ;
1388   int (*set_peripheral)(struct usb_otg * , struct usb_gadget * ) ;
1389   int (*set_vbus)(struct usb_otg * , bool  ) ;
1390   int (*start_srp)(struct usb_otg * ) ;
1391   int (*start_hnp)(struct usb_otg * ) ;
1392};
1393#line 79 "include/linux/usb/otg.h"
1394struct usb_phy {
1395   struct device *dev ;
1396   char const   *label ;
1397   unsigned int flags ;
1398   enum usb_otg_state state ;
1399   enum usb_phy_events last_event ;
1400   struct usb_otg *otg ;
1401   struct device *io_dev ;
1402   struct usb_phy_io_ops *io_ops ;
1403   void *io_priv ;
1404   struct atomic_notifier_head notifier ;
1405   u16 port_status ;
1406   u16 port_change ;
1407   int (*init)(struct usb_phy * ) ;
1408   void (*shutdown)(struct usb_phy * ) ;
1409   int (*set_power)(struct usb_phy * , unsigned int  ) ;
1410   int (*set_suspend)(struct usb_phy * , int  ) ;
1411};
1412#line 278 "include/linux/usb/otg.h"
1413struct nop_usb_xceiv {
1414   struct usb_phy phy ;
1415   struct device *dev ;
1416};
1417#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1418void ldv_spin_lock(void) ;
1419#line 3
1420void ldv_spin_unlock(void) ;
1421#line 4
1422int ldv_spin_trylock(void) ;
1423#line 101 "include/linux/printk.h"
1424extern int printk(char const   *  , ...) ;
1425#line 93 "include/linux/spinlock.h"
1426extern void __raw_spin_lock_init(raw_spinlock_t * , char const   * , struct lock_class_key * ) ;
1427#line 272 "include/linux/spinlock.h"
1428__inline static raw_spinlock_t *spinlock_check(spinlock_t *lock ) 
1429{ 
1430
1431  {
1432#line 274
1433  return ((struct raw_spinlock *)lock);
1434}
1435}
1436#line 26 "include/linux/export.h"
1437extern struct module __this_module ;
1438#line 161 "include/linux/slab.h"
1439extern void kfree(void const   * ) ;
1440#line 220 "include/linux/slub_def.h"
1441extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
1442#line 223
1443void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
1444#line 353 "include/linux/slab.h"
1445__inline static void *kzalloc(size_t size , gfp_t flags ) ;
1446#line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1447extern void *__VERIFIER_nondet_pointer(void) ;
1448#line 11
1449void ldv_check_alloc_flags(gfp_t flags ) ;
1450#line 12
1451void ldv_check_alloc_nonatomic(void) ;
1452#line 14
1453struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
1454#line 792 "include/linux/device.h"
1455extern void *dev_get_drvdata(struct device  const  * ) ;
1456#line 793
1457extern int dev_set_drvdata(struct device * , void * ) ;
1458#line 892
1459extern int dev_err(struct device  const  * , char const   *  , ...) ;
1460#line 40 "include/linux/platform_device.h"
1461extern void platform_device_unregister(struct platform_device * ) ;
1462#line 65
1463extern struct platform_device *platform_device_register_full(struct platform_device_info  const  * ) ;
1464#line 82 "include/linux/platform_device.h"
1465__inline static struct platform_device *platform_device_register_resndata(struct device *parent ,
1466                                                                          char const   *name ,
1467                                                                          int id ,
1468                                                                          struct resource  const  *res ,
1469                                                                          unsigned int num ,
1470                                                                          void const   *data ,
1471                                                                          size_t size ) 
1472{ struct platform_device_info pdevinfo ;
1473  struct platform_device *tmp ;
1474  struct platform_device_info *__cil_tmp10 ;
1475  unsigned long __cil_tmp11 ;
1476  unsigned long __cil_tmp12 ;
1477  unsigned long __cil_tmp13 ;
1478  unsigned long __cil_tmp14 ;
1479  unsigned long __cil_tmp15 ;
1480  unsigned long __cil_tmp16 ;
1481  unsigned long __cil_tmp17 ;
1482  struct platform_device_info  const  *__cil_tmp18 ;
1483
1484  {
1485  {
1486#line 87
1487  __cil_tmp10 = & pdevinfo;
1488#line 87
1489  *((struct device **)__cil_tmp10) = parent;
1490#line 87
1491  __cil_tmp11 = (unsigned long )(& pdevinfo) + 8;
1492#line 87
1493  *((char const   **)__cil_tmp11) = name;
1494#line 87
1495  __cil_tmp12 = (unsigned long )(& pdevinfo) + 16;
1496#line 87
1497  *((int *)__cil_tmp12) = id;
1498#line 87
1499  __cil_tmp13 = (unsigned long )(& pdevinfo) + 24;
1500#line 87
1501  *((struct resource  const  **)__cil_tmp13) = res;
1502#line 87
1503  __cil_tmp14 = (unsigned long )(& pdevinfo) + 32;
1504#line 87
1505  *((unsigned int *)__cil_tmp14) = num;
1506#line 87
1507  __cil_tmp15 = (unsigned long )(& pdevinfo) + 40;
1508#line 87
1509  *((void const   **)__cil_tmp15) = data;
1510#line 87
1511  __cil_tmp16 = (unsigned long )(& pdevinfo) + 48;
1512#line 87
1513  *((size_t *)__cil_tmp16) = size;
1514#line 87
1515  __cil_tmp17 = (unsigned long )(& pdevinfo) + 56;
1516#line 87
1517  *((u64 *)__cil_tmp17) = 0ULL;
1518#line 98
1519  __cil_tmp18 = (struct platform_device_info  const  *)(& pdevinfo);
1520#line 98
1521  tmp = platform_device_register_full(__cil_tmp18);
1522  }
1523#line 98
1524  return (tmp);
1525}
1526}
1527#line 123 "include/linux/platform_device.h"
1528__inline static struct platform_device *platform_device_register_simple(char const   *name ,
1529                                                                        int id , struct resource  const  *res ,
1530                                                                        unsigned int num ) 
1531{ struct platform_device *tmp ;
1532  struct device *__cil_tmp6 ;
1533  void const   *__cil_tmp7 ;
1534
1535  {
1536  {
1537#line 127
1538  __cil_tmp6 = (struct device *)0;
1539#line 127
1540  __cil_tmp7 = (void const   *)0;
1541#line 127
1542  tmp = platform_device_register_resndata(__cil_tmp6, name, id, res, num, __cil_tmp7,
1543                                          0UL);
1544  }
1545#line 127
1546  return (tmp);
1547}
1548}
1549#line 174
1550extern int platform_driver_register(struct platform_driver * ) ;
1551#line 175
1552extern void platform_driver_unregister(struct platform_driver * ) ;
1553#line 183 "include/linux/platform_device.h"
1554__inline static void *platform_get_drvdata(struct platform_device  const  *pdev ) 
1555{ void *tmp ;
1556  unsigned long __cil_tmp3 ;
1557  unsigned long __cil_tmp4 ;
1558  struct device  const  *__cil_tmp5 ;
1559
1560  {
1561  {
1562#line 185
1563  __cil_tmp3 = (unsigned long )pdev;
1564#line 185
1565  __cil_tmp4 = __cil_tmp3 + 16;
1566#line 185
1567  __cil_tmp5 = (struct device  const  *)__cil_tmp4;
1568#line 185
1569  tmp = dev_get_drvdata(__cil_tmp5);
1570  }
1571#line 185
1572  return (tmp);
1573}
1574}
1575#line 188 "include/linux/platform_device.h"
1576__inline static void platform_set_drvdata(struct platform_device *pdev , void *data ) 
1577{ unsigned long __cil_tmp3 ;
1578  unsigned long __cil_tmp4 ;
1579  struct device *__cil_tmp5 ;
1580
1581  {
1582  {
1583#line 190
1584  __cil_tmp3 = (unsigned long )pdev;
1585#line 190
1586  __cil_tmp4 = __cil_tmp3 + 16;
1587#line 190
1588  __cil_tmp5 = (struct device *)__cil_tmp4;
1589#line 190
1590  dev_set_drvdata(__cil_tmp5, data);
1591  }
1592#line 191
1593  return;
1594}
1595}
1596#line 124 "include/linux/usb/otg.h"
1597extern int usb_set_transceiver(struct usb_phy * ) ;
1598#line 128
1599void usb_nop_xceiv_register(void) ;
1600#line 129
1601void usb_nop_xceiv_unregister(void) ;
1602#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1603static struct platform_device *pd  ;
1604#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1605void usb_nop_xceiv_register(void) 
1606{ struct platform_device *__cil_tmp1 ;
1607  unsigned long __cil_tmp2 ;
1608  unsigned long __cil_tmp3 ;
1609  struct resource  const  *__cil_tmp4 ;
1610  struct platform_device *__cil_tmp5 ;
1611  unsigned long __cil_tmp6 ;
1612  unsigned long __cil_tmp7 ;
1613
1614  {
1615  {
1616#line 59
1617  __cil_tmp1 = (struct platform_device *)0;
1618#line 59
1619  __cil_tmp2 = (unsigned long )__cil_tmp1;
1620#line 59
1621  __cil_tmp3 = (unsigned long )pd;
1622#line 59
1623  if (__cil_tmp3 != __cil_tmp2) {
1624#line 60
1625    return;
1626  } else {
1627
1628  }
1629  }
1630  {
1631#line 61
1632  __cil_tmp4 = (struct resource  const  *)0;
1633#line 61
1634  pd = platform_device_register_simple("nop_usb_xceiv", -1, __cil_tmp4, 0U);
1635  }
1636  {
1637#line 62
1638  __cil_tmp5 = (struct platform_device *)0;
1639#line 62
1640  __cil_tmp6 = (unsigned long )__cil_tmp5;
1641#line 62
1642  __cil_tmp7 = (unsigned long )pd;
1643#line 62
1644  if (__cil_tmp7 == __cil_tmp6) {
1645    {
1646#line 63
1647    printk("<3>Unable to register usb nop transceiver\n");
1648    }
1649#line 64
1650    return;
1651  } else {
1652
1653  }
1654  }
1655#line 66
1656  return;
1657}
1658}
1659#line 69 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1660void usb_nop_xceiv_unregister(void) 
1661{ 
1662
1663  {
1664  {
1665#line 71
1666  platform_device_unregister(pd);
1667#line 72
1668  pd = (struct platform_device *)0;
1669  }
1670#line 73
1671  return;
1672}
1673}
1674#line 76 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1675static int nop_set_suspend(struct usb_phy *x , int suspend ) 
1676{ 
1677
1678  {
1679#line 78
1680  return (0);
1681}
1682}
1683#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1684static int nop_set_peripheral(struct usb_otg *otg , struct usb_gadget *gadget ) 
1685{ struct usb_otg *__cil_tmp3 ;
1686  unsigned long __cil_tmp4 ;
1687  unsigned long __cil_tmp5 ;
1688  struct usb_gadget *__cil_tmp6 ;
1689  unsigned long __cil_tmp7 ;
1690  unsigned long __cil_tmp8 ;
1691  unsigned long __cil_tmp9 ;
1692  unsigned long __cil_tmp10 ;
1693  unsigned long __cil_tmp11 ;
1694  unsigned long __cil_tmp12 ;
1695  unsigned long __cil_tmp13 ;
1696  unsigned long __cil_tmp14 ;
1697  struct usb_phy *__cil_tmp15 ;
1698  unsigned long __cil_tmp16 ;
1699  unsigned long __cil_tmp17 ;
1700
1701  {
1702  {
1703#line 83
1704  __cil_tmp3 = (struct usb_otg *)0;
1705#line 83
1706  __cil_tmp4 = (unsigned long )__cil_tmp3;
1707#line 83
1708  __cil_tmp5 = (unsigned long )otg;
1709#line 83
1710  if (__cil_tmp5 == __cil_tmp4) {
1711#line 84
1712    return (-19);
1713  } else {
1714
1715  }
1716  }
1717  {
1718#line 86
1719  __cil_tmp6 = (struct usb_gadget *)0;
1720#line 86
1721  __cil_tmp7 = (unsigned long )__cil_tmp6;
1722#line 86
1723  __cil_tmp8 = (unsigned long )gadget;
1724#line 86
1725  if (__cil_tmp8 == __cil_tmp7) {
1726#line 87
1727    __cil_tmp9 = (unsigned long )otg;
1728#line 87
1729    __cil_tmp10 = __cil_tmp9 + 24;
1730#line 87
1731    *((struct usb_gadget **)__cil_tmp10) = (struct usb_gadget *)0;
1732#line 88
1733    return (-19);
1734  } else {
1735
1736  }
1737  }
1738#line 91
1739  __cil_tmp11 = (unsigned long )otg;
1740#line 91
1741  __cil_tmp12 = __cil_tmp11 + 24;
1742#line 91
1743  *((struct usb_gadget **)__cil_tmp12) = gadget;
1744#line 92
1745  __cil_tmp13 = (unsigned long )otg;
1746#line 92
1747  __cil_tmp14 = __cil_tmp13 + 8;
1748#line 92
1749  __cil_tmp15 = *((struct usb_phy **)__cil_tmp14);
1750#line 92
1751  __cil_tmp16 = (unsigned long )__cil_tmp15;
1752#line 92
1753  __cil_tmp17 = __cil_tmp16 + 20;
1754#line 92
1755  *((enum usb_otg_state *)__cil_tmp17) = (enum usb_otg_state )1;
1756#line 93
1757  return (0);
1758}
1759}
1760#line 96 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1761static int nop_set_host(struct usb_otg *otg , struct usb_bus *host ) 
1762{ struct usb_otg *__cil_tmp3 ;
1763  unsigned long __cil_tmp4 ;
1764  unsigned long __cil_tmp5 ;
1765  struct usb_bus *__cil_tmp6 ;
1766  unsigned long __cil_tmp7 ;
1767  unsigned long __cil_tmp8 ;
1768  unsigned long __cil_tmp9 ;
1769  unsigned long __cil_tmp10 ;
1770  unsigned long __cil_tmp11 ;
1771  unsigned long __cil_tmp12 ;
1772
1773  {
1774  {
1775#line 98
1776  __cil_tmp3 = (struct usb_otg *)0;
1777#line 98
1778  __cil_tmp4 = (unsigned long )__cil_tmp3;
1779#line 98
1780  __cil_tmp5 = (unsigned long )otg;
1781#line 98
1782  if (__cil_tmp5 == __cil_tmp4) {
1783#line 99
1784    return (-19);
1785  } else {
1786
1787  }
1788  }
1789  {
1790#line 101
1791  __cil_tmp6 = (struct usb_bus *)0;
1792#line 101
1793  __cil_tmp7 = (unsigned long )__cil_tmp6;
1794#line 101
1795  __cil_tmp8 = (unsigned long )host;
1796#line 101
1797  if (__cil_tmp8 == __cil_tmp7) {
1798#line 102
1799    __cil_tmp9 = (unsigned long )otg;
1800#line 102
1801    __cil_tmp10 = __cil_tmp9 + 16;
1802#line 102
1803    *((struct usb_bus **)__cil_tmp10) = (struct usb_bus *)0;
1804#line 103
1805    return (-19);
1806  } else {
1807
1808  }
1809  }
1810#line 106
1811  __cil_tmp11 = (unsigned long )otg;
1812#line 106
1813  __cil_tmp12 = __cil_tmp11 + 16;
1814#line 106
1815  *((struct usb_bus **)__cil_tmp12) = host;
1816#line 107
1817  return (0);
1818}
1819}
1820#line 110 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
1821static int nop_usb_xceiv_probe(struct platform_device *pdev ) 
1822{ struct nop_usb_xceiv *nop ;
1823  int err ;
1824  void *tmp ;
1825  void *tmp___0 ;
1826  struct lock_class_key __key ;
1827  struct nop_usb_xceiv *__cil_tmp7 ;
1828  unsigned long __cil_tmp8 ;
1829  unsigned long __cil_tmp9 ;
1830  unsigned long __cil_tmp10 ;
1831  unsigned long __cil_tmp11 ;
1832  unsigned long __cil_tmp12 ;
1833  struct usb_otg *__cil_tmp13 ;
1834  unsigned long __cil_tmp14 ;
1835  unsigned long __cil_tmp15 ;
1836  unsigned long __cil_tmp16 ;
1837  unsigned long __cil_tmp17 ;
1838  struct usb_otg *__cil_tmp18 ;
1839  unsigned long __cil_tmp19 ;
1840  void const   *__cil_tmp20 ;
1841  unsigned long __cil_tmp21 ;
1842  unsigned long __cil_tmp22 ;
1843  unsigned long __cil_tmp23 ;
1844  unsigned long __cil_tmp24 ;
1845  unsigned long __cil_tmp25 ;
1846  unsigned long __cil_tmp26 ;
1847  unsigned long __cil_tmp27 ;
1848  unsigned long __cil_tmp28 ;
1849  unsigned long __cil_tmp29 ;
1850  unsigned long __cil_tmp30 ;
1851  unsigned long __cil_tmp31 ;
1852  unsigned long __cil_tmp32 ;
1853  unsigned long __cil_tmp33 ;
1854  unsigned long __cil_tmp34 ;
1855  unsigned long __cil_tmp35 ;
1856  unsigned long __cil_tmp36 ;
1857  unsigned long __cil_tmp37 ;
1858  unsigned long __cil_tmp38 ;
1859  struct usb_otg *__cil_tmp39 ;
1860  unsigned long __cil_tmp40 ;
1861  unsigned long __cil_tmp41 ;
1862  unsigned long __cil_tmp42 ;
1863  unsigned long __cil_tmp43 ;
1864  unsigned long __cil_tmp44 ;
1865  struct usb_otg *__cil_tmp45 ;
1866  unsigned long __cil_tmp46 ;
1867  unsigned long __cil_tmp47 ;
1868  unsigned long __cil_tmp48 ;
1869  unsigned long __cil_tmp49 ;
1870  unsigned long __cil_tmp50 ;
1871  struct usb_otg *__cil_tmp51 ;
1872  unsigned long __cil_tmp52 ;
1873  unsigned long __cil_tmp53 ;
1874  struct usb_phy *__cil_tmp54 ;
1875  unsigned long __cil_tmp55 ;
1876  unsigned long __cil_tmp56 ;
1877  struct device *__cil_tmp57 ;
1878  struct device  const  *__cil_tmp58 ;
1879  void *__cil_tmp59 ;
1880  unsigned long __cil_tmp60 ;
1881  unsigned long __cil_tmp61 ;
1882  unsigned long __cil_tmp62 ;
1883  spinlock_t *__cil_tmp63 ;
1884  unsigned long __cil_tmp64 ;
1885  unsigned long __cil_tmp65 ;
1886  unsigned long __cil_tmp66 ;
1887  struct raw_spinlock *__cil_tmp67 ;
1888  unsigned long __cil_tmp68 ;
1889  unsigned long __cil_tmp69 ;
1890  unsigned long __cil_tmp70 ;
1891  unsigned long __cil_tmp71 ;
1892  unsigned long __cil_tmp72 ;
1893  unsigned long __cil_tmp73 ;
1894  unsigned long __cil_tmp74 ;
1895  struct usb_otg *__cil_tmp75 ;
1896  void const   *__cil_tmp76 ;
1897  void const   *__cil_tmp77 ;
1898
1899  {
1900  {
1901#line 115
1902  tmp = kzalloc(192UL, 208U);
1903#line 115
1904  nop = (struct nop_usb_xceiv *)tmp;
1905  }
1906  {
1907#line 116
1908  __cil_tmp7 = (struct nop_usb_xceiv *)0;
1909#line 116
1910  __cil_tmp8 = (unsigned long )__cil_tmp7;
1911#line 116
1912  __cil_tmp9 = (unsigned long )nop;
1913#line 116
1914  if (__cil_tmp9 == __cil_tmp8) {
1915#line 117
1916    return (-12);
1917  } else {
1918
1919  }
1920  }
1921  {
1922#line 119
1923  tmp___0 = kzalloc(72UL, 208U);
1924#line 119
1925  __cil_tmp10 = 0 + 32;
1926#line 119
1927  __cil_tmp11 = (unsigned long )nop;
1928#line 119
1929  __cil_tmp12 = __cil_tmp11 + __cil_tmp10;
1930#line 119
1931  *((struct usb_otg **)__cil_tmp12) = (struct usb_otg *)tmp___0;
1932  }
1933  {
1934#line 120
1935  __cil_tmp13 = (struct usb_otg *)0;
1936#line 120
1937  __cil_tmp14 = (unsigned long )__cil_tmp13;
1938#line 120
1939  __cil_tmp15 = 0 + 32;
1940#line 120
1941  __cil_tmp16 = (unsigned long )nop;
1942#line 120
1943  __cil_tmp17 = __cil_tmp16 + __cil_tmp15;
1944#line 120
1945  __cil_tmp18 = *((struct usb_otg **)__cil_tmp17);
1946#line 120
1947  __cil_tmp19 = (unsigned long )__cil_tmp18;
1948#line 120
1949  if (__cil_tmp19 == __cil_tmp14) {
1950    {
1951#line 121
1952    __cil_tmp20 = (void const   *)nop;
1953#line 121
1954    kfree(__cil_tmp20);
1955    }
1956#line 122
1957    return (-12);
1958  } else {
1959
1960  }
1961  }
1962  {
1963#line 125
1964  __cil_tmp21 = (unsigned long )nop;
1965#line 125
1966  __cil_tmp22 = __cil_tmp21 + 184;
1967#line 125
1968  __cil_tmp23 = (unsigned long )pdev;
1969#line 125
1970  __cil_tmp24 = __cil_tmp23 + 16;
1971#line 125
1972  *((struct device **)__cil_tmp22) = (struct device *)__cil_tmp24;
1973#line 126
1974  __cil_tmp25 = (unsigned long )nop;
1975#line 126
1976  __cil_tmp26 = __cil_tmp25 + 184;
1977#line 126
1978  *((struct device **)nop) = *((struct device **)__cil_tmp26);
1979#line 127
1980  __cil_tmp27 = 0 + 8;
1981#line 127
1982  __cil_tmp28 = (unsigned long )nop;
1983#line 127
1984  __cil_tmp29 = __cil_tmp28 + __cil_tmp27;
1985#line 127
1986  *((char const   **)__cil_tmp29) = "nop-xceiv";
1987#line 128
1988  __cil_tmp30 = 0 + 176;
1989#line 128
1990  __cil_tmp31 = (unsigned long )nop;
1991#line 128
1992  __cil_tmp32 = __cil_tmp31 + __cil_tmp30;
1993#line 128
1994  *((int (**)(struct usb_phy * , int  ))__cil_tmp32) = & nop_set_suspend;
1995#line 129
1996  __cil_tmp33 = 0 + 20;
1997#line 129
1998  __cil_tmp34 = (unsigned long )nop;
1999#line 129
2000  __cil_tmp35 = __cil_tmp34 + __cil_tmp33;
2001#line 129
2002  *((enum usb_otg_state *)__cil_tmp35) = (enum usb_otg_state )0;
2003#line 131
2004  __cil_tmp36 = 0 + 32;
2005#line 131
2006  __cil_tmp37 = (unsigned long )nop;
2007#line 131
2008  __cil_tmp38 = __cil_tmp37 + __cil_tmp36;
2009#line 131
2010  __cil_tmp39 = *((struct usb_otg **)__cil_tmp38);
2011#line 131
2012  __cil_tmp40 = (unsigned long )__cil_tmp39;
2013#line 131
2014  __cil_tmp41 = __cil_tmp40 + 8;
2015#line 131
2016  *((struct usb_phy **)__cil_tmp41) = (struct usb_phy *)nop;
2017#line 132
2018  __cil_tmp42 = 0 + 32;
2019#line 132
2020  __cil_tmp43 = (unsigned long )nop;
2021#line 132
2022  __cil_tmp44 = __cil_tmp43 + __cil_tmp42;
2023#line 132
2024  __cil_tmp45 = *((struct usb_otg **)__cil_tmp44);
2025#line 132
2026  __cil_tmp46 = (unsigned long )__cil_tmp45;
2027#line 132
2028  __cil_tmp47 = __cil_tmp46 + 32;
2029#line 132
2030  *((int (**)(struct usb_otg * , struct usb_bus * ))__cil_tmp47) = & nop_set_host;
2031#line 133
2032  __cil_tmp48 = 0 + 32;
2033#line 133
2034  __cil_tmp49 = (unsigned long )nop;
2035#line 133
2036  __cil_tmp50 = __cil_tmp49 + __cil_tmp48;
2037#line 133
2038  __cil_tmp51 = *((struct usb_otg **)__cil_tmp50);
2039#line 133
2040  __cil_tmp52 = (unsigned long )__cil_tmp51;
2041#line 133
2042  __cil_tmp53 = __cil_tmp52 + 40;
2043#line 133
2044  *((int (**)(struct usb_otg * , struct usb_gadget * ))__cil_tmp53) = & nop_set_peripheral;
2045#line 135
2046  __cil_tmp54 = (struct usb_phy *)nop;
2047#line 135
2048  err = usb_set_transceiver(__cil_tmp54);
2049  }
2050#line 136
2051  if (err != 0) {
2052    {
2053#line 137
2054    __cil_tmp55 = (unsigned long )pdev;
2055#line 137
2056    __cil_tmp56 = __cil_tmp55 + 16;
2057#line 137
2058    __cil_tmp57 = (struct device *)__cil_tmp56;
2059#line 137
2060    __cil_tmp58 = (struct device  const  *)__cil_tmp57;
2061#line 137
2062    dev_err(__cil_tmp58, "can\'t register transceiver, err: %d\n", err);
2063    }
2064#line 139
2065    goto exit;
2066  } else {
2067
2068  }
2069  {
2070#line 142
2071  __cil_tmp59 = (void *)nop;
2072#line 142
2073  platform_set_drvdata(pdev, __cil_tmp59);
2074#line 144
2075  __cil_tmp60 = 0 + 64;
2076#line 144
2077  __cil_tmp61 = (unsigned long )nop;
2078#line 144
2079  __cil_tmp62 = __cil_tmp61 + __cil_tmp60;
2080#line 144
2081  __cil_tmp63 = (spinlock_t *)__cil_tmp62;
2082#line 144
2083  spinlock_check(__cil_tmp63);
2084#line 144
2085  __cil_tmp64 = 0 + 64;
2086#line 144
2087  __cil_tmp65 = (unsigned long )nop;
2088#line 144
2089  __cil_tmp66 = __cil_tmp65 + __cil_tmp64;
2090#line 144
2091  __cil_tmp67 = (struct raw_spinlock *)__cil_tmp66;
2092#line 144
2093  __raw_spin_lock_init(__cil_tmp67, "&(&(&nop->phy.notifier)->lock)->rlock", & __key);
2094#line 144
2095  __cil_tmp68 = 64 + 72;
2096#line 144
2097  __cil_tmp69 = 0 + __cil_tmp68;
2098#line 144
2099  __cil_tmp70 = (unsigned long )nop;
2100#line 144
2101  __cil_tmp71 = __cil_tmp70 + __cil_tmp69;
2102#line 144
2103  *((struct notifier_block **)__cil_tmp71) = (struct notifier_block *)0;
2104  }
2105#line 146
2106  return (0);
2107  exit: 
2108  {
2109#line 148
2110  __cil_tmp72 = 0 + 32;
2111#line 148
2112  __cil_tmp73 = (unsigned long )nop;
2113#line 148
2114  __cil_tmp74 = __cil_tmp73 + __cil_tmp72;
2115#line 148
2116  __cil_tmp75 = *((struct usb_otg **)__cil_tmp74);
2117#line 148
2118  __cil_tmp76 = (void const   *)__cil_tmp75;
2119#line 148
2120  kfree(__cil_tmp76);
2121#line 149
2122  __cil_tmp77 = (void const   *)nop;
2123#line 149
2124  kfree(__cil_tmp77);
2125  }
2126#line 150
2127  return (err);
2128}
2129}
2130#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2131static int nop_usb_xceiv_remove(struct platform_device *pdev ) 
2132{ struct nop_usb_xceiv *nop ;
2133  void *tmp ;
2134  struct platform_device  const  *__cil_tmp4 ;
2135  struct usb_phy *__cil_tmp5 ;
2136  void *__cil_tmp6 ;
2137  unsigned long __cil_tmp7 ;
2138  unsigned long __cil_tmp8 ;
2139  unsigned long __cil_tmp9 ;
2140  struct usb_otg *__cil_tmp10 ;
2141  void const   *__cil_tmp11 ;
2142  void const   *__cil_tmp12 ;
2143
2144  {
2145  {
2146#line 155
2147  __cil_tmp4 = (struct platform_device  const  *)pdev;
2148#line 155
2149  tmp = platform_get_drvdata(__cil_tmp4);
2150#line 155
2151  nop = (struct nop_usb_xceiv *)tmp;
2152#line 157
2153  __cil_tmp5 = (struct usb_phy *)0;
2154#line 157
2155  usb_set_transceiver(__cil_tmp5);
2156#line 159
2157  __cil_tmp6 = (void *)0;
2158#line 159
2159  platform_set_drvdata(pdev, __cil_tmp6);
2160#line 160
2161  __cil_tmp7 = 0 + 32;
2162#line 160
2163  __cil_tmp8 = (unsigned long )nop;
2164#line 160
2165  __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
2166#line 160
2167  __cil_tmp10 = *((struct usb_otg **)__cil_tmp9);
2168#line 160
2169  __cil_tmp11 = (void const   *)__cil_tmp10;
2170#line 160
2171  kfree(__cil_tmp11);
2172#line 161
2173  __cil_tmp12 = (void const   *)nop;
2174#line 161
2175  kfree(__cil_tmp12);
2176  }
2177#line 163
2178  return (0);
2179}
2180}
2181#line 166 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2182static struct platform_driver nop_usb_xceiv_driver  =    {& nop_usb_xceiv_probe, & nop_usb_xceiv_remove, (void (*)(struct platform_device * ))0,
2183    (int (*)(struct platform_device * , pm_message_t  ))0, (int (*)(struct platform_device * ))0,
2184    {"nop_usb_xceiv", (struct bus_type *)0, & __this_module, (char const   *)0, (_Bool)0,
2185     (struct of_device_id  const  *)0, (int (*)(struct device * ))0, (int (*)(struct device * ))0,
2186     (void (*)(struct device * ))0, (int (*)(struct device * , pm_message_t  ))0,
2187     (int (*)(struct device * ))0, (struct attribute_group  const  **)0, (struct dev_pm_ops  const  *)0,
2188     (struct driver_private *)0}, (struct platform_device_id  const  *)0};
2189#line 175 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2190static int nop_usb_xceiv_init(void) 
2191{ int tmp ;
2192
2193  {
2194  {
2195#line 177
2196  tmp = platform_driver_register(& nop_usb_xceiv_driver);
2197  }
2198#line 177
2199  return (tmp);
2200}
2201}
2202#line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2203static void nop_usb_xceiv_exit(void) 
2204{ 
2205
2206  {
2207  {
2208#line 183
2209  platform_driver_unregister(& nop_usb_xceiv_driver);
2210  }
2211#line 184
2212  return;
2213}
2214}
2215#line 208
2216extern void ldv_check_final_state(void) ;
2217#line 211
2218extern void ldv_check_return_value(int  ) ;
2219#line 214
2220extern void ldv_initialize(void) ;
2221#line 217
2222extern int __VERIFIER_nondet_int(void) ;
2223#line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2224int LDV_IN_INTERRUPT  ;
2225#line 223 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2226void main(void) 
2227{ struct platform_device *var_group1 ;
2228  int res_nop_usb_xceiv_probe_5 ;
2229  int ldv_s_nop_usb_xceiv_driver_platform_driver ;
2230  int tmp ;
2231  int tmp___0 ;
2232  int tmp___1 ;
2233
2234  {
2235  {
2236#line 260
2237  ldv_s_nop_usb_xceiv_driver_platform_driver = 0;
2238#line 243
2239  LDV_IN_INTERRUPT = 1;
2240#line 252
2241  ldv_initialize();
2242#line 258
2243  tmp = nop_usb_xceiv_init();
2244  }
2245#line 258
2246  if (tmp != 0) {
2247#line 259
2248    goto ldv_final;
2249  } else {
2250
2251  }
2252#line 263
2253  goto ldv_18860;
2254  ldv_18859: 
2255  {
2256#line 267
2257  tmp___0 = __VERIFIER_nondet_int();
2258  }
2259#line 269
2260  if (tmp___0 == 0) {
2261#line 269
2262    goto case_0;
2263  } else {
2264    {
2265#line 288
2266    goto switch_default;
2267#line 267
2268    if (0) {
2269      case_0: /* CIL Label */ ;
2270#line 272
2271      if (ldv_s_nop_usb_xceiv_driver_platform_driver == 0) {
2272        {
2273#line 277
2274        res_nop_usb_xceiv_probe_5 = nop_usb_xceiv_probe(var_group1);
2275#line 278
2276        ldv_check_return_value(res_nop_usb_xceiv_probe_5);
2277        }
2278#line 279
2279        if (res_nop_usb_xceiv_probe_5 != 0) {
2280#line 280
2281          goto ldv_module_exit;
2282        } else {
2283
2284        }
2285#line 281
2286        ldv_s_nop_usb_xceiv_driver_platform_driver = 0;
2287      } else {
2288
2289      }
2290#line 287
2291      goto ldv_18857;
2292      switch_default: /* CIL Label */ ;
2293#line 288
2294      goto ldv_18857;
2295    } else {
2296      switch_break: /* CIL Label */ ;
2297    }
2298    }
2299  }
2300  ldv_18857: ;
2301  ldv_18860: 
2302  {
2303#line 263
2304  tmp___1 = __VERIFIER_nondet_int();
2305  }
2306#line 263
2307  if (tmp___1 != 0) {
2308#line 265
2309    goto ldv_18859;
2310  } else
2311#line 263
2312  if (ldv_s_nop_usb_xceiv_driver_platform_driver != 0) {
2313#line 265
2314    goto ldv_18859;
2315  } else {
2316#line 267
2317    goto ldv_18861;
2318  }
2319  ldv_18861: ;
2320  ldv_module_exit: 
2321  {
2322#line 300
2323  nop_usb_xceiv_exit();
2324  }
2325  ldv_final: 
2326  {
2327#line 303
2328  ldv_check_final_state();
2329  }
2330#line 306
2331  return;
2332}
2333}
2334#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
2335void ldv_blast_assert(void) 
2336{ 
2337
2338  {
2339  ERROR: ;
2340#line 6
2341  goto ERROR;
2342}
2343}
2344#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
2345extern int __VERIFIER_nondet_int(void) ;
2346#line 327 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2347int ldv_spin  =    0;
2348#line 331 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2349void ldv_check_alloc_flags(gfp_t flags ) 
2350{ 
2351
2352  {
2353#line 334
2354  if (ldv_spin != 0) {
2355#line 334
2356    if (flags != 32U) {
2357      {
2358#line 334
2359      ldv_blast_assert();
2360      }
2361    } else {
2362
2363    }
2364  } else {
2365
2366  }
2367#line 337
2368  return;
2369}
2370}
2371#line 337
2372extern struct page *ldv_some_page(void) ;
2373#line 340 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2374struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
2375{ struct page *tmp ;
2376
2377  {
2378#line 343
2379  if (ldv_spin != 0) {
2380#line 343
2381    if (flags != 32U) {
2382      {
2383#line 343
2384      ldv_blast_assert();
2385      }
2386    } else {
2387
2388    }
2389  } else {
2390
2391  }
2392  {
2393#line 345
2394  tmp = ldv_some_page();
2395  }
2396#line 345
2397  return (tmp);
2398}
2399}
2400#line 349 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2401void ldv_check_alloc_nonatomic(void) 
2402{ 
2403
2404  {
2405#line 352
2406  if (ldv_spin != 0) {
2407    {
2408#line 352
2409    ldv_blast_assert();
2410    }
2411  } else {
2412
2413  }
2414#line 355
2415  return;
2416}
2417}
2418#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2419void ldv_spin_lock(void) 
2420{ 
2421
2422  {
2423#line 359
2424  ldv_spin = 1;
2425#line 360
2426  return;
2427}
2428}
2429#line 363 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2430void ldv_spin_unlock(void) 
2431{ 
2432
2433  {
2434#line 366
2435  ldv_spin = 0;
2436#line 367
2437  return;
2438}
2439}
2440#line 370 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2441int ldv_spin_trylock(void) 
2442{ int is_lock ;
2443
2444  {
2445  {
2446#line 375
2447  is_lock = __VERIFIER_nondet_int();
2448  }
2449#line 377
2450  if (is_lock != 0) {
2451#line 380
2452    return (0);
2453  } else {
2454#line 385
2455    ldv_spin = 1;
2456#line 387
2457    return (1);
2458  }
2459}
2460}
2461#line 554 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2462void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
2463{ 
2464
2465  {
2466  {
2467#line 560
2468  ldv_check_alloc_flags(ldv_func_arg2);
2469#line 562
2470  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
2471  }
2472#line 563
2473  return ((void *)0);
2474}
2475}
2476#line 565 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/1866/dscv_tempdir/dscv/ri/43_1a/drivers/usb/otg/nop-usb-xceiv.c.p"
2477__inline static void *kzalloc(size_t size , gfp_t flags ) 
2478{ void *tmp ;
2479
2480  {
2481  {
2482#line 571
2483  ldv_check_alloc_flags(flags);
2484#line 572
2485  tmp = __VERIFIER_nondet_pointer();
2486  }
2487#line 572
2488  return (tmp);
2489}
2490}