1
2
3
4#line 43 "include/asm-generic/int-ll64.h"
5typedef unsigned char u8;
6#line 45 "include/asm-generic/int-ll64.h"
7typedef short s16;
8#line 46 "include/asm-generic/int-ll64.h"
9typedef unsigned short u16;
10#line 48 "include/asm-generic/int-ll64.h"
11typedef int s32;
12#line 49 "include/asm-generic/int-ll64.h"
13typedef unsigned int u32;
14#line 51 "include/asm-generic/int-ll64.h"
15typedef long long s64;
16#line 14 "include/asm-generic/posix_types.h"
17typedef long __kernel_long_t;
18#line 15 "include/asm-generic/posix_types.h"
19typedef unsigned long __kernel_ulong_t;
20#line 75 "include/asm-generic/posix_types.h"
21typedef __kernel_ulong_t __kernel_size_t;
22#line 76 "include/asm-generic/posix_types.h"
23typedef __kernel_long_t __kernel_ssize_t;
24#line 27 "include/linux/types.h"
25typedef unsigned short umode_t;
26#line 63 "include/linux/types.h"
27typedef __kernel_size_t size_t;
28#line 68 "include/linux/types.h"
29typedef __kernel_ssize_t ssize_t;
30#line 202 "include/linux/types.h"
31typedef unsigned int gfp_t;
32#line 221 "include/linux/types.h"
33struct __anonstruct_atomic_t_6 {
34 int counter ;
35};
36#line 221 "include/linux/types.h"
37typedef struct __anonstruct_atomic_t_6 atomic_t;
38#line 226 "include/linux/types.h"
39struct __anonstruct_atomic64_t_7 {
40 long counter ;
41};
42#line 226 "include/linux/types.h"
43typedef struct __anonstruct_atomic64_t_7 atomic64_t;
44#line 227 "include/linux/types.h"
45struct list_head {
46 struct list_head *next ;
47 struct list_head *prev ;
48};
49#line 46 "include/linux/dynamic_debug.h"
50struct device;
51#line 46
52struct device;
53#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
54struct page;
55#line 58
56struct page;
57#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
58struct arch_spinlock;
59#line 327
60struct arch_spinlock;
61#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
62struct kmem_cache;
63#line 23 "include/asm-generic/atomic-long.h"
64typedef atomic64_t atomic_long_t;
65#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
66typedef u16 __ticket_t;
67#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
68typedef u32 __ticketpair_t;
69#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
70struct __raw_tickets {
71 __ticket_t head ;
72 __ticket_t tail ;
73};
74#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
75union __anonunion_ldv_5907_29 {
76 __ticketpair_t head_tail ;
77 struct __raw_tickets tickets ;
78};
79#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
80struct arch_spinlock {
81 union __anonunion_ldv_5907_29 ldv_5907 ;
82};
83#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
84typedef struct arch_spinlock arch_spinlock_t;
85#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
86struct __anonstruct_ldv_5914_31 {
87 u32 read ;
88 s32 write ;
89};
90#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
91union __anonunion_arch_rwlock_t_30 {
92 s64 lock ;
93 struct __anonstruct_ldv_5914_31 ldv_5914 ;
94};
95#line 33 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
96typedef union __anonunion_arch_rwlock_t_30 arch_rwlock_t;
97#line 34
98struct lockdep_map;
99#line 34
100struct lockdep_map;
101#line 55 "include/linux/debug_locks.h"
102struct stack_trace {
103 unsigned int nr_entries ;
104 unsigned int max_entries ;
105 unsigned long *entries ;
106 int skip ;
107};
108#line 26 "include/linux/stacktrace.h"
109struct lockdep_subclass_key {
110 char __one_byte ;
111};
112#line 53 "include/linux/lockdep.h"
113struct lock_class_key {
114 struct lockdep_subclass_key subkeys[8U] ;
115};
116#line 59 "include/linux/lockdep.h"
117struct lock_class {
118 struct list_head hash_entry ;
119 struct list_head lock_entry ;
120 struct lockdep_subclass_key *key ;
121 unsigned int subclass ;
122 unsigned int dep_gen_id ;
123 unsigned long usage_mask ;
124 struct stack_trace usage_traces[13U] ;
125 struct list_head locks_after ;
126 struct list_head locks_before ;
127 unsigned int version ;
128 unsigned long ops ;
129 char const *name ;
130 int name_version ;
131 unsigned long contention_point[4U] ;
132 unsigned long contending_point[4U] ;
133};
134#line 144 "include/linux/lockdep.h"
135struct lockdep_map {
136 struct lock_class_key *key ;
137 struct lock_class *class_cache[2U] ;
138 char const *name ;
139 int cpu ;
140 unsigned long ip ;
141};
142#line 556 "include/linux/lockdep.h"
143struct raw_spinlock {
144 arch_spinlock_t raw_lock ;
145 unsigned int magic ;
146 unsigned int owner_cpu ;
147 void *owner ;
148 struct lockdep_map dep_map ;
149};
150#line 32 "include/linux/spinlock_types.h"
151typedef struct raw_spinlock raw_spinlock_t;
152#line 33 "include/linux/spinlock_types.h"
153struct __anonstruct_ldv_6122_33 {
154 u8 __padding[24U] ;
155 struct lockdep_map dep_map ;
156};
157#line 33 "include/linux/spinlock_types.h"
158union __anonunion_ldv_6123_32 {
159 struct raw_spinlock rlock ;
160 struct __anonstruct_ldv_6122_33 ldv_6122 ;
161};
162#line 33 "include/linux/spinlock_types.h"
163struct spinlock {
164 union __anonunion_ldv_6123_32 ldv_6123 ;
165};
166#line 76 "include/linux/spinlock_types.h"
167typedef struct spinlock spinlock_t;
168#line 23 "include/linux/rwlock_types.h"
169struct __anonstruct_rwlock_t_34 {
170 arch_rwlock_t raw_lock ;
171 unsigned int magic ;
172 unsigned int owner_cpu ;
173 void *owner ;
174 struct lockdep_map dep_map ;
175};
176#line 23 "include/linux/rwlock_types.h"
177typedef struct __anonstruct_rwlock_t_34 rwlock_t;
178#line 171 "include/linux/mutex.h"
179struct rw_semaphore;
180#line 171
181struct rw_semaphore;
182#line 172 "include/linux/mutex.h"
183struct rw_semaphore {
184 long count ;
185 raw_spinlock_t wait_lock ;
186 struct list_head wait_list ;
187 struct lockdep_map dep_map ;
188};
189#line 341 "include/linux/ktime.h"
190struct tvec_base;
191#line 341
192struct tvec_base;
193#line 342 "include/linux/ktime.h"
194struct timer_list {
195 struct list_head entry ;
196 unsigned long expires ;
197 struct tvec_base *base ;
198 void (*function)(unsigned long ) ;
199 unsigned long data ;
200 int slack ;
201 int start_pid ;
202 void *start_site ;
203 char start_comm[16U] ;
204 struct lockdep_map lockdep_map ;
205};
206#line 302 "include/linux/timer.h"
207struct work_struct;
208#line 302
209struct work_struct;
210#line 45 "include/linux/workqueue.h"
211struct work_struct {
212 atomic_long_t data ;
213 struct list_head entry ;
214 void (*func)(struct work_struct * ) ;
215 struct lockdep_map lockdep_map ;
216};
217#line 445 "include/linux/elf.h"
218struct sock;
219#line 445
220struct sock;
221#line 446
222struct kobject;
223#line 446
224struct kobject;
225#line 447
226enum kobj_ns_type {
227 KOBJ_NS_TYPE_NONE = 0,
228 KOBJ_NS_TYPE_NET = 1,
229 KOBJ_NS_TYPES = 2
230} ;
231#line 453 "include/linux/elf.h"
232struct kobj_ns_type_operations {
233 enum kobj_ns_type type ;
234 void *(*grab_current_ns)(void) ;
235 void const *(*netlink_ns)(struct sock * ) ;
236 void const *(*initial_ns)(void) ;
237 void (*drop_ns)(void * ) ;
238};
239#line 57 "include/linux/kobject_ns.h"
240struct attribute {
241 char const *name ;
242 umode_t mode ;
243 struct lock_class_key *key ;
244 struct lock_class_key skey ;
245};
246#line 98 "include/linux/sysfs.h"
247struct sysfs_ops {
248 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
249 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
250 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
251};
252#line 117
253struct sysfs_dirent;
254#line 117
255struct sysfs_dirent;
256#line 182 "include/linux/sysfs.h"
257struct kref {
258 atomic_t refcount ;
259};
260#line 49 "include/linux/kobject.h"
261struct kset;
262#line 49
263struct kobj_type;
264#line 49 "include/linux/kobject.h"
265struct kobject {
266 char const *name ;
267 struct list_head entry ;
268 struct kobject *parent ;
269 struct kset *kset ;
270 struct kobj_type *ktype ;
271 struct sysfs_dirent *sd ;
272 struct kref kref ;
273 unsigned char state_initialized : 1 ;
274 unsigned char state_in_sysfs : 1 ;
275 unsigned char state_add_uevent_sent : 1 ;
276 unsigned char state_remove_uevent_sent : 1 ;
277 unsigned char uevent_suppress : 1 ;
278};
279#line 107 "include/linux/kobject.h"
280struct kobj_type {
281 void (*release)(struct kobject * ) ;
282 struct sysfs_ops const *sysfs_ops ;
283 struct attribute **default_attrs ;
284 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
285 void const *(*namespace)(struct kobject * ) ;
286};
287#line 115 "include/linux/kobject.h"
288struct kobj_uevent_env {
289 char *envp[32U] ;
290 int envp_idx ;
291 char buf[2048U] ;
292 int buflen ;
293};
294#line 122 "include/linux/kobject.h"
295struct kset_uevent_ops {
296 int (* const filter)(struct kset * , struct kobject * ) ;
297 char const *(* const name)(struct kset * , struct kobject * ) ;
298 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
299};
300#line 139 "include/linux/kobject.h"
301struct kset {
302 struct list_head list ;
303 spinlock_t list_lock ;
304 struct kobject kobj ;
305 struct kset_uevent_ops const *uevent_ops ;
306};
307#line 215
308struct kernel_param;
309#line 215
310struct kernel_param;
311#line 216 "include/linux/kobject.h"
312struct kernel_param_ops {
313 int (*set)(char const * , struct kernel_param const * ) ;
314 int (*get)(char * , struct kernel_param const * ) ;
315 void (*free)(void * ) ;
316};
317#line 49 "include/linux/moduleparam.h"
318struct kparam_string;
319#line 49
320struct kparam_array;
321#line 49 "include/linux/moduleparam.h"
322union __anonunion_ldv_13363_134 {
323 void *arg ;
324 struct kparam_string const *str ;
325 struct kparam_array const *arr ;
326};
327#line 49 "include/linux/moduleparam.h"
328struct kernel_param {
329 char const *name ;
330 struct kernel_param_ops const *ops ;
331 u16 perm ;
332 s16 level ;
333 union __anonunion_ldv_13363_134 ldv_13363 ;
334};
335#line 61 "include/linux/moduleparam.h"
336struct kparam_string {
337 unsigned int maxlen ;
338 char *string ;
339};
340#line 67 "include/linux/moduleparam.h"
341struct kparam_array {
342 unsigned int max ;
343 unsigned int elemsize ;
344 unsigned int *num ;
345 struct kernel_param_ops const *ops ;
346 void *elem ;
347};
348#line 88 "include/linux/kmemleak.h"
349struct kmem_cache_cpu {
350 void **freelist ;
351 unsigned long tid ;
352 struct page *page ;
353 struct page *partial ;
354 int node ;
355 unsigned int stat[26U] ;
356};
357#line 55 "include/linux/slub_def.h"
358struct kmem_cache_node {
359 spinlock_t list_lock ;
360 unsigned long nr_partial ;
361 struct list_head partial ;
362 atomic_long_t nr_slabs ;
363 atomic_long_t total_objects ;
364 struct list_head full ;
365};
366#line 66 "include/linux/slub_def.h"
367struct kmem_cache_order_objects {
368 unsigned long x ;
369};
370#line 76 "include/linux/slub_def.h"
371struct kmem_cache {
372 struct kmem_cache_cpu *cpu_slab ;
373 unsigned long flags ;
374 unsigned long min_partial ;
375 int size ;
376 int objsize ;
377 int offset ;
378 int cpu_partial ;
379 struct kmem_cache_order_objects oo ;
380 struct kmem_cache_order_objects max ;
381 struct kmem_cache_order_objects min ;
382 gfp_t allocflags ;
383 int refcount ;
384 void (*ctor)(void * ) ;
385 int inuse ;
386 int align ;
387 int reserved ;
388 char const *name ;
389 struct list_head list ;
390 struct kobject kobj ;
391 int remote_node_defrag_ratio ;
392 struct kmem_cache_node *node[1024U] ;
393};
394#line 15 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
395enum led_brightness {
396 LED_OFF = 0,
397 LED_HALF = 127,
398 LED_FULL = 255
399} ;
400#line 21
401struct led_trigger;
402#line 21 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
403struct led_classdev {
404 char const *name ;
405 int brightness ;
406 int max_brightness ;
407 int flags ;
408 void (*brightness_set)(struct led_classdev * , enum led_brightness ) ;
409 enum led_brightness (*brightness_get)(struct led_classdev * ) ;
410 int (*blink_set)(struct led_classdev * , unsigned long * , unsigned long * ) ;
411 struct device *dev ;
412 struct list_head node ;
413 char const *default_trigger ;
414 unsigned long blink_delay_on ;
415 unsigned long blink_delay_off ;
416 struct timer_list blink_timer ;
417 int blink_brightness ;
418 struct rw_semaphore trigger_lock ;
419 struct led_trigger *trigger ;
420 struct list_head trig_list ;
421 void *trigger_data ;
422};
423#line 113 "include/linux/leds.h"
424struct led_trigger {
425 char const *name ;
426 void (*activate)(struct led_classdev * ) ;
427 void (*deactivate)(struct led_classdev * ) ;
428 rwlock_t leddev_list_lock ;
429 struct list_head led_cdevs ;
430 struct list_head next_trig ;
431};
432#line 261
433enum power_supply_property {
434 POWER_SUPPLY_PROP_STATUS = 0,
435 POWER_SUPPLY_PROP_CHARGE_TYPE = 1,
436 POWER_SUPPLY_PROP_HEALTH = 2,
437 POWER_SUPPLY_PROP_PRESENT = 3,
438 POWER_SUPPLY_PROP_ONLINE = 4,
439 POWER_SUPPLY_PROP_TECHNOLOGY = 5,
440 POWER_SUPPLY_PROP_CYCLE_COUNT = 6,
441 POWER_SUPPLY_PROP_VOLTAGE_MAX = 7,
442 POWER_SUPPLY_PROP_VOLTAGE_MIN = 8,
443 POWER_SUPPLY_PROP_VOLTAGE_MAX_DESIGN = 9,
444 POWER_SUPPLY_PROP_VOLTAGE_MIN_DESIGN = 10,
445 POWER_SUPPLY_PROP_VOLTAGE_NOW = 11,
446 POWER_SUPPLY_PROP_VOLTAGE_AVG = 12,
447 POWER_SUPPLY_PROP_CURRENT_MAX = 13,
448 POWER_SUPPLY_PROP_CURRENT_NOW = 14,
449 POWER_SUPPLY_PROP_CURRENT_AVG = 15,
450 POWER_SUPPLY_PROP_POWER_NOW = 16,
451 POWER_SUPPLY_PROP_POWER_AVG = 17,
452 POWER_SUPPLY_PROP_CHARGE_FULL_DESIGN = 18,
453 POWER_SUPPLY_PROP_CHARGE_EMPTY_DESIGN = 19,
454 POWER_SUPPLY_PROP_CHARGE_FULL = 20,
455 POWER_SUPPLY_PROP_CHARGE_EMPTY = 21,
456 POWER_SUPPLY_PROP_CHARGE_NOW = 22,
457 POWER_SUPPLY_PROP_CHARGE_AVG = 23,
458 POWER_SUPPLY_PROP_CHARGE_COUNTER = 24,
459 POWER_SUPPLY_PROP_ENERGY_FULL_DESIGN = 25,
460 POWER_SUPPLY_PROP_ENERGY_EMPTY_DESIGN = 26,
461 POWER_SUPPLY_PROP_ENERGY_FULL = 27,
462 POWER_SUPPLY_PROP_ENERGY_EMPTY = 28,
463 POWER_SUPPLY_PROP_ENERGY_NOW = 29,
464 POWER_SUPPLY_PROP_ENERGY_AVG = 30,
465 POWER_SUPPLY_PROP_CAPACITY = 31,
466 POWER_SUPPLY_PROP_CAPACITY_LEVEL = 32,
467 POWER_SUPPLY_PROP_TEMP = 33,
468 POWER_SUPPLY_PROP_TEMP_AMBIENT = 34,
469 POWER_SUPPLY_PROP_TIME_TO_EMPTY_NOW = 35,
470 POWER_SUPPLY_PROP_TIME_TO_EMPTY_AVG = 36,
471 POWER_SUPPLY_PROP_TIME_TO_FULL_NOW = 37,
472 POWER_SUPPLY_PROP_TIME_TO_FULL_AVG = 38,
473 POWER_SUPPLY_PROP_TYPE = 39,
474 POWER_SUPPLY_PROP_SCOPE = 40,
475 POWER_SUPPLY_PROP_MODEL_NAME = 41,
476 POWER_SUPPLY_PROP_MANUFACTURER = 42,
477 POWER_SUPPLY_PROP_SERIAL_NUMBER = 43
478} ;
479#line 308
480enum power_supply_type {
481 POWER_SUPPLY_TYPE_UNKNOWN = 0,
482 POWER_SUPPLY_TYPE_BATTERY = 1,
483 POWER_SUPPLY_TYPE_UPS = 2,
484 POWER_SUPPLY_TYPE_MAINS = 3,
485 POWER_SUPPLY_TYPE_USB = 4,
486 POWER_SUPPLY_TYPE_USB_DCP = 5,
487 POWER_SUPPLY_TYPE_USB_CDP = 6,
488 POWER_SUPPLY_TYPE_USB_ACA = 7
489} ;
490#line 319 "include/linux/leds.h"
491union power_supply_propval {
492 int intval ;
493 char const *strval ;
494};
495#line 148 "include/linux/power_supply.h"
496struct power_supply {
497 char const *name ;
498 enum power_supply_type type ;
499 enum power_supply_property *properties ;
500 size_t num_properties ;
501 char **supplied_to ;
502 size_t num_supplicants ;
503 int (*get_property)(struct power_supply * , enum power_supply_property , union power_supply_propval * ) ;
504 int (*set_property)(struct power_supply * , enum power_supply_property , union power_supply_propval const * ) ;
505 int (*property_is_writeable)(struct power_supply * , enum power_supply_property ) ;
506 void (*external_power_changed)(struct power_supply * ) ;
507 void (*set_charged)(struct power_supply * ) ;
508 int use_for_apm ;
509 struct device *dev ;
510 struct work_struct changed_work ;
511 struct led_trigger *charging_full_trig ;
512 char *charging_full_trig_name ;
513 struct led_trigger *charging_trig ;
514 char *charging_trig_name ;
515 struct led_trigger *full_trig ;
516 char *full_trig_name ;
517 struct led_trigger *online_trig ;
518 char *online_trig_name ;
519 struct led_trigger *charging_blink_full_solid_trig ;
520 char *charging_blink_full_solid_trig_name ;
521};
522#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
523struct battery_property_map {
524 int value ;
525 char const *key ;
526};
527#line 2
528void ldv_spin_lock(void) ;
529#line 3
530void ldv_spin_unlock(void) ;
531#line 4
532int ldv_spin_trylock(void) ;
533#line 101 "include/linux/printk.h"
534extern int printk(char const * , ...) ;
535#line 335 "include/linux/kernel.h"
536extern int sscanf(char const * , char const * , ...) ;
537#line 61 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/string_64.h"
538extern size_t strlen(char const * ) ;
539#line 62
540extern char *strcpy(char * , char const * ) ;
541#line 27 "include/linux/string.h"
542extern char *strncpy(char * , char const * , __kernel_size_t ) ;
543#line 54
544extern int strncasecmp(char const * , char const * , size_t ) ;
545#line 84
546extern __kernel_size_t strnlen(char const * , __kernel_size_t ) ;
547#line 220 "include/linux/slub_def.h"
548extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
549#line 223
550void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
551#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
552void ldv_check_alloc_flags(gfp_t flags ) ;
553#line 12
554void ldv_check_alloc_nonatomic(void) ;
555#line 14
556struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
557#line 210 "include/linux/power_supply.h"
558extern void power_supply_changed(struct power_supply * ) ;
559#line 220
560extern int power_supply_register(struct device * , struct power_supply * ) ;
561#line 222
562extern void power_supply_unregister(struct power_supply * ) ;
563#line 46 "include/linux/delay.h"
564extern void msleep(unsigned int ) ;
565#line 50 "include/linux/delay.h"
566__inline static void ssleep(unsigned int seconds )
567{ unsigned int __cil_tmp2 ;
568
569 {
570 {
571#line 52
572 __cil_tmp2 = seconds * 1000U;
573#line 52
574 msleep(__cil_tmp2);
575 }
576#line 53
577 return;
578}
579}
580#line 39 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
581static int ac_online = 1;
582#line 40 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
583static int battery_status = 2;
584#line 41 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
585static int battery_health = 1;
586#line 42 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
587static int battery_present = 1;
588#line 43 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
589static int battery_technology = 2;
590#line 44 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
591static int battery_capacity = 50;
592#line 46 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
593static int test_power_get_ac_property(struct power_supply *psy , enum power_supply_property psp ,
594 union power_supply_propval *val )
595{ unsigned int __cil_tmp4 ;
596 int *__cil_tmp5 ;
597
598 {
599 {
600#line 50
601 __cil_tmp4 = (unsigned int )psp;
602#line 51
603 if ((int )__cil_tmp4 == 4) {
604#line 51
605 goto case_4;
606 } else {
607 {
608#line 54
609 goto switch_default;
610#line 50
611 if (0) {
612 case_4:
613#line 52
614 __cil_tmp5 = & ac_online;
615#line 52
616 *((int *)val) = *__cil_tmp5;
617#line 53
618 goto ldv_14485;
619 switch_default: ;
620#line 55
621 return (-22);
622 } else {
623 switch_break: ;
624 }
625 }
626 }
627 }
628 ldv_14485: ;
629#line 57
630 return (0);
631}
632}
633#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
634static int test_power_get_battery_property(struct power_supply *psy , enum power_supply_property psp ,
635 union power_supply_propval *val )
636{ unsigned int __cil_tmp4 ;
637 int *__cil_tmp5 ;
638 int *__cil_tmp6 ;
639 int *__cil_tmp7 ;
640 int *__cil_tmp8 ;
641 int *__cil_tmp9 ;
642
643 {
644 {
645#line 64
646 __cil_tmp4 = (unsigned int )psp;
647#line 65
648 if ((int )__cil_tmp4 == 41) {
649#line 65
650 goto case_41;
651 } else
652#line 68
653 if ((int )__cil_tmp4 == 42) {
654#line 68
655 goto case_42;
656 } else
657#line 71
658 if ((int )__cil_tmp4 == 43) {
659#line 71
660 goto case_43;
661 } else
662#line 74
663 if ((int )__cil_tmp4 == 0) {
664#line 74
665 goto case_0;
666 } else
667#line 77
668 if ((int )__cil_tmp4 == 1) {
669#line 77
670 goto case_1;
671 } else
672#line 80
673 if ((int )__cil_tmp4 == 2) {
674#line 80
675 goto case_2;
676 } else
677#line 83
678 if ((int )__cil_tmp4 == 3) {
679#line 83
680 goto case_3;
681 } else
682#line 86
683 if ((int )__cil_tmp4 == 5) {
684#line 86
685 goto case_5;
686 } else
687#line 89
688 if ((int )__cil_tmp4 == 32) {
689#line 89
690 goto case_32;
691 } else
692#line 92
693 if ((int )__cil_tmp4 == 31) {
694#line 92
695 goto case_31;
696 } else
697#line 93
698 if ((int )__cil_tmp4 == 22) {
699#line 93
700 goto case_22;
701 } else
702#line 96
703 if ((int )__cil_tmp4 == 18) {
704#line 96
705 goto case_18;
706 } else
707#line 97
708 if ((int )__cil_tmp4 == 20) {
709#line 97
710 goto case_20;
711 } else
712#line 100
713 if ((int )__cil_tmp4 == 36) {
714#line 100
715 goto case_36;
716 } else
717#line 101
718 if ((int )__cil_tmp4 == 37) {
719#line 101
720 goto case_37;
721 } else {
722 {
723#line 104
724 goto switch_default;
725#line 64
726 if (0) {
727 case_41:
728#line 66
729 *((char const **)val) = "Test battery";
730#line 67
731 goto ldv_14493;
732 case_42:
733#line 69
734 *((char const **)val) = "Linux";
735#line 70
736 goto ldv_14493;
737 case_43:
738#line 72
739 *((char const **)val) = "3.4.0";
740#line 73
741 goto ldv_14493;
742 case_0:
743#line 75
744 __cil_tmp5 = & battery_status;
745#line 75
746 *((int *)val) = *__cil_tmp5;
747#line 76
748 goto ldv_14493;
749 case_1:
750#line 78
751 *((int *)val) = 3;
752#line 79
753 goto ldv_14493;
754 case_2:
755#line 81
756 __cil_tmp6 = & battery_health;
757#line 81
758 *((int *)val) = *__cil_tmp6;
759#line 82
760 goto ldv_14493;
761 case_3:
762#line 84
763 __cil_tmp7 = & battery_present;
764#line 84
765 *((int *)val) = *__cil_tmp7;
766#line 85
767 goto ldv_14493;
768 case_5:
769#line 87
770 __cil_tmp8 = & battery_technology;
771#line 87
772 *((int *)val) = *__cil_tmp8;
773#line 88
774 goto ldv_14493;
775 case_32:
776#line 90
777 *((int *)val) = 3;
778#line 91
779 goto ldv_14493;
780 case_31: ;
781 case_22:
782#line 94
783 __cil_tmp9 = & battery_capacity;
784#line 94
785 *((int *)val) = *__cil_tmp9;
786#line 95
787 goto ldv_14493;
788 case_18: ;
789 case_20:
790#line 98
791 *((int *)val) = 100;
792#line 99
793 goto ldv_14493;
794 case_36: ;
795 case_37:
796#line 102
797 *((int *)val) = 3600;
798#line 103
799 goto ldv_14493;
800 switch_default:
801 {
802#line 105
803 printk("<6>%s: some properties deliberately report errors.\n", "test_power_get_battery_property");
804 }
805#line 107
806 return (-22);
807 } else {
808 switch_break: ;
809 }
810 }
811 }
812 }
813 ldv_14493: ;
814#line 109
815 return (0);
816}
817}
818#line 112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
819static enum power_supply_property test_power_ac_props[1U] = { (enum power_supply_property )4};
820#line 116 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
821static enum power_supply_property test_power_battery_props[15U] =
822#line 116
823 { (enum power_supply_property )0, (enum power_supply_property )1, (enum power_supply_property )2, (enum power_supply_property )3,
824 (enum power_supply_property )5, (enum power_supply_property )18, (enum power_supply_property )20, (enum power_supply_property )22,
825 (enum power_supply_property )31, (enum power_supply_property )32, (enum power_supply_property )36, (enum power_supply_property )37,
826 (enum power_supply_property )41, (enum power_supply_property )42, (enum power_supply_property )43};
827#line 134 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
828static char *test_power_ac_supplied_to[1U] = { (char *)"test_battery"};
829#line 138 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
830static struct power_supply test_power_supplies[2U] = { {"test_ac", (enum power_supply_type )3, (enum power_supply_property *)(& test_power_ac_props),
831 1UL, (char **)(& test_power_ac_supplied_to), 1UL, & test_power_get_ac_property,
832 (int (*)(struct power_supply * , enum power_supply_property , union power_supply_propval const * ))0,
833 (int (*)(struct power_supply * , enum power_supply_property ))0, (void (*)(struct power_supply * ))0,
834 (void (*)(struct power_supply * ))0, 0, (struct device *)0, {{0L}, {(struct list_head *)0,
835 (struct list_head *)0},
836 (void (*)(struct work_struct * ))0,
837 {(struct lock_class_key *)0,
838 {(struct lock_class *)0,
839 (struct lock_class *)0},
840 (char const *)0,
841 0, 0UL}}, (struct led_trigger *)0,
842 (char *)0, (struct led_trigger *)0, (char *)0, (struct led_trigger *)0, (char *)0,
843 (struct led_trigger *)0, (char *)0, (struct led_trigger *)0, (char *)0},
844 {"test_battery", (enum power_supply_type )1, (enum power_supply_property *)(& test_power_battery_props),
845 15UL, (char **)0, 0UL, & test_power_get_battery_property, (int (*)(struct power_supply * ,
846 enum power_supply_property ,
847 union power_supply_propval const * ))0,
848 (int (*)(struct power_supply * , enum power_supply_property ))0, (void (*)(struct power_supply * ))0,
849 (void (*)(struct power_supply * ))0, 0, (struct device *)0, {{0L}, {(struct list_head *)0,
850 (struct list_head *)0},
851 (void (*)(struct work_struct * ))0,
852 {(struct lock_class_key *)0,
853 {(struct lock_class *)0,
854 (struct lock_class *)0},
855 (char const *)0,
856 0, 0UL}}, (struct led_trigger *)0,
857 (char *)0, (struct led_trigger *)0, (char *)0, (struct led_trigger *)0, (char *)0,
858 (struct led_trigger *)0, (char *)0, (struct led_trigger *)0, (char *)0}};
859#line 157 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
860static int test_power_init(void)
861{ int i ;
862 int ret ;
863 struct device *__cil_tmp3 ;
864 unsigned long __cil_tmp4 ;
865 struct power_supply *__cil_tmp5 ;
866 struct power_supply *__cil_tmp6 ;
867 unsigned long __cil_tmp7 ;
868 unsigned long __cil_tmp8 ;
869 char const *__cil_tmp9 ;
870 unsigned int __cil_tmp10 ;
871 unsigned long __cil_tmp11 ;
872 struct power_supply *__cil_tmp12 ;
873 struct power_supply *__cil_tmp13 ;
874
875 {
876#line 162
877 i = 0;
878#line 162
879 goto ldv_14530;
880 ldv_14529:
881 {
882#line 163
883 __cil_tmp3 = (struct device *)0;
884#line 163
885 __cil_tmp4 = (unsigned long )i;
886#line 163
887 __cil_tmp5 = (struct power_supply *)(& test_power_supplies);
888#line 163
889 __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
890#line 163
891 ret = power_supply_register(__cil_tmp3, __cil_tmp6);
892 }
893#line 164
894 if (ret != 0) {
895 {
896#line 165
897 __cil_tmp7 = i * 264UL;
898#line 165
899 __cil_tmp8 = (unsigned long )(test_power_supplies) + __cil_tmp7;
900#line 165
901 __cil_tmp9 = *((char const **)__cil_tmp8);
902#line 165
903 printk("<3>%s: failed to register %s\n", "test_power_init", __cil_tmp9);
904 }
905#line 167
906 goto failed;
907 } else {
908
909 }
910#line 162
911 i = i + 1;
912 ldv_14530: ;
913 {
914#line 162
915 __cil_tmp10 = (unsigned int )i;
916#line 162
917 if (__cil_tmp10 <= 1U) {
918#line 163
919 goto ldv_14529;
920 } else {
921#line 165
922 goto ldv_14531;
923 }
924 }
925 ldv_14531: ;
926#line 171
927 return (0);
928 failed: ;
929#line 173
930 goto ldv_14533;
931 ldv_14532:
932 {
933#line 174
934 __cil_tmp11 = (unsigned long )i;
935#line 174
936 __cil_tmp12 = (struct power_supply *)(& test_power_supplies);
937#line 174
938 __cil_tmp13 = __cil_tmp12 + __cil_tmp11;
939#line 174
940 power_supply_unregister(__cil_tmp13);
941 }
942 ldv_14533:
943#line 173
944 i = i - 1;
945#line 173
946 if (i >= 0) {
947#line 174
948 goto ldv_14532;
949 } else {
950#line 176
951 goto ldv_14534;
952 }
953 ldv_14534: ;
954#line 175
955 return (ret);
956}
957}
958#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
959static void test_power_exit(void)
960{ int i ;
961 int *__cil_tmp2 ;
962 int *__cil_tmp3 ;
963 unsigned long __cil_tmp4 ;
964 struct power_supply *__cil_tmp5 ;
965 struct power_supply *__cil_tmp6 ;
966 unsigned int __cil_tmp7 ;
967 unsigned long __cil_tmp8 ;
968 struct power_supply *__cil_tmp9 ;
969 struct power_supply *__cil_tmp10 ;
970 unsigned int __cil_tmp11 ;
971
972 {
973#line 184
974 __cil_tmp2 = & ac_online;
975#line 184
976 *__cil_tmp2 = 0;
977#line 185
978 __cil_tmp3 = & battery_status;
979#line 185
980 *__cil_tmp3 = 2;
981#line 186
982 i = 0;
983#line 186
984 goto ldv_14547;
985 ldv_14546:
986 {
987#line 187
988 __cil_tmp4 = (unsigned long )i;
989#line 187
990 __cil_tmp5 = (struct power_supply *)(& test_power_supplies);
991#line 187
992 __cil_tmp6 = __cil_tmp5 + __cil_tmp4;
993#line 187
994 power_supply_changed(__cil_tmp6);
995#line 186
996 i = i + 1;
997 }
998 ldv_14547: ;
999 {
1000#line 186
1001 __cil_tmp7 = (unsigned int )i;
1002#line 186
1003 if (__cil_tmp7 <= 1U) {
1004#line 187
1005 goto ldv_14546;
1006 } else {
1007#line 189
1008 goto ldv_14548;
1009 }
1010 }
1011 ldv_14548:
1012 {
1013#line 188
1014 printk("<6>%s: \'changed\' event sent, sleeping for 10 seconds...\n", "test_power_exit");
1015#line 190
1016 ssleep(10U);
1017#line 192
1018 i = 0;
1019 }
1020#line 192
1021 goto ldv_14553;
1022 ldv_14552:
1023 {
1024#line 193
1025 __cil_tmp8 = (unsigned long )i;
1026#line 193
1027 __cil_tmp9 = (struct power_supply *)(& test_power_supplies);
1028#line 193
1029 __cil_tmp10 = __cil_tmp9 + __cil_tmp8;
1030#line 193
1031 power_supply_unregister(__cil_tmp10);
1032#line 192
1033 i = i + 1;
1034 }
1035 ldv_14553: ;
1036 {
1037#line 192
1038 __cil_tmp11 = (unsigned int )i;
1039#line 192
1040 if (__cil_tmp11 <= 1U) {
1041#line 193
1042 goto ldv_14552;
1043 } else {
1044#line 195
1045 goto ldv_14554;
1046 }
1047 }
1048 ldv_14554: ;
1049#line 197
1050 return;
1051}
1052}
1053#line 205 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1054static struct battery_property_map map_ac_online[3U] = { {0, "on"},
1055 {1, "off"},
1056 {-1, (char const *)0}};
1057#line 211 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1058static struct battery_property_map map_status[5U] = { {1, "charging"},
1059 {2, "discharging"},
1060 {3, "not-charging"},
1061 {4, "full"},
1062 {-1, (char const *)0}};
1063#line 219 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1064static struct battery_property_map map_health[6U] = { {1, "good"},
1065 {2, "overheat"},
1066 {3, "dead"},
1067 {4, "overvoltage"},
1068 {5, "failure"},
1069 {-1, (char const *)0}};
1070#line 228 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1071static struct battery_property_map map_present[3U] = { {0, "false"},
1072 {1, "true"},
1073 {-1, (char const *)0}};
1074#line 234 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1075static struct battery_property_map map_technology[7U] = { {1, "NiMH"},
1076 {2, "LION"},
1077 {3, "LIPO"},
1078 {4, "LiFe"},
1079 {5, "NiCd"},
1080 {6, "LiMn"},
1081 {-1, (char const *)0}};
1082#line 245 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1083static int map_get_value(struct battery_property_map *map , char const *key , int def_val )
1084{ char buf[256U] ;
1085 int cr ;
1086 __kernel_size_t tmp ;
1087 int tmp___0 ;
1088 char *__cil_tmp8 ;
1089 unsigned long __cil_tmp9 ;
1090 unsigned long __cil_tmp10 ;
1091 char const *__cil_tmp11 ;
1092 unsigned int __cil_tmp12 ;
1093 unsigned int __cil_tmp13 ;
1094 unsigned long __cil_tmp14 ;
1095 unsigned long __cil_tmp15 ;
1096 char __cil_tmp16 ;
1097 signed char __cil_tmp17 ;
1098 int __cil_tmp18 ;
1099 unsigned long __cil_tmp19 ;
1100 unsigned long __cil_tmp20 ;
1101 unsigned long __cil_tmp21 ;
1102 unsigned long __cil_tmp22 ;
1103 char const *__cil_tmp23 ;
1104 char const *__cil_tmp24 ;
1105 char const *__cil_tmp25 ;
1106 unsigned long __cil_tmp26 ;
1107 unsigned long __cil_tmp27 ;
1108 unsigned long __cil_tmp28 ;
1109 char const *__cil_tmp29 ;
1110 unsigned long __cil_tmp30 ;
1111
1112 {
1113 {
1114#line 251
1115 __cil_tmp8 = (char *)(& buf);
1116#line 251
1117 strncpy(__cil_tmp8, key, 256UL);
1118#line 252
1119 __cil_tmp9 = 255 * 1UL;
1120#line 252
1121 __cil_tmp10 = (unsigned long )(buf) + __cil_tmp9;
1122#line 252
1123 *((char *)__cil_tmp10) = (char)0;
1124#line 254
1125 __cil_tmp11 = (char const *)(& buf);
1126#line 254
1127 tmp = strnlen(__cil_tmp11, 256UL);
1128#line 254
1129 __cil_tmp12 = (unsigned int )tmp;
1130#line 254
1131 __cil_tmp13 = __cil_tmp12 - 1U;
1132#line 254
1133 cr = (int )__cil_tmp13;
1134 }
1135 {
1136#line 255
1137 __cil_tmp14 = cr * 1UL;
1138#line 255
1139 __cil_tmp15 = (unsigned long )(buf) + __cil_tmp14;
1140#line 255
1141 __cil_tmp16 = *((char *)__cil_tmp15);
1142#line 255
1143 __cil_tmp17 = (signed char )__cil_tmp16;
1144#line 255
1145 __cil_tmp18 = (int )__cil_tmp17;
1146#line 255
1147 if (__cil_tmp18 == 10) {
1148#line 256
1149 __cil_tmp19 = cr * 1UL;
1150#line 256
1151 __cil_tmp20 = (unsigned long )(buf) + __cil_tmp19;
1152#line 256
1153 *((char *)__cil_tmp20) = (char)0;
1154 } else {
1155
1156 }
1157 }
1158#line 258
1159 goto ldv_14576;
1160 ldv_14575:
1161 {
1162#line 259
1163 __cil_tmp21 = (unsigned long )map;
1164#line 259
1165 __cil_tmp22 = __cil_tmp21 + 8;
1166#line 259
1167 __cil_tmp23 = *((char const **)__cil_tmp22);
1168#line 259
1169 __cil_tmp24 = (char const *)(& buf);
1170#line 259
1171 tmp___0 = strncasecmp(__cil_tmp23, __cil_tmp24, 256UL);
1172 }
1173#line 259
1174 if (tmp___0 == 0) {
1175#line 260
1176 return (*((int *)map));
1177 } else {
1178
1179 }
1180#line 261
1181 map = map + 1;
1182 ldv_14576: ;
1183 {
1184#line 258
1185 __cil_tmp25 = (char const *)0;
1186#line 258
1187 __cil_tmp26 = (unsigned long )__cil_tmp25;
1188#line 258
1189 __cil_tmp27 = (unsigned long )map;
1190#line 258
1191 __cil_tmp28 = __cil_tmp27 + 8;
1192#line 258
1193 __cil_tmp29 = *((char const **)__cil_tmp28);
1194#line 258
1195 __cil_tmp30 = (unsigned long )__cil_tmp29;
1196#line 258
1197 if (__cil_tmp30 != __cil_tmp26) {
1198#line 259
1199 goto ldv_14575;
1200 } else {
1201#line 261
1202 goto ldv_14577;
1203 }
1204 }
1205 ldv_14577: ;
1206#line 264
1207 return (def_val);
1208}
1209}
1210#line 268 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1211static char const *map_get_key(struct battery_property_map *map , int value , char const *def_key )
1212{ int __cil_tmp4 ;
1213 unsigned long __cil_tmp5 ;
1214 unsigned long __cil_tmp6 ;
1215 char const *__cil_tmp7 ;
1216 unsigned long __cil_tmp8 ;
1217 unsigned long __cil_tmp9 ;
1218 unsigned long __cil_tmp10 ;
1219 char const *__cil_tmp11 ;
1220 unsigned long __cil_tmp12 ;
1221
1222 {
1223#line 271
1224 goto ldv_14584;
1225 ldv_14583: ;
1226 {
1227#line 272
1228 __cil_tmp4 = *((int *)map);
1229#line 272
1230 if (__cil_tmp4 == value) {
1231 {
1232#line 273
1233 __cil_tmp5 = (unsigned long )map;
1234#line 273
1235 __cil_tmp6 = __cil_tmp5 + 8;
1236#line 273
1237 return (*((char const **)__cil_tmp6));
1238 }
1239 } else {
1240
1241 }
1242 }
1243#line 274
1244 map = map + 1;
1245 ldv_14584: ;
1246 {
1247#line 271
1248 __cil_tmp7 = (char const *)0;
1249#line 271
1250 __cil_tmp8 = (unsigned long )__cil_tmp7;
1251#line 271
1252 __cil_tmp9 = (unsigned long )map;
1253#line 271
1254 __cil_tmp10 = __cil_tmp9 + 8;
1255#line 271
1256 __cil_tmp11 = *((char const **)__cil_tmp10);
1257#line 271
1258 __cil_tmp12 = (unsigned long )__cil_tmp11;
1259#line 271
1260 if (__cil_tmp12 != __cil_tmp8) {
1261#line 272
1262 goto ldv_14583;
1263 } else {
1264#line 274
1265 goto ldv_14585;
1266 }
1267 }
1268 ldv_14585: ;
1269#line 277
1270 return (def_key);
1271}
1272}
1273#line 280 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1274static int param_set_ac_online(char const *key , struct kernel_param const *kp )
1275{ int *__cil_tmp3 ;
1276 struct battery_property_map *__cil_tmp4 ;
1277 int *__cil_tmp5 ;
1278 int __cil_tmp6 ;
1279 struct power_supply *__cil_tmp7 ;
1280
1281 {
1282 {
1283#line 282
1284 __cil_tmp3 = & ac_online;
1285#line 282
1286 __cil_tmp4 = (struct battery_property_map *)(& map_ac_online);
1287#line 282
1288 __cil_tmp5 = & ac_online;
1289#line 282
1290 __cil_tmp6 = *__cil_tmp5;
1291#line 282
1292 *__cil_tmp3 = map_get_value(__cil_tmp4, key, __cil_tmp6);
1293#line 283
1294 __cil_tmp7 = (struct power_supply *)(& test_power_supplies);
1295#line 283
1296 power_supply_changed(__cil_tmp7);
1297 }
1298#line 284
1299 return (0);
1300}
1301}
1302#line 287 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1303static int param_get_ac_online(char *buffer , struct kernel_param const *kp )
1304{ char const *tmp ;
1305 size_t tmp___0 ;
1306 struct battery_property_map *__cil_tmp5 ;
1307 int *__cil_tmp6 ;
1308 int __cil_tmp7 ;
1309 char const *__cil_tmp8 ;
1310
1311 {
1312 {
1313#line 289
1314 __cil_tmp5 = (struct battery_property_map *)(& map_ac_online);
1315#line 289
1316 __cil_tmp6 = & ac_online;
1317#line 289
1318 __cil_tmp7 = *__cil_tmp6;
1319#line 289
1320 tmp = map_get_key(__cil_tmp5, __cil_tmp7, "unknown");
1321#line 289
1322 strcpy(buffer, tmp);
1323#line 290
1324 __cil_tmp8 = (char const *)buffer;
1325#line 290
1326 tmp___0 = strlen(__cil_tmp8);
1327 }
1328#line 290
1329 return ((int )tmp___0);
1330}
1331}
1332#line 293 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1333static int param_set_battery_status(char const *key , struct kernel_param const *kp )
1334{ int *__cil_tmp3 ;
1335 struct battery_property_map *__cil_tmp4 ;
1336 int *__cil_tmp5 ;
1337 int __cil_tmp6 ;
1338 struct power_supply *__cil_tmp7 ;
1339 struct power_supply *__cil_tmp8 ;
1340
1341 {
1342 {
1343#line 296
1344 __cil_tmp3 = & battery_status;
1345#line 296
1346 __cil_tmp4 = (struct battery_property_map *)(& map_status);
1347#line 296
1348 __cil_tmp5 = & battery_status;
1349#line 296
1350 __cil_tmp6 = *__cil_tmp5;
1351#line 296
1352 *__cil_tmp3 = map_get_value(__cil_tmp4, key, __cil_tmp6);
1353#line 297
1354 __cil_tmp7 = (struct power_supply *)(& test_power_supplies);
1355#line 297
1356 __cil_tmp8 = __cil_tmp7 + 1UL;
1357#line 297
1358 power_supply_changed(__cil_tmp8);
1359 }
1360#line 298
1361 return (0);
1362}
1363}
1364#line 301 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1365static int param_get_battery_status(char *buffer , struct kernel_param const *kp )
1366{ char const *tmp ;
1367 size_t tmp___0 ;
1368 struct battery_property_map *__cil_tmp5 ;
1369 int *__cil_tmp6 ;
1370 int __cil_tmp7 ;
1371 char const *__cil_tmp8 ;
1372
1373 {
1374 {
1375#line 303
1376 __cil_tmp5 = (struct battery_property_map *)(& map_status);
1377#line 303
1378 __cil_tmp6 = & battery_status;
1379#line 303
1380 __cil_tmp7 = *__cil_tmp6;
1381#line 303
1382 tmp = map_get_key(__cil_tmp5, __cil_tmp7, "unknown");
1383#line 303
1384 strcpy(buffer, tmp);
1385#line 304
1386 __cil_tmp8 = (char const *)buffer;
1387#line 304
1388 tmp___0 = strlen(__cil_tmp8);
1389 }
1390#line 304
1391 return ((int )tmp___0);
1392}
1393}
1394#line 307 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1395static int param_set_battery_health(char const *key , struct kernel_param const *kp )
1396{ int *__cil_tmp3 ;
1397 struct battery_property_map *__cil_tmp4 ;
1398 int *__cil_tmp5 ;
1399 int __cil_tmp6 ;
1400 struct power_supply *__cil_tmp7 ;
1401 struct power_supply *__cil_tmp8 ;
1402
1403 {
1404 {
1405#line 310
1406 __cil_tmp3 = & battery_health;
1407#line 310
1408 __cil_tmp4 = (struct battery_property_map *)(& map_health);
1409#line 310
1410 __cil_tmp5 = & battery_health;
1411#line 310
1412 __cil_tmp6 = *__cil_tmp5;
1413#line 310
1414 *__cil_tmp3 = map_get_value(__cil_tmp4, key, __cil_tmp6);
1415#line 311
1416 __cil_tmp7 = (struct power_supply *)(& test_power_supplies);
1417#line 311
1418 __cil_tmp8 = __cil_tmp7 + 1UL;
1419#line 311
1420 power_supply_changed(__cil_tmp8);
1421 }
1422#line 312
1423 return (0);
1424}
1425}
1426#line 315 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1427static int param_get_battery_health(char *buffer , struct kernel_param const *kp )
1428{ char const *tmp ;
1429 size_t tmp___0 ;
1430 struct battery_property_map *__cil_tmp5 ;
1431 int *__cil_tmp6 ;
1432 int __cil_tmp7 ;
1433 char const *__cil_tmp8 ;
1434
1435 {
1436 {
1437#line 317
1438 __cil_tmp5 = (struct battery_property_map *)(& map_health);
1439#line 317
1440 __cil_tmp6 = & battery_health;
1441#line 317
1442 __cil_tmp7 = *__cil_tmp6;
1443#line 317
1444 tmp = map_get_key(__cil_tmp5, __cil_tmp7, "unknown");
1445#line 317
1446 strcpy(buffer, tmp);
1447#line 318
1448 __cil_tmp8 = (char const *)buffer;
1449#line 318
1450 tmp___0 = strlen(__cil_tmp8);
1451 }
1452#line 318
1453 return ((int )tmp___0);
1454}
1455}
1456#line 321 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1457static int param_set_battery_present(char const *key , struct kernel_param const *kp )
1458{ int *__cil_tmp3 ;
1459 struct battery_property_map *__cil_tmp4 ;
1460 int *__cil_tmp5 ;
1461 int __cil_tmp6 ;
1462 struct power_supply *__cil_tmp7 ;
1463
1464 {
1465 {
1466#line 324
1467 __cil_tmp3 = & battery_present;
1468#line 324
1469 __cil_tmp4 = (struct battery_property_map *)(& map_present);
1470#line 324
1471 __cil_tmp5 = & battery_present;
1472#line 324
1473 __cil_tmp6 = *__cil_tmp5;
1474#line 324
1475 *__cil_tmp3 = map_get_value(__cil_tmp4, key, __cil_tmp6);
1476#line 325
1477 __cil_tmp7 = (struct power_supply *)(& test_power_supplies);
1478#line 325
1479 power_supply_changed(__cil_tmp7);
1480 }
1481#line 326
1482 return (0);
1483}
1484}
1485#line 329 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1486static int param_get_battery_present(char *buffer , struct kernel_param const *kp )
1487{ char const *tmp ;
1488 size_t tmp___0 ;
1489 struct battery_property_map *__cil_tmp5 ;
1490 int *__cil_tmp6 ;
1491 int __cil_tmp7 ;
1492 char const *__cil_tmp8 ;
1493
1494 {
1495 {
1496#line 332
1497 __cil_tmp5 = (struct battery_property_map *)(& map_present);
1498#line 332
1499 __cil_tmp6 = & battery_present;
1500#line 332
1501 __cil_tmp7 = *__cil_tmp6;
1502#line 332
1503 tmp = map_get_key(__cil_tmp5, __cil_tmp7, "unknown");
1504#line 332
1505 strcpy(buffer, tmp);
1506#line 333
1507 __cil_tmp8 = (char const *)buffer;
1508#line 333
1509 tmp___0 = strlen(__cil_tmp8);
1510 }
1511#line 333
1512 return ((int )tmp___0);
1513}
1514}
1515#line 336 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1516static int param_set_battery_technology(char const *key , struct kernel_param const *kp )
1517{ int *__cil_tmp3 ;
1518 struct battery_property_map *__cil_tmp4 ;
1519 int *__cil_tmp5 ;
1520 int __cil_tmp6 ;
1521 struct power_supply *__cil_tmp7 ;
1522 struct power_supply *__cil_tmp8 ;
1523
1524 {
1525 {
1526#line 339
1527 __cil_tmp3 = & battery_technology;
1528#line 339
1529 __cil_tmp4 = (struct battery_property_map *)(& map_technology);
1530#line 339
1531 __cil_tmp5 = & battery_technology;
1532#line 339
1533 __cil_tmp6 = *__cil_tmp5;
1534#line 339
1535 *__cil_tmp3 = map_get_value(__cil_tmp4, key, __cil_tmp6);
1536#line 341
1537 __cil_tmp7 = (struct power_supply *)(& test_power_supplies);
1538#line 341
1539 __cil_tmp8 = __cil_tmp7 + 1UL;
1540#line 341
1541 power_supply_changed(__cil_tmp8);
1542 }
1543#line 342
1544 return (0);
1545}
1546}
1547#line 345 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1548static int param_get_battery_technology(char *buffer , struct kernel_param const *kp )
1549{ char const *tmp ;
1550 size_t tmp___0 ;
1551 struct battery_property_map *__cil_tmp5 ;
1552 int *__cil_tmp6 ;
1553 int __cil_tmp7 ;
1554 char const *__cil_tmp8 ;
1555
1556 {
1557 {
1558#line 348
1559 __cil_tmp5 = (struct battery_property_map *)(& map_technology);
1560#line 348
1561 __cil_tmp6 = & battery_technology;
1562#line 348
1563 __cil_tmp7 = *__cil_tmp6;
1564#line 348
1565 tmp = map_get_key(__cil_tmp5, __cil_tmp7, "unknown");
1566#line 348
1567 strcpy(buffer, tmp);
1568#line 350
1569 __cil_tmp8 = (char const *)buffer;
1570#line 350
1571 tmp___0 = strlen(__cil_tmp8);
1572 }
1573#line 350
1574 return ((int )tmp___0);
1575}
1576}
1577#line 353 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1578static int param_set_battery_capacity(char const *key , struct kernel_param const *kp )
1579{ int tmp ;
1580 int tmp___0 ;
1581 int *__cil_tmp5 ;
1582 int *__cil_tmp6 ;
1583 struct power_supply *__cil_tmp7 ;
1584 struct power_supply *__cil_tmp8 ;
1585
1586 {
1587 {
1588#line 358
1589 tmp___0 = sscanf(key, "%d", & tmp);
1590 }
1591#line 358
1592 if (tmp___0 != 1) {
1593#line 359
1594 return (-22);
1595 } else {
1596
1597 }
1598 {
1599#line 361
1600 __cil_tmp5 = & battery_capacity;
1601#line 361
1602 __cil_tmp6 = & tmp;
1603#line 361
1604 *__cil_tmp5 = *__cil_tmp6;
1605#line 362
1606 __cil_tmp7 = (struct power_supply *)(& test_power_supplies);
1607#line 362
1608 __cil_tmp8 = __cil_tmp7 + 1UL;
1609#line 362
1610 power_supply_changed(__cil_tmp8);
1611 }
1612#line 363
1613 return (0);
1614}
1615}
1616#line 452
1617extern void ldv_check_final_state(void) ;
1618#line 458
1619extern void ldv_initialize(void) ;
1620#line 461
1621extern int __VERIFIER_nondet_int(void) ;
1622#line 464 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1623int LDV_IN_INTERRUPT ;
1624#line 467 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1625void main(void)
1626{ char const *var_param_set_ac_online_6_p0 ;
1627 struct kernel_param const *var_param_set_ac_online_6_p1 ;
1628 char *var_param_get_ac_online_7_p0 ;
1629 struct kernel_param const *var_param_get_ac_online_7_p1 ;
1630 char const *var_param_set_battery_status_8_p0 ;
1631 struct kernel_param const *var_param_set_battery_status_8_p1 ;
1632 char *var_param_get_battery_status_9_p0 ;
1633 struct kernel_param const *var_param_get_battery_status_9_p1 ;
1634 char const *var_param_set_battery_present_12_p0 ;
1635 struct kernel_param const *var_param_set_battery_present_12_p1 ;
1636 char *var_param_get_battery_present_13_p0 ;
1637 struct kernel_param const *var_param_get_battery_present_13_p1 ;
1638 char const *var_param_set_battery_technology_14_p0 ;
1639 struct kernel_param const *var_param_set_battery_technology_14_p1 ;
1640 char *var_param_get_battery_technology_15_p0 ;
1641 struct kernel_param const *var_param_get_battery_technology_15_p1 ;
1642 char const *var_param_set_battery_health_10_p0 ;
1643 struct kernel_param const *var_param_set_battery_health_10_p1 ;
1644 char *var_param_get_battery_health_11_p0 ;
1645 struct kernel_param const *var_param_get_battery_health_11_p1 ;
1646 char const *var_param_set_battery_capacity_16_p0 ;
1647 struct kernel_param const *var_param_set_battery_capacity_16_p1 ;
1648 int tmp ;
1649 int tmp___0 ;
1650 int tmp___1 ;
1651
1652 {
1653 {
1654#line 678
1655 LDV_IN_INTERRUPT = 1;
1656#line 687
1657 ldv_initialize();
1658#line 693
1659 tmp = test_power_init();
1660 }
1661#line 693
1662 if (tmp != 0) {
1663#line 694
1664 goto ldv_final;
1665 } else {
1666
1667 }
1668#line 718
1669 goto ldv_14761;
1670 ldv_14760:
1671 {
1672#line 721
1673 tmp___0 = __VERIFIER_nondet_int();
1674 }
1675#line 723
1676 if (tmp___0 == 0) {
1677#line 723
1678 goto case_0;
1679 } else
1680#line 750
1681 if (tmp___0 == 1) {
1682#line 750
1683 goto case_1;
1684 } else
1685#line 777
1686 if (tmp___0 == 2) {
1687#line 777
1688 goto case_2;
1689 } else
1690#line 804
1691 if (tmp___0 == 3) {
1692#line 804
1693 goto case_3;
1694 } else
1695#line 831
1696 if (tmp___0 == 4) {
1697#line 831
1698 goto case_4;
1699 } else
1700#line 858
1701 if (tmp___0 == 5) {
1702#line 858
1703 goto case_5;
1704 } else
1705#line 885
1706 if (tmp___0 == 6) {
1707#line 885
1708 goto case_6;
1709 } else
1710#line 912
1711 if (tmp___0 == 7) {
1712#line 912
1713 goto case_7;
1714 } else
1715#line 939
1716 if (tmp___0 == 8) {
1717#line 939
1718 goto case_8;
1719 } else
1720#line 966
1721 if (tmp___0 == 9) {
1722#line 966
1723 goto case_9;
1724 } else
1725#line 993
1726 if (tmp___0 == 10) {
1727#line 993
1728 goto case_10;
1729 } else {
1730 {
1731#line 1020
1732 goto switch_default;
1733#line 721
1734 if (0) {
1735 case_0:
1736 {
1737#line 733
1738 param_set_ac_online(var_param_set_ac_online_6_p0, var_param_set_ac_online_6_p1);
1739 }
1740#line 749
1741 goto ldv_14748;
1742 case_1:
1743 {
1744#line 760
1745 param_get_ac_online(var_param_get_ac_online_7_p0, var_param_get_ac_online_7_p1);
1746 }
1747#line 776
1748 goto ldv_14748;
1749 case_2:
1750 {
1751#line 787
1752 param_set_battery_status(var_param_set_battery_status_8_p0, var_param_set_battery_status_8_p1);
1753 }
1754#line 803
1755 goto ldv_14748;
1756 case_3:
1757 {
1758#line 814
1759 param_get_battery_status(var_param_get_battery_status_9_p0, var_param_get_battery_status_9_p1);
1760 }
1761#line 830
1762 goto ldv_14748;
1763 case_4:
1764 {
1765#line 841
1766 param_set_battery_present(var_param_set_battery_present_12_p0, var_param_set_battery_present_12_p1);
1767 }
1768#line 857
1769 goto ldv_14748;
1770 case_5:
1771 {
1772#line 868
1773 param_get_battery_present(var_param_get_battery_present_13_p0, var_param_get_battery_present_13_p1);
1774 }
1775#line 884
1776 goto ldv_14748;
1777 case_6:
1778 {
1779#line 895
1780 param_set_battery_technology(var_param_set_battery_technology_14_p0, var_param_set_battery_technology_14_p1);
1781 }
1782#line 911
1783 goto ldv_14748;
1784 case_7:
1785 {
1786#line 922
1787 param_get_battery_technology(var_param_get_battery_technology_15_p0, var_param_get_battery_technology_15_p1);
1788 }
1789#line 938
1790 goto ldv_14748;
1791 case_8:
1792 {
1793#line 949
1794 param_set_battery_health(var_param_set_battery_health_10_p0, var_param_set_battery_health_10_p1);
1795 }
1796#line 965
1797 goto ldv_14748;
1798 case_9:
1799 {
1800#line 976
1801 param_get_battery_health(var_param_get_battery_health_11_p0, var_param_get_battery_health_11_p1);
1802 }
1803#line 992
1804 goto ldv_14748;
1805 case_10:
1806 {
1807#line 1003
1808 param_set_battery_capacity(var_param_set_battery_capacity_16_p0, var_param_set_battery_capacity_16_p1);
1809 }
1810#line 1019
1811 goto ldv_14748;
1812 switch_default: ;
1813#line 1020
1814 goto ldv_14748;
1815 } else {
1816 switch_break: ;
1817 }
1818 }
1819 }
1820 ldv_14748: ;
1821 ldv_14761:
1822 {
1823#line 718
1824 tmp___1 = __VERIFIER_nondet_int();
1825 }
1826#line 718
1827 if (tmp___1 != 0) {
1828#line 719
1829 goto ldv_14760;
1830 } else {
1831#line 721
1832 goto ldv_14762;
1833 }
1834 ldv_14762: ;
1835 {
1836#line 1032
1837 test_power_exit();
1838 }
1839 ldv_final:
1840 {
1841#line 1045
1842 ldv_check_final_state();
1843 }
1844#line 1048
1845 return;
1846}
1847}
1848#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
1849void ldv_blast_assert(void)
1850{
1851
1852 {
1853 ERROR: ;
1854#line 6
1855 goto ERROR;
1856}
1857}
1858#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
1859extern int __VERIFIER_nondet_int(void) ;
1860#line 1069 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1861int ldv_spin = 0;
1862#line 1073 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1863void ldv_check_alloc_flags(gfp_t flags )
1864{
1865
1866 {
1867#line 1076
1868 if (ldv_spin != 0) {
1869#line 1076
1870 if (flags != 32U) {
1871 {
1872#line 1076
1873 ldv_blast_assert();
1874 }
1875 } else {
1876
1877 }
1878 } else {
1879
1880 }
1881#line 1079
1882 return;
1883}
1884}
1885#line 1079
1886extern struct page *ldv_some_page(void) ;
1887#line 1082 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1888struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
1889{ struct page *tmp ;
1890
1891 {
1892#line 1085
1893 if (ldv_spin != 0) {
1894#line 1085
1895 if (flags != 32U) {
1896 {
1897#line 1085
1898 ldv_blast_assert();
1899 }
1900 } else {
1901
1902 }
1903 } else {
1904
1905 }
1906 {
1907#line 1087
1908 tmp = ldv_some_page();
1909 }
1910#line 1087
1911 return (tmp);
1912}
1913}
1914#line 1091 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1915void ldv_check_alloc_nonatomic(void)
1916{
1917
1918 {
1919#line 1094
1920 if (ldv_spin != 0) {
1921 {
1922#line 1094
1923 ldv_blast_assert();
1924 }
1925 } else {
1926
1927 }
1928#line 1097
1929 return;
1930}
1931}
1932#line 1098 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1933void ldv_spin_lock(void)
1934{
1935
1936 {
1937#line 1101
1938 ldv_spin = 1;
1939#line 1102
1940 return;
1941}
1942}
1943#line 1105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1944void ldv_spin_unlock(void)
1945{
1946
1947 {
1948#line 1108
1949 ldv_spin = 0;
1950#line 1109
1951 return;
1952}
1953}
1954#line 1112 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1955int ldv_spin_trylock(void)
1956{ int is_lock ;
1957
1958 {
1959 {
1960#line 1117
1961 is_lock = __VERIFIER_nondet_int();
1962 }
1963#line 1119
1964 if (is_lock != 0) {
1965#line 1122
1966 return (0);
1967 } else {
1968#line 1127
1969 ldv_spin = 1;
1970#line 1129
1971 return (1);
1972 }
1973}
1974}
1975#line 1296 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/4728/dscv_tempdir/dscv/ri/43_1a/drivers/power/test_power.c.p"
1976void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
1977{
1978
1979 {
1980 {
1981#line 1302
1982 ldv_check_alloc_flags(ldv_func_arg2);
1983#line 1304
1984 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1985 }
1986#line 1305
1987 return ((void *)0);
1988}
1989}