ClabureDB: Classified Bug-Reports Database

   /* Generated by CIL v. 1.3.7 */
   /* print_CIL_Input is true */
   
   #line 45 "include/asm-generic/int-ll64.h"
   typedef short s16;
   #line 46 "include/asm-generic/int-ll64.h"
   typedef unsigned short u16;
   #line 48 "include/asm-generic/int-ll64.h"
   typedef int s32;
  #line 49 "include/asm-generic/int-ll64.h"
  typedef unsigned int u32;
  #line 51 "include/asm-generic/int-ll64.h"
  typedef long long s64;
  #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 63 "include/linux/types.h"
  typedef __kernel_size_t size_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 47 "include/linux/dynamic_debug.h"
  struct device;
  #line 47
  struct device;
  #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 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
  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 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 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
  struct __anonstruct____missing_field_name_38 {
     u32 read ;
     s32 write ;
  };
  #line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
  union __anonunion_arch_rwlock_t_37 {
     s64 lock ;
     struct __anonstruct____missing_field_name_38 __annonCompField18 ;
  };
  #line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
  typedef union __anonunion_arch_rwlock_t_37 arch_rwlock_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 20 "include/linux/spinlock_types.h"
 typedef struct raw_spinlock raw_spinlock_t;
 #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 11 "include/linux/rwlock_types.h"
 struct __anonstruct_rwlock_t_40 {
    arch_rwlock_t raw_lock ;
    unsigned int magic ;
    unsigned int owner_cpu ;
    void *owner ;
 };
 #line 11 "include/linux/rwlock_types.h"
 typedef struct __anonstruct_rwlock_t_40 rwlock_t;
 #line 55 "include/linux/wait.h"
 struct task_struct;
 #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 19 "include/linux/rwsem.h"
 struct rw_semaphore;
 #line 19
 struct rw_semaphore;
 #line 25 "include/linux/rwsem.h"
 struct rw_semaphore {
    long count ;
    raw_spinlock_t wait_lock ;
    struct list_head wait_list ;
 };
 #line 202 "include/linux/ioport.h"
 struct device;
 #line 103 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/mpspec.h"
 struct device;
 #line 10 "include/linux/timer.h"
 struct tvec_base;
 #line 10
 struct tvec_base;
 #line 12 "include/linux/timer.h"
 struct timer_list {
    struct list_head entry ;
    unsigned long expires ;
    struct tvec_base *base ;
    void (*function)(unsigned long  ) ;
    unsigned long data ;
    int slack ;
    int start_pid ;
    void *start_site ;
    char start_comm[16] ;
 };
 #line 17 "include/linux/workqueue.h"
 struct work_struct;
 #line 17
 struct work_struct;
 #line 79 "include/linux/workqueue.h"
 struct work_struct {
    atomic_long_t data ;
    struct list_head entry ;
    void (*func)(struct work_struct *work ) ;
 };
 #line 42 "include/linux/pm.h"
 struct device;
 #line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
 struct task_struct;
 #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 20 "include/linux/leds.h"
 struct device;
 #line 25
 enum led_brightness {
     LED_OFF = 0,
     LED_HALF = 127,
     LED_FULL = 255
 } ;
 #line 31
 struct led_trigger;
 #line 31 "include/linux/leds.h"
 struct led_classdev {
    char const   *name ;
    int brightness ;
    int max_brightness ;
    int flags ;
    void (*brightness_set)(struct led_classdev *led_cdev , enum led_brightness brightness ) ;
    enum led_brightness (*brightness_get)(struct led_classdev *led_cdev ) ;
    int (*blink_set)(struct led_classdev *led_cdev , unsigned long *delay_on , unsigned long *delay_off ) ;
    struct device *dev ;
    struct list_head node ;
    char const   *default_trigger ;
    unsigned long blink_delay_on ;
    unsigned long blink_delay_off ;
    struct timer_list blink_timer ;
    int blink_brightness ;
    struct rw_semaphore trigger_lock ;
    struct led_trigger *trigger ;
    struct list_head trig_list ;
    void *trigger_data ;
 };
 #line 122 "include/linux/leds.h"
 struct led_trigger {
    char const   *name ;
    void (*activate)(struct led_classdev *led_cdev ) ;
    void (*deactivate)(struct led_classdev *led_cdev ) ;
    rwlock_t leddev_list_lock ;
    struct list_head led_cdevs ;
    struct list_head next_trig ;
 };
 #line 19 "include/linux/power_supply.h"
 struct device;
 #line 84
 enum power_supply_property {
     POWER_SUPPLY_PROP_STATUS = 0,
     POWER_SUPPLY_PROP_CHARGE_TYPE = 1,
     POWER_SUPPLY_PROP_HEALTH = 2,
     POWER_SUPPLY_PROP_PRESENT = 3,
     POWER_SUPPLY_PROP_ONLINE = 4,
     POWER_SUPPLY_PROP_TECHNOLOGY = 5,
     POWER_SUPPLY_PROP_CYCLE_COUNT = 6,
     POWER_SUPPLY_PROP_VOLTAGE_MAX = 7,
     POWER_SUPPLY_PROP_VOLTAGE_MIN = 8,
     POWER_SUPPLY_PROP_VOLTAGE_MAX_DESIGN = 9,
     POWER_SUPPLY_PROP_VOLTAGE_MIN_DESIGN = 10,
     POWER_SUPPLY_PROP_VOLTAGE_NOW = 11,
     POWER_SUPPLY_PROP_VOLTAGE_AVG = 12,
     POWER_SUPPLY_PROP_CURRENT_MAX = 13,
     POWER_SUPPLY_PROP_CURRENT_NOW = 14,
     POWER_SUPPLY_PROP_CURRENT_AVG = 15,
     POWER_SUPPLY_PROP_POWER_NOW = 16,
     POWER_SUPPLY_PROP_POWER_AVG = 17,
     POWER_SUPPLY_PROP_CHARGE_FULL_DESIGN = 18,
     POWER_SUPPLY_PROP_CHARGE_EMPTY_DESIGN = 19,
     POWER_SUPPLY_PROP_CHARGE_FULL = 20,
     POWER_SUPPLY_PROP_CHARGE_EMPTY = 21,
     POWER_SUPPLY_PROP_CHARGE_NOW = 22,
     POWER_SUPPLY_PROP_CHARGE_AVG = 23,
     POWER_SUPPLY_PROP_CHARGE_COUNTER = 24,
     POWER_SUPPLY_PROP_ENERGY_FULL_DESIGN = 25,
     POWER_SUPPLY_PROP_ENERGY_EMPTY_DESIGN = 26,
     POWER_SUPPLY_PROP_ENERGY_FULL = 27,
     POWER_SUPPLY_PROP_ENERGY_EMPTY = 28,
     POWER_SUPPLY_PROP_ENERGY_NOW = 29,
     POWER_SUPPLY_PROP_ENERGY_AVG = 30,
     POWER_SUPPLY_PROP_CAPACITY = 31,
     POWER_SUPPLY_PROP_CAPACITY_LEVEL = 32,
     POWER_SUPPLY_PROP_TEMP = 33,
     POWER_SUPPLY_PROP_TEMP_AMBIENT = 34,
     POWER_SUPPLY_PROP_TIME_TO_EMPTY_NOW = 35,
     POWER_SUPPLY_PROP_TIME_TO_EMPTY_AVG = 36,
     POWER_SUPPLY_PROP_TIME_TO_FULL_NOW = 37,
     POWER_SUPPLY_PROP_TIME_TO_FULL_AVG = 38,
     POWER_SUPPLY_PROP_TYPE = 39,
     POWER_SUPPLY_PROP_SCOPE = 40,
     POWER_SUPPLY_PROP_MODEL_NAME = 41,
     POWER_SUPPLY_PROP_MANUFACTURER = 42,
     POWER_SUPPLY_PROP_SERIAL_NUMBER = 43
 } ;
 #line 133
 enum power_supply_type {
     POWER_SUPPLY_TYPE_UNKNOWN = 0,
     POWER_SUPPLY_TYPE_BATTERY = 1,
     POWER_SUPPLY_TYPE_UPS = 2,
     POWER_SUPPLY_TYPE_MAINS = 3,
     POWER_SUPPLY_TYPE_USB = 4,
     POWER_SUPPLY_TYPE_USB_DCP = 5,
     POWER_SUPPLY_TYPE_USB_CDP = 6,
     POWER_SUPPLY_TYPE_USB_ACA = 7
 } ;
 #line 144 "include/linux/power_supply.h"
 union power_supply_propval {
    int intval ;
    char const   *strval ;
 };
 #line 149 "include/linux/power_supply.h"
 struct power_supply {
    char const   *name ;
    enum power_supply_type type ;
    enum power_supply_property *properties ;
    size_t num_properties ;
    char **supplied_to ;
    size_t num_supplicants ;
    int (*get_property)(struct power_supply *psy , enum power_supply_property psp ,
                        union power_supply_propval *val ) ;
    int (*set_property)(struct power_supply *psy , enum power_supply_property psp ,
                        union power_supply_propval  const  *val ) ;
    int (*property_is_writeable)(struct power_supply *psy , enum power_supply_property psp ) ;
    void (*external_power_changed)(struct power_supply *psy ) ;
    void (*set_charged)(struct power_supply *psy ) ;
    int use_for_apm ;
    struct device *dev ;
    struct work_struct changed_work ;
    struct led_trigger *charging_full_trig ;
    char *charging_full_trig_name ;
    struct led_trigger *charging_trig ;
    char *charging_trig_name ;
    struct led_trigger *full_trig ;
    char *full_trig_name ;
    struct led_trigger *online_trig ;
    char *online_trig_name ;
    struct led_trigger *charging_blink_full_solid_trig ;
    char *charging_blink_full_solid_trig_name ;
 };
 #line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 struct __anonstruct_207 {
    int  : 0 ;
 };
 #line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 struct __anonstruct_208 {
    int  : 0 ;
 };
 #line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 struct __anonstruct_209 {
    int  : 0 ;
 };
 #line 148 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 struct __anonstruct_210 {
    int  : 0 ;
 };
 #line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 struct __anonstruct_211 {
    int  : 0 ;
 };
 #line 178 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 struct __anonstruct_212 {
    int  : 0 ;
 };
 #line 186 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 struct battery_property_map {
    int value ;
    char const   *key ;
 };
 #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 334 "include/linux/kernel.h"
 extern int ( /* format attribute */  sscanf)(char const   * , char const   *  , ...) ;
 #line 61 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
 extern unsigned long strlen(char const   *s ) ;
 #line 62
 extern char *strcpy(char *dest , char const   *src ) ;
 #line 27 "include/linux/string.h"
 extern char *strncpy(char * , char const   * , __kernel_size_t  ) ;
 #line 54
 extern int strncasecmp(char const   *s1 , char const   *s2 , size_t n ) ;
 #line 84
 extern __kernel_size_t strnlen(char const   * , __kernel_size_t  ) ;
 #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 358 "include/linux/moduleparam.h"
 extern int param_get_int(char *buffer , struct kernel_param  const  *kp ) ;
 #line 67 "include/linux/module.h"
 int init_module(void) ;
 #line 68
 void cleanup_module(void) ;
 #line 210 "include/linux/power_supply.h"
 extern void power_supply_changed(struct power_supply *psy ) ;
 #line 220
 extern int power_supply_register(struct device *parent , struct power_supply *psy ) ;
 #line 222
 extern void power_supply_unregister(struct power_supply *psy ) ;
 #line 46 "include/linux/delay.h"
 extern void msleep(unsigned int msecs ) ;
 #line 50
 __inline static void ssleep(unsigned int seconds )  __attribute__((__no_instrument_function__)) ;
 #line 50 "include/linux/delay.h"
 __inline static void ssleep(unsigned int seconds ) 
 { unsigned int __cil_tmp2 ;
 
   {
   {
 #line 52
   __cil_tmp2 = seconds * 1000U;
 #line 52
   msleep(__cil_tmp2);
   }
 #line 53
   return;
 }
 }
 #line 25 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int ac_online  =    1;
 #line 26 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int battery_status  =    2;
 #line 27 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int battery_health  =    1;
 #line 28 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int battery_present  =    1;
 #line 29 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int battery_technology  =    2;
 #line 30 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int battery_capacity  =    50;
 #line 32 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int test_power_get_ac_property(struct power_supply *psy , enum power_supply_property psp ,
                                       union power_supply_propval *val ) 
 { int *__cil_tmp4 ;
 
   {
 #line 37
   if ((int )psp == 4) {
 #line 37
     goto case_4;
   } else {
     {
 #line 40
     goto switch_default;
 #line 36
     if (0) {
       case_4: /* CIL Label */ 
 #line 38
       __cil_tmp4 = & ac_online;
 #line 38
       *((int *)val) = *__cil_tmp4;
 #line 39
       goto switch_break;
       switch_default: /* CIL Label */ 
 #line 41
       return (-22);
     } else {
       switch_break: /* CIL Label */ ;
     }
     }
   }
 #line 43
   return (0);
 }
 }
 #line 46 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int test_power_get_battery_property(struct power_supply *psy , enum power_supply_property psp ,
                                            union power_supply_propval *val ) 
 { int *__cil_tmp4 ;
   int *__cil_tmp5 ;
   int *__cil_tmp6 ;
   int *__cil_tmp7 ;
   int *__cil_tmp8 ;
 
   {
 #line 51
   if ((int )psp == 41) {
 #line 51
     goto case_41;
   } else
 #line 54
   if ((int )psp == 42) {
 #line 54
     goto case_42;
   } else
 #line 57
   if ((int )psp == 43) {
 #line 57
     goto case_43;
   } else
 #line 60
   if ((int )psp == 0) {
 #line 60
     goto case_0;
   } else
 #line 63
   if ((int )psp == 1) {
 #line 63
     goto case_1;
   } else
 #line 66
   if ((int )psp == 2) {
 #line 66
     goto case_2;
   } else
 #line 69
   if ((int )psp == 3) {
 #line 69
     goto case_3;
   } else
 #line 72
   if ((int )psp == 5) {
 #line 72
     goto case_5;
   } else
 #line 75
   if ((int )psp == 32) {
 #line 75
     goto case_32;
   } else
 #line 78
   if ((int )psp == 31) {
 #line 78
     goto case_31;
   } else
 #line 79
   if ((int )psp == 22) {
 #line 79
     goto case_31;
   } else
 #line 82
   if ((int )psp == 18) {
 #line 82
     goto case_18;
   } else
 #line 83
   if ((int )psp == 20) {
 #line 83
     goto case_18;
   } else
 #line 86
   if ((int )psp == 36) {
 #line 86
     goto case_36;
   } else
 #line 87
   if ((int )psp == 37) {
 #line 87
     goto case_36;
   } else {
     {
 #line 90
     goto switch_default;
 #line 50
     if (0) {
       case_41: /* CIL Label */ 
 #line 52
       *((char const   **)val) = "Test battery";
 #line 53
       goto switch_break;
       case_42: /* CIL Label */ 
 #line 55
       *((char const   **)val) = "Linux";
 #line 56
       goto switch_break;
       case_43: /* CIL Label */ 
 #line 58
       *((char const   **)val) = "3.4.0";
 #line 59
       goto switch_break;
       case_0: /* CIL Label */ 
 #line 61
       __cil_tmp4 = & battery_status;
 #line 61
       *((int *)val) = *__cil_tmp4;
 #line 62
       goto switch_break;
       case_1: /* CIL Label */ 
 #line 64
       *((int *)val) = 3;
 #line 65
       goto switch_break;
       case_2: /* CIL Label */ 
 #line 67
       __cil_tmp5 = & battery_health;
 #line 67
       *((int *)val) = *__cil_tmp5;
 #line 68
       goto switch_break;
       case_3: /* CIL Label */ 
 #line 70
       __cil_tmp6 = & battery_present;
 #line 70
       *((int *)val) = *__cil_tmp6;
 #line 71
       goto switch_break;
       case_5: /* CIL Label */ 
 #line 73
       __cil_tmp7 = & battery_technology;
 #line 73
       *((int *)val) = *__cil_tmp7;
 #line 74
       goto switch_break;
       case_32: /* CIL Label */ 
 #line 76
       *((int *)val) = 3;
 #line 77
       goto switch_break;
       case_31: /* CIL Label */ 
       case_22: /* CIL Label */ 
 #line 80
       __cil_tmp8 = & battery_capacity;
 #line 80
       *((int *)val) = *__cil_tmp8;
 #line 81
       goto switch_break;
       case_18: /* CIL Label */ 
       case_20: /* CIL Label */ 
 #line 84
       *((int *)val) = 100;
 #line 85
       goto switch_break;
       case_36: /* CIL Label */ 
       case_37: /* CIL Label */ 
 #line 88
       *((int *)val) = 3600;
 #line 89
       goto switch_break;
       switch_default: /* CIL Label */ 
       {
 #line 91
       printk("<6>%s: some properties deliberately report errors.\n", "test_power_get_battery_property");
       }
 #line 93
       return (-22);
     } else {
       switch_break: /* CIL Label */ ;
     }
     }
   }
 #line 95
   return (0);
 }
 }
 #line 98 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static enum power_supply_property test_power_ac_props[1]  = {      (enum power_supply_property )4};
 #line 102 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static enum power_supply_property test_power_battery_props[15]  = 
 #line 102
   {      (enum power_supply_property )0,      (enum power_supply_property )1,      (enum power_supply_property )2,      (enum power_supply_property )3, 
         (enum power_supply_property )5,      (enum power_supply_property )18,      (enum power_supply_property )20,      (enum power_supply_property )22, 
         (enum power_supply_property )31,      (enum power_supply_property )32,      (enum power_supply_property )36,      (enum power_supply_property )37, 
         (enum power_supply_property )41,      (enum power_supply_property )42,      (enum power_supply_property )43};
 #line 120 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static char *test_power_ac_supplied_to[1]  = {      (char *)"test_battery"};
 #line 124 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static struct power_supply test_power_supplies[2]  = {      {"test_ac", (enum power_supply_type )3, test_power_ac_props, sizeof(test_power_ac_props) / sizeof(test_power_ac_props[0]) + sizeof(struct __anonstruct_208 ),
       test_power_ac_supplied_to, sizeof(test_power_ac_supplied_to) / sizeof(test_power_ac_supplied_to[0]) + sizeof(struct __anonstruct_207 ),
       & test_power_get_ac_property, (int (*)(struct power_supply *psy , enum power_supply_property psp ,
                                              union power_supply_propval  const  *val ))0,
       (int (*)(struct power_supply *psy , enum power_supply_property psp ))0, (void (*)(struct power_supply *psy ))0,
       (void (*)(struct power_supply *psy ))0, 0, (struct device *)0, {{0L}, {(struct list_head *)0,
                                                                              (struct list_head *)0},
                                                                       (void (*)(struct work_struct *work ))0},
       (struct led_trigger *)0, (char *)0, (struct led_trigger *)0, (char *)0, (struct led_trigger *)0,
       (char *)0, (struct led_trigger *)0, (char *)0, (struct led_trigger *)0, (char *)0}, 
         {"test_battery",
       (enum power_supply_type )1, test_power_battery_props, sizeof(test_power_battery_props) / sizeof(test_power_battery_props[0]) + sizeof(struct __anonstruct_209 ),
       (char **)0, 0UL, & test_power_get_battery_property, (int (*)(struct power_supply *psy ,
                                                                    enum power_supply_property psp ,
                                                                    union power_supply_propval  const  *val ))0,
       (int (*)(struct power_supply *psy , enum power_supply_property psp ))0, (void (*)(struct power_supply *psy ))0,
       (void (*)(struct power_supply *psy ))0, 0, (struct device *)0, {{0L}, {(struct list_head *)0,
                                                                              (struct list_head *)0},
                                                                       (void (*)(struct work_struct *work ))0},
       (struct led_trigger *)0, (char *)0, (struct led_trigger *)0, (char *)0, (struct led_trigger *)0,
       (char *)0, (struct led_trigger *)0, (char *)0, (struct led_trigger *)0, (char *)0}};
 #line 143
 static int test_power_init(void)  __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
 #line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int test_power_init(void) 
 { int i ;
   int ret ;
   unsigned long __cil_tmp3 ;
   unsigned long __cil_tmp4 ;
   unsigned long __cil_tmp5 ;
   void *__cil_tmp6 ;
   struct device *__cil_tmp7 ;
   unsigned long __cil_tmp8 ;
   unsigned long __cil_tmp9 ;
   struct power_supply *__cil_tmp10 ;
   unsigned long __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   char const   *__cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   unsigned long __cil_tmp15 ;
   struct power_supply *__cil_tmp16 ;
 
   {
 #line 148
   i = 0;
   {
 #line 148
   while (1) {
     while_continue: /* CIL Label */ ;
     {
 #line 148
     __cil_tmp3 = 432UL / 216UL;
 #line 148
     __cil_tmp4 = __cil_tmp3 + 0UL;
 #line 148
     __cil_tmp5 = (unsigned long )i;
 #line 148
     if (__cil_tmp5 < __cil_tmp4) {
 
     } else {
 #line 148
       goto while_break;
     }
     }
     {
 #line 149
     __cil_tmp6 = (void *)0;
 #line 149
     __cil_tmp7 = (struct device *)__cil_tmp6;
 #line 149
     __cil_tmp8 = i * 216UL;
 #line 149
     __cil_tmp9 = (unsigned long )(test_power_supplies) + __cil_tmp8;
 #line 149
     __cil_tmp10 = (struct power_supply *)__cil_tmp9;
 #line 149
     ret = power_supply_register(__cil_tmp7, __cil_tmp10);
     }
 #line 150
     if (ret) {
       {
 #line 151
       __cil_tmp11 = i * 216UL;
 #line 151
       __cil_tmp12 = (unsigned long )(test_power_supplies) + __cil_tmp11;
 #line 151
       __cil_tmp13 = *((char const   **)__cil_tmp12);
 #line 151
       printk("<3>%s: failed to register %s\n", "test_power_init", __cil_tmp13);
       }
 #line 153
       goto failed;
     } else {
 
     }
 #line 148
     i = i + 1;
   }
   while_break: /* CIL Label */ ;
   }
 #line 157
   return (0);
   failed: 
   {
 #line 159
   while (1) {
     while_continue___0: /* CIL Label */ ;
 #line 159
     i = i - 1;
 #line 159
     if (i >= 0) {
 
     } else {
 #line 159
       goto while_break___0;
     }
     {
 #line 160
     __cil_tmp14 = i * 216UL;
 #line 160
     __cil_tmp15 = (unsigned long )(test_power_supplies) + __cil_tmp14;
 #line 160
     __cil_tmp16 = (struct power_supply *)__cil_tmp15;
 #line 160
     power_supply_unregister(__cil_tmp16);
     }
   }
   while_break___0: /* CIL Label */ ;
   }
 #line 161
   return (ret);
 }
 }
 #line 163 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 int init_module(void) 
 { int tmp ;
 
   {
   {
 #line 163
   tmp = test_power_init();
   }
 #line 163
   return (tmp);
 }
 }
 #line 165
 static void test_power_exit(void)  __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
 #line 165 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static void test_power_exit(void) 
 { int i ;
   int *__cil_tmp2 ;
   int *__cil_tmp3 ;
   unsigned long __cil_tmp4 ;
   unsigned long __cil_tmp5 ;
   unsigned long __cil_tmp6 ;
   unsigned long __cil_tmp7 ;
   unsigned long __cil_tmp8 ;
   struct power_supply *__cil_tmp9 ;
   unsigned long __cil_tmp10 ;
   unsigned long __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   struct power_supply *__cil_tmp15 ;
 
   {
 #line 170
   __cil_tmp2 = & ac_online;
 #line 170
   *__cil_tmp2 = 0;
 #line 171
   __cil_tmp3 = & battery_status;
 #line 171
   *__cil_tmp3 = 2;
 #line 172
   i = 0;
   {
 #line 172
   while (1) {
     while_continue: /* CIL Label */ ;
     {
 #line 172
     __cil_tmp4 = 432UL / 216UL;
 #line 172
     __cil_tmp5 = __cil_tmp4 + 0UL;
 #line 172
     __cil_tmp6 = (unsigned long )i;
 #line 172
     if (__cil_tmp6 < __cil_tmp5) {
 
     } else {
 #line 172
       goto while_break;
     }
     }
     {
 #line 173
     __cil_tmp7 = i * 216UL;
 #line 173
     __cil_tmp8 = (unsigned long )(test_power_supplies) + __cil_tmp7;
 #line 173
     __cil_tmp9 = (struct power_supply *)__cil_tmp8;
 #line 173
     power_supply_changed(__cil_tmp9);
 #line 172
     i = i + 1;
     }
   }
   while_break: /* CIL Label */ ;
   }
   {
 #line 174
   printk("<6>%s: \'changed\' event sent, sleeping for 10 seconds...\n", "test_power_exit");
 #line 176
   ssleep(10U);
 #line 178
   i = 0;
   }
   {
 #line 178
   while (1) {
     while_continue___0: /* CIL Label */ ;
     {
 #line 178
     __cil_tmp10 = 432UL / 216UL;
 #line 178
     __cil_tmp11 = __cil_tmp10 + 0UL;
 #line 178
     __cil_tmp12 = (unsigned long )i;
 #line 178
     if (__cil_tmp12 < __cil_tmp11) {
 
     } else {
 #line 178
       goto while_break___0;
     }
     }
     {
 #line 179
     __cil_tmp13 = i * 216UL;
 #line 179
     __cil_tmp14 = (unsigned long )(test_power_supplies) + __cil_tmp13;
 #line 179
     __cil_tmp15 = (struct power_supply *)__cil_tmp14;
 #line 179
     power_supply_unregister(__cil_tmp15);
 #line 178
     i = i + 1;
     }
   }
   while_break___0: /* CIL Label */ ;
   }
 #line 180
   return;
 }
 }
 #line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 void cleanup_module(void) 
 { 
 
   {
   {
 #line 181
   test_power_exit();
   }
 #line 181
   return;
 }
 }
 #line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static struct battery_property_map map_ac_online[3]  = {      {0, "on"}, 
         {1, "off"}, 
         {-1, (char const   *)((void *)0)}};
 #line 197 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static struct battery_property_map map_status[5]  = {      {1, "charging"}, 
         {2, "discharging"}, 
         {3, "not-charging"}, 
         {4, "full"}, 
         {-1, (char const   *)((void *)0)}};
 #line 205 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static struct battery_property_map map_health[6]  = {      {1, "good"}, 
         {2, "overheat"}, 
         {3, "dead"}, 
         {4, "overvoltage"}, 
         {5, "failure"}, 
         {-1, (char const   *)((void *)0)}};
 #line 214 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static struct battery_property_map map_present[3]  = {      {0, "false"}, 
         {1, "true"}, 
         {-1, (char const   *)((void *)0)}};
 #line 220 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static struct battery_property_map map_technology[7]  = {      {1, "NiMH"}, 
         {2, "LION"}, 
         {3, "LIPO"}, 
         {4, "LiFe"}, 
         {5, "NiCd"}, 
         {6, "LiMn"}, 
         {-1, (char const   *)((void *)0)}};
 #line 231 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
 static int map_get_value(struct battery_property_map *map , char const   *key , int def_val ) 
 { char buf[256] ;
   int cr ;
   __kernel_size_t tmp ;
   int tmp___0 ;
   unsigned long __cil_tmp8 ;
   unsigned long __cil_tmp9 ;
   char *__cil_tmp10 ;
   __kernel_size_t __cil_tmp11 ;
   unsigned long __cil_tmp12 ;
   unsigned long __cil_tmp13 ;
   unsigned long __cil_tmp14 ;
   unsigned long __cil_tmp15 ;
   char *__cil_tmp16 ;
   char const   *__cil_tmp17 ;
   __kernel_size_t __cil_tmp18 ;
   __kernel_size_t __cil_tmp19 ;
   unsigned long __cil_tmp20 ;
   unsigned long __cil_tmp21 ;
   char __cil_tmp22 ;
   int __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 ;
  char const   *__cil_tmp30 ;
  unsigned long __cil_tmp31 ;
  unsigned long __cil_tmp32 ;
  char *__cil_tmp33 ;
  char const   *__cil_tmp34 ;
  size_t __cil_tmp35 ;

  {
  {
#line 237
  __cil_tmp8 = 0 * 1UL;
#line 237
  __cil_tmp9 = (unsigned long )(buf) + __cil_tmp8;
#line 237
  __cil_tmp10 = (char *)__cil_tmp9;
#line 237
  __cil_tmp11 = (__kernel_size_t )256;
#line 237
  strncpy(__cil_tmp10, key, __cil_tmp11);
#line 238
  __cil_tmp12 = 255 * 1UL;
#line 238
  __cil_tmp13 = (unsigned long )(buf) + __cil_tmp12;
#line 238
  *((char *)__cil_tmp13) = (char )'\000';
#line 240
  __cil_tmp14 = 0 * 1UL;
#line 240
  __cil_tmp15 = (unsigned long )(buf) + __cil_tmp14;
#line 240
  __cil_tmp16 = (char *)__cil_tmp15;
#line 240
  __cil_tmp17 = (char const   *)__cil_tmp16;
#line 240
  __cil_tmp18 = (__kernel_size_t )256;
#line 240
  tmp = strnlen(__cil_tmp17, __cil_tmp18);
#line 240
  __cil_tmp19 = tmp - 1UL;
#line 240
  cr = (int )__cil_tmp19;
  }
  {
#line 241
  __cil_tmp20 = cr * 1UL;
#line 241
  __cil_tmp21 = (unsigned long )(buf) + __cil_tmp20;
#line 241
  __cil_tmp22 = *((char *)__cil_tmp21);
#line 241
  __cil_tmp23 = (int )__cil_tmp22;
#line 241
  if (__cil_tmp23 == 10) {
#line 242
    __cil_tmp24 = cr * 1UL;
#line 242
    __cil_tmp25 = (unsigned long )(buf) + __cil_tmp24;
#line 242
    *((char *)__cil_tmp25) = (char )'\000';
  } else {

  }
  }
  {
#line 244
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 244
    __cil_tmp26 = (unsigned long )map;
#line 244
    __cil_tmp27 = __cil_tmp26 + 8;
#line 244
    if (*((char const   **)__cil_tmp27)) {

    } else {
#line 244
      goto while_break;
    }
    }
    {
#line 245
    __cil_tmp28 = (unsigned long )map;
#line 245
    __cil_tmp29 = __cil_tmp28 + 8;
#line 245
    __cil_tmp30 = *((char const   **)__cil_tmp29);
#line 245
    __cil_tmp31 = 0 * 1UL;
#line 245
    __cil_tmp32 = (unsigned long )(buf) + __cil_tmp31;
#line 245
    __cil_tmp33 = (char *)__cil_tmp32;
#line 245
    __cil_tmp34 = (char const   *)__cil_tmp33;
#line 245
    __cil_tmp35 = (size_t )256;
#line 245
    tmp___0 = strncasecmp(__cil_tmp30, __cil_tmp34, __cil_tmp35);
    }
#line 245
    if (tmp___0 == 0) {
#line 246
      return (*((int *)map));
    } else {

    }
#line 247
    map = map + 1;
  }
  while_break: /* CIL Label */ ;
  }
#line 250
  return (def_val);
}
}
#line 254 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   *map_get_key(struct battery_property_map *map , int value , char const   *def_key ) 
{ unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  int __cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;

  {
  {
#line 257
  while (1) {
    while_continue: /* CIL Label */ ;
    {
#line 257
    __cil_tmp4 = (unsigned long )map;
#line 257
    __cil_tmp5 = __cil_tmp4 + 8;
#line 257
    if (*((char const   **)__cil_tmp5)) {

    } else {
#line 257
      goto while_break;
    }
    }
    {
#line 258
    __cil_tmp6 = *((int *)map);
#line 258
    if (__cil_tmp6 == value) {
      {
#line 259
      __cil_tmp7 = (unsigned long )map;
#line 259
      __cil_tmp8 = __cil_tmp7 + 8;
#line 259
      return (*((char const   **)__cil_tmp8));
      }
    } else {

    }
    }
#line 260
    map = map + 1;
  }
  while_break: /* CIL Label */ ;
  }
#line 263
  return (def_key);
}
}
#line 266 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_set_ac_online(char const   *key , struct kernel_param  const  *kp ) 
{ int *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  struct battery_property_map *__cil_tmp6 ;
  int *__cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  struct power_supply *__cil_tmp11 ;

  {
  {
#line 268
  __cil_tmp3 = & ac_online;
#line 268
  __cil_tmp4 = 0 * 16UL;
#line 268
  __cil_tmp5 = (unsigned long )(map_ac_online) + __cil_tmp4;
#line 268
  __cil_tmp6 = (struct battery_property_map *)__cil_tmp5;
#line 268
  __cil_tmp7 = & ac_online;
#line 268
  __cil_tmp8 = *__cil_tmp7;
#line 268
  *__cil_tmp3 = map_get_value(__cil_tmp6, key, __cil_tmp8);
#line 269
  __cil_tmp9 = 0 * 216UL;
#line 269
  __cil_tmp10 = (unsigned long )(test_power_supplies) + __cil_tmp9;
#line 269
  __cil_tmp11 = (struct power_supply *)__cil_tmp10;
#line 269
  power_supply_changed(__cil_tmp11);
  }
#line 270
  return (0);
}
}
#line 273 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_get_ac_online(char *buffer , struct kernel_param  const  *kp ) 
{ char const   *tmp ;
  unsigned long tmp___0 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct battery_property_map *__cil_tmp7 ;
  int *__cil_tmp8 ;
  int __cil_tmp9 ;
  char const   *__cil_tmp10 ;

  {
  {
#line 275
  __cil_tmp5 = 0 * 16UL;
#line 275
  __cil_tmp6 = (unsigned long )(map_ac_online) + __cil_tmp5;
#line 275
  __cil_tmp7 = (struct battery_property_map *)__cil_tmp6;
#line 275
  __cil_tmp8 = & ac_online;
#line 275
  __cil_tmp9 = *__cil_tmp8;
#line 275
  tmp = map_get_key(__cil_tmp7, __cil_tmp9, "unknown");
#line 275
  strcpy(buffer, tmp);
#line 276
  __cil_tmp10 = (char const   *)buffer;
#line 276
  tmp___0 = strlen(__cil_tmp10);
  }
#line 276
  return ((int )tmp___0);
}
}
#line 279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_set_battery_status(char const   *key , struct kernel_param  const  *kp ) 
{ int *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  struct battery_property_map *__cil_tmp6 ;
  int *__cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  struct power_supply *__cil_tmp11 ;

  {
  {
#line 282
  __cil_tmp3 = & battery_status;
#line 282
  __cil_tmp4 = 0 * 16UL;
#line 282
  __cil_tmp5 = (unsigned long )(map_status) + __cil_tmp4;
#line 282
  __cil_tmp6 = (struct battery_property_map *)__cil_tmp5;
#line 282
  __cil_tmp7 = & battery_status;
#line 282
  __cil_tmp8 = *__cil_tmp7;
#line 282
  *__cil_tmp3 = map_get_value(__cil_tmp6, key, __cil_tmp8);
#line 283
  __cil_tmp9 = 1 * 216UL;
#line 283
  __cil_tmp10 = (unsigned long )(test_power_supplies) + __cil_tmp9;
#line 283
  __cil_tmp11 = (struct power_supply *)__cil_tmp10;
#line 283
  power_supply_changed(__cil_tmp11);
  }
#line 284
  return (0);
}
}
#line 287 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_get_battery_status(char *buffer , struct kernel_param  const  *kp ) 
{ char const   *tmp ;
  unsigned long tmp___0 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct battery_property_map *__cil_tmp7 ;
  int *__cil_tmp8 ;
  int __cil_tmp9 ;
  char const   *__cil_tmp10 ;

  {
  {
#line 289
  __cil_tmp5 = 0 * 16UL;
#line 289
  __cil_tmp6 = (unsigned long )(map_status) + __cil_tmp5;
#line 289
  __cil_tmp7 = (struct battery_property_map *)__cil_tmp6;
#line 289
  __cil_tmp8 = & battery_status;
#line 289
  __cil_tmp9 = *__cil_tmp8;
#line 289
  tmp = map_get_key(__cil_tmp7, __cil_tmp9, "unknown");
#line 289
  strcpy(buffer, tmp);
#line 290
  __cil_tmp10 = (char const   *)buffer;
#line 290
  tmp___0 = strlen(__cil_tmp10);
  }
#line 290
  return ((int )tmp___0);
}
}
#line 293 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_set_battery_health(char const   *key , struct kernel_param  const  *kp ) 
{ int *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  struct battery_property_map *__cil_tmp6 ;
  int *__cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  struct power_supply *__cil_tmp11 ;

  {
  {
#line 296
  __cil_tmp3 = & battery_health;
#line 296
  __cil_tmp4 = 0 * 16UL;
#line 296
  __cil_tmp5 = (unsigned long )(map_health) + __cil_tmp4;
#line 296
  __cil_tmp6 = (struct battery_property_map *)__cil_tmp5;
#line 296
  __cil_tmp7 = & battery_health;
#line 296
  __cil_tmp8 = *__cil_tmp7;
#line 296
  *__cil_tmp3 = map_get_value(__cil_tmp6, key, __cil_tmp8);
#line 297
  __cil_tmp9 = 1 * 216UL;
#line 297
  __cil_tmp10 = (unsigned long )(test_power_supplies) + __cil_tmp9;
#line 297
  __cil_tmp11 = (struct power_supply *)__cil_tmp10;
#line 297
  power_supply_changed(__cil_tmp11);
  }
#line 298
  return (0);
}
}
#line 301 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_get_battery_health(char *buffer , struct kernel_param  const  *kp ) 
{ char const   *tmp ;
  unsigned long tmp___0 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct battery_property_map *__cil_tmp7 ;
  int *__cil_tmp8 ;
  int __cil_tmp9 ;
  char const   *__cil_tmp10 ;

  {
  {
#line 303
  __cil_tmp5 = 0 * 16UL;
#line 303
  __cil_tmp6 = (unsigned long )(map_health) + __cil_tmp5;
#line 303
  __cil_tmp7 = (struct battery_property_map *)__cil_tmp6;
#line 303
  __cil_tmp8 = & battery_health;
#line 303
  __cil_tmp9 = *__cil_tmp8;
#line 303
  tmp = map_get_key(__cil_tmp7, __cil_tmp9, "unknown");
#line 303
  strcpy(buffer, tmp);
#line 304
  __cil_tmp10 = (char const   *)buffer;
#line 304
  tmp___0 = strlen(__cil_tmp10);
  }
#line 304
  return ((int )tmp___0);
}
}
#line 307 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_set_battery_present(char const   *key , struct kernel_param  const  *kp ) 
{ int *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  struct battery_property_map *__cil_tmp6 ;
  int *__cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  struct power_supply *__cil_tmp11 ;

  {
  {
#line 310
  __cil_tmp3 = & battery_present;
#line 310
  __cil_tmp4 = 0 * 16UL;
#line 310
  __cil_tmp5 = (unsigned long )(map_present) + __cil_tmp4;
#line 310
  __cil_tmp6 = (struct battery_property_map *)__cil_tmp5;
#line 310
  __cil_tmp7 = & battery_present;
#line 310
  __cil_tmp8 = *__cil_tmp7;
#line 310
  *__cil_tmp3 = map_get_value(__cil_tmp6, key, __cil_tmp8);
#line 311
  __cil_tmp9 = 0 * 216UL;
#line 311
  __cil_tmp10 = (unsigned long )(test_power_supplies) + __cil_tmp9;
#line 311
  __cil_tmp11 = (struct power_supply *)__cil_tmp10;
#line 311
  power_supply_changed(__cil_tmp11);
  }
#line 312
  return (0);
}
}
#line 315 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_get_battery_present(char *buffer , struct kernel_param  const  *kp ) 
{ char const   *tmp ;
  unsigned long tmp___0 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct battery_property_map *__cil_tmp7 ;
  int *__cil_tmp8 ;
  int __cil_tmp9 ;
  char const   *__cil_tmp10 ;

  {
  {
#line 318
  __cil_tmp5 = 0 * 16UL;
#line 318
  __cil_tmp6 = (unsigned long )(map_present) + __cil_tmp5;
#line 318
  __cil_tmp7 = (struct battery_property_map *)__cil_tmp6;
#line 318
  __cil_tmp8 = & battery_present;
#line 318
  __cil_tmp9 = *__cil_tmp8;
#line 318
  tmp = map_get_key(__cil_tmp7, __cil_tmp9, "unknown");
#line 318
  strcpy(buffer, tmp);
#line 319
  __cil_tmp10 = (char const   *)buffer;
#line 319
  tmp___0 = strlen(__cil_tmp10);
  }
#line 319
  return ((int )tmp___0);
}
}
#line 322 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_set_battery_technology(char const   *key , struct kernel_param  const  *kp ) 
{ int *__cil_tmp3 ;
  unsigned long __cil_tmp4 ;
  unsigned long __cil_tmp5 ;
  struct battery_property_map *__cil_tmp6 ;
  int *__cil_tmp7 ;
  int __cil_tmp8 ;
  unsigned long __cil_tmp9 ;
  unsigned long __cil_tmp10 ;
  struct power_supply *__cil_tmp11 ;

  {
  {
#line 325
  __cil_tmp3 = & battery_technology;
#line 325
  __cil_tmp4 = 0 * 16UL;
#line 325
  __cil_tmp5 = (unsigned long )(map_technology) + __cil_tmp4;
#line 325
  __cil_tmp6 = (struct battery_property_map *)__cil_tmp5;
#line 325
  __cil_tmp7 = & battery_technology;
#line 325
  __cil_tmp8 = *__cil_tmp7;
#line 325
  *__cil_tmp3 = map_get_value(__cil_tmp6, key, __cil_tmp8);
#line 327
  __cil_tmp9 = 1 * 216UL;
#line 327
  __cil_tmp10 = (unsigned long )(test_power_supplies) + __cil_tmp9;
#line 327
  __cil_tmp11 = (struct power_supply *)__cil_tmp10;
#line 327
  power_supply_changed(__cil_tmp11);
  }
#line 328
  return (0);
}
}
#line 331 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_get_battery_technology(char *buffer , struct kernel_param  const  *kp ) 
{ char const   *tmp ;
  unsigned long tmp___0 ;
  unsigned long __cil_tmp5 ;
  unsigned long __cil_tmp6 ;
  struct battery_property_map *__cil_tmp7 ;
  int *__cil_tmp8 ;
  int __cil_tmp9 ;
  char const   *__cil_tmp10 ;

  {
  {
#line 334
  __cil_tmp5 = 0 * 16UL;
#line 334
  __cil_tmp6 = (unsigned long )(map_technology) + __cil_tmp5;
#line 334
  __cil_tmp7 = (struct battery_property_map *)__cil_tmp6;
#line 334
  __cil_tmp8 = & battery_technology;
#line 334
  __cil_tmp9 = *__cil_tmp8;
#line 334
  tmp = map_get_key(__cil_tmp7, __cil_tmp9, "unknown");
#line 334
  strcpy(buffer, tmp);
#line 336
  __cil_tmp10 = (char const   *)buffer;
#line 336
  tmp___0 = strlen(__cil_tmp10);
  }
#line 336
  return ((int )tmp___0);
}
}
#line 339 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static int param_set_battery_capacity(char const   *key , struct kernel_param  const  *kp ) 
{ int tmp ;
  int tmp___0 ;
  int *__cil_tmp5 ;
  int *__cil_tmp6 ;
  unsigned long __cil_tmp7 ;
  unsigned long __cil_tmp8 ;
  struct power_supply *__cil_tmp9 ;

  {
  {
#line 344
  tmp___0 = sscanf(key, "%d", & tmp);
  }
#line 344
  if (1 != tmp___0) {
#line 345
    return (-22);
  } else {

  }
  {
#line 347
  __cil_tmp5 = & battery_capacity;
#line 347
  __cil_tmp6 = & tmp;
#line 347
  *__cil_tmp5 = *__cil_tmp6;
#line 348
  __cil_tmp7 = 1 * 216UL;
#line 348
  __cil_tmp8 = (unsigned long )(test_power_supplies) + __cil_tmp7;
#line 348
  __cil_tmp9 = (struct power_supply *)__cil_tmp8;
#line 348
  power_supply_changed(__cil_tmp9);
  }
#line 349
  return (0);
}
}
#line 356 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param_ops param_ops_ac_online  =    {& param_set_ac_online, & param_get_ac_online, (void (*)(void *arg ))0};
#line 361 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param_ops param_ops_battery_status  =    {& param_set_battery_status, & param_get_battery_status, (void (*)(void *arg ))0};
#line 366 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param_ops param_ops_battery_present  =    {& param_set_battery_present, & param_get_battery_present, (void (*)(void *arg ))0};
#line 371 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param_ops param_ops_battery_technology  =    {& param_set_battery_technology, & param_get_battery_technology, (void (*)(void *arg ))0};
#line 376 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param_ops param_ops_battery_health  =    {& param_set_battery_health, & param_get_battery_health, (void (*)(void *arg ))0};
#line 381 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param_ops param_ops_battery_capacity  =    {& param_set_battery_capacity, & param_get_int, (void (*)(void *arg ))0};
#line 395 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __param_str_ac_online[10]  = 
#line 395
  {      (char const   )'a',      (char const   )'c',      (char const   )'_',      (char const   )'o', 
        (char const   )'n',      (char const   )'l',      (char const   )'i',      (char const   )'n', 
        (char const   )'e',      (char const   )'\000'};
#line 395 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param  const  __param_ac_online  __attribute__((__used__, __unused__,
__section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_ac_online, (struct kernel_param_ops  const  *)(& param_ops_ac_online),
    (u16 )420, (s16 )0, {(void *)(& ac_online)}};
#line 395 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_ac_onlinetype395[29]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 395
  {      (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   )'a',      (char const   )'c',      (char const   )'_', 
        (char const   )'o',      (char const   )'n',      (char const   )'l',      (char const   )'i', 
        (char const   )'n',      (char const   )'e',      (char const   )':',      (char const   )'a', 
        (char const   )'c',      (char const   )'_',      (char const   )'o',      (char const   )'n', 
        (char const   )'l',      (char const   )'i',      (char const   )'n',      (char const   )'e', 
        (char const   )'\000'};
#line 396 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_ac_online396[42]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 396
  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
        (char const   )'=',      (char const   )'a',      (char const   )'c',      (char const   )'_', 
        (char const   )'o',      (char const   )'n',      (char const   )'l',      (char const   )'i', 
        (char const   )'n',      (char const   )'e',      (char const   )':',      (char const   )'A', 
        (char const   )'C',      (char const   )' ',      (char const   )'c',      (char const   )'h', 
        (char const   )'a',      (char const   )'r',      (char const   )'g',      (char const   )'i', 
        (char const   )'n',      (char const   )'g',      (char const   )' ',      (char const   )'s', 
        (char const   )'t',      (char const   )'a',      (char const   )'t',      (char const   )'e', 
        (char const   )' ',      (char const   )'<',      (char const   )'o',      (char const   )'n', 
        (char const   )'|',      (char const   )'o',      (char const   )'f',      (char const   )'f', 
        (char const   )'>',      (char const   )'\000'};
#line 398 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __param_str_battery_status[15]  = 
#line 398
  {      (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )'_', 
        (char const   )'s',      (char const   )'t',      (char const   )'a',      (char const   )'t', 
        (char const   )'u',      (char const   )'s',      (char const   )'\000'};
#line 398 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param  const  __param_battery_status  __attribute__((__used__,
__unused__, __section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_battery_status, (struct kernel_param_ops  const  *)(& param_ops_battery_status),
    (u16 )420, (s16 )0, {(void *)(& battery_status)}};
#line 398 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_statustype398[39]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 398
  {      (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   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'s',      (char const   )'t',      (char const   )'a', 
        (char const   )'t',      (char const   )'u',      (char const   )'s',      (char const   )':', 
        (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )'_', 
        (char const   )'s',      (char const   )'t',      (char const   )'a',      (char const   )'t', 
        (char const   )'u',      (char const   )'s',      (char const   )'\000'};
#line 399 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_status400[76]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 399
  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
        (char const   )'=',      (char const   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'s',      (char const   )'t',      (char const   )'a', 
        (char const   )'t',      (char const   )'u',      (char const   )'s',      (char const   )':', 
        (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )' ', 
        (char const   )'s',      (char const   )'t',      (char const   )'a',      (char const   )'t', 
        (char const   )'u',      (char const   )'s',      (char const   )' ',      (char const   )'<', 
        (char const   )'c',      (char const   )'h',      (char const   )'a',      (char const   )'r', 
        (char const   )'g',      (char const   )'i',      (char const   )'n',      (char const   )'g', 
        (char const   )'|',      (char const   )'d',      (char const   )'i',      (char const   )'s', 
        (char const   )'c',      (char const   )'h',      (char const   )'a',      (char const   )'r', 
        (char const   )'g',      (char const   )'i',      (char const   )'n',      (char const   )'g', 
        (char const   )'|',      (char const   )'n',      (char const   )'o',      (char const   )'t', 
        (char const   )'-',      (char const   )'c',      (char const   )'h',      (char const   )'a', 
        (char const   )'r',      (char const   )'g',      (char const   )'i',      (char const   )'n', 
        (char const   )'g',      (char const   )'|',      (char const   )'f',      (char const   )'u', 
        (char const   )'l',      (char const   )'l',      (char const   )'>',      (char const   )'\000'};
#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __param_str_battery_present[16]  = 
#line 402
  {      (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )'_', 
        (char const   )'p',      (char const   )'r',      (char const   )'e',      (char const   )'s', 
        (char const   )'e',      (char const   )'n',      (char const   )'t',      (char const   )'\000'};
#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param  const  __param_battery_present  __attribute__((__used__,
__unused__, __section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_battery_present, (struct kernel_param_ops  const  *)(& param_ops_battery_present),
    (u16 )420, (s16 )0, {(void *)(& battery_present)}};
#line 402 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_presenttype402[41]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 402
  {      (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   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'p',      (char const   )'r',      (char const   )'e', 
        (char const   )'s',      (char const   )'e',      (char const   )'n',      (char const   )'t', 
        (char const   )':',      (char const   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'p',      (char const   )'r',      (char const   )'e', 
        (char const   )'s',      (char const   )'e',      (char const   )'n',      (char const   )'t', 
        (char const   )'\000'};
#line 403 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_present404[85]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 403
  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
        (char const   )'=',      (char const   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'p',      (char const   )'r',      (char const   )'e', 
        (char const   )'s',      (char const   )'e',      (char const   )'n',      (char const   )'t', 
        (char const   )':',      (char const   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )' ',      (char const   )'p',      (char const   )'r',      (char const   )'e', 
        (char const   )'s',      (char const   )'e',      (char const   )'n',      (char const   )'c', 
        (char const   )'e',      (char const   )' ',      (char const   )'s',      (char const   )'t', 
        (char const   )'a',      (char const   )'t',      (char const   )'e',      (char const   )' ', 
        (char const   )'<',      (char const   )'g',      (char const   )'o',      (char const   )'o', 
        (char const   )'d',      (char const   )'|',      (char const   )'o',      (char const   )'v', 
        (char const   )'e',      (char const   )'r',      (char const   )'h',      (char const   )'e', 
        (char const   )'a',      (char const   )'t',      (char const   )'|',      (char const   )'d', 
        (char const   )'e',      (char const   )'a',      (char const   )'d',      (char const   )'|', 
        (char const   )'o',      (char const   )'v',      (char const   )'e',      (char const   )'r', 
        (char const   )'v',      (char const   )'o',      (char const   )'l',      (char const   )'t', 
        (char const   )'a',      (char const   )'g',      (char const   )'e',      (char const   )'|', 
        (char const   )'f',      (char const   )'a',      (char const   )'i',      (char const   )'l', 
        (char const   )'u',      (char const   )'r',      (char const   )'e',      (char const   )'>', 
        (char const   )'\000'};
#line 406 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __param_str_battery_technology[19]  = 
#line 406
  {      (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )'_', 
        (char const   )'t',      (char const   )'e',      (char const   )'c',      (char const   )'h', 
        (char const   )'n',      (char const   )'o',      (char const   )'l',      (char const   )'o', 
        (char const   )'g',      (char const   )'y',      (char const   )'\000'};
#line 406 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param  const  __param_battery_technology  __attribute__((__used__,
__unused__, __section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_battery_technology, (struct kernel_param_ops  const  *)(& param_ops_battery_technology),
    (u16 )420, (s16 )0, {(void *)(& battery_technology)}};
#line 406 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_technologytype406[47]  __attribute__((__used__,
__unused__, __section__(".modinfo"), __aligned__(1)))  = 
#line 406
  {      (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   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'t',      (char const   )'e',      (char const   )'c', 
        (char const   )'h',      (char const   )'n',      (char const   )'o',      (char const   )'l', 
        (char const   )'o',      (char const   )'g',      (char const   )'y',      (char const   )':', 
        (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )'_', 
        (char const   )'t',      (char const   )'e',      (char const   )'c',      (char const   )'h', 
        (char const   )'n',      (char const   )'o',      (char const   )'l',      (char const   )'o', 
        (char const   )'g',      (char const   )'y',      (char const   )'\000'};
#line 407 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_technology408[75]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 407
  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
        (char const   )'=',      (char const   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'t',      (char const   )'e',      (char const   )'c', 
        (char const   )'h',      (char const   )'n',      (char const   )'o',      (char const   )'l', 
        (char const   )'o',      (char const   )'g',      (char const   )'y',      (char const   )':', 
        (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )' ', 
        (char const   )'t',      (char const   )'e',      (char const   )'c',      (char const   )'h', 
        (char const   )'n',      (char const   )'o',      (char const   )'l',      (char const   )'o', 
        (char const   )'g',      (char const   )'y',      (char const   )' ',      (char const   )'<', 
        (char const   )'N',      (char const   )'i',      (char const   )'M',      (char const   )'H', 
        (char const   )'|',      (char const   )'L',      (char const   )'I',      (char const   )'O', 
        (char const   )'N',      (char const   )'|',      (char const   )'L',      (char const   )'I', 
        (char const   )'P',      (char const   )'O',      (char const   )'|',      (char const   )'L', 
        (char const   )'i',      (char const   )'F',      (char const   )'e',      (char const   )'|', 
        (char const   )'N',      (char const   )'i',      (char const   )'C',      (char const   )'d', 
        (char const   )'|',      (char const   )'L',      (char const   )'i',      (char const   )'M', 
        (char const   )'n',      (char const   )'>',      (char const   )'\000'};
#line 410 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __param_str_battery_health[15]  = 
#line 410
  {      (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )'_', 
        (char const   )'h',      (char const   )'e',      (char const   )'a',      (char const   )'l', 
        (char const   )'t',      (char const   )'h',      (char const   )'\000'};
#line 410 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param  const  __param_battery_health  __attribute__((__used__,
__unused__, __section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_battery_health, (struct kernel_param_ops  const  *)(& param_ops_battery_health),
    (u16 )420, (s16 )0, {(void *)(& battery_health)}};
#line 410 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_healthtype410[39]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 410
  {      (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   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'h',      (char const   )'e',      (char const   )'a', 
        (char const   )'l',      (char const   )'t',      (char const   )'h',      (char const   )':', 
        (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )'_', 
        (char const   )'h',      (char const   )'e',      (char const   )'a',      (char const   )'l', 
        (char const   )'t',      (char const   )'h',      (char const   )'\000'};
#line 411 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_health412[82]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 411
  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
        (char const   )'=',      (char const   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'h',      (char const   )'e',      (char const   )'a', 
        (char const   )'l',      (char const   )'t',      (char const   )'h',      (char const   )':', 
        (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )' ', 
        (char const   )'h',      (char const   )'e',      (char const   )'a',      (char const   )'l', 
        (char const   )'t',      (char const   )'h',      (char const   )' ',      (char const   )'s', 
        (char const   )'t',      (char const   )'a',      (char const   )'t',      (char const   )'e', 
        (char const   )' ',      (char const   )'<',      (char const   )'g',      (char const   )'o', 
        (char const   )'o',      (char const   )'d',      (char const   )'|',      (char const   )'o', 
        (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )'h', 
        (char const   )'e',      (char const   )'a',      (char const   )'t',      (char const   )'|', 
        (char const   )'d',      (char const   )'e',      (char const   )'a',      (char const   )'d', 
        (char const   )'|',      (char const   )'o',      (char const   )'v',      (char const   )'e', 
        (char const   )'r',      (char const   )'v',      (char const   )'o',      (char const   )'l', 
        (char const   )'t',      (char const   )'a',      (char const   )'g',      (char const   )'e', 
        (char const   )'|',      (char const   )'f',      (char const   )'a',      (char const   )'i', 
        (char const   )'l',      (char const   )'u',      (char const   )'r',      (char const   )'e', 
        (char const   )'>',      (char const   )'\000'};
#line 414 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __param_str_battery_capacity[17]  = 
#line 414
  {      (char const   )'b',      (char const   )'a',      (char const   )'t',      (char const   )'t', 
        (char const   )'e',      (char const   )'r',      (char const   )'y',      (char const   )'_', 
        (char const   )'c',      (char const   )'a',      (char const   )'p',      (char const   )'a', 
        (char const   )'c',      (char const   )'i',      (char const   )'t',      (char const   )'y', 
        (char const   )'\000'};
#line 414 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static struct kernel_param  const  __param_battery_capacity  __attribute__((__used__,
__unused__, __section__("__param"), __aligned__(sizeof(void *))))  =    {__param_str_battery_capacity, (struct kernel_param_ops  const  *)(& param_ops_battery_capacity),
    (u16 )420, (s16 )0, {(void *)(& battery_capacity)}};
#line 414 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_capacitytype414[43]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 414
  {      (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   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'c',      (char const   )'a',      (char const   )'p', 
        (char const   )'a',      (char const   )'c',      (char const   )'i',      (char const   )'t', 
        (char const   )'y',      (char const   )':',      (char const   )'b',      (char const   )'a', 
        (char const   )'t',      (char const   )'t',      (char const   )'e',      (char const   )'r', 
        (char const   )'y',      (char const   )'_',      (char const   )'c',      (char const   )'a', 
        (char const   )'p',      (char const   )'a',      (char const   )'c',      (char const   )'i', 
        (char const   )'t',      (char const   )'y',      (char const   )'\000'};
#line 415 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_battery_capacity415[52]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 415
  {      (char const   )'p',      (char const   )'a',      (char const   )'r',      (char const   )'m', 
        (char const   )'=',      (char const   )'b',      (char const   )'a',      (char const   )'t', 
        (char const   )'t',      (char const   )'e',      (char const   )'r',      (char const   )'y', 
        (char const   )'_',      (char const   )'c',      (char const   )'a',      (char const   )'p', 
        (char const   )'a',      (char const   )'c',      (char const   )'i',      (char const   )'t', 
        (char const   )'y',      (char const   )':',      (char const   )'b',      (char const   )'a', 
        (char const   )'t',      (char const   )'t',      (char const   )'e',      (char const   )'r', 
        (char const   )'y',      (char const   )' ',      (char const   )'c',      (char const   )'a', 
        (char const   )'p',      (char const   )'a',      (char const   )'c',      (char const   )'i', 
        (char const   )'t',      (char const   )'y',      (char const   )' ',      (char const   )'(', 
        (char const   )'p',      (char const   )'e',      (char const   )'r',      (char const   )'c', 
        (char const   )'e',      (char const   )'n',      (char const   )'t',      (char const   )'a', 
        (char const   )'g',      (char const   )'e',      (char const   )')',      (char const   )'\000'};
#line 418 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_description418[44]  __attribute__((__used__, __unused__,
__section__(".modinfo"), __aligned__(1)))  = 
#line 418
  {      (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   )'P',      (char const   )'o',      (char const   )'w',      (char const   )'e', 
        (char const   )'r',      (char const   )' ',      (char const   )'s',      (char const   )'u', 
        (char const   )'p',      (char const   )'p',      (char const   )'l',      (char const   )'y', 
        (char const   )' ',      (char const   )'d',      (char const   )'r',      (char const   )'i', 
        (char const   )'v',      (char const   )'e',      (char const   )'r',      (char const   )' ', 
        (char const   )'f',      (char const   )'o',      (char const   )'r',      (char const   )' ', 
        (char const   )'t',      (char const   )'e',      (char const   )'s',      (char const   )'t', 
        (char const   )'i',      (char const   )'n',      (char const   )'g',      (char const   )'\000'};
#line 419 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_author419[48]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 419
  {      (char const   )'a',      (char const   )'u',      (char const   )'t',      (char const   )'h', 
        (char const   )'o',      (char const   )'r',      (char const   )'=',      (char const   )'A', 
        (char const   )'n',      (char const   )'t',      (char const   )'o',      (char const   )'n', 
        (char const   )' ',      (char const   )'V',      (char const   )'o',      (char const   )'r', 
        (char const   )'o',      (char const   )'n',      (char const   )'t',      (char const   )'s', 
        (char const   )'o',      (char const   )'v',      (char const   )' ',      (char const   )'<', 
        (char const   )'c',      (char const   )'b',      (char const   )'o',      (char const   )'u', 
        (char const   )'a',      (char const   )'t',      (char const   )'m',      (char const   )'a', 
        (char const   )'i',      (char const   )'l',      (char const   )'r',      (char const   )'u', 
        (char const   )'@',      (char const   )'g',      (char const   )'m',      (char const   )'a', 
        (char const   )'i',      (char const   )'l',      (char const   )'.',      (char const   )'c', 
        (char const   )'o',      (char const   )'m',      (char const   )'>',      (char const   )'\000'};
#line 420 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
static char const   __mod_license420[12]  __attribute__((__used__, __unused__, __section__(".modinfo"),
__aligned__(1)))  = 
#line 420
  {      (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 438
void ldv_check_final_state(void) ;
#line 444
extern void ldv_initialize(void) ;
#line 447
extern int __VERIFIER_nondet_int(void) ;
#line 450 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
int LDV_IN_INTERRUPT  ;
#line 453 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
void main(void) 
{ char const   *var_param_set_ac_online_6_p0 ;
  struct kernel_param  const  *var_param_set_ac_online_6_p1 ;
  char *var_param_get_ac_online_7_p0 ;
  struct kernel_param  const  *var_param_get_ac_online_7_p1 ;
  char const   *var_param_set_battery_status_8_p0 ;
  struct kernel_param  const  *var_param_set_battery_status_8_p1 ;
  char *var_param_get_battery_status_9_p0 ;
  struct kernel_param  const  *var_param_get_battery_status_9_p1 ;
  char const   *var_param_set_battery_present_12_p0 ;
  struct kernel_param  const  *var_param_set_battery_present_12_p1 ;
  char *var_param_get_battery_present_13_p0 ;
  struct kernel_param  const  *var_param_get_battery_present_13_p1 ;
  char const   *var_param_set_battery_technology_14_p0 ;
  struct kernel_param  const  *var_param_set_battery_technology_14_p1 ;
  char *var_param_get_battery_technology_15_p0 ;
  struct kernel_param  const  *var_param_get_battery_technology_15_p1 ;
  char const   *var_param_set_battery_health_10_p0 ;
  struct kernel_param  const  *var_param_set_battery_health_10_p1 ;
  char *var_param_get_battery_health_11_p0 ;
  struct kernel_param  const  *var_param_get_battery_health_11_p1 ;
  char const   *var_param_set_battery_capacity_16_p0 ;
  struct kernel_param  const  *var_param_set_battery_capacity_16_p1 ;
  int tmp ;
  int tmp___0 ;
  int tmp___1 ;

  {
  {
#line 664
  LDV_IN_INTERRUPT = 1;
#line 673
  ldv_initialize();
#line 679
  tmp = test_power_init();
  }
#line 679
  if (tmp) {
#line 680
    goto ldv_final;
  } else {

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

    } else {
#line 704
      goto while_break;
    }
    {
#line 707
    tmp___0 = __VERIFIER_nondet_int();
    }
#line 709
    if (tmp___0 == 0) {
#line 709
      goto case_0;
    } else
#line 736
    if (tmp___0 == 1) {
#line 736
      goto case_1;
    } else
#line 763
    if (tmp___0 == 2) {
#line 763
      goto case_2;
    } else
#line 790
    if (tmp___0 == 3) {
#line 790
      goto case_3;
    } else
#line 817
    if (tmp___0 == 4) {
#line 817
      goto case_4;
    } else
#line 844
    if (tmp___0 == 5) {
#line 844
      goto case_5;
    } else
#line 871
    if (tmp___0 == 6) {
#line 871
      goto case_6;
    } else
#line 898
    if (tmp___0 == 7) {
#line 898
      goto case_7;
    } else
#line 925
    if (tmp___0 == 8) {
#line 925
      goto case_8;
    } else
#line 952
    if (tmp___0 == 9) {
#line 952
      goto case_9;
    } else
#line 979
    if (tmp___0 == 10) {
#line 979
      goto case_10;
    } else {
      {
#line 1006
      goto switch_default;
#line 707
      if (0) {
        case_0: /* CIL Label */ 
        {
#line 719
        param_set_ac_online(var_param_set_ac_online_6_p0, var_param_set_ac_online_6_p1);
        }
#line 735
        goto switch_break;
        case_1: /* CIL Label */ 
        {
#line 746
        param_get_ac_online(var_param_get_ac_online_7_p0, var_param_get_ac_online_7_p1);
        }
#line 762
        goto switch_break;
        case_2: /* CIL Label */ 
        {
#line 773
        param_set_battery_status(var_param_set_battery_status_8_p0, var_param_set_battery_status_8_p1);
        }
#line 789
        goto switch_break;
        case_3: /* CIL Label */ 
        {
#line 800
        param_get_battery_status(var_param_get_battery_status_9_p0, var_param_get_battery_status_9_p1);
        }
#line 816
        goto switch_break;
        case_4: /* CIL Label */ 
        {
#line 827
        param_set_battery_present(var_param_set_battery_present_12_p0, var_param_set_battery_present_12_p1);
        }
#line 843
        goto switch_break;
        case_5: /* CIL Label */ 
        {
#line 854
        param_get_battery_present(var_param_get_battery_present_13_p0, var_param_get_battery_present_13_p1);
        }
#line 870
        goto switch_break;
        case_6: /* CIL Label */ 
        {
#line 881
        param_set_battery_technology(var_param_set_battery_technology_14_p0, var_param_set_battery_technology_14_p1);
        }
#line 897
        goto switch_break;
        case_7: /* CIL Label */ 
        {
#line 908
        param_get_battery_technology(var_param_get_battery_technology_15_p0, var_param_get_battery_technology_15_p1);
        }
#line 924
        goto switch_break;
        case_8: /* CIL Label */ 
        {
#line 935
        param_set_battery_health(var_param_set_battery_health_10_p0, var_param_set_battery_health_10_p1);
        }
#line 951
        goto switch_break;
        case_9: /* CIL Label */ 
        {
#line 962
        param_get_battery_health(var_param_get_battery_health_11_p0, var_param_get_battery_health_11_p1);
        }
#line 978
        goto switch_break;
        case_10: /* CIL Label */ 
        {
#line 989
        param_set_battery_capacity(var_param_set_battery_capacity_16_p0, var_param_set_battery_capacity_16_p1);
        }
#line 1005
        goto switch_break;
        switch_default: /* CIL Label */ 
#line 1006
        goto switch_break;
      } else {
        switch_break: /* CIL Label */ ;
      }
      }
    }
  }
  while_break: /* CIL Label */ ;
  }
  {
#line 1018
  test_power_exit();
  }
  ldv_final: 
  {
#line 1031
  ldv_check_final_state();
  }
#line 1034
  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/1058/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/1058/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/1058/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/1058/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/1058/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/1058/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/1058/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/1058/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/1058/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/1058/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 1043 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1058/dscv_tempdir/dscv/ri/32_1/drivers/power/test_power.c.common.c"
long s__builtin_expect(long val , long res ) 
{ 

  {
#line 1044
  return (val);
}
}