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 221 "include/linux/types.h"
  struct __anonstruct_atomic_t_6 {
     int counter ;
  };
  #line 221 "include/linux/types.h"
  typedef struct __anonstruct_atomic_t_6 atomic_t;
  #line 226 "include/linux/types.h"
  struct __anonstruct_atomic64_t_7 {
     long counter ;
  };
  #line 226 "include/linux/types.h"
  typedef struct __anonstruct_atomic64_t_7 atomic64_t;
  #line 227 "include/linux/types.h"
  struct list_head {
     struct list_head *next ;
     struct list_head *prev ;
  };
  #line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
  struct module;
  #line 55
  struct module;
  #line 146 "include/linux/init.h"
  typedef void (*ctor_fn_t)(void);
  #line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
  struct page;
  #line 58
  struct page;
  #line 26 "include/asm-generic/getorder.h"
  struct task_struct;
  #line 26
  struct task_struct;
  #line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  struct arch_spinlock;
  #line 327
  struct arch_spinlock;
  #line 306 "include/linux/bitmap.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 16 "/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 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
  union __anonunion_ldv_5907_29 {
     __ticketpair_t head_tail ;
     struct __raw_tickets tickets ;
  };
 #line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
 struct arch_spinlock {
    union __anonunion_ldv_5907_29 ldv_5907 ;
 };
 #line 27 "/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 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
 struct lockdep_map;
 #line 34
 struct lockdep_map;
 #line 55 "include/linux/debug_locks.h"
 struct stack_trace {
    unsigned int nr_entries ;
    unsigned int max_entries ;
    unsigned long *entries ;
    int skip ;
 };
 #line 26 "include/linux/stacktrace.h"
 struct lockdep_subclass_key {
    char __one_byte ;
 };
 #line 53 "include/linux/lockdep.h"
 struct lock_class_key {
    struct lockdep_subclass_key subkeys[8U] ;
 };
 #line 59 "include/linux/lockdep.h"
 struct lock_class {
    struct list_head hash_entry ;
    struct list_head lock_entry ;
    struct lockdep_subclass_key *key ;
    unsigned int subclass ;
    unsigned int dep_gen_id ;
    unsigned long usage_mask ;
    struct stack_trace usage_traces[13U] ;
    struct list_head locks_after ;
    struct list_head locks_before ;
    unsigned int version ;
    unsigned long ops ;
    char const   *name ;
    int name_version ;
    unsigned long contention_point[4U] ;
    unsigned long contending_point[4U] ;
 };
 #line 144 "include/linux/lockdep.h"
 struct lockdep_map {
    struct lock_class_key *key ;
    struct lock_class *class_cache[2U] ;
    char const   *name ;
    int cpu ;
    unsigned long ip ;
 };
 #line 556 "include/linux/lockdep.h"
 struct raw_spinlock {
    arch_spinlock_t raw_lock ;
    unsigned int magic ;
    unsigned int owner_cpu ;
    void *owner ;
    struct lockdep_map dep_map ;
 };
 #line 33 "include/linux/spinlock_types.h"
 struct __anonstruct_ldv_6122_33 {
    u8 __padding[24U] ;
    struct lockdep_map dep_map ;
 };
 #line 33 "include/linux/spinlock_types.h"
 union __anonunion_ldv_6123_32 {
    struct raw_spinlock rlock ;
    struct __anonstruct_ldv_6122_33 ldv_6122 ;
 };
 #line 33 "include/linux/spinlock_types.h"
 struct spinlock {
    union __anonunion_ldv_6123_32 ldv_6123 ;
 };
 #line 76 "include/linux/spinlock_types.h"
 typedef struct spinlock spinlock_t;
 #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 193 "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 201 "include/linux/elf.h"
 typedef struct elf64_sym Elf64_Sym;
 #line 445
 struct sock;
 #line 445
 struct sock;
 #line 446
 struct kobject;
 #line 446
 struct kobject;
 #line 447
 enum kobj_ns_type {
     KOBJ_NS_TYPE_NONE = 0,
     KOBJ_NS_TYPE_NET = 1,
     KOBJ_NS_TYPES = 2
 } ;
 #line 453 "include/linux/elf.h"
 struct kobj_ns_type_operations {
    enum kobj_ns_type type ;
    void *(*grab_current_ns)(void) ;
    void const   *(*netlink_ns)(struct sock * ) ;
    void const   *(*initial_ns)(void) ;
    void (*drop_ns)(void * ) ;
 };
 #line 57 "include/linux/kobject_ns.h"
 struct attribute {
    char const   *name ;
    umode_t mode ;
    struct lock_class_key *key ;
    struct lock_class_key skey ;
 };
 #line 98 "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 117
 struct sysfs_dirent;
 #line 117
 struct sysfs_dirent;
 #line 182 "include/linux/sysfs.h"
 struct kref {
    atomic_t refcount ;
 };
 #line 49 "include/linux/kobject.h"
 struct kset;
 #line 49
 struct kobj_type;
 #line 49 "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 char state_initialized : 1 ;
    unsigned char state_in_sysfs : 1 ;
    unsigned char state_add_uevent_sent : 1 ;
    unsigned char state_remove_uevent_sent : 1 ;
    unsigned char uevent_suppress : 1 ;
 };
 #line 107 "include/linux/kobject.h"
 struct kobj_type {
    void (*release)(struct kobject * ) ;
    struct sysfs_ops  const  *sysfs_ops ;
    struct attribute **default_attrs ;
    struct kobj_ns_type_operations  const  *(*child_ns_type)(struct kobject * ) ;
    void const   *(*namespace)(struct kobject * ) ;
 };
 #line 115 "include/linux/kobject.h"
 struct kobj_uevent_env {
    char *envp[32U] ;
    int envp_idx ;
    char buf[2048U] ;
    int buflen ;
 };
 #line 122 "include/linux/kobject.h"
 struct kset_uevent_ops {
    int (* const  filter)(struct kset * , struct kobject * ) ;
    char const   *(* const  name)(struct kset * , struct kobject * ) ;
    int (* const  uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
 };
 #line 139 "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 215
 struct kernel_param;
 #line 215
 struct kernel_param;
 #line 216 "include/linux/kobject.h"
 struct kernel_param_ops {
    int (*set)(char const   * , struct kernel_param  const  * ) ;
    int (*get)(char * , struct kernel_param  const  * ) ;
    void (*free)(void * ) ;
 };
 #line 49 "include/linux/moduleparam.h"
 struct kparam_string;
 #line 49
 struct kparam_array;
 #line 49 "include/linux/moduleparam.h"
 union __anonunion_ldv_13363_134 {
    void *arg ;
    struct kparam_string  const  *str ;
    struct kparam_array  const  *arr ;
 };
 #line 49 "include/linux/moduleparam.h"
 struct kernel_param {
    char const   *name ;
    struct kernel_param_ops  const  *ops ;
    u16 perm ;
    s16 level ;
    union __anonunion_ldv_13363_134 ldv_13363 ;
 };
 #line 61 "include/linux/moduleparam.h"
 struct kparam_string {
    unsigned int maxlen ;
    char *string ;
 };
 #line 67 "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 458 "include/linux/moduleparam.h"
 struct static_key {
    atomic_t enabled ;
 };
 #line 225 "include/linux/jump_label.h"
 struct tracepoint;
 #line 225
 struct tracepoint;
 #line 226 "include/linux/jump_label.h"
 struct tracepoint_func {
    void *func ;
    void *data ;
 };
 #line 29 "include/linux/tracepoint.h"
 struct tracepoint {
    char const   *name ;
    struct static_key key ;
    void (*regfunc)(void) ;
    void (*unregfunc)(void) ;
    struct tracepoint_func *funcs ;
 };
 #line 86 "include/linux/tracepoint.h"
 struct kernel_symbol {
    unsigned long value ;
    char const   *name ;
 };
 #line 27 "include/linux/export.h"
 struct mod_arch_specific {
 
 };
 #line 34 "include/linux/module.h"
 struct module_param_attrs;
 #line 34 "include/linux/module.h"
 struct module_kobject {
    struct kobject kobj ;
    struct module *mod ;
    struct kobject *drivers_dir ;
    struct module_param_attrs *mp ;
 };
 #line 43 "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  ) ;
    void (*setup)(struct module * , char const   * ) ;
    int (*test)(struct module * ) ;
    void (*free)(struct module * ) ;
 };
 #line 69
 struct exception_table_entry;
 #line 69
 struct exception_table_entry;
 #line 198
 enum module_state {
     MODULE_STATE_LIVE = 0,
     MODULE_STATE_COMING = 1,
     MODULE_STATE_GOING = 2
 } ;
 #line 204 "include/linux/module.h"
 struct module_ref {
    unsigned long incs ;
    unsigned long decs ;
 };
 #line 219
 struct module_sect_attrs;
 #line 219
 struct module_notes_attrs;
 #line 219
 struct ftrace_event_call;
 #line 219 "include/linux/module.h"
 struct module {
    enum module_state state ;
    struct list_head list ;
    char name[56U] ;
    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)(void) ;
    unsigned int num_ctors ;
 };
 #line 88 "include/linux/kmemleak.h"
 struct kmem_cache_cpu {
    void **freelist ;
    unsigned long tid ;
    struct page *page ;
    struct page *partial ;
    int node ;
    unsigned int stat[26U] ;
 };
 #line 55 "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 66 "include/linux/slub_def.h"
 struct kmem_cache_order_objects {
    unsigned long x ;
 };
 #line 76 "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[1024U] ;
 };
 #line 54 "include/linux/delay.h"
 struct videocodec;
 #line 54 "include/linux/delay.h"
 struct zr36016 {
    char name[32U] ;
    int num ;
    struct videocodec *codec ;
    __u8 version ;
    int mode ;
    __u16 xoff ;
    __u16 yoff ;
    __u16 width ;
    __u16 height ;
    __u16 xdec ;
    __u16 ydec ;
 };
 #line 2306 "include/linux/videodev2.h"
 struct vfe_polarity {
    unsigned char vsync_pol : 1 ;
    unsigned char hsync_pol : 1 ;
    unsigned char field_pol : 1 ;
    unsigned char blank_pol : 1 ;
    unsigned char subimg_pol : 1 ;
    unsigned char poe_pol : 1 ;
    unsigned char pvalid_pol : 1 ;
    unsigned char vclk_pol : 1 ;
 };
 #line 233 "/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 241 "/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 256
 struct videocodec_master;
 #line 256 "/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[32U] ;
    unsigned long magic ;
    unsigned long flags ;
    unsigned int type ;
    struct videocodec_master *master_data ;
    void *data ;
    int (*setup)(struct videocodec * ) ;
    int (*unset)(struct videocodec * ) ;
    int (*set_mode)(struct videocodec * , int  ) ;
    int (*set_video)(struct videocodec * , struct tvnorm * , struct vfe_settings * ,
                     struct vfe_polarity * ) ;
    int (*control)(struct videocodec * , int  , int  , void * ) ;
    int (*setup_interrupt)(struct videocodec * , long  ) ;
    int (*handle_interrupt)(struct videocodec * , int  , long  ) ;
    long (*put_image)(struct videocodec * , int  , int  , long * , long * , long  ,
                      void * ) ;
    long (*get_image)(struct videocodec * , int  , int  , long * , long * , long  ,
                      void * ) ;
 };
 #line 309 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/media/video/zoran/videocodec.h"
 struct videocodec_master {
    char name[32U] ;
    unsigned long magic ;
    unsigned long flags ;
    unsigned int type ;
    void *data ;
    __u32 (*readreg)(struct videocodec * , __u16  ) ;
    void (*writereg)(struct videocodec * , __u16  , __u32  ) ;
 };
 #line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
 void ldv_spin_lock(void) ;
 #line 3
 void ldv_spin_unlock(void) ;
 #line 4
 int ldv_spin_trylock(void) ;
 #line 101 "include/linux/printk.h"
 extern int printk(char const   *  , ...) ;
 #line 323 "include/linux/kernel.h"
 extern int snprintf(char * , size_t  , char const   *  , ...) ;
 #line 26 "include/linux/export.h"
 extern struct module __this_module ;
 #line 161 "include/linux/slab.h"
 extern void kfree(void const   * ) ;
 #line 220 "include/linux/slub_def.h"
 extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t  ) ;
 #line 223
 void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
 #line 353 "include/linux/slab.h"
 __inline static void *kzalloc(size_t size , gfp_t flags ) ;
 #line 10 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
 extern void *__VERIFIER_nondet_pointer(void) ;
 #line 11
 void ldv_check_alloc_flags(gfp_t flags ) ;
 #line 12
 void ldv_check_alloc_nonatomic(void) ;
 #line 14
 struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
 #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 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
 static int zr36016_codecs  ;
 #line 71 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
 static int debug  ;
 #line 89 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
 static u8 zr36016_read(struct zr36016 *ptr , u16 reg ) 
 { u8 value ;
   __u32 tmp ;
   __u32 (*__cil_tmp5)(struct videocodec * , __u16  ) ;
   unsigned long __cil_tmp6 ;
   unsigned long __cil_tmp7 ;
   unsigned long __cil_tmp8 ;
   struct videocodec *__cil_tmp9 ;
   unsigned long __cil_tmp10 ;
   unsigned long __cil_tmp11 ;
   struct videocodec_master *__cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   __u32 (*__cil_tmp15)(struct videocodec * , __u16  ) ;
   unsigned long __cil_tmp16 ;
   unsigned long __cil_tmp17 ;
   unsigned long __cil_tmp18 ;
   struct videocodec *__cil_tmp19 ;
   unsigned long __cil_tmp20 ;
   unsigned long __cil_tmp21 ;
   struct videocodec_master *__cil_tmp22 ;
   unsigned long __cil_tmp23 ;
   unsigned long __cil_tmp24 ;
   __u32 (*__cil_tmp25)(struct videocodec * , __u16  ) ;
   unsigned long __cil_tmp26 ;
   unsigned long __cil_tmp27 ;
   struct videocodec *__cil_tmp28 ;
   int __cil_tmp29 ;
   __u16 __cil_tmp30 ;
   int *__cil_tmp31 ;
   int __cil_tmp32 ;
   char (*__cil_tmp33)[32U] ;
   char *__cil_tmp34 ;
   int *__cil_tmp35 ;
   int __cil_tmp36 ;
   char (*__cil_tmp37)[32U] ;
   char *__cil_tmp38 ;
   int __cil_tmp39 ;
   int __cil_tmp40 ;
 
   {
 #line 92
   value = (u8 )0U;
   {
 #line 95
   __cil_tmp5 = (__u32 (*)(struct videocodec * , __u16  ))0;
 #line 95
   __cil_tmp6 = (unsigned long )__cil_tmp5;
 #line 95
   __cil_tmp7 = (unsigned long )ptr;
 #line 95
   __cil_tmp8 = __cil_tmp7 + 40;
 #line 95
   __cil_tmp9 = *((struct videocodec **)__cil_tmp8);
 #line 95
   __cil_tmp10 = (unsigned long )__cil_tmp9;
 #line 95
   __cil_tmp11 = __cil_tmp10 + 64;
 #line 95
   __cil_tmp12 = *((struct videocodec_master **)__cil_tmp11);
 #line 95
   __cil_tmp13 = (unsigned long )__cil_tmp12;
 #line 95
   __cil_tmp14 = __cil_tmp13 + 64;
 #line 95
   __cil_tmp15 = *((__u32 (**)(struct videocodec * , __u16  ))__cil_tmp14);
 #line 95
   __cil_tmp16 = (unsigned long )__cil_tmp15;
 #line 95
   if (__cil_tmp16 != __cil_tmp6) {
     {
 #line 96
     __cil_tmp17 = (unsigned long )ptr;
 #line 96
     __cil_tmp18 = __cil_tmp17 + 40;
 #line 96
     __cil_tmp19 = *((struct videocodec **)__cil_tmp18);
 #line 96
     __cil_tmp20 = (unsigned long )__cil_tmp19;
 #line 96
     __cil_tmp21 = __cil_tmp20 + 64;
 #line 96
     __cil_tmp22 = *((struct videocodec_master **)__cil_tmp21);
 #line 96
     __cil_tmp23 = (unsigned long )__cil_tmp22;
 #line 96
     __cil_tmp24 = __cil_tmp23 + 64;
 #line 96
     __cil_tmp25 = *((__u32 (**)(struct videocodec * , __u16  ))__cil_tmp24);
 #line 96
     __cil_tmp26 = (unsigned long )ptr;
 #line 96
     __cil_tmp27 = __cil_tmp26 + 40;
 #line 96
     __cil_tmp28 = *((struct videocodec **)__cil_tmp27);
 #line 96
     __cil_tmp29 = (int )reg;
 #line 96
     __cil_tmp30 = (__u16 )__cil_tmp29;
 #line 96
     tmp = (*__cil_tmp25)(__cil_tmp28, __cil_tmp30);
 #line 96
     value = (u8 )tmp;
     }
   } else {
     {
 #line 100
     __cil_tmp31 = & debug;
 #line 100
     __cil_tmp32 = *__cil_tmp31;
 #line 100
     if (__cil_tmp32 > 0) {
       {
 #line 100
       __cil_tmp33 = (char (*)[32U])ptr;
 #line 100
       __cil_tmp34 = (char *)__cil_tmp33;
 #line 100
       printk("<3>%s: invalid I/O setup, nothing read!\n", __cil_tmp34);
       }
     } else {
 
     }
     }
   }
   }
   {
 #line 104
   __cil_tmp35 = & debug;
 #line 104
   __cil_tmp36 = *__cil_tmp35;
 #line 104
   if (__cil_tmp36 > 3) {
     {
 #line 104
     __cil_tmp37 = (char (*)[32U])ptr;
 #line 104
     __cil_tmp38 = (char *)__cil_tmp37;
 #line 104
     __cil_tmp39 = (int )reg;
 #line 104
     __cil_tmp40 = (int )value;
 #line 104
     printk("%s: reading from 0x%04x: %02x\n", __cil_tmp38, __cil_tmp39, __cil_tmp40);
     }
   } else {
 
   }
   }
 #line 107
   return (value);
 }
 }
 #line 111 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
 static void zr36016_write(struct zr36016 *ptr , u16 reg , u8 value ) 
 { int *__cil_tmp4 ;
   int __cil_tmp5 ;
   char (*__cil_tmp6)[32U] ;
   char *__cil_tmp7 ;
   int __cil_tmp8 ;
   int __cil_tmp9 ;
   void (*__cil_tmp10)(struct videocodec * , __u16  , __u32  ) ;
   unsigned long __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   struct videocodec *__cil_tmp14 ;
   unsigned long __cil_tmp15 ;
   unsigned long __cil_tmp16 ;
   struct videocodec_master *__cil_tmp17 ;
   unsigned long __cil_tmp18 ;
   unsigned long __cil_tmp19 ;
   void (*__cil_tmp20)(struct videocodec * , __u16  , __u32  ) ;
   unsigned long __cil_tmp21 ;
   unsigned long __cil_tmp22 ;
   unsigned long __cil_tmp23 ;
   struct videocodec *__cil_tmp24 ;
   unsigned long __cil_tmp25 ;
   unsigned long __cil_tmp26 ;
   struct videocodec_master *__cil_tmp27 ;
   unsigned long __cil_tmp28 ;
   unsigned long __cil_tmp29 ;
   void (*__cil_tmp30)(struct videocodec * , __u16  , __u32  ) ;
   unsigned long __cil_tmp31 ;
   unsigned long __cil_tmp32 ;
   struct videocodec *__cil_tmp33 ;
   int __cil_tmp34 ;
   __u16 __cil_tmp35 ;
   __u32 __cil_tmp36 ;
   int *__cil_tmp37 ;
   int __cil_tmp38 ;
   char (*__cil_tmp39)[32U] ;
   char *__cil_tmp40 ;
 
   {
   {
 #line 115
   __cil_tmp4 = & debug;
 #line 115
   __cil_tmp5 = *__cil_tmp4;
 #line 115
   if (__cil_tmp5 > 3) {
     {
 #line 115
     __cil_tmp6 = (char (*)[32U])ptr;
 #line 115
     __cil_tmp7 = (char *)__cil_tmp6;
 #line 115
     __cil_tmp8 = (int )value;
 #line 115
     __cil_tmp9 = (int )reg;
 #line 115
     printk("%s: writing 0x%02x to 0x%04x\n", __cil_tmp7, __cil_tmp8, __cil_tmp9);
     }
   } else {
 
   }
   }
   {
 #line 119
   __cil_tmp10 = (void (*)(struct videocodec * , __u16  , __u32  ))0;
 #line 119
   __cil_tmp11 = (unsigned long )__cil_tmp10;
 #line 119
   __cil_tmp12 = (unsigned long )ptr;
 #line 119
   __cil_tmp13 = __cil_tmp12 + 40;
 #line 119
   __cil_tmp14 = *((struct videocodec **)__cil_tmp13);
 #line 119
   __cil_tmp15 = (unsigned long )__cil_tmp14;
 #line 119
   __cil_tmp16 = __cil_tmp15 + 64;
 #line 119
   __cil_tmp17 = *((struct videocodec_master **)__cil_tmp16);
 #line 119
   __cil_tmp18 = (unsigned long )__cil_tmp17;
 #line 119
   __cil_tmp19 = __cil_tmp18 + 72;
 #line 119
   __cil_tmp20 = *((void (**)(struct videocodec * , __u16  , __u32  ))__cil_tmp19);
 #line 119
   __cil_tmp21 = (unsigned long )__cil_tmp20;
 #line 119
   if (__cil_tmp21 != __cil_tmp11) {
     {
 #line 120
     __cil_tmp22 = (unsigned long )ptr;
 #line 120
     __cil_tmp23 = __cil_tmp22 + 40;
 #line 120
     __cil_tmp24 = *((struct videocodec **)__cil_tmp23);
 #line 120
     __cil_tmp25 = (unsigned long )__cil_tmp24;
 #line 120
     __cil_tmp26 = __cil_tmp25 + 64;
 #line 120
     __cil_tmp27 = *((struct videocodec_master **)__cil_tmp26);
 #line 120
     __cil_tmp28 = (unsigned long )__cil_tmp27;
 #line 120
     __cil_tmp29 = __cil_tmp28 + 72;
 #line 120
     __cil_tmp30 = *((void (**)(struct videocodec * , __u16  , __u32  ))__cil_tmp29);
 #line 120
     __cil_tmp31 = (unsigned long )ptr;
 #line 120
     __cil_tmp32 = __cil_tmp31 + 40;
 #line 120
     __cil_tmp33 = *((struct videocodec **)__cil_tmp32);
 #line 120
     __cil_tmp34 = (int )reg;
 #line 120
     __cil_tmp35 = (__u16 )__cil_tmp34;
 #line 120
     __cil_tmp36 = (__u32 )value;
 #line 120
     (*__cil_tmp30)(__cil_tmp33, __cil_tmp35, __cil_tmp36);
     }
   } else {
     {
 #line 122
     __cil_tmp37 = & debug;
 #line 122
     __cil_tmp38 = *__cil_tmp37;
 #line 122
     if (__cil_tmp38 > 0) {
       {
 #line 122
       __cil_tmp39 = (char (*)[32U])ptr;
 #line 122
       __cil_tmp40 = (char *)__cil_tmp39;
 #line 122
       printk("<3>%s: invalid I/O setup, nothing written!\n", __cil_tmp40);
       }
     } else {
 
     }
     }
   }
   }
 #line 123
   return;
 }
 }
 #line 132 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
 static u8 zr36016_readi(struct zr36016 *ptr , u16 reg ) 
 { u8 value ;
   __u32 tmp ;
   void (*__cil_tmp5)(struct videocodec * , __u16  , __u32  ) ;
   unsigned long __cil_tmp6 ;
   unsigned long __cil_tmp7 ;
   unsigned long __cil_tmp8 ;
   struct videocodec *__cil_tmp9 ;
   unsigned long __cil_tmp10 ;
   unsigned long __cil_tmp11 ;
   struct videocodec_master *__cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   void (*__cil_tmp15)(struct videocodec * , __u16  , __u32  ) ;
   unsigned long __cil_tmp16 ;
   __u32 (*__cil_tmp17)(struct videocodec * , __u16  ) ;
   unsigned long __cil_tmp18 ;
   unsigned long __cil_tmp19 ;
   unsigned long __cil_tmp20 ;
   struct videocodec *__cil_tmp21 ;
   unsigned long __cil_tmp22 ;
   unsigned long __cil_tmp23 ;
   struct videocodec_master *__cil_tmp24 ;
   unsigned long __cil_tmp25 ;
   unsigned long __cil_tmp26 ;
   __u32 (*__cil_tmp27)(struct videocodec * , __u16  ) ;
   unsigned long __cil_tmp28 ;
   unsigned long __cil_tmp29 ;
   unsigned long __cil_tmp30 ;
   struct videocodec *__cil_tmp31 ;
   unsigned long __cil_tmp32 ;
   unsigned long __cil_tmp33 ;
   struct videocodec_master *__cil_tmp34 ;
   unsigned long __cil_tmp35 ;
   unsigned long __cil_tmp36 ;
   void (*__cil_tmp37)(struct videocodec * , __u16  , __u32  ) ;
   unsigned long __cil_tmp38 ;
   unsigned long __cil_tmp39 ;
   struct videocodec *__cil_tmp40 ;
   __u16 __cil_tmp41 ;
   __u32 __cil_tmp42 ;
   unsigned int __cil_tmp43 ;
   unsigned long __cil_tmp44 ;
   unsigned long __cil_tmp45 ;
   struct videocodec *__cil_tmp46 ;
   unsigned long __cil_tmp47 ;
   unsigned long __cil_tmp48 ;
   struct videocodec_master *__cil_tmp49 ;
   unsigned long __cil_tmp50 ;
   unsigned long __cil_tmp51 ;
   __u32 (*__cil_tmp52)(struct videocodec * , __u16  ) ;
   unsigned long __cil_tmp53 ;
   unsigned long __cil_tmp54 ;
   struct videocodec *__cil_tmp55 ;
   __u16 __cil_tmp56 ;
   int *__cil_tmp57 ;
   int __cil_tmp58 ;
   char (*__cil_tmp59)[32U] ;
   char *__cil_tmp60 ;
   int *__cil_tmp61 ;
   int __cil_tmp62 ;
   char (*__cil_tmp63)[32U] ;
   char *__cil_tmp64 ;
   int __cil_tmp65 ;
   int __cil_tmp66 ;
 
   {
 #line 135
  value = (u8 )0U;
  {
#line 138
  __cil_tmp5 = (void (*)(struct videocodec * , __u16  , __u32  ))0;
#line 138
  __cil_tmp6 = (unsigned long )__cil_tmp5;
#line 138
  __cil_tmp7 = (unsigned long )ptr;
#line 138
  __cil_tmp8 = __cil_tmp7 + 40;
#line 138
  __cil_tmp9 = *((struct videocodec **)__cil_tmp8);
#line 138
  __cil_tmp10 = (unsigned long )__cil_tmp9;
#line 138
  __cil_tmp11 = __cil_tmp10 + 64;
#line 138
  __cil_tmp12 = *((struct videocodec_master **)__cil_tmp11);
#line 138
  __cil_tmp13 = (unsigned long )__cil_tmp12;
#line 138
  __cil_tmp14 = __cil_tmp13 + 72;
#line 138
  __cil_tmp15 = *((void (**)(struct videocodec * , __u16  , __u32  ))__cil_tmp14);
#line 138
  __cil_tmp16 = (unsigned long )__cil_tmp15;
#line 138
  if (__cil_tmp16 != __cil_tmp6) {
    {
#line 138
    __cil_tmp17 = (__u32 (*)(struct videocodec * , __u16  ))0;
#line 138
    __cil_tmp18 = (unsigned long )__cil_tmp17;
#line 138
    __cil_tmp19 = (unsigned long )ptr;
#line 138
    __cil_tmp20 = __cil_tmp19 + 40;
#line 138
    __cil_tmp21 = *((struct videocodec **)__cil_tmp20);
#line 138
    __cil_tmp22 = (unsigned long )__cil_tmp21;
#line 138
    __cil_tmp23 = __cil_tmp22 + 64;
#line 138
    __cil_tmp24 = *((struct videocodec_master **)__cil_tmp23);
#line 138
    __cil_tmp25 = (unsigned long )__cil_tmp24;
#line 138
    __cil_tmp26 = __cil_tmp25 + 64;
#line 138
    __cil_tmp27 = *((__u32 (**)(struct videocodec * , __u16  ))__cil_tmp26);
#line 138
    __cil_tmp28 = (unsigned long )__cil_tmp27;
#line 138
    if (__cil_tmp28 != __cil_tmp18) {
      {
#line 140
      __cil_tmp29 = (unsigned long )ptr;
#line 140
      __cil_tmp30 = __cil_tmp29 + 40;
#line 140
      __cil_tmp31 = *((struct videocodec **)__cil_tmp30);
#line 140
      __cil_tmp32 = (unsigned long )__cil_tmp31;
#line 140
      __cil_tmp33 = __cil_tmp32 + 64;
#line 140
      __cil_tmp34 = *((struct videocodec_master **)__cil_tmp33);
#line 140
      __cil_tmp35 = (unsigned long )__cil_tmp34;
#line 140
      __cil_tmp36 = __cil_tmp35 + 72;
#line 140
      __cil_tmp37 = *((void (**)(struct videocodec * , __u16  , __u32  ))__cil_tmp36);
#line 140
      __cil_tmp38 = (unsigned long )ptr;
#line 140
      __cil_tmp39 = __cil_tmp38 + 40;
#line 140
      __cil_tmp40 = *((struct videocodec **)__cil_tmp39);
#line 140
      __cil_tmp41 = (__u16 )2;
#line 140
      __cil_tmp42 = (__u32 )reg;
#line 140
      __cil_tmp43 = __cil_tmp42 & 15U;
#line 140
      (*__cil_tmp37)(__cil_tmp40, __cil_tmp41, __cil_tmp43);
#line 141
      __cil_tmp44 = (unsigned long )ptr;
#line 141
      __cil_tmp45 = __cil_tmp44 + 40;
#line 141
      __cil_tmp46 = *((struct videocodec **)__cil_tmp45);
#line 141
      __cil_tmp47 = (unsigned long )__cil_tmp46;
#line 141
      __cil_tmp48 = __cil_tmp47 + 64;
#line 141
      __cil_tmp49 = *((struct videocodec_master **)__cil_tmp48);
#line 141
      __cil_tmp50 = (unsigned long )__cil_tmp49;
#line 141
      __cil_tmp51 = __cil_tmp50 + 64;
#line 141
      __cil_tmp52 = *((__u32 (**)(struct videocodec * , __u16  ))__cil_tmp51);
#line 141
      __cil_tmp53 = (unsigned long )ptr;
#line 141
      __cil_tmp54 = __cil_tmp53 + 40;
#line 141
      __cil_tmp55 = *((struct videocodec **)__cil_tmp54);
#line 141
      __cil_tmp56 = (__u16 )3;
#line 141
      tmp = (*__cil_tmp52)(__cil_tmp55, __cil_tmp56);
#line 141
      value = (u8 )tmp;
      }
    } else {
#line 138
      goto _L;
    }
    }
  } else {
    _L: /* CIL Label */ 
    {
#line 143
    __cil_tmp57 = & debug;
#line 143
    __cil_tmp58 = *__cil_tmp57;
#line 143
    if (__cil_tmp58 > 0) {
      {
#line 143
      __cil_tmp59 = (char (*)[32U])ptr;
#line 143
      __cil_tmp60 = (char *)__cil_tmp59;
#line 143
      printk("<3>%s: invalid I/O setup, nothing read (i)!\n", __cil_tmp60);
      }
    } else {

    }
    }
  }
  }
  {
#line 148
  __cil_tmp61 = & debug;
#line 148
  __cil_tmp62 = *__cil_tmp61;
#line 148
  if (__cil_tmp62 > 3) {
    {
#line 148
    __cil_tmp63 = (char (*)[32U])ptr;
#line 148
    __cil_tmp64 = (char *)__cil_tmp63;
#line 148
    __cil_tmp65 = (int )reg;
#line 148
    __cil_tmp66 = (int )value;
#line 148
    printk("%s: reading indirect from 0x%04x: %02x\n", __cil_tmp64, __cil_tmp65, __cil_tmp66);
    }
  } else {

  }
  }
#line 150
  return (value);
}
}
#line 154 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
static void zr36016_writei(struct zr36016 *ptr , u16 reg , u8 value ) 
{ int *__cil_tmp4 ;
  int __cil_tmp5 ;
  char (*__cil_tmp6)[32U] ;
  char *__cil_tmp7 ;
  int __cil_tmp8 ;
  int __cil_tmp9 ;
  void (*__cil_tmp10)(struct videocodec * , __u16  , __u32  ) ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  struct videocodec *__cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  unsigned long __cil_tmp16 ;
  struct videocodec_master *__cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  void (*__cil_tmp20)(struct videocodec * , __u16  , __u32  ) ;
  unsigned long __cil_tmp21 ;
  unsigned long __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  struct videocodec *__cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  struct videocodec_master *__cil_tmp27 ;
  unsigned long __cil_tmp28 ;
  unsigned long __cil_tmp29 ;
  void (*__cil_tmp30)(struct videocodec * , __u16  , __u32  ) ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  struct videocodec *__cil_tmp33 ;
  __u16 __cil_tmp34 ;
  __u32 __cil_tmp35 ;
  unsigned int __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 * , __u16  , __u32  ) ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  struct videocodec *__cil_tmp48 ;
  __u16 __cil_tmp49 ;
  __u32 __cil_tmp50 ;
  int *__cil_tmp51 ;
  int __cil_tmp52 ;
  char (*__cil_tmp53)[32U] ;
  char *__cil_tmp54 ;

  {
  {
#line 158
  __cil_tmp4 = & debug;
#line 158
  __cil_tmp5 = *__cil_tmp4;
#line 158
  if (__cil_tmp5 > 3) {
    {
#line 158
    __cil_tmp6 = (char (*)[32U])ptr;
#line 158
    __cil_tmp7 = (char *)__cil_tmp6;
#line 158
    __cil_tmp8 = (int )value;
#line 158
    __cil_tmp9 = (int )reg;
#line 158
    printk("%s: writing indirect 0x%02x to 0x%04x\n", __cil_tmp7, __cil_tmp8, __cil_tmp9);
    }
  } else {

  }
  }
  {
#line 162
  __cil_tmp10 = (void (*)(struct videocodec * , __u16  , __u32  ))0;
#line 162
  __cil_tmp11 = (unsigned long )__cil_tmp10;
#line 162
  __cil_tmp12 = (unsigned long )ptr;
#line 162
  __cil_tmp13 = __cil_tmp12 + 40;
#line 162
  __cil_tmp14 = *((struct videocodec **)__cil_tmp13);
#line 162
  __cil_tmp15 = (unsigned long )__cil_tmp14;
#line 162
  __cil_tmp16 = __cil_tmp15 + 64;
#line 162
  __cil_tmp17 = *((struct videocodec_master **)__cil_tmp16);
#line 162
  __cil_tmp18 = (unsigned long )__cil_tmp17;
#line 162
  __cil_tmp19 = __cil_tmp18 + 72;
#line 162
  __cil_tmp20 = *((void (**)(struct videocodec * , __u16  , __u32  ))__cil_tmp19);
#line 162
  __cil_tmp21 = (unsigned long )__cil_tmp20;
#line 162
  if (__cil_tmp21 != __cil_tmp11) {
    {
#line 163
    __cil_tmp22 = (unsigned long )ptr;
#line 163
    __cil_tmp23 = __cil_tmp22 + 40;
#line 163
    __cil_tmp24 = *((struct videocodec **)__cil_tmp23);
#line 163
    __cil_tmp25 = (unsigned long )__cil_tmp24;
#line 163
    __cil_tmp26 = __cil_tmp25 + 64;
#line 163
    __cil_tmp27 = *((struct videocodec_master **)__cil_tmp26);
#line 163
    __cil_tmp28 = (unsigned long )__cil_tmp27;
#line 163
    __cil_tmp29 = __cil_tmp28 + 72;
#line 163
    __cil_tmp30 = *((void (**)(struct videocodec * , __u16  , __u32  ))__cil_tmp29);
#line 163
    __cil_tmp31 = (unsigned long )ptr;
#line 163
    __cil_tmp32 = __cil_tmp31 + 40;
#line 163
    __cil_tmp33 = *((struct videocodec **)__cil_tmp32);
#line 163
    __cil_tmp34 = (__u16 )2;
#line 163
    __cil_tmp35 = (__u32 )reg;
#line 163
    __cil_tmp36 = __cil_tmp35 & 15U;
#line 163
    (*__cil_tmp30)(__cil_tmp33, __cil_tmp34, __cil_tmp36);
#line 164
    __cil_tmp37 = (unsigned long )ptr;
#line 164
    __cil_tmp38 = __cil_tmp37 + 40;
#line 164
    __cil_tmp39 = *((struct videocodec **)__cil_tmp38);
#line 164
    __cil_tmp40 = (unsigned long )__cil_tmp39;
#line 164
    __cil_tmp41 = __cil_tmp40 + 64;
#line 164
    __cil_tmp42 = *((struct videocodec_master **)__cil_tmp41);
#line 164
    __cil_tmp43 = (unsigned long )__cil_tmp42;
#line 164
    __cil_tmp44 = __cil_tmp43 + 72;
#line 164
    __cil_tmp45 = *((void (**)(struct videocodec * , __u16  , __u32  ))__cil_tmp44);
#line 164
    __cil_tmp46 = (unsigned long )ptr;
#line 164
    __cil_tmp47 = __cil_tmp46 + 40;
#line 164
    __cil_tmp48 = *((struct videocodec **)__cil_tmp47);
#line 164
    __cil_tmp49 = (__u16 )3;
#line 164
    __cil_tmp50 = (__u32 )value;
#line 164
    (*__cil_tmp45)(__cil_tmp48, __cil_tmp49, __cil_tmp50);
    }
  } else {
    {
#line 166
    __cil_tmp51 = & debug;
#line 166
    __cil_tmp52 = *__cil_tmp51;
#line 166
    if (__cil_tmp52 > 0) {
      {
#line 166
      __cil_tmp53 = (char (*)[32U])ptr;
#line 166
      __cil_tmp54 = (char *)__cil_tmp53;
#line 166
      printk("<3>%s: invalid I/O setup, nothing written (i)!\n", __cil_tmp54);
      }
    } else {

    }
    }
  }
  }
#line 167
  return;
}
}
#line 180 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
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 182
  __cil_tmp3 = (u16 )0;
#line 182
  tmp = zr36016_read(ptr, __cil_tmp3);
#line 182
  __cil_tmp4 = (unsigned long )ptr;
#line 182
  __cil_tmp5 = __cil_tmp4 + 48;
#line 182
  __cil_tmp6 = (int )tmp;
#line 182
  __cil_tmp7 = __cil_tmp6 >> 4;
#line 182
  *((__u8 *)__cil_tmp5) = (__u8 )__cil_tmp7;
  }
  {
#line 183
  __cil_tmp8 = (unsigned long )ptr;
#line 183
  __cil_tmp9 = __cil_tmp8 + 48;
#line 183
  return (*((__u8 *)__cil_tmp9));
  }
}
}
#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
static int zr36016_basic_test(struct zr36016 *ptr ) 
{ int i ;
  u8 tmp ;
  u8 tmp___0 ;
  u8 tmp___1 ;
  int *__cil_tmp6 ;
  int __cil_tmp7 ;
  u16 __cil_tmp8 ;
  u8 __cil_tmp9 ;
  int *__cil_tmp10 ;
  int __cil_tmp11 ;
  char (*__cil_tmp12)[32U] ;
  char *__cil_tmp13 ;
  int *__cil_tmp14 ;
  int __cil_tmp15 ;
  u16 __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 ;
  unsigned int __cil_tmp25 ;
  int *__cil_tmp26 ;
  int __cil_tmp27 ;
  char (*__cil_tmp28)[32U] ;
  char *__cil_tmp29 ;
  u16 __cil_tmp30 ;
  u8 __cil_tmp31 ;
  u16 __cil_tmp32 ;
  unsigned int __cil_tmp33 ;
  int *__cil_tmp34 ;
  int __cil_tmp35 ;
  char (*__cil_tmp36)[32U] ;
  char *__cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  __u8 __cil_tmp40 ;
  int __cil_tmp41 ;
  int __cil_tmp42 ;
  int *__cil_tmp43 ;
  int __cil_tmp44 ;
  char (*__cil_tmp45)[32U] ;
  char *__cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  unsigned long __cil_tmp48 ;
  __u8 __cil_tmp49 ;
  int __cil_tmp50 ;

  {
  {
#line 195
  __cil_tmp6 = & debug;
#line 195
  __cil_tmp7 = *__cil_tmp6;
#line 195
  if (__cil_tmp7 != 0) {
    {
#line 197
    __cil_tmp8 = (u16 )4;
#line 197
    __cil_tmp9 = (u8 )85;
#line 197
    zr36016_writei(ptr, __cil_tmp8, __cil_tmp9);
    }
    {
#line 198
    __cil_tmp10 = & debug;
#line 198
    __cil_tmp11 = *__cil_tmp10;
#line 198
    if (__cil_tmp11 > 0) {
      {
#line 198
      __cil_tmp12 = (char (*)[32U])ptr;
#line 198
      __cil_tmp13 = (char *)__cil_tmp12;
#line 198
      printk("<6>%s: registers: ", __cil_tmp13);
      }
    } else {

    }
    }
#line 199
    i = 0;
#line 199
    goto ldv_15128;
    ldv_15127: ;
    {
#line 200
    __cil_tmp14 = & debug;
#line 200
    __cil_tmp15 = *__cil_tmp14;
#line 200
    if (__cil_tmp15 > 0) {
      {
#line 200
      __cil_tmp16 = (u16 )i;
#line 200
      __cil_tmp17 = (int )__cil_tmp16;
#line 200
      __cil_tmp18 = (u16 )__cil_tmp17;
#line 200
      tmp = zr36016_readi(ptr, __cil_tmp18);
#line 200
      __cil_tmp19 = (int )tmp;
#line 200
      printk("%02x ", __cil_tmp19);
      }
    } else {

    }
    }
#line 199
    i = i + 1;
    ldv_15128: ;
#line 199
    if (i <= 11) {
#line 200
      goto ldv_15127;
    } else {
#line 202
      goto ldv_15129;
    }
    ldv_15129: ;
    {
#line 201
    __cil_tmp20 = & debug;
#line 201
    __cil_tmp21 = *__cil_tmp20;
#line 201
    if (__cil_tmp21 > 0) {
      {
#line 201
      printk("\n");
      }
    } else {

    }
    }
  } else {

  }
  }
  {
#line 205
  __cil_tmp22 = (u16 )4;
#line 205
  __cil_tmp23 = (u8 )0;
#line 205
  zr36016_writei(ptr, __cil_tmp22, __cil_tmp23);
#line 206
  __cil_tmp24 = (u16 )4;
#line 206
  tmp___0 = zr36016_readi(ptr, __cil_tmp24);
  }
  {
#line 206
  __cil_tmp25 = (unsigned int )tmp___0;
#line 206
  if (__cil_tmp25 != 0U) {
    {
#line 207
    __cil_tmp26 = & debug;
#line 207
    __cil_tmp27 = *__cil_tmp26;
#line 207
    if (__cil_tmp27 > 0) {
      {
#line 207
      __cil_tmp28 = (char (*)[32U])ptr;
#line 207
      __cil_tmp29 = (char *)__cil_tmp28;
#line 207
      printk("<3>%s: attach failed, can\'t connect to vfe processor!\n", __cil_tmp29);
      }
    } else {

    }
    }
#line 211
    return (-6);
  } else {

  }
  }
  {
#line 213
  __cil_tmp30 = (u16 )4;
#line 213
  __cil_tmp31 = (u8 )208;
#line 213
  zr36016_writei(ptr, __cil_tmp30, __cil_tmp31);
#line 214
  __cil_tmp32 = (u16 )4;
#line 214
  tmp___1 = zr36016_readi(ptr, __cil_tmp32);
  }
  {
#line 214
  __cil_tmp33 = (unsigned int )tmp___1;
#line 214
  if (__cil_tmp33 != 208U) {
    {
#line 215
    __cil_tmp34 = & debug;
#line 215
    __cil_tmp35 = *__cil_tmp34;
#line 215
    if (__cil_tmp35 > 0) {
      {
#line 215
      __cil_tmp36 = (char (*)[32U])ptr;
#line 215
      __cil_tmp37 = (char *)__cil_tmp36;
#line 215
      printk("<3>%s: attach failed, can\'t connect to vfe processor!\n", __cil_tmp37);
      }
    } else {

    }
    }
#line 219
    return (-6);
  } else {

  }
  }
  {
#line 222
  zr36016_read_version(ptr);
  }
  {
#line 223
  __cil_tmp38 = (unsigned long )ptr;
#line 223
  __cil_tmp39 = __cil_tmp38 + 48;
#line 223
  __cil_tmp40 = *((__u8 *)__cil_tmp39);
#line 223
  __cil_tmp41 = (int )__cil_tmp40;
#line 223
  __cil_tmp42 = __cil_tmp41 & 12;
#line 223
  if (__cil_tmp42 != 0) {
    {
#line 224
    __cil_tmp43 = & debug;
#line 224
    __cil_tmp44 = *__cil_tmp43;
#line 224
    if (__cil_tmp44 > 0) {
      {
#line 224
      __cil_tmp45 = (char (*)[32U])ptr;
#line 224
      __cil_tmp46 = (char *)__cil_tmp45;
#line 224
      __cil_tmp47 = (unsigned long )ptr;
#line 224
      __cil_tmp48 = __cil_tmp47 + 48;
#line 224
      __cil_tmp49 = *((__u8 *)__cil_tmp48);
#line 224
      __cil_tmp50 = (int )__cil_tmp49;
#line 224
      printk("<3>%s: attach failed, suspicious version %d found...\n", __cil_tmp46,
             __cil_tmp50);
      }
    } else {

    }
    }
#line 228
    return (-6);
  } else {

  }
  }
#line 231
  return (0);
}
}
#line 269 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
static void zr36016_init(struct zr36016 *ptr ) 
{ int tmp ;
  int tmp___0 ;
  u16 __cil_tmp4 ;
  u8 __cil_tmp5 ;
  u16 __cil_tmp6 ;
  u8 __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  __u16 __cil_tmp10 ;
  unsigned int __cil_tmp11 ;
  unsigned long __cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  __u16 __cil_tmp14 ;
  unsigned int __cil_tmp15 ;
  u16 __cil_tmp16 ;
  int __cil_tmp17 ;
  int __cil_tmp18 ;
  u8 __cil_tmp19 ;
  int __cil_tmp20 ;
  u8 __cil_tmp21 ;
  u16 __cil_tmp22 ;
  u8 __cil_tmp23 ;
  u16 __cil_tmp24 ;
  unsigned long __cil_tmp25 ;
  unsigned long __cil_tmp26 ;
  __u16 __cil_tmp27 ;
  int __cil_tmp28 ;
  int __cil_tmp29 ;
  u8 __cil_tmp30 ;
  int __cil_tmp31 ;
  u8 __cil_tmp32 ;
  u16 __cil_tmp33 ;
  unsigned long __cil_tmp34 ;
  unsigned long __cil_tmp35 ;
  __u16 __cil_tmp36 ;
  u8 __cil_tmp37 ;
  int __cil_tmp38 ;
  u8 __cil_tmp39 ;
  u16 __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  __u16 __cil_tmp43 ;
  int __cil_tmp44 ;
  int __cil_tmp45 ;
  u8 __cil_tmp46 ;
  int __cil_tmp47 ;
  u8 __cil_tmp48 ;
  u16 __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  __u16 __cil_tmp52 ;
  u8 __cil_tmp53 ;
  int __cil_tmp54 ;
  u8 __cil_tmp55 ;
  u16 __cil_tmp56 ;
  unsigned long __cil_tmp57 ;
  unsigned long __cil_tmp58 ;
  __u16 __cil_tmp59 ;
  int __cil_tmp60 ;
  int __cil_tmp61 ;
  u8 __cil_tmp62 ;
  int __cil_tmp63 ;
  u8 __cil_tmp64 ;
  u16 __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  __u16 __cil_tmp68 ;
  u8 __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 ;
  int __cil_tmp79 ;
  u8 __cil_tmp80 ;
  u16 __cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  unsigned long __cil_tmp83 ;
  __u16 __cil_tmp84 ;
  u8 __cil_tmp85 ;
  int __cil_tmp86 ;
  u8 __cil_tmp87 ;
  u16 __cil_tmp88 ;
  u8 __cil_tmp89 ;

  {
  {
#line 272
  __cil_tmp4 = (u16 )0;
#line 272
  __cil_tmp5 = (u8 )0;
#line 272
  zr36016_write(ptr, __cil_tmp4, __cil_tmp5);
#line 275
  __cil_tmp6 = (u16 )1;
#line 275
  __cil_tmp7 = (u8 )209;
#line 275
  zr36016_write(ptr, __cil_tmp6, __cil_tmp7);
  }
  {
#line 281
  __cil_tmp8 = (unsigned long )ptr;
#line 281
  __cil_tmp9 = __cil_tmp8 + 64;
#line 281
  __cil_tmp10 = *((__u16 *)__cil_tmp9);
#line 281
  __cil_tmp11 = (unsigned int )__cil_tmp10;
#line 281
  if (__cil_tmp11 != 0U) {
#line 281
    tmp = 48;
  } else {
#line 281
    tmp = 0;
  }
  }
  {
#line 281
  __cil_tmp12 = (unsigned long )ptr;
#line 281
  __cil_tmp13 = __cil_tmp12 + 66;
#line 281
  __cil_tmp14 = *((__u16 *)__cil_tmp13);
#line 281
  __cil_tmp15 = (unsigned int )__cil_tmp14;
#line 281
  if (__cil_tmp15 != 0U) {
#line 281
    tmp___0 = 64;
  } else {
#line 281
    tmp___0 = 0;
  }
  }
  {
#line 281
  __cil_tmp16 = (u16 )0;
#line 281
  __cil_tmp17 = tmp | tmp___0;
#line 281
  __cil_tmp18 = __cil_tmp17 | 1;
#line 281
  __cil_tmp19 = (u8 )__cil_tmp18;
#line 281
  __cil_tmp20 = (int )__cil_tmp19;
#line 281
  __cil_tmp21 = (u8 )__cil_tmp20;
#line 281
  zr36016_writei(ptr, __cil_tmp16, __cil_tmp21);
#line 284
  __cil_tmp22 = (u16 )1;
#line 284
  __cil_tmp23 = (u8 )4;
#line 284
  zr36016_writei(ptr, __cil_tmp22, __cil_tmp23);
#line 288
  __cil_tmp24 = (u16 )5;
#line 288
  __cil_tmp25 = (unsigned long )ptr;
#line 288
  __cil_tmp26 = __cil_tmp25 + 60;
#line 288
  __cil_tmp27 = *((__u16 *)__cil_tmp26);
#line 288
  __cil_tmp28 = (int )__cil_tmp27;
#line 288
  __cil_tmp29 = __cil_tmp28 >> 8;
#line 288
  __cil_tmp30 = (u8 )__cil_tmp29;
#line 288
  __cil_tmp31 = (int )__cil_tmp30;
#line 288
  __cil_tmp32 = (u8 )__cil_tmp31;
#line 288
  zr36016_writei(ptr, __cil_tmp24, __cil_tmp32);
#line 289
  __cil_tmp33 = (u16 )4;
#line 289
  __cil_tmp34 = (unsigned long )ptr;
#line 289
  __cil_tmp35 = __cil_tmp34 + 60;
#line 289
  __cil_tmp36 = *((__u16 *)__cil_tmp35);
#line 289
  __cil_tmp37 = (u8 )__cil_tmp36;
#line 289
  __cil_tmp38 = (int )__cil_tmp37;
#line 289
  __cil_tmp39 = (u8 )__cil_tmp38;
#line 289
  zr36016_writei(ptr, __cil_tmp33, __cil_tmp39);
#line 290
  __cil_tmp40 = (u16 )9;
#line 290
  __cil_tmp41 = (unsigned long )ptr;
#line 290
  __cil_tmp42 = __cil_tmp41 + 62;
#line 290
  __cil_tmp43 = *((__u16 *)__cil_tmp42);
#line 290
  __cil_tmp44 = (int )__cil_tmp43;
#line 290
  __cil_tmp45 = __cil_tmp44 >> 8;
#line 290
  __cil_tmp46 = (u8 )__cil_tmp45;
#line 290
  __cil_tmp47 = (int )__cil_tmp46;
#line 290
  __cil_tmp48 = (u8 )__cil_tmp47;
#line 290
  zr36016_writei(ptr, __cil_tmp40, __cil_tmp48);
#line 291
  __cil_tmp49 = (u16 )8;
#line 291
  __cil_tmp50 = (unsigned long )ptr;
#line 291
  __cil_tmp51 = __cil_tmp50 + 62;
#line 291
  __cil_tmp52 = *((__u16 *)__cil_tmp51);
#line 291
  __cil_tmp53 = (u8 )__cil_tmp52;
#line 291
  __cil_tmp54 = (int )__cil_tmp53;
#line 291
  __cil_tmp55 = (u8 )__cil_tmp54;
#line 291
  zr36016_writei(ptr, __cil_tmp49, __cil_tmp55);
#line 292
  __cil_tmp56 = (u16 )3;
#line 292
  __cil_tmp57 = (unsigned long )ptr;
#line 292
  __cil_tmp58 = __cil_tmp57 + 56;
#line 292
  __cil_tmp59 = *((__u16 *)__cil_tmp58);
#line 292
  __cil_tmp60 = (int )__cil_tmp59;
#line 292
  __cil_tmp61 = __cil_tmp60 >> 8;
#line 292
  __cil_tmp62 = (u8 )__cil_tmp61;
#line 292
  __cil_tmp63 = (int )__cil_tmp62;
#line 292
  __cil_tmp64 = (u8 )__cil_tmp63;
#line 292
  zr36016_writei(ptr, __cil_tmp56, __cil_tmp64);
#line 293
  __cil_tmp65 = (u16 )2;
#line 293
  __cil_tmp66 = (unsigned long )ptr;
#line 293
  __cil_tmp67 = __cil_tmp66 + 56;
#line 293
  __cil_tmp68 = *((__u16 *)__cil_tmp67);
#line 293
  __cil_tmp69 = (u8 )__cil_tmp68;
#line 293
  __cil_tmp70 = (int )__cil_tmp69;
#line 293
  __cil_tmp71 = (u8 )__cil_tmp70;
#line 293
  zr36016_writei(ptr, __cil_tmp65, __cil_tmp71);
#line 294
  __cil_tmp72 = (u16 )7;
#line 294
  __cil_tmp73 = (unsigned long )ptr;
#line 294
  __cil_tmp74 = __cil_tmp73 + 58;
#line 294
  __cil_tmp75 = *((__u16 *)__cil_tmp74);
#line 294
  __cil_tmp76 = (int )__cil_tmp75;
#line 294
  __cil_tmp77 = __cil_tmp76 >> 8;
#line 294
  __cil_tmp78 = (u8 )__cil_tmp77;
#line 294
  __cil_tmp79 = (int )__cil_tmp78;
#line 294
  __cil_tmp80 = (u8 )__cil_tmp79;
#line 294
  zr36016_writei(ptr, __cil_tmp72, __cil_tmp80);
#line 295
  __cil_tmp81 = (u16 )6;
#line 295
  __cil_tmp82 = (unsigned long )ptr;
#line 295
  __cil_tmp83 = __cil_tmp82 + 58;
#line 295
  __cil_tmp84 = *((__u16 *)__cil_tmp83);
#line 295
  __cil_tmp85 = (u8 )__cil_tmp84;
#line 295
  __cil_tmp86 = (int )__cil_tmp85;
#line 295
  __cil_tmp87 = (u8 )__cil_tmp86;
#line 295
  zr36016_writei(ptr, __cil_tmp81, __cil_tmp87);
#line 298
  __cil_tmp88 = (u16 )0;
#line 298
  __cil_tmp89 = (u8 )1;
#line 298
  zr36016_write(ptr, __cil_tmp88, __cil_tmp89);
  }
#line 299
  return;
}
}
#line 310 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
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 ;
  char (*__cil_tmp9)[32U] ;
  char *__cil_tmp10 ;
  unsigned long __cil_tmp11 ;
  unsigned long __cil_tmp12 ;

  {
#line 313
  __cil_tmp4 = (unsigned long )codec;
#line 313
  __cil_tmp5 = __cil_tmp4 + 72;
#line 313
  __cil_tmp6 = *((void **)__cil_tmp5);
#line 313
  ptr = (struct zr36016 *)__cil_tmp6;
  {
#line 315
  __cil_tmp7 = & debug;
#line 315
  __cil_tmp8 = *__cil_tmp7;
#line 315
  if (__cil_tmp8 > 1) {
    {
#line 315
    __cil_tmp9 = (char (*)[32U])ptr;
#line 315
    __cil_tmp10 = (char *)__cil_tmp9;
#line 315
    printk("%s: set_mode %d call\n", __cil_tmp10, mode);
    }
  } else {

  }
  }
#line 317
  if (mode != 1) {
#line 317
    if (mode != 0) {
#line 318
      return (-22);
    } else {

    }
  } else {

  }
  {
#line 320
  __cil_tmp11 = (unsigned long )ptr;
#line 320
  __cil_tmp12 = __cil_tmp11 + 52;
#line 320
  *((int *)__cil_tmp12) = mode;
#line 321
  zr36016_init(ptr);
  }
#line 323
  return (0);
}
}
#line 328 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
static int zr36016_set_video(struct videocodec *codec , struct tvnorm *norm , struct vfe_settings *cap ,
                             struct vfe_polarity *pol ) 
{ struct zr36016 *ptr ;
  unsigned int tmp ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  void *__cil_tmp9 ;
  int *__cil_tmp10 ;
  int __cil_tmp11 ;
  char (*__cil_tmp12)[32U] ;
  char *__cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  unsigned long __cil_tmp15 ;
  u16 __cil_tmp16 ;
  int __cil_tmp17 ;
  unsigned long __cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  u16 __cil_tmp20 ;
  int __cil_tmp21 ;
  __u32 __cil_tmp22 ;
  unsigned long __cil_tmp23 ;
  unsigned long __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 ;
  __u16 __cil_tmp34 ;
  int __cil_tmp35 ;
  unsigned long __cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  unsigned long __cil_tmp39 ;
  __u32 __cil_tmp40 ;
  unsigned long __cil_tmp41 ;
  unsigned long __cil_tmp42 ;
  unsigned long __cil_tmp43 ;
  unsigned long __cil_tmp44 ;
  __u32 __cil_tmp45 ;
  unsigned long __cil_tmp46 ;
  unsigned long __cil_tmp47 ;
  u16 __cil_tmp48 ;
  unsigned int __cil_tmp49 ;
  unsigned long __cil_tmp50 ;
  unsigned long __cil_tmp51 ;
  u16 __cil_tmp52 ;
  unsigned long __cil_tmp53 ;
  unsigned long __cil_tmp54 ;
  __u32 __cil_tmp55 ;
  __u16 __cil_tmp56 ;
  unsigned int __cil_tmp57 ;
  unsigned int __cil_tmp58 ;
  unsigned long __cil_tmp59 ;
  unsigned long __cil_tmp60 ;
  unsigned long __cil_tmp61 ;
  unsigned long __cil_tmp62 ;
  __u32 __cil_tmp63 ;
  __u16 __cil_tmp64 ;
  int __cil_tmp65 ;
  unsigned long __cil_tmp66 ;
  unsigned long __cil_tmp67 ;
  u16 __cil_tmp68 ;
  int __cil_tmp69 ;
  int __cil_tmp70 ;
  unsigned long __cil_tmp71 ;
  unsigned long __cil_tmp72 ;
  unsigned long __cil_tmp73 ;
  unsigned long __cil_tmp74 ;
  __u16 __cil_tmp75 ;
  int __cil_tmp76 ;
  int __cil_tmp77 ;
  int __cil_tmp78 ;
  unsigned long __cil_tmp79 ;
  unsigned long __cil_tmp80 ;
  unsigned long __cil_tmp81 ;
  unsigned long __cil_tmp82 ;
  __u16 __cil_tmp83 ;
  int __cil_tmp84 ;
  int __cil_tmp85 ;
  int __cil_tmp86 ;
  int __cil_tmp87 ;

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

  }
  }
#line 343
  __cil_tmp36 = (unsigned long )ptr;
#line 343
  __cil_tmp37 = __cil_tmp36 + 60;
#line 343
  __cil_tmp38 = (unsigned long )cap;
#line 343
  __cil_tmp39 = __cil_tmp38 + 8;
#line 343
  __cil_tmp40 = *((__u32 *)__cil_tmp39);
#line 343
  *((__u16 *)__cil_tmp37) = (__u16 )__cil_tmp40;
#line 344
  __cil_tmp41 = (unsigned long )ptr;
#line 344
  __cil_tmp42 = __cil_tmp41 + 62;
#line 344
  __cil_tmp43 = (unsigned long )cap;
#line 344
  __cil_tmp44 = __cil_tmp43 + 12;
#line 344
  __cil_tmp45 = *((__u32 *)__cil_tmp44);
#line 344
  *((__u16 *)__cil_tmp42) = (__u16 )__cil_tmp45;
  {
#line 351
  __cil_tmp46 = (unsigned long )norm;
#line 351
  __cil_tmp47 = __cil_tmp46 + 4;
#line 351
  __cil_tmp48 = *((u16 *)__cil_tmp47);
#line 351
  __cil_tmp49 = (unsigned int )__cil_tmp48;
#line 351
  if (__cil_tmp49 != 0U) {
#line 351
    __cil_tmp50 = (unsigned long )norm;
#line 351
    __cil_tmp51 = __cil_tmp50 + 4;
#line 351
    __cil_tmp52 = *((u16 *)__cil_tmp51);
#line 351
    tmp = (unsigned int )__cil_tmp52;
  } else {
#line 351
    tmp = 1U;
  }
  }
#line 351
  __cil_tmp53 = (unsigned long )ptr;
#line 351
  __cil_tmp54 = __cil_tmp53 + 56;
#line 351
  __cil_tmp55 = *((__u32 *)cap);
#line 351
  __cil_tmp56 = (__u16 )__cil_tmp55;
#line 351
  __cil_tmp57 = (unsigned int )__cil_tmp56;
#line 351
  __cil_tmp58 = tmp + __cil_tmp57;
#line 351
  *((__u16 *)__cil_tmp54) = (__u16 )__cil_tmp58;
#line 356
  __cil_tmp59 = (unsigned long )ptr;
#line 356
  __cil_tmp60 = __cil_tmp59 + 58;
#line 356
  __cil_tmp61 = (unsigned long )cap;
#line 356
  __cil_tmp62 = __cil_tmp61 + 4;
#line 356
  __cil_tmp63 = *((__u32 *)__cil_tmp62);
#line 356
  __cil_tmp64 = (__u16 )__cil_tmp63;
#line 356
  __cil_tmp65 = (int )__cil_tmp64;
#line 356
  __cil_tmp66 = (unsigned long )norm;
#line 356
  __cil_tmp67 = __cil_tmp66 + 12;
#line 356
  __cil_tmp68 = *((u16 *)__cil_tmp67);
#line 356
  __cil_tmp69 = (int )__cil_tmp68;
#line 356
  __cil_tmp70 = __cil_tmp69 + __cil_tmp65;
#line 356
  *((__u16 *)__cil_tmp60) = (__u16 )__cil_tmp70;
#line 358
  __cil_tmp71 = (unsigned long )ptr;
#line 358
  __cil_tmp72 = __cil_tmp71 + 64;
#line 358
  __cil_tmp73 = (unsigned long )cap;
#line 358
  __cil_tmp74 = __cil_tmp73 + 16;
#line 358
  __cil_tmp75 = *((__u16 *)__cil_tmp74);
#line 358
  __cil_tmp76 = (int )__cil_tmp75;
#line 358
  __cil_tmp77 = __cil_tmp76 & 255;
#line 358
  __cil_tmp78 = __cil_tmp77 != 1;
#line 358
  *((__u16 *)__cil_tmp72) = (__u16 )__cil_tmp78;
#line 359
  __cil_tmp79 = (unsigned long )ptr;
#line 359
  __cil_tmp80 = __cil_tmp79 + 66;
#line 359
  __cil_tmp81 = (unsigned long )cap;
#line 359
  __cil_tmp82 = __cil_tmp81 + 16;
#line 359
  __cil_tmp83 = *((__u16 *)__cil_tmp82);
#line 359
  __cil_tmp84 = (int )__cil_tmp83;
#line 359
  __cil_tmp85 = __cil_tmp84 >> 8;
#line 359
  __cil_tmp86 = __cil_tmp85 & 255;
#line 359
  __cil_tmp87 = __cil_tmp86 != 1;
#line 359
  *((__u16 *)__cil_tmp80) = (__u16 )__cil_tmp87;
#line 361
  return (0);
}
}
#line 366 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
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 ;
  char (*__cil_tmp12)[32U] ;
  char *__cil_tmp13 ;
  int __cil_tmp14 ;

  {
#line 371
  __cil_tmp7 = (unsigned long )codec;
#line 371
  __cil_tmp8 = __cil_tmp7 + 72;
#line 371
  __cil_tmp9 = *((void **)__cil_tmp8);
#line 371
  ptr = (struct zr36016 *)__cil_tmp9;
#line 372
  ival = (int *)data;
  {
#line 374
  __cil_tmp10 = & debug;
#line 374
  __cil_tmp11 = *__cil_tmp10;
#line 374
  if (__cil_tmp11 > 1) {
    {
#line 374
    __cil_tmp12 = (char (*)[32U])ptr;
#line 374
    __cil_tmp13 = (char *)__cil_tmp12;
#line 374
    printk("%s: control %d call with %d byte\n", __cil_tmp13, type, size);
    }
  } else {

  }
  }
#line 378
  if (type == 0) {
#line 378
    goto case_0;
  } else
#line 384
  if (type == 32769) {
#line 384
    goto case_32769;
  } else
#line 390
  if (type == 1) {
#line 390
    goto case_1;
  } else
#line 398
  if (type == 32770) {
#line 398
    goto case_32770;
  } else
#line 399
  if (type == 2) {
#line 399
    goto case_2;
  } else
#line 402
  if (type == 3) {
#line 402
    goto case_3;
  } else {
    {
#line 406
    goto switch_default;
#line 377
    if (0) {
      case_0: /* CIL Label */ ;
#line 379
      if (size != 4) {
#line 380
        return (-14);
      } else {

      }
#line 381
      *ival = 0;
#line 382
      goto ldv_15156;
      case_32769: /* CIL Label */ ;
#line 385
      if (size != 4) {
#line 386
        return (-14);
      } else {

      }
#line 387
      *ival = 0;
#line 388
      goto ldv_15156;
      case_1: /* CIL Label */ ;
#line 391
      if (size != 4) {
#line 392
        return (-14);
      } else {

      }
      {
#line 393
      __cil_tmp14 = *ival;
#line 393
      if (__cil_tmp14 != 0) {
#line 394
        return (-22);
      } else {

      }
      }
#line 396
      return (0);
      case_32770: /* CIL Label */ ;
      case_2: /* CIL Label */ ;
#line 400
      return (0);
      case_3: /* CIL Label */ ;
#line 404
      return (-6);
      switch_default: /* CIL Label */ ;
#line 407
      return (-22);
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
  ldv_15156: ;
#line 410
  return (size);
}
}
#line 420 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
static int zr36016_unset(struct videocodec *codec ) 
{ struct zr36016 *ptr ;
  unsigned long __cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  void *__cil_tmp5 ;
  struct zr36016 *__cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  int *__cil_tmp9 ;
  int __cil_tmp10 ;
  char (*__cil_tmp11)[32U] ;
  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 422
  __cil_tmp3 = (unsigned long )codec;
#line 422
  __cil_tmp4 = __cil_tmp3 + 72;
#line 422
  __cil_tmp5 = *((void **)__cil_tmp4);
#line 422
  ptr = (struct zr36016 *)__cil_tmp5;
  {
#line 424
  __cil_tmp6 = (struct zr36016 *)0;
#line 424
  __cil_tmp7 = (unsigned long )__cil_tmp6;
#line 424
  __cil_tmp8 = (unsigned long )ptr;
#line 424
  if (__cil_tmp8 != __cil_tmp7) {
    {
#line 427
    __cil_tmp9 = & debug;
#line 427
    __cil_tmp10 = *__cil_tmp9;
#line 427
    if (__cil_tmp10 > 0) {
      {
#line 427
      __cil_tmp11 = (char (*)[32U])ptr;
#line 427
      __cil_tmp12 = (char *)__cil_tmp11;
#line 427
      __cil_tmp13 = (unsigned long )ptr;
#line 427
      __cil_tmp14 = __cil_tmp13 + 32;
#line 427
      __cil_tmp15 = *((int *)__cil_tmp14);
#line 427
      printk("%s: finished codec #%d\n", __cil_tmp12, __cil_tmp15);
      }
    } else {

    }
    }
    {
#line 429
    __cil_tmp16 = (void const   *)ptr;
#line 429
    kfree(__cil_tmp16);
#line 430
    __cil_tmp17 = (unsigned long )codec;
#line 430
    __cil_tmp18 = __cil_tmp17 + 72;
#line 430
    *((void **)__cil_tmp18) = (void *)0;
#line 432
    zr36016_codecs = zr36016_codecs - 1;
    }
#line 433
    return (0);
  } else {

  }
  }
#line 436
  return (-14);
}
}
#line 449 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
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 ;
  struct zr36016 *__cil_tmp12 ;
  unsigned long __cil_tmp13 ;
  unsigned long __cil_tmp14 ;
  int *__cil_tmp15 ;
  int __cil_tmp16 ;
  char (*__cil_tmp17)[32U] ;
  char *__cil_tmp18 ;
  unsigned long __cil_tmp19 ;
  unsigned long __cil_tmp20 ;
  unsigned long __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 ;
  int *__cil_tmp33 ;
  int __cil_tmp34 ;
  char (*__cil_tmp35)[32U] ;
  char *__cil_tmp36 ;
  unsigned long __cil_tmp37 ;
  unsigned long __cil_tmp38 ;
  __u8 __cil_tmp39 ;
  int __cil_tmp40 ;

  {
  {
#line 454
  __cil_tmp6 = & debug;
#line 454
  __cil_tmp7 = *__cil_tmp6;
#line 454
  if (__cil_tmp7 > 1) {
    {
#line 454
    printk("zr36016: initializing VFE subsystem #%d.\n", zr36016_codecs);
    }
  } else {

  }
  }
#line 457
  if (zr36016_codecs == 20) {
    {
#line 458
    __cil_tmp8 = & debug;
#line 458
    __cil_tmp9 = *__cil_tmp8;
#line 458
    if (__cil_tmp9 > 0) {
      {
#line 458
      printk("<3>zr36016: Can\'t attach more codecs!\n");
      }
    } else {

    }
    }
#line 460
    return (-28);
  } else {

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

    }
    }
#line 466
    return (-12);
  } else {

  }
  }
  {
#line 469
  __cil_tmp17 = (char (*)[32U])ptr;
#line 469
  __cil_tmp18 = (char *)__cil_tmp17;
#line 469
  snprintf(__cil_tmp18, 32UL, "zr36016[%d]", zr36016_codecs);
#line 471
  tmp___0 = zr36016_codecs;
#line 471
  zr36016_codecs = zr36016_codecs + 1;
#line 471
  __cil_tmp19 = (unsigned long )ptr;
#line 471
  __cil_tmp20 = __cil_tmp19 + 32;
#line 471
  *((int *)__cil_tmp20) = tmp___0;
#line 472
  __cil_tmp21 = (unsigned long )ptr;
#line 472
  __cil_tmp22 = __cil_tmp21 + 40;
#line 472
  *((struct videocodec **)__cil_tmp22) = codec;
#line 475
  res = zr36016_basic_test(ptr);
  }
#line 476
  if (res < 0) {
    {
#line 477
    zr36016_unset(codec);
    }
#line 478
    return (res);
  } else {

  }
  {
#line 481
  __cil_tmp23 = (unsigned long )ptr;
#line 481
  __cil_tmp24 = __cil_tmp23 + 52;
#line 481
  *((int *)__cil_tmp24) = 0;
#line 482
  __cil_tmp25 = (unsigned long )ptr;
#line 482
  __cil_tmp26 = __cil_tmp25 + 60;
#line 482
  *((__u16 *)__cil_tmp26) = (__u16 )768U;
#line 483
  __cil_tmp27 = (unsigned long )ptr;
#line 483
  __cil_tmp28 = __cil_tmp27 + 62;
#line 483
  *((__u16 *)__cil_tmp28) = (__u16 )288U;
#line 484
  __cil_tmp29 = (unsigned long )ptr;
#line 484
  __cil_tmp30 = __cil_tmp29 + 64;
#line 484
  *((__u16 *)__cil_tmp30) = (__u16 )1U;
#line 485
  __cil_tmp31 = (unsigned long )ptr;
#line 485
  __cil_tmp32 = __cil_tmp31 + 66;
#line 485
  *((__u16 *)__cil_tmp32) = (__u16 )0U;
#line 486
  zr36016_init(ptr);
  }
  {
#line 488
  __cil_tmp33 = & debug;
#line 488
  __cil_tmp34 = *__cil_tmp33;
#line 488
  if (__cil_tmp34 > 0) {
    {
#line 488
    __cil_tmp35 = (char (*)[32U])ptr;
#line 488
    __cil_tmp36 = (char *)__cil_tmp35;
#line 488
    __cil_tmp37 = (unsigned long )ptr;
#line 488
    __cil_tmp38 = __cil_tmp37 + 48;
#line 488
    __cil_tmp39 = *((__u8 *)__cil_tmp38);
#line 488
    __cil_tmp40 = (int )__cil_tmp39;
#line 488
    printk("<6>%s: codec v%d attached and running\n", __cil_tmp36, __cil_tmp40);
    }
  } else {

  }
  }
#line 491
  return (0);
}
}
#line 494 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
static struct videocodec  const  zr36016_codec  = 
#line 494
     {& __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 * , long  ))0, (int (*)(struct videocodec * ,
                                                                          int  , long  ))0,
    (long (*)(struct videocodec * , int  , int  , long * , long * , long  , void * ))0,
    (long (*)(struct videocodec * , int  , int  , long * , long * , long  , void * ))0};
#line 515 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
static int zr36016_init_module(void) 
{ int tmp ;

  {
  {
#line 518
  zr36016_codecs = 0;
#line 519
  tmp = videocodec_register(& zr36016_codec);
  }
#line 519
  return (tmp);
}
}
#line 523 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
static void zr36016_cleanup_module(void) 
{ int *__cil_tmp1 ;
  int __cil_tmp2 ;

  {
#line 525
  if (zr36016_codecs != 0) {
    {
#line 526
    __cil_tmp1 = & debug;
#line 526
    __cil_tmp2 = *__cil_tmp1;
#line 526
    if (__cil_tmp2 > 0) {
      {
#line 526
      printk("zr36016: something\'s wrong - %d codecs left somehow.\n", zr36016_codecs);
      }
    } else {

    }
    }
  } else {

  }
  {
#line 530
  videocodec_unregister(& zr36016_codec);
  }
#line 531
  return;
}
}
#line 557
extern void ldv_check_final_state(void) ;
#line 563
extern void ldv_initialize(void) ;
#line 566
extern int __VERIFIER_nondet_int(void) ;
#line 569 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
int LDV_IN_INTERRUPT  ;
#line 572 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
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 662
  LDV_IN_INTERRUPT = 1;
#line 671
  ldv_initialize();
#line 687
  tmp = zr36016_init_module();
  }
#line 687
  if (tmp != 0) {
#line 688
    goto ldv_final;
  } else {

  }
#line 692
  goto ldv_15221;
  ldv_15220: 
  {
#line 695
  tmp___0 = __VERIFIER_nondet_int();
  }
#line 697
  if (tmp___0 == 0) {
#line 697
    goto case_0;
  } else
#line 723
  if (tmp___0 == 1) {
#line 723
    goto case_1;
  } else
#line 749
  if (tmp___0 == 2) {
#line 749
    goto case_2;
  } else
#line 775
  if (tmp___0 == 3) {
#line 775
    goto case_3;
  } else
#line 801
  if (tmp___0 == 4) {
#line 801
    goto case_4;
  } else {
    {
#line 827
    goto switch_default;
#line 695
    if (0) {
      case_0: /* CIL Label */ 
      {
#line 715
      zr36016_setup(var_group1);
      }
#line 722
      goto ldv_15214;
      case_1: /* CIL Label */ 
      {
#line 741
      zr36016_unset(var_group1);
      }
#line 748
      goto ldv_15214;
      case_2: /* CIL Label */ 
      {
#line 767
      zr36016_set_mode(var_group1, var_zr36016_set_mode_8_p1);
      }
#line 774
      goto ldv_15214;
      case_3: /* CIL Label */ 
      {
#line 793
      zr36016_set_video(var_group1, var_group2, var_zr36016_set_video_9_p2, var_zr36016_set_video_9_p3);
      }
#line 800
      goto ldv_15214;
      case_4: /* CIL Label */ 
      {
#line 819
      zr36016_control(var_group1, var_zr36016_control_10_p1, var_zr36016_control_10_p2,
                      var_zr36016_control_10_p3);
      }
#line 826
      goto ldv_15214;
      switch_default: /* CIL Label */ ;
#line 827
      goto ldv_15214;
    } else {
      switch_break: /* CIL Label */ ;
    }
    }
  }
  ldv_15214: ;
  ldv_15221: 
  {
#line 692
  tmp___1 = __VERIFIER_nondet_int();
  }
#line 692
  if (tmp___1 != 0) {
#line 693
    goto ldv_15220;
  } else {
#line 695
    goto ldv_15222;
  }
  ldv_15222: ;
  {
#line 849
  zr36016_cleanup_module();
  }
  ldv_final: 
  {
#line 852
  ldv_check_final_state();
  }
#line 855
  return;
}
}
#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/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--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
extern int __VERIFIER_nondet_int(void) ;
#line 876 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
int ldv_spin  =    0;
#line 880 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
void ldv_check_alloc_flags(gfp_t flags ) 
{ 

  {
#line 883
  if (ldv_spin != 0) {
#line 883
    if (flags != 32U) {
      {
#line 883
      ldv_blast_assert();
      }
    } else {

    }
  } else {

  }
#line 886
  return;
}
}
#line 886
extern struct page *ldv_some_page(void) ;
#line 889 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) 
{ struct page *tmp ;

  {
#line 892
  if (ldv_spin != 0) {
#line 892
    if (flags != 32U) {
      {
#line 892
      ldv_blast_assert();
      }
    } else {

    }
  } else {

  }
  {
#line 894
  tmp = ldv_some_page();
  }
#line 894
  return (tmp);
}
}
#line 898 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
void ldv_check_alloc_nonatomic(void) 
{ 

  {
#line 901
  if (ldv_spin != 0) {
    {
#line 901
    ldv_blast_assert();
    }
  } else {

  }
#line 904
  return;
}
}
#line 905 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
void ldv_spin_lock(void) 
{ 

  {
#line 908
  ldv_spin = 1;
#line 909
  return;
}
}
#line 912 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
void ldv_spin_unlock(void) 
{ 

  {
#line 915
  ldv_spin = 0;
#line 916
  return;
}
}
#line 919 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
int ldv_spin_trylock(void) 
{ int is_lock ;

  {
  {
#line 924
  is_lock = __VERIFIER_nondet_int();
  }
#line 926
  if (is_lock != 0) {
#line 929
    return (0);
  } else {
#line 934
    ldv_spin = 1;
#line 936
    return (1);
  }
}
}
#line 1103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) 
{ 

  {
  {
#line 1109
  ldv_check_alloc_flags(ldv_func_arg2);
#line 1111
  kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
  }
#line 1112
  return ((void *)0);
}
}
#line 1114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/7511/dscv_tempdir/dscv/ri/43_1a/drivers/media/video/zoran/zr36016.c.p"
__inline static void *kzalloc(size_t size , gfp_t flags ) 
{ void *tmp ;

  {
  {
#line 1120
  ldv_check_alloc_flags(flags);
#line 1121
  tmp = __VERIFIER_nondet_pointer();
  }
#line 1121
  return (tmp);
}
}