ClabureDB: Classified Bug-Reports Database

   /* Generated by CIL v. 1.3.7 */
   /* print_CIL_Input is true */
   
   #line 20 "include/asm-generic/int-ll64.h"
   typedef unsigned char __u8;
   #line 23 "include/asm-generic/int-ll64.h"
   typedef unsigned short __u16;
   #line 26 "include/asm-generic/int-ll64.h"
   typedef unsigned int __u32;
  #line 30 "include/asm-generic/int-ll64.h"
  typedef unsigned long long __u64;
  #line 43 "include/asm-generic/int-ll64.h"
  typedef unsigned char u8;
  #line 45 "include/asm-generic/int-ll64.h"
  typedef short s16;
  #line 46 "include/asm-generic/int-ll64.h"
  typedef unsigned short u16;
  #line 49 "include/asm-generic/int-ll64.h"
  typedef unsigned int u32;
  #line 14 "include/asm-generic/posix_types.h"
  typedef long __kernel_long_t;
  #line 15 "include/asm-generic/posix_types.h"
  typedef unsigned long __kernel_ulong_t;
  #line 75 "include/asm-generic/posix_types.h"
  typedef __kernel_ulong_t __kernel_size_t;
  #line 76 "include/asm-generic/posix_types.h"
  typedef __kernel_long_t __kernel_ssize_t;
  #line 27 "include/linux/types.h"
  typedef unsigned short umode_t;
  #line 63 "include/linux/types.h"
  typedef __kernel_size_t size_t;
  #line 68 "include/linux/types.h"
  typedef __kernel_ssize_t ssize_t;
  #line 202 "include/linux/types.h"
  typedef unsigned int gfp_t;
  #line 219 "include/linux/types.h"
  struct __anonstruct_atomic_t_7 {
     int counter ;
  };
  #line 219 "include/linux/types.h"
  typedef struct __anonstruct_atomic_t_7 atomic_t;
  #line 224 "include/linux/types.h"
  struct __anonstruct_atomic64_t_8 {
     long counter ;
  };
  #line 224 "include/linux/types.h"
  typedef struct __anonstruct_atomic64_t_8 atomic64_t;
  #line 229 "include/linux/types.h"
  struct list_head {
     struct list_head *next ;
     struct list_head *prev ;
  };
  #line 56 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  struct module;
  #line 56
  struct module;
  #line 146 "include/linux/init.h"
  typedef void (*ctor_fn_t)(void);
  #line 18 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page.h"
  struct page;
  #line 18
  struct page;
  #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
  struct task_struct;
  #line 20
  struct task_struct;
  #line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  struct task_struct;
  #line 46 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  struct page;
  #line 52
  struct task_struct;
  #line 329
  struct arch_spinlock;
  #line 329
  struct arch_spinlock;
  #line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
  struct task_struct;
  #line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
  struct task_struct;
  #line 10 "include/asm-generic/bug.h"
  struct bug_entry {
     int bug_addr_disp ;
     int file_disp ;
     unsigned short line ;
     unsigned short flags ;
  };
  #line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
  struct static_key;
  #line 234
  struct static_key;
  #line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
  struct kmem_cache;
  #line 23 "include/asm-generic/atomic-long.h"
  typedef atomic64_t atomic_long_t;
  #line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  typedef u16 __ticket_t;
  #line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  typedef u32 __ticketpair_t;
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 struct __raw_tickets {
    __ticket_t head ;
    __ticket_t tail ;
 };
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 union __anonunion____missing_field_name_36 {
    __ticketpair_t head_tail ;
    struct __raw_tickets tickets ;
 };
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 struct arch_spinlock {
    union __anonunion____missing_field_name_36 __annonCompField17 ;
 };
 #line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 typedef struct arch_spinlock arch_spinlock_t;
 #line 12 "include/linux/lockdep.h"
 struct task_struct;
 #line 20 "include/linux/spinlock_types.h"
 struct raw_spinlock {
    arch_spinlock_t raw_lock ;
    unsigned int magic ;
    unsigned int owner_cpu ;
    void *owner ;
 };
 #line 64 "include/linux/spinlock_types.h"
 union __anonunion____missing_field_name_39 {
    struct raw_spinlock rlock ;
 };
 #line 64 "include/linux/spinlock_types.h"
 struct spinlock {
    union __anonunion____missing_field_name_39 __annonCompField19 ;
 };
 #line 64 "include/linux/spinlock_types.h"
 typedef struct spinlock spinlock_t;
 #line 55 "include/linux/wait.h"
 struct task_struct;
 #line 60 "include/linux/pageblock-flags.h"
 struct page;
 #line 48 "include/linux/mutex.h"
 struct mutex {
    atomic_t count ;
    spinlock_t wait_lock ;
    struct list_head wait_list ;
    struct task_struct *owner ;
    char const   *name ;
    void *magic ;
 };
 #line 9 "include/linux/memory_hotplug.h"
 struct page;
 #line 994 "include/linux/mmzone.h"
 struct page;
 #line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 struct task_struct;
 #line 18 "include/linux/elf.h"
 typedef __u64 Elf64_Addr;
 #line 19 "include/linux/elf.h"
 typedef __u16 Elf64_Half;
 #line 23 "include/linux/elf.h"
 typedef __u32 Elf64_Word;
 #line 24 "include/linux/elf.h"
 typedef __u64 Elf64_Xword;
 #line 194 "include/linux/elf.h"
 struct elf64_sym {
    Elf64_Word st_name ;
    unsigned char st_info ;
    unsigned char st_other ;
    Elf64_Half st_shndx ;
    Elf64_Addr st_value ;
    Elf64_Xword st_size ;
 };
 #line 194 "include/linux/elf.h"
 typedef struct elf64_sym Elf64_Sym;
 #line 20 "include/linux/kobject_ns.h"
 struct sock;
 #line 20
 struct sock;
 #line 21
 struct kobject;
 #line 21
 struct kobject;
 #line 27
 enum kobj_ns_type {
     KOBJ_NS_TYPE_NONE = 0,
     KOBJ_NS_TYPE_NET = 1,
     KOBJ_NS_TYPES = 2
 } ;
 #line 40 "include/linux/kobject_ns.h"
 struct kobj_ns_type_operations {
    enum kobj_ns_type type ;
    void *(*grab_current_ns)(void) ;
    void const   *(*netlink_ns)(struct sock *sk ) ;
    void const   *(*initial_ns)(void) ;
    void (*drop_ns)(void * ) ;
 };
 #line 22 "include/linux/sysfs.h"
 struct kobject;
 #line 23
 struct module;
 #line 24
 enum kobj_ns_type;
 #line 26 "include/linux/sysfs.h"
 struct attribute {
    char const   *name ;
    umode_t mode ;
 };
 #line 112 "include/linux/sysfs.h"
 struct sysfs_ops {
    ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
    ssize_t (*store)(struct kobject * , struct attribute * , char const   * , size_t  ) ;
    void const   *(*namespace)(struct kobject * , struct attribute  const  * ) ;
 };
 #line 118
 struct sysfs_dirent;
 #line 118
 struct sysfs_dirent;
 #line 22 "include/linux/kref.h"
 struct kref {
    atomic_t refcount ;
 };
 #line 60 "include/linux/kobject.h"
 struct kset;
 #line 60
 struct kobj_type;
 #line 60 "include/linux/kobject.h"
 struct kobject {
    char const   *name ;
    struct list_head entry ;
    struct kobject *parent ;
    struct kset *kset ;
    struct kobj_type *ktype ;
    struct sysfs_dirent *sd ;
    struct kref kref ;
    unsigned int state_initialized : 1 ;
    unsigned int state_in_sysfs : 1 ;
    unsigned int state_add_uevent_sent : 1 ;
    unsigned int state_remove_uevent_sent : 1 ;
    unsigned int uevent_suppress : 1 ;
 };
 #line 108 "include/linux/kobject.h"
 struct kobj_type {
    void (*release)(struct kobject *kobj ) ;
    struct sysfs_ops  const  *sysfs_ops ;
    struct attribute **default_attrs ;
    struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject *kobj ) ;
    void const   *(*namespace)(struct kobject *kobj ) ;
 };
 #line 116 "include/linux/kobject.h"
 struct kobj_uevent_env {
    char *envp[32] ;
    int envp_idx ;
    char buf[2048] ;
    int buflen ;
 };
 #line 123 "include/linux/kobject.h"
 struct kset_uevent_ops {
    int (* const  filter)(struct kset *kset , struct kobject *kobj ) ;
    char const   *(* const  name)(struct kset *kset , struct kobject *kobj ) ;
    int (* const  uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
 };
 #line 140
 struct sock;
 #line 159 "include/linux/kobject.h"
 struct kset {
    struct list_head list ;
    spinlock_t list_lock ;
    struct kobject kobj ;
    struct kset_uevent_ops  const  *uevent_ops ;
 };
 #line 39 "include/linux/moduleparam.h"
 struct kernel_param;
 #line 39
 struct kernel_param;
 #line 41 "include/linux/moduleparam.h"
 struct kernel_param_ops {
    int (*set)(char const   *val , struct kernel_param  const  *kp ) ;
    int (*get)(char *buffer , struct kernel_param  const  *kp ) ;
    void (*free)(void *arg ) ;
 };
 #line 50
 struct kparam_string;
 #line 50
 struct kparam_array;
 #line 50 "include/linux/moduleparam.h"
 union __anonunion____missing_field_name_199 {
    void *arg ;
    struct kparam_string  const  *str ;
    struct kparam_array  const  *arr ;
 };
 #line 50 "include/linux/moduleparam.h"
 struct kernel_param {
    char const   *name ;
    struct kernel_param_ops  const  *ops ;
    u16 perm ;
    s16 level ;
    union __anonunion____missing_field_name_199 __annonCompField32 ;
 };
 #line 63 "include/linux/moduleparam.h"
 struct kparam_string {
    unsigned int maxlen ;
    char *string ;
 };
 #line 69 "include/linux/moduleparam.h"
 struct kparam_array {
    unsigned int max ;
    unsigned int elemsize ;
    unsigned int *num ;
    struct kernel_param_ops  const  *ops ;
    void *elem ;
 };
 #line 445
 struct module;
 #line 80 "include/linux/jump_label.h"
 struct module;
 #line 143 "include/linux/jump_label.h"
 struct static_key {
    atomic_t enabled ;
 };
 #line 22 "include/linux/tracepoint.h"
 struct module;
 #line 23
 struct tracepoint;
 #line 23
 struct tracepoint;
 #line 25 "include/linux/tracepoint.h"
 struct tracepoint_func {
    void *func ;
    void *data ;
 };
 #line 30 "include/linux/tracepoint.h"
 struct tracepoint {
    char const   *name ;
    struct static_key key ;
    void (*regfunc)(void) ;
    void (*unregfunc)(void) ;
    struct tracepoint_func *funcs ;
 };
 #line 19 "include/linux/export.h"
 struct kernel_symbol {
    unsigned long value ;
    char const   *name ;
 };
 #line 8 "include/asm-generic/module.h"
 struct mod_arch_specific {
 
 };
 #line 35 "include/linux/module.h"
 struct module;
 #line 37
 struct module_param_attrs;
 #line 37 "include/linux/module.h"
 struct module_kobject {
    struct kobject kobj ;
    struct module *mod ;
    struct kobject *drivers_dir ;
    struct module_param_attrs *mp ;
 };
 #line 44 "include/linux/module.h"
 struct module_attribute {
    struct attribute attr ;
    ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
    ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const   * ,
                     size_t count ) ;
    void (*setup)(struct module * , char const   * ) ;
    int (*test)(struct module * ) ;
    void (*free)(struct module * ) ;
 };
 #line 71
 struct exception_table_entry;
 #line 71
 struct exception_table_entry;
 #line 199
 enum module_state {
     MODULE_STATE_LIVE = 0,
     MODULE_STATE_COMING = 1,
     MODULE_STATE_GOING = 2
 } ;
 #line 215 "include/linux/module.h"
 struct module_ref {
    unsigned long incs ;
    unsigned long decs ;
 } __attribute__((__aligned__((2) *  (sizeof(unsigned long )) ))) ;
 #line 220
 struct module_sect_attrs;
 #line 220
 struct module_notes_attrs;
 #line 220
 struct ftrace_event_call;
 #line 220 "include/linux/module.h"
 struct module {
    enum module_state state ;
    struct list_head list ;
    char name[64UL - sizeof(unsigned long )] ;
    struct module_kobject mkobj ;
    struct module_attribute *modinfo_attrs ;
    char const   *version ;
    char const   *srcversion ;
    struct kobject *holders_dir ;
    struct kernel_symbol  const  *syms ;
    unsigned long const   *crcs ;
    unsigned int num_syms ;
    struct kernel_param *kp ;
    unsigned int num_kp ;
    unsigned int num_gpl_syms ;
    struct kernel_symbol  const  *gpl_syms ;
    unsigned long const   *gpl_crcs ;
    struct kernel_symbol  const  *unused_syms ;
    unsigned long const   *unused_crcs ;
    unsigned int num_unused_syms ;
    unsigned int num_unused_gpl_syms ;
    struct kernel_symbol  const  *unused_gpl_syms ;
    unsigned long const   *unused_gpl_crcs ;
    struct kernel_symbol  const  *gpl_future_syms ;
    unsigned long const   *gpl_future_crcs ;
    unsigned int num_gpl_future_syms ;
    unsigned int num_exentries ;
    struct exception_table_entry *extable ;
    int (*init)(void) ;
    void *module_init ;
    void *module_core ;
    unsigned int init_size ;
    unsigned int core_size ;
    unsigned int init_text_size ;
    unsigned int core_text_size ;
    unsigned int init_ro_size ;
    unsigned int core_ro_size ;
    struct mod_arch_specific arch ;
    unsigned int taints ;
    unsigned int num_bugs ;
    struct list_head bug_list ;
    struct bug_entry *bug_table ;
    Elf64_Sym *symtab ;
    Elf64_Sym *core_symtab ;
    unsigned int num_symtab ;
    unsigned int core_num_syms ;
    char *strtab ;
    char *core_strtab ;
    struct module_sect_attrs *sect_attrs ;
    struct module_notes_attrs *notes_attrs ;
    char *args ;
    void *percpu ;
    unsigned int percpu_size ;
    unsigned int num_tracepoints ;
    struct tracepoint * const  *tracepoints_ptrs ;
    unsigned int num_trace_bprintk_fmt ;
    char const   **trace_bprintk_fmt_start ;
    struct ftrace_event_call **trace_events ;
    unsigned int num_trace_events ;
    struct list_head source_list ;
    struct list_head target_list ;
    struct task_struct *waiter ;
    void (*exit)(void) ;
    struct module_ref *refptr ;
    ctor_fn_t *ctors ;
    unsigned int num_ctors ;
 };
 #line 46 "include/linux/slub_def.h"
 struct kmem_cache_cpu {
    void **freelist ;
    unsigned long tid ;
    struct page *page ;
    struct page *partial ;
    int node ;
    unsigned int stat[26] ;
 };
 #line 57 "include/linux/slub_def.h"
 struct kmem_cache_node {
    spinlock_t list_lock ;
    unsigned long nr_partial ;
    struct list_head partial ;
    atomic_long_t nr_slabs ;
    atomic_long_t total_objects ;
    struct list_head full ;
 };
 #line 73 "include/linux/slub_def.h"
 struct kmem_cache_order_objects {
    unsigned long x ;
 };
 #line 80 "include/linux/slub_def.h"
 struct kmem_cache {
    struct kmem_cache_cpu *cpu_slab ;
    unsigned long flags ;
    unsigned long min_partial ;
    int size ;
    int objsize ;
    int offset ;
    int cpu_partial ;
    struct kmem_cache_order_objects oo ;
    struct kmem_cache_order_objects max ;
    struct kmem_cache_order_objects min ;
    gfp_t allocflags ;
    int refcount ;
    void (*ctor)(void * ) ;
    int inuse ;
    int align ;
    int reserved ;
    char const   *name ;
    struct list_head list ;
    struct kobject kobj ;
    int remote_node_defrag_ratio ;
    struct kmem_cache_node *node[1 << 10] ;
 };
 #line 31 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/zr36016.h"
 struct videocodec;
 #line 31 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/zr36016.h"
 struct zr36016 {
    char name[32] ;
    int num ;
    struct videocodec *codec ;
    __u8 version ;
    int mode ;
    __u16 xoff ;
    __u16 yoff ;
    __u16 width ;
    __u16 height ;
    __u16 xdec ;
    __u16 ydec ;
 };
 #line 223 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/videocodec.h"
 struct vfe_polarity {
    unsigned int vsync_pol : 1 ;
    unsigned int hsync_pol : 1 ;
    unsigned int field_pol : 1 ;
    unsigned int blank_pol : 1 ;
    unsigned int subimg_pol : 1 ;
    unsigned int poe_pol : 1 ;
    unsigned int pvalid_pol : 1 ;
    unsigned int vclk_pol : 1 ;
 };
 #line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/videocodec.h"
 struct vfe_settings {
    __u32 x ;
    __u32 y ;
    __u32 width ;
    __u32 height ;
    __u16 decimation ;
    __u16 flags ;
    __u16 quality ;
 };
 #line 242 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/videocodec.h"
 struct tvnorm {
    u16 Wt ;
    u16 Wa ;
    u16 HStart ;
    u16 HSyncStart ;
    u16 Ht ;
    u16 Ha ;
    u16 VStart ;
 };
 #line 257
 struct videocodec_master;
 #line 257 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/videocodec.h"
 struct videocodec {
    struct module *owner ;
    char name[32] ;
    unsigned long magic ;
    unsigned long flags ;
    unsigned int type ;
    struct videocodec_master *master_data ;
    void *data ;
    int (*setup)(struct videocodec *codec ) ;
    int (*unset)(struct videocodec *codec ) ;
    int (*set_mode)(struct videocodec *codec , int mode ) ;
    int (*set_video)(struct videocodec *codec , struct tvnorm *norm , struct vfe_settings *cap ,
                     struct vfe_polarity *pol ) ;
    int (*control)(struct videocodec *codec , int type , int size , void *data ) ;
    int (*setup_interrupt)(struct videocodec *codec , long mode ) ;
    int (*handle_interrupt)(struct videocodec *codec , int source , long flag ) ;
    long (*put_image)(struct videocodec *codec , int tr_type , int block , long *fr_num ,
                      long *flag , long size , void *buf ) ;
    long (*get_image)(struct videocodec *codec , int tr_type , int block , long *fr_num ,
                      long *flag , long size , void *buf ) ;
 };
 #line 316 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/videocodec.h"
 struct videocodec_master {
    char name[32] ;
    unsigned long magic ;
    unsigned long flags ;
    unsigned int type ;
    void *data ;
    __u32 (*readreg)(struct videocodec *codec , __u16 reg ) ;
    void (*writereg)(struct videocodec *codec , __u16 reg , __u32 value ) ;
 };
 #line 1 "<compiler builtins>"
 long __builtin_expect(long val , long res ) ;
 #line 100 "include/linux/printk.h"
 extern int ( /* format attribute */  printk)(char const   *fmt  , ...) ;
 #line 322 "include/linux/kernel.h"
 extern int ( /* format attribute */  snprintf)(char *buf , size_t size , char const   *fmt 
                                                , ...) ;
 #line 152 "include/linux/mutex.h"
 void mutex_lock(struct mutex *lock ) ;
 #line 153
 int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) ;
 #line 154
 int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) ;
 #line 168
 int mutex_trylock(struct mutex *lock ) ;
 #line 169
 void mutex_unlock(struct mutex *lock ) ;
 #line 170
 int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
 #line 356 "include/linux/moduleparam.h"
 extern struct kernel_param_ops param_ops_int ;
 #line 26 "include/linux/export.h"
 extern struct module __this_module ;
 #line 67 "include/linux/module.h"
 int init_module(void) ;
 #line 68
 void cleanup_module(void) ;
 #line 161 "include/linux/slab.h"
 extern void kfree(void const   * ) ;
 #line 221 "include/linux/slub_def.h"
 extern void *__kmalloc(size_t size , gfp_t flags ) ;
 #line 268
 __inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
                                                                     gfp_t flags )  __attribute__((__no_instrument_function__)) ;
 #line 268 "include/linux/slub_def.h"
 __inline static void *( __attribute__((__always_inline__)) kmalloc)(size_t size ,
                                                                     gfp_t flags ) 
 { void *tmp___2 ;
 
   {
   {
 #line 283
   tmp___2 = __kmalloc(size, flags);
   }
 #line 283
   return (tmp___2);
 }
 }
 #line 349 "include/linux/slab.h"
 __inline static void *kzalloc(size_t size , gfp_t flags )  __attribute__((__no_instrument_function__)) ;
 #line 349 "include/linux/slab.h"
 __inline static void *kzalloc(size_t size , gfp_t flags ) 
 { void *tmp ;
   unsigned int __cil_tmp4 ;
 
   {
   {
 #line 351
   __cil_tmp4 = flags | 32768U;
 #line 351
   tmp = kmalloc(size, __cil_tmp4);
   }
 #line 351
   return (tmp);
 }
 }
 #line 347 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/videocodec.h"
 extern int videocodec_register(struct videocodec  const  * ) ;
 #line 349
 extern int videocodec_unregister(struct videocodec  const  * ) ;
 #line 54 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
 static int zr36016_codecs  ;
 #line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
 static int debug  ;
 #line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
 static char const   __param_str_debug[6]  = {      (char const   )'d',      (char const   )'e',      (char const   )'b',      (char const   )'u', 
         (char const   )'g',      (char const   )'\000'};
 #line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
 static struct kernel_param  const  __param_debug  __attribute__((__used__, __unused__,
 __section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_debug, (struct kernel_param_ops  const  *)(& param_ops_int), (u16 )0,
     (s16 )0, {(void *)(& debug)}};
 #line 58 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
 static char const   __mod_debugtype58[19]  __attribute__((__used__, __unused__, __section__(".modinfo"),
 __aligned__(1)))  = 
 #line 58
   {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
         (char const   )'t',      (char const   )'y',      (char const   )'p',      (char const   )'e', 
         (char const   )'=',      (char const   )'d',      (char const   )'e',      (char const   )'b', 
         (char const   )'u',      (char const   )'g',      (char const   )':',      (char const   )'i', 
         (char const   )'n',      (char const   )'t',      (char const   )'\000'};
 #line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
 static char const   __mod_debug59[29]  __attribute__((__used__, __unused__, __section__(".modinfo"),
 __aligned__(1)))  = 
 #line 59
   {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
         (char const   )'=',      (char const   )'d',      (char const   )'e',      (char const   )'b', 
         (char const   )'u',      (char const   )'g',      (char const   )':',      (char const   )'D', 
         (char const   )'e',      (char const   )'b',      (char const   )'u',      (char const   )'g', 
         (char const   )' ',      (char const   )'l',      (char const   )'e',      (char const   )'v', 
         (char const   )'e',      (char const   )'l',      (char const   )' ',      (char const   )'(', 
         (char const   )'0',      (char const   )'-',      (char const   )'4',      (char const   )')', 
         (char const   )'\000'};
 #line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
 static u8 zr36016_read(struct zr36016 *ptr , u16 reg ) 
 { u8 value ;
   __u32 tmp ;
   unsigned long __cil_tmp5 ;
   unsigned long __cil_tmp6 ;
   struct videocodec *__cil_tmp7 ;
   unsigned long __cil_tmp8 ;
   unsigned long __cil_tmp9 ;
   struct videocodec_master *__cil_tmp10 ;
   unsigned long __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   struct videocodec *__cil_tmp15 ;
   unsigned long __cil_tmp16 ;
   unsigned long __cil_tmp17 ;
   struct videocodec_master *__cil_tmp18 ;
   unsigned long __cil_tmp19 ;
   unsigned long __cil_tmp20 ;
   __u32 (*__cil_tmp21)(struct videocodec *codec , __u16 reg ) ;
   unsigned long __cil_tmp22 ;
   unsigned long __cil_tmp23 ;
   struct videocodec *__cil_tmp24 ;
   unsigned int __cil_tmp25 ;
   int *__cil_tmp26 ;
   int __cil_tmp27 ;
   unsigned long __cil_tmp28 ;
   unsigned long __cil_tmp29 ;
   unsigned long __cil_tmp30 ;
   unsigned long __cil_tmp31 ;
   char *__cil_tmp32 ;
   int *__cil_tmp33 ;
   int __cil_tmp34 ;
   unsigned long __cil_tmp35 ;
   unsigned long __cil_tmp36 ;
   unsigned long __cil_tmp37 ;
   unsigned long __cil_tmp38 ;
   char *__cil_tmp39 ;
   int __cil_tmp40 ;
   int __cil_tmp41 ;
 
   {
 #line 78
   value = (u8 )0;
   {
 #line 81
   __cil_tmp5 = (unsigned long )ptr;
 #line 81
   __cil_tmp6 = __cil_tmp5 + 40;
 #line 81
   __cil_tmp7 = *((struct videocodec **)__cil_tmp6);
 #line 81
   __cil_tmp8 = (unsigned long )__cil_tmp7;
 #line 81
   __cil_tmp9 = __cil_tmp8 + 64;
 #line 81
   __cil_tmp10 = *((struct videocodec_master **)__cil_tmp9);
 #line 81
   __cil_tmp11 = (unsigned long )__cil_tmp10;
 #line 81
   __cil_tmp12 = __cil_tmp11 + 64;
 #line 81
   if (*((__u32 (**)(struct videocodec *codec , __u16 reg ))__cil_tmp12)) {
     {
 #line 82
     __cil_tmp13 = (unsigned long )ptr;
 #line 82
     __cil_tmp14 = __cil_tmp13 + 40;
 #line 82
     __cil_tmp15 = *((struct videocodec **)__cil_tmp14);
 #line 82
     __cil_tmp16 = (unsigned long )__cil_tmp15;
 #line 82
     __cil_tmp17 = __cil_tmp16 + 64;
 #line 82
     __cil_tmp18 = *((struct videocodec_master **)__cil_tmp17);
 #line 82
     __cil_tmp19 = (unsigned long )__cil_tmp18;
 #line 82
     __cil_tmp20 = __cil_tmp19 + 64;
 #line 82
     __cil_tmp21 = *((__u32 (**)(struct videocodec *codec , __u16 reg ))__cil_tmp20);
 #line 82
     __cil_tmp22 = (unsigned long )ptr;
 #line 82
     __cil_tmp23 = __cil_tmp22 + 40;
 #line 82
     __cil_tmp24 = *((struct videocodec **)__cil_tmp23);
 #line 82
     tmp = (*__cil_tmp21)(__cil_tmp24, reg);
 #line 82
     __cil_tmp25 = tmp & 255U;
 #line 82
     value = (u8 )__cil_tmp25;
     }
   } else {
     {
 #line 86
     while (1) {
       while_continue: /* CIL Label */ ;
       {
 #line 86
       __cil_tmp26 = & debug;
 #line 86
       __cil_tmp27 = *__cil_tmp26;
 #line 86
       if (__cil_tmp27 >= 1) {
         {
 #line 86
         __cil_tmp28 = 0 * 1UL;
 #line 86
         __cil_tmp29 = 0 + __cil_tmp28;
 #line 86
         __cil_tmp30 = (unsigned long )ptr;
 #line 86
         __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
 #line 86
         __cil_tmp32 = (char *)__cil_tmp31;
 #line 86
         printk("<3>%s: invalid I/O setup, nothing read!\n", __cil_tmp32);
         }
       } else {
 
       }
       }
 #line 86
       goto while_break;
     }
     while_break: /* CIL Label */ ;
     }
   }
   }
   {
 #line 90
   while (1) {
     while_continue___0: /* CIL Label */ ;
     {
 #line 90
     __cil_tmp33 = & debug;
 #line 90
     __cil_tmp34 = *__cil_tmp33;
 #line 90
     if (__cil_tmp34 >= 4) {
       {
 #line 90
       __cil_tmp35 = 0 * 1UL;
 #line 90
       __cil_tmp36 = 0 + __cil_tmp35;
 #line 90
       __cil_tmp37 = (unsigned long )ptr;
 #line 90
       __cil_tmp38 = __cil_tmp37 + __cil_tmp36;
 #line 90
       __cil_tmp39 = (char *)__cil_tmp38;
 #line 90
       __cil_tmp40 = (int )reg;
 #line 90
       __cil_tmp41 = (int )value;
 #line 90
       printk("%s: reading from 0x%04x: %02x\n", __cil_tmp39, __cil_tmp40, __cil_tmp41);
       }
     } else {
 
     }
     }
 #line 90
     goto while_break___0;
   }
   while_break___0: /* CIL Label */ ;
   }
 #line 93
   return (value);
 }
 }
 #line 96 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
 static void zr36016_write(struct zr36016 *ptr , u16 reg , u8 value ) 
 { int *__cil_tmp4 ;
   int __cil_tmp5 ;
   unsigned long __cil_tmp6 ;
   unsigned long __cil_tmp7 ;
   unsigned long __cil_tmp8 ;
   unsigned long __cil_tmp9 ;
   char *__cil_tmp10 ;
   int __cil_tmp11 ;
   int __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   struct videocodec *__cil_tmp15 ;
   unsigned long __cil_tmp16 ;
   unsigned long __cil_tmp17 ;
   struct videocodec_master *__cil_tmp18 ;
   unsigned long __cil_tmp19 ;
   unsigned long __cil_tmp20 ;
   unsigned long __cil_tmp21 ;
   unsigned long __cil_tmp22 ;
   struct videocodec *__cil_tmp23 ;
   unsigned long __cil_tmp24 ;
   unsigned long __cil_tmp25 ;
   struct videocodec_master *__cil_tmp26 ;
   unsigned long __cil_tmp27 ;
   unsigned long __cil_tmp28 ;
   void (*__cil_tmp29)(struct videocodec *codec , __u16 reg , __u32 value ) ;
   unsigned long __cil_tmp30 ;
   unsigned long __cil_tmp31 ;
   struct videocodec *__cil_tmp32 ;
   __u32 __cil_tmp33 ;
   int *__cil_tmp34 ;
   int __cil_tmp35 ;
   unsigned long __cil_tmp36 ;
   unsigned long __cil_tmp37 ;
   unsigned long __cil_tmp38 ;
   unsigned long __cil_tmp39 ;
   char *__cil_tmp40 ;
 
   {
   {
 #line 101
   while (1) {
     while_continue: /* CIL Label */ ;
     {
 #line 101
     __cil_tmp4 = & debug;
 #line 101
     __cil_tmp5 = *__cil_tmp4;
 #line 101
     if (__cil_tmp5 >= 4) {
       {
 #line 101
       __cil_tmp6 = 0 * 1UL;
 #line 101
       __cil_tmp7 = 0 + __cil_tmp6;
 #line 101
       __cil_tmp8 = (unsigned long )ptr;
 #line 101
       __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
 #line 101
       __cil_tmp10 = (char *)__cil_tmp9;
 #line 101
       __cil_tmp11 = (int )value;
 #line 101
       __cil_tmp12 = (int )reg;
 #line 101
       printk("%s: writing 0x%02x to 0x%04x\n", __cil_tmp10, __cil_tmp11, __cil_tmp12);
       }
     } else {
 
     }
     }
 #line 101
     goto while_break;
   }
   while_break: /* CIL Label */ ;
   }
   {
 #line 105
   __cil_tmp13 = (unsigned long )ptr;
 #line 105
   __cil_tmp14 = __cil_tmp13 + 40;
 #line 105
   __cil_tmp15 = *((struct videocodec **)__cil_tmp14);
 #line 105
   __cil_tmp16 = (unsigned long )__cil_tmp15;
 #line 105
   __cil_tmp17 = __cil_tmp16 + 64;
 #line 105
   __cil_tmp18 = *((struct videocodec_master **)__cil_tmp17);
 #line 105
   __cil_tmp19 = (unsigned long )__cil_tmp18;
 #line 105
   __cil_tmp20 = __cil_tmp19 + 72;
 #line 105
   if (*((void (**)(struct videocodec *codec , __u16 reg , __u32 value ))__cil_tmp20)) {
     {
 #line 106
     __cil_tmp21 = (unsigned long )ptr;
 #line 106
     __cil_tmp22 = __cil_tmp21 + 40;
 #line 106
     __cil_tmp23 = *((struct videocodec **)__cil_tmp22);
 #line 106
     __cil_tmp24 = (unsigned long )__cil_tmp23;
 #line 106
     __cil_tmp25 = __cil_tmp24 + 64;
 #line 106
     __cil_tmp26 = *((struct videocodec_master **)__cil_tmp25);
 #line 106
     __cil_tmp27 = (unsigned long )__cil_tmp26;
 #line 106
     __cil_tmp28 = __cil_tmp27 + 72;
 #line 106
     __cil_tmp29 = *((void (**)(struct videocodec *codec , __u16 reg , __u32 value ))__cil_tmp28);
 #line 106
     __cil_tmp30 = (unsigned long )ptr;
 #line 106
     __cil_tmp31 = __cil_tmp30 + 40;
 #line 106
     __cil_tmp32 = *((struct videocodec **)__cil_tmp31);
 #line 106
     __cil_tmp33 = (__u32 )value;
 #line 106
     (*__cil_tmp29)(__cil_tmp32, reg, __cil_tmp33);
     }
   } else {
     {
 #line 108
     while (1) {
       while_continue___0: /* CIL Label */ ;
       {
 #line 108
       __cil_tmp34 = & debug;
 #line 108
       __cil_tmp35 = *__cil_tmp34;
 #line 108
       if (__cil_tmp35 >= 1) {
        {
#line 108
        __cil_tmp36 = 0 * 1UL;
#line 108
        __cil_tmp37 = 0 + __cil_tmp36;
#line 108
        __cil_tmp38 = (unsigned long )ptr;
#line 108
        __cil_tmp39 = __cil_tmp38 + __cil_tmp37;
#line 108
        __cil_tmp40 = (char *)__cil_tmp39;
#line 108
        printk("<3>%s: invalid I/O setup, nothing written!\n", __cil_tmp40);
        }
      } else {

      }
      }
#line 108
      goto while_break___0;
    }
    while_break___0: /* CIL Label */ ;
    }
  }
  }
#line 112
  return;
}
}
#line 117 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static u8 zr36016_readi(struct zr36016 *ptr , u16 reg ) 
{ u8 value ;
  __u32 tmp ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct videocodec *__cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  struct videocodec_master *__cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  struct videocodec *__cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  struct videocodec_master *__cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  struct videocodec *__cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  struct videocodec_master *__cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  void (*__cil_tmp29)(struct videocodec *codec , __u16 reg , __u32 value ) ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  struct videocodec *__cil_tmp32 ;
  __u16 __cil_tmp33 ;
  int __cil_tmp34 ;
  int __cil_tmp35 ;
  __u32 __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  struct videocodec *__cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  struct videocodec_master *__cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  __u32 (*__cil_tmp45)(struct videocodec *codec , __u16 reg ) ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  struct videocodec *__cil_tmp48 ;
  __u16 __cil_tmp49 ;
  unsigned int __cil_tmp50 ;
  int *__cil_tmp51 ;
  int __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  char *__cil_tmp57 ;
  int *__cil_tmp58 ;
  int __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  unsigned long __cil_tmp63 ;
  char *__cil_tmp64 ;
  int __cil_tmp65 ;
  int __cil_tmp66 ;

  {
#line 121
  value = (u8 )0;
  {
#line 124
  __cil_tmp5 = (unsigned long )ptr;
#line 124
  __cil_tmp6 = __cil_tmp5 + 40;
#line 124
  __cil_tmp7 = *((struct videocodec **)__cil_tmp6);
#line 124
  __cil_tmp8 = (unsigned long )__cil_tmp7;
#line 124
  __cil_tmp9 = __cil_tmp8 + 64;
#line 124
  __cil_tmp10 = *((struct videocodec_master **)__cil_tmp9);
#line 124
  __cil_tmp11 = (unsigned long )__cil_tmp10;
#line 124
  __cil_tmp12 = __cil_tmp11 + 72;
#line 124
  if (*((void (**)(struct videocodec *codec , __u16 reg , __u32 value ))__cil_tmp12)) {
    {
#line 124
    __cil_tmp13 = (unsigned long )ptr;
#line 124
    __cil_tmp14 = __cil_tmp13 + 40;
#line 124
    __cil_tmp15 = *((struct videocodec **)__cil_tmp14);
#line 124
    __cil_tmp16 = (unsigned long )__cil_tmp15;
#line 124
    __cil_tmp17 = __cil_tmp16 + 64;
#line 124
    __cil_tmp18 = *((struct videocodec_master **)__cil_tmp17);
#line 124
    __cil_tmp19 = (unsigned long )__cil_tmp18;
#line 124
    __cil_tmp20 = __cil_tmp19 + 64;
#line 124
    if (*((__u32 (**)(struct videocodec *codec , __u16 reg ))__cil_tmp20)) {
      {
#line 126
      __cil_tmp21 = (unsigned long )ptr;
#line 126
      __cil_tmp22 = __cil_tmp21 + 40;
#line 126
      __cil_tmp23 = *((struct videocodec **)__cil_tmp22);
#line 126
      __cil_tmp24 = (unsigned long )__cil_tmp23;
#line 126
      __cil_tmp25 = __cil_tmp24 + 64;
#line 126
      __cil_tmp26 = *((struct videocodec_master **)__cil_tmp25);
#line 126
      __cil_tmp27 = (unsigned long )__cil_tmp26;
#line 126
      __cil_tmp28 = __cil_tmp27 + 72;
#line 126
      __cil_tmp29 = *((void (**)(struct videocodec *codec , __u16 reg , __u32 value ))__cil_tmp28);
#line 126
      __cil_tmp30 = (unsigned long )ptr;
#line 126
      __cil_tmp31 = __cil_tmp30 + 40;
#line 126
      __cil_tmp32 = *((struct videocodec **)__cil_tmp31);
#line 126
      __cil_tmp33 = (__u16 )2;
#line 126
      __cil_tmp34 = (int )reg;
#line 126
      __cil_tmp35 = __cil_tmp34 & 15;
#line 126
      __cil_tmp36 = (__u32 )__cil_tmp35;
#line 126
      (*__cil_tmp29)(__cil_tmp32, __cil_tmp33, __cil_tmp36);
#line 127
      __cil_tmp37 = (unsigned long )ptr;
#line 127
      __cil_tmp38 = __cil_tmp37 + 40;
#line 127
      __cil_tmp39 = *((struct videocodec **)__cil_tmp38);
#line 127
      __cil_tmp40 = (unsigned long )__cil_tmp39;
#line 127
      __cil_tmp41 = __cil_tmp40 + 64;
#line 127
      __cil_tmp42 = *((struct videocodec_master **)__cil_tmp41);
#line 127
      __cil_tmp43 = (unsigned long )__cil_tmp42;
#line 127
      __cil_tmp44 = __cil_tmp43 + 64;
#line 127
      __cil_tmp45 = *((__u32 (**)(struct videocodec *codec , __u16 reg ))__cil_tmp44);
#line 127
      __cil_tmp46 = (unsigned long )ptr;
#line 127
      __cil_tmp47 = __cil_tmp46 + 40;
#line 127
      __cil_tmp48 = *((struct videocodec **)__cil_tmp47);
#line 127
      __cil_tmp49 = (__u16 )3;
#line 127
      tmp = (*__cil_tmp45)(__cil_tmp48, __cil_tmp49);
#line 127
      __cil_tmp50 = tmp & 255U;
#line 127
      value = (u8 )__cil_tmp50;
      }
    } else {
#line 124
      goto _L;
    }
    }
  } else {
    _L: /* CIL Label */ 
    {
#line 129
    while (1) {
      while_continue: /* CIL Label */ ;
      {
#line 129
      __cil_tmp51 = & debug;
#line 129
      __cil_tmp52 = *__cil_tmp51;
#line 129
      if (__cil_tmp52 >= 1) {
        {
#line 129
        __cil_tmp53 = 0 * 1UL;
#line 129
        __cil_tmp54 = 0 + __cil_tmp53;
#line 129
        __cil_tmp55 = (unsigned long )ptr;
#line 129
        __cil_tmp56 = __cil_tmp55 + __cil_tmp54;
#line 129
        __cil_tmp57 = (char *)__cil_tmp56;
#line 129
        printk("<3>%s: invalid I/O setup, nothing read (i)!\n", __cil_tmp57);
        }
      } else {

      }
      }
#line 129
      goto while_break;
    }
    while_break: /* CIL Label */ ;
    }
  }
  }
  {
#line 134
  while (1) {
    while_continue___0: /* CIL Label */ ;
    {
#line 134
    __cil_tmp58 = & debug;
#line 134
    __cil_tmp59 = *__cil_tmp58;
#line 134
    if (__cil_tmp59 >= 4) {
      {
#line 134
      __cil_tmp60 = 0 * 1UL;
#line 134
      __cil_tmp61 = 0 + __cil_tmp60;
#line 134
      __cil_tmp62 = (unsigned long )ptr;
#line 134
      __cil_tmp63 = __cil_tmp62 + __cil_tmp61;
#line 134
      __cil_tmp64 = (char *)__cil_tmp63;
#line 134
      __cil_tmp65 = (int )reg;
#line 134
      __cil_tmp66 = (int )value;
#line 134
      printk("%s: reading indirect from 0x%04x: %02x\n", __cil_tmp64, __cil_tmp65,
             __cil_tmp66);
      }
    } else {

    }
    }
#line 134
    goto while_break___0;
  }
  while_break___0: /* CIL Label */ ;
  }
#line 136
  return (value);
}
}
#line 139 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static void zr36016_writei(struct zr36016 *ptr , u16 reg , u8 value ) 
{ int *__cil_tmp4 ;
  int __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  char *__cil_tmp10 ;
  int __cil_tmp11 ;
  int __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  struct videocodec *__cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  struct videocodec_master *__cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  struct videocodec *__cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  struct videocodec_master *__cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  void (*__cil_tmp29)(struct videocodec *codec , __u16 reg , __u32 value ) ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  struct videocodec *__cil_tmp32 ;
  __u16 __cil_tmp33 ;
  int __cil_tmp34 ;
  int __cil_tmp35 ;
  __u32 __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  struct videocodec *__cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  struct videocodec_master *__cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  void (*__cil_tmp45)(struct videocodec *codec , __u16 reg , __u32 value ) ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  struct videocodec *__cil_tmp48 ;
  __u16 __cil_tmp49 ;
  int __cil_tmp50 ;
  int __cil_tmp51 ;
  __u32 __cil_tmp52 ;
  int *__cil_tmp53 ;
  int __cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  char *__cil_tmp59 ;

  {
  {
#line 144
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 144
    __cil_tmp4 = & debug;
#line 144
    __cil_tmp5 = *__cil_tmp4;
#line 144
    if (__cil_tmp5 >= 4) {
      {
#line 144
      __cil_tmp6 = 0 * 1UL;
#line 144
      __cil_tmp7 = 0 + __cil_tmp6;
#line 144
      __cil_tmp8 = (unsigned long )ptr;
#line 144
      __cil_tmp9 = __cil_tmp8 + __cil_tmp7;
#line 144
      __cil_tmp10 = (char *)__cil_tmp9;
#line 144
      __cil_tmp11 = (int )value;
#line 144
      __cil_tmp12 = (int )reg;
#line 144
      printk("%s: writing indirect 0x%02x to 0x%04x\n", __cil_tmp10, __cil_tmp11,
             __cil_tmp12);
      }
    } else {

    }
    }
#line 144
    goto while_break;
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 148
  __cil_tmp13 = (unsigned long )ptr;
#line 148
  __cil_tmp14 = __cil_tmp13 + 40;
#line 148
  __cil_tmp15 = *((struct videocodec **)__cil_tmp14);
#line 148
  __cil_tmp16 = (unsigned long )__cil_tmp15;
#line 148
  __cil_tmp17 = __cil_tmp16 + 64;
#line 148
  __cil_tmp18 = *((struct videocodec_master **)__cil_tmp17);
#line 148
  __cil_tmp19 = (unsigned long )__cil_tmp18;
#line 148
  __cil_tmp20 = __cil_tmp19 + 72;
#line 148
  if (*((void (**)(struct videocodec *codec , __u16 reg , __u32 value ))__cil_tmp20)) {
    {
#line 149
    __cil_tmp21 = (unsigned long )ptr;
#line 149
    __cil_tmp22 = __cil_tmp21 + 40;
#line 149
    __cil_tmp23 = *((struct videocodec **)__cil_tmp22);
#line 149
    __cil_tmp24 = (unsigned long )__cil_tmp23;
#line 149
    __cil_tmp25 = __cil_tmp24 + 64;
#line 149
    __cil_tmp26 = *((struct videocodec_master **)__cil_tmp25);
#line 149
    __cil_tmp27 = (unsigned long )__cil_tmp26;
#line 149
    __cil_tmp28 = __cil_tmp27 + 72;
#line 149
    __cil_tmp29 = *((void (**)(struct videocodec *codec , __u16 reg , __u32 value ))__cil_tmp28);
#line 149
    __cil_tmp30 = (unsigned long )ptr;
#line 149
    __cil_tmp31 = __cil_tmp30 + 40;
#line 149
    __cil_tmp32 = *((struct videocodec **)__cil_tmp31);
#line 149
    __cil_tmp33 = (__u16 )2;
#line 149
    __cil_tmp34 = (int )reg;
#line 149
    __cil_tmp35 = __cil_tmp34 & 15;
#line 149
    __cil_tmp36 = (__u32 )__cil_tmp35;
#line 149
    (*__cil_tmp29)(__cil_tmp32, __cil_tmp33, __cil_tmp36);
#line 150
    __cil_tmp37 = (unsigned long )ptr;
#line 150
    __cil_tmp38 = __cil_tmp37 + 40;
#line 150
    __cil_tmp39 = *((struct videocodec **)__cil_tmp38);
#line 150
    __cil_tmp40 = (unsigned long )__cil_tmp39;
#line 150
    __cil_tmp41 = __cil_tmp40 + 64;
#line 150
    __cil_tmp42 = *((struct videocodec_master **)__cil_tmp41);
#line 150
    __cil_tmp43 = (unsigned long )__cil_tmp42;
#line 150
    __cil_tmp44 = __cil_tmp43 + 72;
#line 150
    __cil_tmp45 = *((void (**)(struct videocodec *codec , __u16 reg , __u32 value ))__cil_tmp44);
#line 150
    __cil_tmp46 = (unsigned long )ptr;
#line 150
    __cil_tmp47 = __cil_tmp46 + 40;
#line 150
    __cil_tmp48 = *((struct videocodec **)__cil_tmp47);
#line 150
    __cil_tmp49 = (__u16 )3;
#line 150
    __cil_tmp50 = (int )value;
#line 150
    __cil_tmp51 = __cil_tmp50 & 255;
#line 150
    __cil_tmp52 = (__u32 )__cil_tmp51;
#line 150
    (*__cil_tmp45)(__cil_tmp48, __cil_tmp49, __cil_tmp52);
    }
  } else {
    {
#line 152
    while (1) {
      while_continue___0: /* CIL Label */ ;
      {
#line 152
      __cil_tmp53 = & debug;
#line 152
      __cil_tmp54 = *__cil_tmp53;
#line 152
      if (__cil_tmp54 >= 1) {
        {
#line 152
        __cil_tmp55 = 0 * 1UL;
#line 152
        __cil_tmp56 = 0 + __cil_tmp55;
#line 152
        __cil_tmp57 = (unsigned long )ptr;
#line 152
        __cil_tmp58 = __cil_tmp57 + __cil_tmp56;
#line 152
        __cil_tmp59 = (char *)__cil_tmp58;
#line 152
        printk("<3>%s: invalid I/O setup, nothing written (i)!\n", __cil_tmp59);
        }
      } else {

      }
      }
#line 152
      goto while_break___0;
    }
    while_break___0: /* CIL Label */ ;
    }
  }
  }
#line 156
  return;
}
}
#line 165 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static u8 zr36016_read_version(struct zr36016 *ptr ) 
{ u8 tmp ;
  u16 __cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  int __cil_tmp6 ;
  int __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;

  {
  {
#line 168
  __cil_tmp3 = (u16 )0;
#line 168
  tmp = zr36016_read(ptr, __cil_tmp3);
#line 168
  __cil_tmp4 = (unsigned long )ptr;
#line 168
  __cil_tmp5 = __cil_tmp4 + 48;
#line 168
  __cil_tmp6 = (int )tmp;
#line 168
  __cil_tmp7 = __cil_tmp6 >> 4;
#line 168
  *((__u8 *)__cil_tmp5) = (__u8 )__cil_tmp7;
  }
  {
#line 169
  __cil_tmp8 = (unsigned long )ptr;
#line 169
  __cil_tmp9 = __cil_tmp8 + 48;
#line 169
  return (*((__u8 *)__cil_tmp9));
  }
}
}
#line 178 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static int zr36016_basic_test(struct zr36016 *ptr ) 
{ int i ;
  u8 tmp ;
  u8 tmp___0 ;
  u8 tmp___1 ;
  int *__cil_tmp6 ;
  u16 __cil_tmp7 ;
  u8 __cil_tmp8 ;
  int *__cil_tmp9 ;
  int __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  char *__cil_tmp15 ;
  int *__cil_tmp16 ;
  int __cil_tmp17 ;
  u16 __cil_tmp18 ;
  int __cil_tmp19 ;
  int *__cil_tmp20 ;
  int __cil_tmp21 ;
  u16 __cil_tmp22 ;
  u8 __cil_tmp23 ;
  u16 __cil_tmp24 ;
  int __cil_tmp25 ;
  int *__cil_tmp26 ;
  int __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  char *__cil_tmp32 ;
  u16 __cil_tmp33 ;
  u8 __cil_tmp34 ;
  u16 __cil_tmp35 ;
  int __cil_tmp36 ;
  int *__cil_tmp37 ;
  int __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  char *__cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  __u8 __cil_tmp46 ;
  int __cil_tmp47 ;
  int *__cil_tmp48 ;
  int __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  char *__cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  unsigned long __cil_tmp56 ;
  __u8 __cil_tmp57 ;
  int __cil_tmp58 ;

  {
  {
#line 181
  __cil_tmp6 = & debug;
#line 181
  if (*__cil_tmp6) {
    {
#line 183
    __cil_tmp7 = (u16 )4;
#line 183
    __cil_tmp8 = (u8 )85;
#line 183
    zr36016_writei(ptr, __cil_tmp7, __cil_tmp8);
    }
    {
#line 184
    while (1) {
      while_continue: /* CIL Label */ ;
      {
#line 184
      __cil_tmp9 = & debug;
#line 184
      __cil_tmp10 = *__cil_tmp9;
#line 184
      if (__cil_tmp10 >= 1) {
        {
#line 184
        __cil_tmp11 = 0 * 1UL;
#line 184
        __cil_tmp12 = 0 + __cil_tmp11;
#line 184
        __cil_tmp13 = (unsigned long )ptr;
#line 184
        __cil_tmp14 = __cil_tmp13 + __cil_tmp12;
#line 184
        __cil_tmp15 = (char *)__cil_tmp14;
#line 184
        printk("<6>%s: registers: ", __cil_tmp15);
        }
      } else {

      }
      }
#line 184
      goto while_break;
    }
    while_break: /* CIL Label */ ;
    }
#line 185
    i = 0;
    {
#line 185
    while (1) {
      while_continue___0: /* CIL Label */ ;
#line 185
      if (i <= 11) {

      } else {
#line 185
        goto while_break___0;
      }
      {
#line 186
      while (1) {
        while_continue___1: /* CIL Label */ ;
        {
#line 186
        __cil_tmp16 = & debug;
#line 186
        __cil_tmp17 = *__cil_tmp16;
#line 186
        if (__cil_tmp17 >= 1) {
          {
#line 186
          __cil_tmp18 = (u16 )i;
#line 186
          tmp = zr36016_readi(ptr, __cil_tmp18);
#line 186
          __cil_tmp19 = (int )tmp;
#line 186
          printk("%02x ", __cil_tmp19);
          }
        } else {

        }
        }
#line 186
        goto while_break___1;
      }
      while_break___1: /* CIL Label */ ;
      }
#line 185
      i = i + 1;
    }
    while_break___0: /* CIL Label */ ;
    }
    {
#line 187
    while (1) {
      while_continue___2: /* CIL Label */ ;
      {
#line 187
      __cil_tmp20 = & debug;
#line 187
      __cil_tmp21 = *__cil_tmp20;
#line 187
      if (__cil_tmp21 >= 1) {
        {
#line 187
        printk("\n");
        }
      } else {

      }
      }
#line 187
      goto while_break___2;
    }
    while_break___2: /* CIL Label */ ;
    }
  } else {

  }
  }
  {
#line 191
  __cil_tmp22 = (u16 )4;
#line 191
  __cil_tmp23 = (u8 )0;
#line 191
  zr36016_writei(ptr, __cil_tmp22, __cil_tmp23);
#line 192
  __cil_tmp24 = (u16 )4;
#line 192
  tmp___0 = zr36016_readi(ptr, __cil_tmp24);
  }
  {
#line 192
  __cil_tmp25 = (int )tmp___0;
#line 192
  if (__cil_tmp25 != 0) {
    {
#line 193
    while (1) {
      while_continue___3: /* CIL Label */ ;
      {
#line 193
      __cil_tmp26 = & debug;
#line 193
      __cil_tmp27 = *__cil_tmp26;
#line 193
      if (__cil_tmp27 >= 1) {
        {
#line 193
        __cil_tmp28 = 0 * 1UL;
#line 193
        __cil_tmp29 = 0 + __cil_tmp28;
#line 193
        __cil_tmp30 = (unsigned long )ptr;
#line 193
        __cil_tmp31 = __cil_tmp30 + __cil_tmp29;
#line 193
        __cil_tmp32 = (char *)__cil_tmp31;
#line 193
        printk("<3>%s: attach failed, can\'t connect to vfe processor!\n", __cil_tmp32);
        }
      } else {

      }
      }
#line 193
      goto while_break___3;
    }
    while_break___3: /* CIL Label */ ;
    }
#line 197
    return (-6);
  } else {

  }
  }
  {
#line 199
  __cil_tmp33 = (u16 )4;
#line 199
  __cil_tmp34 = (u8 )208;
#line 199
  zr36016_writei(ptr, __cil_tmp33, __cil_tmp34);
#line 200
  __cil_tmp35 = (u16 )4;
#line 200
  tmp___1 = zr36016_readi(ptr, __cil_tmp35);
  }
  {
#line 200
  __cil_tmp36 = (int )tmp___1;
#line 200
  if (__cil_tmp36 != 208) {
    {
#line 201
    while (1) {
      while_continue___4: /* CIL Label */ ;
      {
#line 201
      __cil_tmp37 = & debug;
#line 201
      __cil_tmp38 = *__cil_tmp37;
#line 201
      if (__cil_tmp38 >= 1) {
        {
#line 201
        __cil_tmp39 = 0 * 1UL;
#line 201
        __cil_tmp40 = 0 + __cil_tmp39;
#line 201
        __cil_tmp41 = (unsigned long )ptr;
#line 201
        __cil_tmp42 = __cil_tmp41 + __cil_tmp40;
#line 201
        __cil_tmp43 = (char *)__cil_tmp42;
#line 201
        printk("<3>%s: attach failed, can\'t connect to vfe processor!\n", __cil_tmp43);
        }
      } else {

      }
      }
#line 201
      goto while_break___4;
    }
    while_break___4: /* CIL Label */ ;
    }
#line 205
    return (-6);
  } else {

  }
  }
  {
#line 208
  zr36016_read_version(ptr);
  }
  {
#line 209
  __cil_tmp44 = (unsigned long )ptr;
#line 209
  __cil_tmp45 = __cil_tmp44 + 48;
#line 209
  __cil_tmp46 = *((__u8 *)__cil_tmp45);
#line 209
  __cil_tmp47 = (int )__cil_tmp46;
#line 209
  if (__cil_tmp47 & 12) {
    {
#line 210
    while (1) {
      while_continue___5: /* CIL Label */ ;
      {
#line 210
      __cil_tmp48 = & debug;
#line 210
      __cil_tmp49 = *__cil_tmp48;
#line 210
      if (__cil_tmp49 >= 1) {
        {
#line 210
        __cil_tmp50 = 0 * 1UL;
#line 210
        __cil_tmp51 = 0 + __cil_tmp50;
#line 210
        __cil_tmp52 = (unsigned long )ptr;
#line 210
        __cil_tmp53 = __cil_tmp52 + __cil_tmp51;
#line 210
        __cil_tmp54 = (char *)__cil_tmp53;
#line 210
        __cil_tmp55 = (unsigned long )ptr;
#line 210
        __cil_tmp56 = __cil_tmp55 + 48;
#line 210
        __cil_tmp57 = *((__u8 *)__cil_tmp56);
#line 210
        __cil_tmp58 = (int )__cil_tmp57;
#line 210
        printk("<3>%s: attach failed, suspicious version %d found...\n", __cil_tmp54,
               __cil_tmp58);
        }
      } else {

      }
      }
#line 210
      goto while_break___5;
    }
    while_break___5: /* CIL Label */ ;
    }
#line 214
    return (-6);
  } else {

  }
  }
#line 217
  return (0);
}
}
#line 254 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static void zr36016_init(struct zr36016 *ptr ) 
{ int tmp ;
  int tmp___0 ;
  int tmp___1 ;
  u16 __cil_tmp5 ;
  u8 __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  int __cil_tmp9 ;
  u16 __cil_tmp10 ;
  int __cil_tmp11 ;
  u8 __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  u16 __cil_tmp17 ;
  int __cil_tmp18 ;
  int __cil_tmp19 ;
  u8 __cil_tmp20 ;
  u16 __cil_tmp21 ;
  u8 __cil_tmp22 ;
  u16 __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  __u16 __cil_tmp26 ;
  int __cil_tmp27 ;
  int __cil_tmp28 ;
  u8 __cil_tmp29 ;
  u16 __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  __u16 __cil_tmp33 ;
  int __cil_tmp34 ;
  int __cil_tmp35 ;
  u8 __cil_tmp36 ;
  u16 __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  __u16 __cil_tmp40 ;
  int __cil_tmp41 ;
  int __cil_tmp42 ;
  u8 __cil_tmp43 ;
  u16 __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  __u16 __cil_tmp47 ;
  int __cil_tmp48 ;
  int __cil_tmp49 ;
  u8 __cil_tmp50 ;
  u16 __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  __u16 __cil_tmp54 ;
  int __cil_tmp55 ;
  int __cil_tmp56 ;
  u8 __cil_tmp57 ;
  u16 __cil_tmp58 ;
  unsigned long __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  __u16 __cil_tmp61 ;
  int __cil_tmp62 ;
  int __cil_tmp63 ;
  u8 __cil_tmp64 ;
  u16 __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  __u16 __cil_tmp68 ;
  int __cil_tmp69 ;
  int __cil_tmp70 ;
  u8 __cil_tmp71 ;
  u16 __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  __u16 __cil_tmp75 ;
  int __cil_tmp76 ;
  int __cil_tmp77 ;
  u8 __cil_tmp78 ;
  u16 __cil_tmp79 ;
  u8 __cil_tmp80 ;

  {
  {
#line 258
  __cil_tmp5 = (u16 )0;
#line 258
  __cil_tmp6 = (u8 )0;
#line 258
  zr36016_write(ptr, __cil_tmp5, __cil_tmp6);
  }
  {
#line 261
  __cil_tmp7 = (unsigned long )ptr;
#line 261
  __cil_tmp8 = __cil_tmp7 + 52;
#line 261
  __cil_tmp9 = *((int *)__cil_tmp8);
#line 261
  if (__cil_tmp9 == 0) {
#line 261
    tmp = 128;
  } else {
#line 261
    tmp = 128;
  }
  }
  {
#line 261
  __cil_tmp10 = (u16 )1;
#line 261
  __cil_tmp11 = 81 | tmp;
#line 261
  __cil_tmp12 = (u8 )__cil_tmp11;
#line 261
  zr36016_write(ptr, __cil_tmp10, __cil_tmp12);
  }
  {
#line 267
  __cil_tmp13 = (unsigned long )ptr;
#line 267
  __cil_tmp14 = __cil_tmp13 + 64;
#line 267
  if (*((__u16 *)__cil_tmp14)) {
#line 267
    tmp___0 = 48;
  } else {
#line 267
    tmp___0 = 0;
  }
  }
  {
#line 267
  __cil_tmp15 = (unsigned long )ptr;
#line 267
  __cil_tmp16 = __cil_tmp15 + 66;
#line 267
  if (*((__u16 *)__cil_tmp16)) {
#line 267
    tmp___1 = 64;
  } else {
#line 267
    tmp___1 = 0;
  }
  }
  {
#line 267
  __cil_tmp17 = (u16 )0;
#line 267
  __cil_tmp18 = tmp___0 | tmp___1;
#line 267
  __cil_tmp19 = __cil_tmp18 | 1;
#line 267
  __cil_tmp20 = (u8 )__cil_tmp19;
#line 267
  zr36016_writei(ptr, __cil_tmp17, __cil_tmp20);
#line 270
  __cil_tmp21 = (u16 )1;
#line 270
  __cil_tmp22 = (u8 )4;
#line 270
  zr36016_writei(ptr, __cil_tmp21, __cil_tmp22);
#line 274
  __cil_tmp23 = (u16 )5;
#line 274
  __cil_tmp24 = (unsigned long )ptr;
#line 274
  __cil_tmp25 = __cil_tmp24 + 60;
#line 274
  __cil_tmp26 = *((__u16 *)__cil_tmp25);
#line 274
  __cil_tmp27 = (int )__cil_tmp26;
#line 274
  __cil_tmp28 = __cil_tmp27 >> 8;
#line 274
  __cil_tmp29 = (u8 )__cil_tmp28;
#line 274
  zr36016_writei(ptr, __cil_tmp23, __cil_tmp29);
#line 275
  __cil_tmp30 = (u16 )4;
#line 275
  __cil_tmp31 = (unsigned long )ptr;
#line 275
  __cil_tmp32 = __cil_tmp31 + 60;
#line 275
  __cil_tmp33 = *((__u16 *)__cil_tmp32);
#line 275
  __cil_tmp34 = (int )__cil_tmp33;
#line 275
  __cil_tmp35 = __cil_tmp34 & 255;
#line 275
  __cil_tmp36 = (u8 )__cil_tmp35;
#line 275
  zr36016_writei(ptr, __cil_tmp30, __cil_tmp36);
#line 276
  __cil_tmp37 = (u16 )9;
#line 276
  __cil_tmp38 = (unsigned long )ptr;
#line 276
  __cil_tmp39 = __cil_tmp38 + 62;
#line 276
  __cil_tmp40 = *((__u16 *)__cil_tmp39);
#line 276
  __cil_tmp41 = (int )__cil_tmp40;
#line 276
  __cil_tmp42 = __cil_tmp41 >> 8;
#line 276
  __cil_tmp43 = (u8 )__cil_tmp42;
#line 276
  zr36016_writei(ptr, __cil_tmp37, __cil_tmp43);
#line 277
  __cil_tmp44 = (u16 )8;
#line 277
  __cil_tmp45 = (unsigned long )ptr;
#line 277
  __cil_tmp46 = __cil_tmp45 + 62;
#line 277
  __cil_tmp47 = *((__u16 *)__cil_tmp46);
#line 277
  __cil_tmp48 = (int )__cil_tmp47;
#line 277
  __cil_tmp49 = __cil_tmp48 & 255;
#line 277
  __cil_tmp50 = (u8 )__cil_tmp49;
#line 277
  zr36016_writei(ptr, __cil_tmp44, __cil_tmp50);
#line 278
  __cil_tmp51 = (u16 )3;
#line 278
  __cil_tmp52 = (unsigned long )ptr;
#line 278
  __cil_tmp53 = __cil_tmp52 + 56;
#line 278
  __cil_tmp54 = *((__u16 *)__cil_tmp53);
#line 278
  __cil_tmp55 = (int )__cil_tmp54;
#line 278
  __cil_tmp56 = __cil_tmp55 >> 8;
#line 278
  __cil_tmp57 = (u8 )__cil_tmp56;
#line 278
  zr36016_writei(ptr, __cil_tmp51, __cil_tmp57);
#line 279
  __cil_tmp58 = (u16 )2;
#line 279
  __cil_tmp59 = (unsigned long )ptr;
#line 279
  __cil_tmp60 = __cil_tmp59 + 56;
#line 279
  __cil_tmp61 = *((__u16 *)__cil_tmp60);
#line 279
  __cil_tmp62 = (int )__cil_tmp61;
#line 279
  __cil_tmp63 = __cil_tmp62 & 255;
#line 279
  __cil_tmp64 = (u8 )__cil_tmp63;
#line 279
  zr36016_writei(ptr, __cil_tmp58, __cil_tmp64);
#line 280
  __cil_tmp65 = (u16 )7;
#line 280
  __cil_tmp66 = (unsigned long )ptr;
#line 280
  __cil_tmp67 = __cil_tmp66 + 58;
#line 280
  __cil_tmp68 = *((__u16 *)__cil_tmp67);
#line 280
  __cil_tmp69 = (int )__cil_tmp68;
#line 280
  __cil_tmp70 = __cil_tmp69 >> 8;
#line 280
  __cil_tmp71 = (u8 )__cil_tmp70;
#line 280
  zr36016_writei(ptr, __cil_tmp65, __cil_tmp71);
#line 281
  __cil_tmp72 = (u16 )6;
#line 281
  __cil_tmp73 = (unsigned long )ptr;
#line 281
  __cil_tmp74 = __cil_tmp73 + 58;
#line 281
  __cil_tmp75 = *((__u16 *)__cil_tmp74);
#line 281
  __cil_tmp76 = (int )__cil_tmp75;
#line 281
  __cil_tmp77 = __cil_tmp76 & 255;
#line 281
  __cil_tmp78 = (u8 )__cil_tmp77;
#line 281
  zr36016_writei(ptr, __cil_tmp72, __cil_tmp78);
#line 284
  __cil_tmp79 = (u16 )0;
#line 284
  __cil_tmp80 = (u8 )1;
#line 284
  zr36016_write(ptr, __cil_tmp79, __cil_tmp80);
  }
#line 285
  return;
}
}
#line 295 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static int zr36016_set_mode(struct videocodec *codec , int mode ) 
{ struct zr36016 *ptr ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  void *__cil_tmp6 ;
  int *__cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  char *__cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;

  {
#line 299
  __cil_tmp4 = (unsigned long )codec;
#line 299
  __cil_tmp5 = __cil_tmp4 + 72;
#line 299
  __cil_tmp6 = *((void **)__cil_tmp5);
#line 299
  ptr = (struct zr36016 *)__cil_tmp6;
  {
#line 301
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 301
    __cil_tmp7 = & debug;
#line 301
    __cil_tmp8 = *__cil_tmp7;
#line 301
    if (__cil_tmp8 >= 2) {
      {
#line 301
      __cil_tmp9 = 0 * 1UL;
#line 301
      __cil_tmp10 = 0 + __cil_tmp9;
#line 301
      __cil_tmp11 = (unsigned long )ptr;
#line 301
      __cil_tmp12 = __cil_tmp11 + __cil_tmp10;
#line 301
      __cil_tmp13 = (char *)__cil_tmp12;
#line 301
      printk("%s: set_mode %d call\n", __cil_tmp13, mode);
      }
    } else {

    }
    }
#line 301
    goto while_break;
  }
  while_break: /* CIL Label */ ;
  }
#line 303
  if (mode != 1) {
#line 303
    if (mode != 0) {
#line 304
      return (-22);
    } else {

    }
  } else {

  }
  {
#line 306
  __cil_tmp14 = (unsigned long )ptr;
#line 306
  __cil_tmp15 = __cil_tmp14 + 52;
#line 306
  *((int *)__cil_tmp15) = mode;
#line 307
  zr36016_init(ptr);
  }
#line 309
  return (0);
}
}
#line 313 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static int zr36016_set_video(struct videocodec *codec , struct tvnorm *norm , struct vfe_settings *cap ,
                             struct vfe_polarity *pol ) 
{ struct zr36016 *ptr ;
  int tmp ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  void *__cil_tmp9 ;
  int *__cil_tmp10 ;
  int __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  char *__cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  u16 __cil_tmp19 ;
  int __cil_tmp20 ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  u16 __cil_tmp23 ;
  int __cil_tmp24 ;
  __u32 __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  __u32 __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  __u32 __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  __u32 __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  __u16 __cil_tmp37 ;
  int __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  __u32 __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  unsigned long __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  __u32 __cil_tmp48 ;
  unsigned long __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  unsigned long __cil_tmp52 ;
  u16 __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  unsigned long __cil_tmp55 ;
  __u32 __cil_tmp56 ;
  __u32 __cil_tmp57 ;
  __u32 __cil_tmp58 ;
  unsigned long __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  __u32 __cil_tmp63 ;
  unsigned long __cil_tmp64 ;
  unsigned long __cil_tmp65 ;
  u16 __cil_tmp66 ;
  __u32 __cil_tmp67 ;
  __u32 __cil_tmp68 ;
  unsigned long __cil_tmp69 ;
  unsigned long __cil_tmp70 ;
  __u16 __cil_tmp71 ;
  int __cil_tmp72 ;
  int __cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  unsigned long __cil_tmp75 ;
  unsigned long __cil_tmp76 ;
  unsigned long __cil_tmp77 ;
  unsigned long __cil_tmp78 ;
  unsigned long __cil_tmp79 ;
  __u16 __cil_tmp80 ;
  int __cil_tmp81 ;
  int __cil_tmp82 ;
  int __cil_tmp83 ;
  unsigned long __cil_tmp84 ;
  unsigned long __cil_tmp85 ;
  unsigned long __cil_tmp86 ;
  unsigned long __cil_tmp87 ;

  {
#line 319
  __cil_tmp7 = (unsigned long )codec;
#line 319
  __cil_tmp8 = __cil_tmp7 + 72;
#line 319
  __cil_tmp9 = *((void **)__cil_tmp8);
#line 319
  ptr = (struct zr36016 *)__cil_tmp9;
  {
#line 321
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 321
    __cil_tmp10 = & debug;
#line 321
    __cil_tmp11 = *__cil_tmp10;
#line 321
    if (__cil_tmp11 >= 2) {
      {
#line 321
      __cil_tmp12 = 0 * 1UL;
#line 321
      __cil_tmp13 = 0 + __cil_tmp12;
#line 321
      __cil_tmp14 = (unsigned long )ptr;
#line 321
      __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
#line 321
      __cil_tmp16 = (char *)__cil_tmp15;
#line 321
      __cil_tmp17 = (unsigned long )norm;
#line 321
      __cil_tmp18 = __cil_tmp17 + 4;
#line 321
      __cil_tmp19 = *((u16 *)__cil_tmp18);
#line 321
      __cil_tmp20 = (int )__cil_tmp19;
#line 321
      __cil_tmp21 = (unsigned long )norm;
#line 321
      __cil_tmp22 = __cil_tmp21 + 12;
#line 321
      __cil_tmp23 = *((u16 *)__cil_tmp22);
#line 321
      __cil_tmp24 = (int )__cil_tmp23;
#line 321
      __cil_tmp25 = *((__u32 *)cap);
#line 321
      __cil_tmp26 = (unsigned long )cap;
#line 321
      __cil_tmp27 = __cil_tmp26 + 4;
#line 321
      __cil_tmp28 = *((__u32 *)__cil_tmp27);
#line 321
      __cil_tmp29 = (unsigned long )cap;
#line 321
      __cil_tmp30 = __cil_tmp29 + 8;
#line 321
      __cil_tmp31 = *((__u32 *)__cil_tmp30);
#line 321
      __cil_tmp32 = (unsigned long )cap;
#line 321
      __cil_tmp33 = __cil_tmp32 + 12;
#line 321
      __cil_tmp34 = *((__u32 *)__cil_tmp33);
#line 321
      __cil_tmp35 = (unsigned long )cap;
#line 321
      __cil_tmp36 = __cil_tmp35 + 16;
#line 321
      __cil_tmp37 = *((__u16 *)__cil_tmp36);
#line 321
      __cil_tmp38 = (int )__cil_tmp37;
#line 321
      printk("%s: set_video %d.%d, %d/%d-%dx%d (0x%x) call\n", __cil_tmp16, __cil_tmp20,
             __cil_tmp24, __cil_tmp25, __cil_tmp28, __cil_tmp31, __cil_tmp34, __cil_tmp38);
      }
    } else {

    }
    }
#line 321
    goto while_break;
  }
  while_break: /* CIL Label */ ;
  }
#line 329
  __cil_tmp39 = (unsigned long )ptr;
#line 329
  __cil_tmp40 = __cil_tmp39 + 60;
#line 329
  __cil_tmp41 = (unsigned long )cap;
#line 329
  __cil_tmp42 = __cil_tmp41 + 8;
#line 329
  __cil_tmp43 = *((__u32 *)__cil_tmp42);
#line 329
  *((__u16 *)__cil_tmp40) = (__u16 )__cil_tmp43;
#line 330
  __cil_tmp44 = (unsigned long )ptr;
#line 330
  __cil_tmp45 = __cil_tmp44 + 62;
#line 330
  __cil_tmp46 = (unsigned long )cap;
#line 330
  __cil_tmp47 = __cil_tmp46 + 12;
#line 330
  __cil_tmp48 = *((__u32 *)__cil_tmp47);
#line 330
  *((__u16 *)__cil_tmp45) = (__u16 )__cil_tmp48;
  {
#line 337
  __cil_tmp49 = (unsigned long )norm;
#line 337
  __cil_tmp50 = __cil_tmp49 + 4;
#line 337
  if (*((u16 *)__cil_tmp50)) {
#line 337
    __cil_tmp51 = (unsigned long )norm;
#line 337
    __cil_tmp52 = __cil_tmp51 + 4;
#line 337
    __cil_tmp53 = *((u16 *)__cil_tmp52);
#line 337
    tmp = (int )__cil_tmp53;
  } else {
#line 337
    tmp = 1;
  }
  }
#line 337
  __cil_tmp54 = (unsigned long )ptr;
#line 337
  __cil_tmp55 = __cil_tmp54 + 56;
#line 337
  __cil_tmp56 = *((__u32 *)cap);
#line 337
  __cil_tmp57 = (__u32 )tmp;
#line 337
  __cil_tmp58 = __cil_tmp57 + __cil_tmp56;
#line 337
  *((__u16 *)__cil_tmp55) = (__u16 )__cil_tmp58;
#line 342
  __cil_tmp59 = (unsigned long )ptr;
#line 342
  __cil_tmp60 = __cil_tmp59 + 58;
#line 342
  __cil_tmp61 = (unsigned long )cap;
#line 342
  __cil_tmp62 = __cil_tmp61 + 4;
#line 342
  __cil_tmp63 = *((__u32 *)__cil_tmp62);
#line 342
  __cil_tmp64 = (unsigned long )norm;
#line 342
  __cil_tmp65 = __cil_tmp64 + 12;
#line 342
  __cil_tmp66 = *((u16 *)__cil_tmp65);
#line 342
  __cil_tmp67 = (__u32 )__cil_tmp66;
#line 342
  __cil_tmp68 = __cil_tmp67 + __cil_tmp63;
#line 342
  *((__u16 *)__cil_tmp60) = (__u16 )__cil_tmp68;
  {
#line 344
  __cil_tmp69 = (unsigned long )cap;
#line 344
  __cil_tmp70 = __cil_tmp69 + 16;
#line 344
  __cil_tmp71 = *((__u16 *)__cil_tmp70);
#line 344
  __cil_tmp72 = (int )__cil_tmp71;
#line 344
  __cil_tmp73 = __cil_tmp72 & 255;
#line 344
  if (__cil_tmp73 == 1) {
#line 344
    __cil_tmp74 = (unsigned long )ptr;
#line 344
    __cil_tmp75 = __cil_tmp74 + 64;
#line 344
    *((__u16 *)__cil_tmp75) = (__u16 )0;
  } else {
#line 344
    __cil_tmp76 = (unsigned long )ptr;
#line 344
    __cil_tmp77 = __cil_tmp76 + 64;
#line 344
    *((__u16 *)__cil_tmp77) = (__u16 )1;
  }
  }
  {
#line 345
  __cil_tmp78 = (unsigned long )cap;
#line 345
  __cil_tmp79 = __cil_tmp78 + 16;
#line 345
  __cil_tmp80 = *((__u16 *)__cil_tmp79);
#line 345
  __cil_tmp81 = (int )__cil_tmp80;
#line 345
  __cil_tmp82 = __cil_tmp81 >> 8;
#line 345
  __cil_tmp83 = __cil_tmp82 & 255;
#line 345
  if (__cil_tmp83 == 1) {
#line 345
    __cil_tmp84 = (unsigned long )ptr;
#line 345
    __cil_tmp85 = __cil_tmp84 + 66;
#line 345
    *((__u16 *)__cil_tmp85) = (__u16 )0;
  } else {
#line 345
    __cil_tmp86 = (unsigned long )ptr;
#line 345
    __cil_tmp87 = __cil_tmp86 + 66;
#line 345
    *((__u16 *)__cil_tmp87) = (__u16 )1;
  }
  }
#line 347
  return (0);
}
}
#line 351 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static int zr36016_control(struct videocodec *codec , int type , int size , void *data ) 
{ struct zr36016 *ptr ;
  int *ival ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  void *__cil_tmp9 ;
  int *__cil_tmp10 ;
  int __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  char *__cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  int __cil_tmp20 ;

  {
#line 357
  __cil_tmp7 = (unsigned long )codec;
#line 357
  __cil_tmp8 = __cil_tmp7 + 72;
#line 357
  __cil_tmp9 = *((void **)__cil_tmp8);
#line 357
  ptr = (struct zr36016 *)__cil_tmp9;
#line 358
  ival = (int *)data;
  {
#line 360
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 360
    __cil_tmp10 = & debug;
#line 360
    __cil_tmp11 = *__cil_tmp10;
#line 360
    if (__cil_tmp11 >= 2) {
      {
#line 360
      __cil_tmp12 = 0 * 1UL;
#line 360
      __cil_tmp13 = 0 + __cil_tmp12;
#line 360
      __cil_tmp14 = (unsigned long )ptr;
#line 360
      __cil_tmp15 = __cil_tmp14 + __cil_tmp13;
#line 360
      __cil_tmp16 = (char *)__cil_tmp15;
#line 360
      printk("%s: control %d call with %d byte\n", __cil_tmp16, type, size);
      }
    } else {

    }
    }
#line 360
    goto while_break;
  }
  while_break: /* CIL Label */ ;
  }
#line 364
  if (type == 0) {
#line 364
    goto case_0;
  } else
#line 370
  if (type == 32769) {
#line 370
    goto case_32769;
  } else
#line 376
  if (type == 1) {
#line 376
    goto case_1;
  } else
#line 384
  if (type == 32770) {
#line 384
    goto case_32770;
  } else
#line 385
  if (type == 2) {
#line 385
    goto case_32770;
  } else
#line 388
  if (type == 3) {
#line 388
    goto case_3;
  } else {
    {
#line 392
    goto switch_default;
#line 363
    if (0) {
      case_0: /* CIL Label */ 
      {
#line 365
      __cil_tmp17 = (unsigned long )size;
#line 365
      if (__cil_tmp17 != 4UL) {
#line 366
        return (-14);
      } else {

      }
      }
#line 367
      *ival = 0;
#line 368
      goto switch_break;
      case_32769: /* CIL Label */ 
      {
#line 371
      __cil_tmp18 = (unsigned long )size;
#line 371
      if (__cil_tmp18 != 4UL) {
#line 372
        return (-14);
      } else {

      }
      }
#line 373
      *ival = 0;
#line 374
      goto switch_break;
      case_1: /* CIL Label */ 
      {
#line 377
      __cil_tmp19 = (unsigned long )size;
#line 377
      if (__cil_tmp19 != 4UL) {
#line 378
        return (-14);
      } else {

      }
      }
      {
#line 379
      __cil_tmp20 = *ival;
#line 379
      if (__cil_tmp20 != 0) {
#line 380
        return (-22);
      } else {

      }
      }
#line 382
      return (0);
      case_32770: /* CIL Label */ 
      case_2: /* CIL Label */ 
#line 386
      return (0);
      case_3: /* CIL Label */ 
#line 390
      return (-6);
      switch_default: /* CIL Label */ 
#line 393
      return (-22);
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
#line 396
  return (size);
}
}
#line 405 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static int zr36016_unset(struct videocodec *codec ) 
{ struct zr36016 *ptr ;
  unsigned long __cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  void *__cil_tmp5 ;
  int *__cil_tmp6 ;
  int __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  char *__cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  int __cil_tmp15 ;
  void const   *__cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;

  {
#line 408
  __cil_tmp3 = (unsigned long )codec;
#line 408
  __cil_tmp4 = __cil_tmp3 + 72;
#line 408
  __cil_tmp5 = *((void **)__cil_tmp4);
#line 408
  ptr = (struct zr36016 *)__cil_tmp5;
#line 410
  if (ptr) {
    {
#line 413
    while (1) {
      while_continue: /* CIL Label */ ;
      {
#line 413
      __cil_tmp6 = & debug;
#line 413
      __cil_tmp7 = *__cil_tmp6;
#line 413
      if (__cil_tmp7 >= 1) {
        {
#line 413
        __cil_tmp8 = 0 * 1UL;
#line 413
        __cil_tmp9 = 0 + __cil_tmp8;
#line 413
        __cil_tmp10 = (unsigned long )ptr;
#line 413
        __cil_tmp11 = __cil_tmp10 + __cil_tmp9;
#line 413
        __cil_tmp12 = (char *)__cil_tmp11;
#line 413
        __cil_tmp13 = (unsigned long )ptr;
#line 413
        __cil_tmp14 = __cil_tmp13 + 32;
#line 413
        __cil_tmp15 = *((int *)__cil_tmp14);
#line 413
        printk("%s: finished codec #%d\n", __cil_tmp12, __cil_tmp15);
        }
      } else {

      }
      }
#line 413
      goto while_break;
    }
    while_break: /* CIL Label */ ;
    }
    {
#line 415
    __cil_tmp16 = (void const   *)ptr;
#line 415
    kfree(__cil_tmp16);
#line 416
    __cil_tmp17 = (unsigned long )codec;
#line 416
    __cil_tmp18 = __cil_tmp17 + 72;
#line 416
    *((void **)__cil_tmp18) = (void *)0;
#line 418
    zr36016_codecs = zr36016_codecs - 1;
    }
#line 419
    return (0);
  } else {

  }
#line 422
  return (-14);
}
}
#line 434 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static int zr36016_setup(struct videocodec *codec ) 
{ struct zr36016 *ptr ;
  int res ;
  void *tmp ;
  int tmp___0 ;
  int *__cil_tmp6 ;
  int __cil_tmp7 ;
  int *__cil_tmp8 ;
  int __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  void *__cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  int *__cil_tmp15 ;
  int __cil_tmp16 ;
  unsigned long __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  char *__cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  unsigned long __cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  unsigned long __cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  unsigned long __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  int *__cil_tmp36 ;
  int __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  unsigned long __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  char *__cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  __u8 __cil_tmp45 ;
  int __cil_tmp46 ;

  {
  {
#line 440
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 440
    __cil_tmp6 = & debug;
#line 440
    __cil_tmp7 = *__cil_tmp6;
#line 440
    if (__cil_tmp7 >= 2) {
      {
#line 440
      printk("zr36016: initializing VFE subsystem #%d.\n", zr36016_codecs);
      }
    } else {

    }
    }
#line 440
    goto while_break;
  }
  while_break: /* CIL Label */ ;
  }
#line 443
  if (zr36016_codecs == 20) {
    {
#line 444
    while (1) {
      while_continue___0: /* CIL Label */ ;
      {
#line 444
      __cil_tmp8 = & debug;
#line 444
      __cil_tmp9 = *__cil_tmp8;
#line 444
      if (__cil_tmp9 >= 1) {
        {
#line 444
        printk("<3>zr36016: Can\'t attach more codecs!\n");
        }
      } else {

      }
      }
#line 444
      goto while_break___0;
    }
    while_break___0: /* CIL Label */ ;
    }
#line 446
    return (-28);
  } else {

  }
  {
#line 449
  tmp = kzalloc(72UL, 208U);
#line 449
  ptr = (struct zr36016 *)tmp;
#line 449
  __cil_tmp10 = (unsigned long )codec;
#line 449
  __cil_tmp11 = __cil_tmp10 + 72;
#line 449
  *((void **)__cil_tmp11) = (void *)ptr;
  }
  {
#line 450
  __cil_tmp12 = (unsigned long )ptr;
#line 450
  __cil_tmp13 = (void *)0;
#line 450
  __cil_tmp14 = (unsigned long )__cil_tmp13;
#line 450
  if (__cil_tmp14 == __cil_tmp12) {
    {
#line 451
    while (1) {
      while_continue___1: /* CIL Label */ ;
      {
#line 451
      __cil_tmp15 = & debug;
#line 451
      __cil_tmp16 = *__cil_tmp15;
#line 451
      if (__cil_tmp16 >= 1) {
        {
#line 451
        printk("<3>zr36016: Can\'t get enough memory!\n");
        }
      } else {

      }
      }
#line 451
      goto while_break___1;
    }
    while_break___1: /* CIL Label */ ;
    }
#line 452
    return (-12);
  } else {

  }
  }
  {
#line 455
  __cil_tmp17 = 0 * 1UL;
#line 455
  __cil_tmp18 = 0 + __cil_tmp17;
#line 455
  __cil_tmp19 = (unsigned long )ptr;
#line 455
  __cil_tmp20 = __cil_tmp19 + __cil_tmp18;
#line 455
  __cil_tmp21 = (char *)__cil_tmp20;
#line 455
  snprintf(__cil_tmp21, 32UL, "zr36016[%d]", zr36016_codecs);
#line 457
  tmp___0 = zr36016_codecs;
#line 457
  zr36016_codecs = zr36016_codecs + 1;
#line 457
  __cil_tmp22 = (unsigned long )ptr;
#line 457
  __cil_tmp23 = __cil_tmp22 + 32;
#line 457
  *((int *)__cil_tmp23) = tmp___0;
#line 458
  __cil_tmp24 = (unsigned long )ptr;
#line 458
  __cil_tmp25 = __cil_tmp24 + 40;
#line 458
  *((struct videocodec **)__cil_tmp25) = codec;
#line 461
  res = zr36016_basic_test(ptr);
  }
#line 462
  if (res < 0) {
    {
#line 463
    zr36016_unset(codec);
    }
#line 464
    return (res);
  } else {

  }
  {
#line 467
  __cil_tmp26 = (unsigned long )ptr;
#line 467
  __cil_tmp27 = __cil_tmp26 + 52;
#line 467
  *((int *)__cil_tmp27) = 0;
#line 468
  __cil_tmp28 = (unsigned long )ptr;
#line 468
  __cil_tmp29 = __cil_tmp28 + 60;
#line 468
  *((__u16 *)__cil_tmp29) = (__u16 )768;
#line 469
  __cil_tmp30 = (unsigned long )ptr;
#line 469
  __cil_tmp31 = __cil_tmp30 + 62;
#line 469
  *((__u16 *)__cil_tmp31) = (__u16 )288;
#line 470
  __cil_tmp32 = (unsigned long )ptr;
#line 470
  __cil_tmp33 = __cil_tmp32 + 64;
#line 470
  *((__u16 *)__cil_tmp33) = (__u16 )1;
#line 471
  __cil_tmp34 = (unsigned long )ptr;
#line 471
  __cil_tmp35 = __cil_tmp34 + 66;
#line 471
  *((__u16 *)__cil_tmp35) = (__u16 )0;
#line 472
  zr36016_init(ptr);
  }
  {
#line 474
  while (1) {
    while_continue___2: /* CIL Label */ ;
    {
#line 474
    __cil_tmp36 = & debug;
#line 474
    __cil_tmp37 = *__cil_tmp36;
#line 474
    if (__cil_tmp37 >= 1) {
      {
#line 474
      __cil_tmp38 = 0 * 1UL;
#line 474
      __cil_tmp39 = 0 + __cil_tmp38;
#line 474
      __cil_tmp40 = (unsigned long )ptr;
#line 474
      __cil_tmp41 = __cil_tmp40 + __cil_tmp39;
#line 474
      __cil_tmp42 = (char *)__cil_tmp41;
#line 474
      __cil_tmp43 = (unsigned long )ptr;
#line 474
      __cil_tmp44 = __cil_tmp43 + 48;
#line 474
      __cil_tmp45 = *((__u8 *)__cil_tmp44);
#line 474
      __cil_tmp46 = (int )__cil_tmp45;
#line 474
      printk("<6>%s: codec v%d attached and running\n", __cil_tmp42, __cil_tmp46);
      }
    } else {

    }
    }
#line 474
    goto while_break___2;
  }
  while_break___2: /* CIL Label */ ;
  }
#line 477
  return (0);
}
}
#line 480 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static struct videocodec  const  zr36016_codec  = 
#line 480
     {& __this_module, {(char )'z', (char )'r', (char )'3', (char )'6', (char )'0',
                      (char )'1', (char )'6', (char )'\000'}, 0UL, 61440UL, 3U, (struct videocodec_master *)0,
    (void *)0, & zr36016_setup, & zr36016_unset, & zr36016_set_mode, & zr36016_set_video,
    & zr36016_control, (int (*)(struct videocodec *codec , long mode ))0, (int (*)(struct videocodec *codec ,
                                                                                   int source ,
                                                                                   long flag ))0,
    (long (*)(struct videocodec *codec , int tr_type , int block , long *fr_num ,
              long *flag , long size , void *buf ))0, (long (*)(struct videocodec *codec ,
                                                                int tr_type , int block ,
                                                                long *fr_num , long *flag ,
                                                                long size , void *buf ))0};
#line 500
static int zr36016_init_module(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
#line 500 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static int zr36016_init_module(void) 
{ int tmp ;

  {
  {
#line 504
  zr36016_codecs = 0;
#line 505
  tmp = videocodec_register(& zr36016_codec);
  }
#line 505
  return (tmp);
}
}
#line 508
static void zr36016_cleanup_module(void)  __attribute__((__section__(".exit.text"),
__no_instrument_function__)) ;
#line 508 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static void zr36016_cleanup_module(void) 
{ int *__cil_tmp1 ;
  int __cil_tmp2 ;

  {
#line 511
  if (zr36016_codecs) {
    {
#line 512
    while (1) {
      while_continue: /* CIL Label */ ;
      {
#line 512
      __cil_tmp1 = & debug;
#line 512
      __cil_tmp2 = *__cil_tmp1;
#line 512
      if (__cil_tmp2 >= 1) {
        {
#line 512
        printk("zr36016: something\'s wrong - %d codecs left somehow.\n", zr36016_codecs);
        }
      } else {

      }
      }
#line 512
      goto while_break;
    }
    while_break: /* CIL Label */ ;
    }
  } else {

  }
  {
#line 516
  videocodec_unregister(& zr36016_codec);
  }
#line 517
  return;
}
}
#line 519 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
int init_module(void) 
{ int tmp ;

  {
  {
#line 519
  tmp = zr36016_init_module();
  }
#line 519
  return (tmp);
}
}
#line 520 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
void cleanup_module(void) 
{ 

  {
  {
#line 520
  zr36016_cleanup_module();
  }
#line 520
  return;
}
}
#line 522 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static char const   __mod_author522[43]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 522
  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'W', 
        (char const   )'o',      (char const   )'l',      (char const   )'f',      (char const   )'g', 
        (char const   )'a',      (char const   )'n',      (char const   )'g',      (char const   )' ', 
        (char const   )'S',      (char const   )'c',      (char const   )'h',      (char const   )'e', 
        (char const   )'r',      (char const   )'r',      (char const   )' ',      (char const   )'<', 
        (char const   )'s',      (char const   )'c',      (char const   )'h',      (char const   )'e', 
        (char const   )'r',      (char const   )'r',      (char const   )'@',      (char const   )'n', 
        (char const   )'e',      (char const   )'t',      (char const   )'4',      (char const   )'y', 
        (char const   )'o',      (char const   )'u',      (char const   )'.',      (char const   )'a', 
        (char const   )'t',      (char const   )'>',      (char const   )'\000'};
#line 523 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static char const   __mod_description524[59]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 523
  {      (char const   )'d',      (char const   )'e',      (char const   )'s',      (char const   )'c', 
        (char const   )'r',      (char const   )'i',      (char const   )'p',      (char const   )'t', 
        (char const   )'i',      (char const   )'o',      (char const   )'n',      (char const   )'=', 
        (char const   )'D',      (char const   )'r',      (char const   )'i',      (char const   )'v', 
        (char const   )'e',      (char const   )'r',      (char const   )' ',      (char const   )'m', 
        (char const   )'o',      (char const   )'d',      (char const   )'u',      (char const   )'l', 
        (char const   )'e',      (char const   )' ',      (char const   )'f',      (char const   )'o', 
        (char const   )'r',      (char const   )' ',      (char const   )'Z',      (char const   )'R', 
        (char const   )'3',      (char const   )'6',      (char const   )'0',      (char const   )'1', 
        (char const   )'6',      (char const   )' ',      (char const   )'v',      (char const   )'i', 
        (char const   )'d',      (char const   )'e',      (char const   )'o',      (char const   )' ', 
        (char const   )'f',      (char const   )'r',      (char const   )'o',      (char const   )'n', 
        (char const   )'t',      (char const   )'e',      (char const   )'n',      (char const   )'d', 
        (char const   )'s',      (char const   )' ',      (char const   )'v',      (char const   )'0', 
        (char const   )'.',      (char const   )'7',      (char const   )'\000'};
#line 525 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
static char const   __mod_license525[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 525
  {      (char const   )'l',      (char const   )'i',      (char const   )'c',      (char const   )'e', 
        (char const   )'n',      (char const   )'s',      (char const   )'e',      (char const   )'=', 
        (char const   )'G',      (char const   )'P',      (char const   )'L',      (char const   )'\000'};
#line 543
void ldv_check_final_state(void) ;
#line 549
extern void ldv_initialize(void) ;
#line 552
extern int __VERIFIER_nondet_int(void) ;
#line 555 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
int LDV_IN_INTERRUPT  ;
#line 558 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
void main(void) 
{ struct videocodec *var_group1 ;
  int var_zr36016_set_mode_8_p1 ;
  struct tvnorm *var_group2 ;
  struct vfe_settings *var_zr36016_set_video_9_p2 ;
  struct vfe_polarity *var_zr36016_set_video_9_p3 ;
  int var_zr36016_control_10_p1 ;
  int var_zr36016_control_10_p2 ;
  void *var_zr36016_control_10_p3 ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
  {
#line 648
  LDV_IN_INTERRUPT = 1;
#line 657
  ldv_initialize();
#line 673
  tmp = zr36016_init_module();
  }
#line 673
  if (tmp) {
#line 674
    goto ldv_final;
  } else {

  }
  {
#line 678
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 678
    tmp___1 = __VERIFIER_nondet_int();
    }
#line 678
    if (tmp___1) {

    } else {
#line 678
      goto while_break;
    }
    {
#line 681
    tmp___0 = __VERIFIER_nondet_int();
    }
#line 683
    if (tmp___0 == 0) {
#line 683
      goto case_0;
    } else
#line 709
    if (tmp___0 == 1) {
#line 709
      goto case_1;
    } else
#line 735
    if (tmp___0 == 2) {
#line 735
      goto case_2;
    } else
#line 761
    if (tmp___0 == 3) {
#line 761
      goto case_3;
    } else
#line 787
    if (tmp___0 == 4) {
#line 787
      goto case_4;
    } else {
      {
#line 813
      goto switch_default;
#line 681
      if (0) {
        case_0: /* CIL Label */ 
        {
#line 701
        zr36016_setup(var_group1);
        }
#line 708
        goto switch_break;
        case_1: /* CIL Label */ 
        {
#line 727
        zr36016_unset(var_group1);
        }
#line 734
        goto switch_break;
        case_2: /* CIL Label */ 
        {
#line 753
        zr36016_set_mode(var_group1, var_zr36016_set_mode_8_p1);
        }
#line 760
        goto switch_break;
        case_3: /* CIL Label */ 
        {
#line 779
        zr36016_set_video(var_group1, var_group2, var_zr36016_set_video_9_p2, var_zr36016_set_video_9_p3);
        }
#line 786
        goto switch_break;
        case_4: /* CIL Label */ 
        {
#line 805
        zr36016_control(var_group1, var_zr36016_control_10_p1, var_zr36016_control_10_p2,
                        var_zr36016_control_10_p3);
        }
#line 812
        goto switch_break;
        switch_default: /* CIL Label */ 
#line 813
        goto switch_break;
      } else {
        switch_break: /* CIL Label */ ;
      }
      }
    }
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 835
  zr36016_cleanup_module();
  }
  ldv_final: 
  {
#line 838
  ldv_check_final_state();
  }
#line 841
  return;
}
}
#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
void ldv_blast_assert(void) 
{ 

  {
  ERROR: 
#line 6
  goto ERROR;
}
}
#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
extern int __VERIFIER_nondet_int(void) ;
#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int ldv_mutex  =    1;
#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int __attribute__((__warn_unused_result__))  mutex_lock_interruptible(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 29
  if (ldv_mutex == 1) {

  } else {
    {
#line 29
    ldv_blast_assert();
    }
  }
  {
#line 32
  nondetermined = __VERIFIER_nondet_int();
  }
#line 35
  if (nondetermined) {
#line 38
    ldv_mutex = 2;
#line 40
    return (0);
  } else {
#line 45
    return (-4);
  }
}
}
#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int __attribute__((__warn_unused_result__))  mutex_lock_killable(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 57
  if (ldv_mutex == 1) {

  } else {
    {
#line 57
    ldv_blast_assert();
    }
  }
  {
#line 60
  nondetermined = __VERIFIER_nondet_int();
  }
#line 63
  if (nondetermined) {
#line 66
    ldv_mutex = 2;
#line 68
    return (0);
  } else {
#line 73
    return (-4);
  }
}
}
#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) 
{ int atomic_value_after_dec ;

  {
#line 83
  if (ldv_mutex == 1) {

  } else {
    {
#line 83
    ldv_blast_assert();
    }
  }
  {
#line 86
  atomic_value_after_dec = __VERIFIER_nondet_int();
  }
#line 89
  if (atomic_value_after_dec == 0) {
#line 92
    ldv_mutex = 2;
#line 94
    return (1);
  } else {

  }
#line 98
  return (0);
}
}
#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void mutex_lock(struct mutex *lock ) 
{ 

  {
#line 108
  if (ldv_mutex == 1) {

  } else {
    {
#line 108
    ldv_blast_assert();
    }
  }
#line 110
  ldv_mutex = 2;
#line 111
  return;
}
}
#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
int mutex_trylock(struct mutex *lock ) 
{ int nondetermined ;

  {
#line 121
  if (ldv_mutex == 1) {

  } else {
    {
#line 121
    ldv_blast_assert();
    }
  }
  {
#line 124
  nondetermined = __VERIFIER_nondet_int();
  }
#line 127
  if (nondetermined) {
#line 130
    ldv_mutex = 2;
#line 132
    return (1);
  } else {
#line 137
    return (0);
  }
}
}
#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void mutex_unlock(struct mutex *lock ) 
{ 

  {
#line 147
  if (ldv_mutex == 2) {

  } else {
    {
#line 147
    ldv_blast_assert();
    }
  }
#line 149
  ldv_mutex = 1;
#line 150
  return;
}
}
#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
void ldv_check_final_state(void) 
{ 

  {
#line 156
  if (ldv_mutex == 1) {

  } else {
    {
#line 156
    ldv_blast_assert();
    }
  }
#line 157
  return;
}
}
#line 850 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/14424/dscv_tempdir/dscv/ri/32_1/drivers/media/video/zoran/zr36016.c.common.c"
long s__builtin_expect(long val , long res ) 
{ 

  {
#line 851
  return (val);
}
}