1
2
3
4#line 23 "include/asm-generic/int-ll64.h"
5typedef unsigned short __u16;
6#line 26 "include/asm-generic/int-ll64.h"
7typedef unsigned int __u32;
8#line 30 "include/asm-generic/int-ll64.h"
9typedef unsigned long long __u64;
10#line 43 "include/asm-generic/int-ll64.h"
11typedef unsigned char u8;
12#line 45 "include/asm-generic/int-ll64.h"
13typedef short s16;
14#line 46 "include/asm-generic/int-ll64.h"
15typedef unsigned short u16;
16#line 49 "include/asm-generic/int-ll64.h"
17typedef unsigned int u32;
18#line 14 "include/asm-generic/posix_types.h"
19typedef long __kernel_long_t;
20#line 15 "include/asm-generic/posix_types.h"
21typedef unsigned long __kernel_ulong_t;
22#line 75 "include/asm-generic/posix_types.h"
23typedef __kernel_ulong_t __kernel_size_t;
24#line 76 "include/asm-generic/posix_types.h"
25typedef __kernel_long_t __kernel_ssize_t;
26#line 27 "include/linux/types.h"
27typedef unsigned short umode_t;
28#line 63 "include/linux/types.h"
29typedef __kernel_size_t size_t;
30#line 68 "include/linux/types.h"
31typedef __kernel_ssize_t ssize_t;
32#line 202 "include/linux/types.h"
33typedef unsigned int gfp_t;
34#line 221 "include/linux/types.h"
35struct __anonstruct_atomic_t_6 {
36 int counter ;
37};
38#line 221 "include/linux/types.h"
39typedef struct __anonstruct_atomic_t_6 atomic_t;
40#line 226 "include/linux/types.h"
41struct __anonstruct_atomic64_t_7 {
42 long counter ;
43};
44#line 226 "include/linux/types.h"
45typedef struct __anonstruct_atomic64_t_7 atomic64_t;
46#line 227 "include/linux/types.h"
47struct list_head {
48 struct list_head *next ;
49 struct list_head *prev ;
50};
51#line 55 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/alternative.h"
52struct module;
53#line 55
54struct module;
55#line 146 "include/linux/init.h"
56typedef void (*ctor_fn_t)(void);
57#line 305 "include/linux/printk.h"
58struct _ddebug {
59 char const *modname ;
60 char const *function ;
61 char const *filename ;
62 char const *format ;
63 unsigned int lineno : 18 ;
64 unsigned char flags ;
65};
66#line 57 "include/linux/dynamic_debug.h"
67struct completion;
68#line 57
69struct completion;
70#line 58 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/page_types.h"
71struct page;
72#line 58
73struct page;
74#line 26 "include/asm-generic/getorder.h"
75struct task_struct;
76#line 26
77struct task_struct;
78#line 339 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/pgtable_types.h"
79struct cpumask;
80#line 339
81struct cpumask;
82#line 327 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
83struct arch_spinlock;
84#line 327
85struct arch_spinlock;
86#line 306 "include/linux/bitmap.h"
87struct bug_entry {
88 int bug_addr_disp ;
89 int file_disp ;
90 unsigned short line ;
91 unsigned short flags ;
92};
93#line 89 "include/linux/bug.h"
94struct cpumask {
95 unsigned long bits[64U] ;
96};
97#line 637 "include/linux/cpumask.h"
98typedef struct cpumask *cpumask_var_t;
99#line 234 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt.h"
100struct static_key;
101#line 234
102struct static_key;
103#line 433 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
104struct kmem_cache;
105#line 23 "include/asm-generic/atomic-long.h"
106typedef atomic64_t atomic_long_t;
107#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
108typedef u16 __ticket_t;
109#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
110typedef u32 __ticketpair_t;
111#line 16 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
112struct __raw_tickets {
113 __ticket_t head ;
114 __ticket_t tail ;
115};
116#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
117union __anonunion_ldv_5907_29 {
118 __ticketpair_t head_tail ;
119 struct __raw_tickets tickets ;
120};
121#line 26 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
122struct arch_spinlock {
123 union __anonunion_ldv_5907_29 ldv_5907 ;
124};
125#line 27 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
126typedef struct arch_spinlock arch_spinlock_t;
127#line 34 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/rwlock.h"
128struct lockdep_map;
129#line 34
130struct lockdep_map;
131#line 55 "include/linux/debug_locks.h"
132struct stack_trace {
133 unsigned int nr_entries ;
134 unsigned int max_entries ;
135 unsigned long *entries ;
136 int skip ;
137};
138#line 26 "include/linux/stacktrace.h"
139struct lockdep_subclass_key {
140 char __one_byte ;
141};
142#line 53 "include/linux/lockdep.h"
143struct lock_class_key {
144 struct lockdep_subclass_key subkeys[8U] ;
145};
146#line 59 "include/linux/lockdep.h"
147struct lock_class {
148 struct list_head hash_entry ;
149 struct list_head lock_entry ;
150 struct lockdep_subclass_key *key ;
151 unsigned int subclass ;
152 unsigned int dep_gen_id ;
153 unsigned long usage_mask ;
154 struct stack_trace usage_traces[13U] ;
155 struct list_head locks_after ;
156 struct list_head locks_before ;
157 unsigned int version ;
158 unsigned long ops ;
159 char const *name ;
160 int name_version ;
161 unsigned long contention_point[4U] ;
162 unsigned long contending_point[4U] ;
163};
164#line 144 "include/linux/lockdep.h"
165struct lockdep_map {
166 struct lock_class_key *key ;
167 struct lock_class *class_cache[2U] ;
168 char const *name ;
169 int cpu ;
170 unsigned long ip ;
171};
172#line 556 "include/linux/lockdep.h"
173struct raw_spinlock {
174 arch_spinlock_t raw_lock ;
175 unsigned int magic ;
176 unsigned int owner_cpu ;
177 void *owner ;
178 struct lockdep_map dep_map ;
179};
180#line 33 "include/linux/spinlock_types.h"
181struct __anonstruct_ldv_6122_33 {
182 u8 __padding[24U] ;
183 struct lockdep_map dep_map ;
184};
185#line 33 "include/linux/spinlock_types.h"
186union __anonunion_ldv_6123_32 {
187 struct raw_spinlock rlock ;
188 struct __anonstruct_ldv_6122_33 ldv_6122 ;
189};
190#line 33 "include/linux/spinlock_types.h"
191struct spinlock {
192 union __anonunion_ldv_6123_32 ldv_6123 ;
193};
194#line 76 "include/linux/spinlock_types.h"
195typedef struct spinlock spinlock_t;
196#line 48 "include/linux/wait.h"
197struct __wait_queue_head {
198 spinlock_t lock ;
199 struct list_head task_list ;
200};
201#line 53 "include/linux/wait.h"
202typedef struct __wait_queue_head wait_queue_head_t;
203#line 128 "include/linux/rwsem.h"
204struct completion {
205 unsigned int done ;
206 wait_queue_head_t wait ;
207};
208#line 302 "include/linux/timer.h"
209struct work_struct;
210#line 302
211struct work_struct;
212#line 45 "include/linux/workqueue.h"
213struct work_struct {
214 atomic_long_t data ;
215 struct list_head entry ;
216 void (*func)(struct work_struct * ) ;
217 struct lockdep_map lockdep_map ;
218};
219#line 18 "include/linux/elf.h"
220typedef __u64 Elf64_Addr;
221#line 19 "include/linux/elf.h"
222typedef __u16 Elf64_Half;
223#line 23 "include/linux/elf.h"
224typedef __u32 Elf64_Word;
225#line 24 "include/linux/elf.h"
226typedef __u64 Elf64_Xword;
227#line 193 "include/linux/elf.h"
228struct elf64_sym {
229 Elf64_Word st_name ;
230 unsigned char st_info ;
231 unsigned char st_other ;
232 Elf64_Half st_shndx ;
233 Elf64_Addr st_value ;
234 Elf64_Xword st_size ;
235};
236#line 201 "include/linux/elf.h"
237typedef struct elf64_sym Elf64_Sym;
238#line 445
239struct sock;
240#line 445
241struct sock;
242#line 446
243struct kobject;
244#line 446
245struct kobject;
246#line 447
247enum kobj_ns_type {
248 KOBJ_NS_TYPE_NONE = 0,
249 KOBJ_NS_TYPE_NET = 1,
250 KOBJ_NS_TYPES = 2
251} ;
252#line 453 "include/linux/elf.h"
253struct kobj_ns_type_operations {
254 enum kobj_ns_type type ;
255 void *(*grab_current_ns)(void) ;
256 void const *(*netlink_ns)(struct sock * ) ;
257 void const *(*initial_ns)(void) ;
258 void (*drop_ns)(void * ) ;
259};
260#line 57 "include/linux/kobject_ns.h"
261struct attribute {
262 char const *name ;
263 umode_t mode ;
264 struct lock_class_key *key ;
265 struct lock_class_key skey ;
266};
267#line 98 "include/linux/sysfs.h"
268struct sysfs_ops {
269 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
270 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
271 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
272};
273#line 117
274struct sysfs_dirent;
275#line 117
276struct sysfs_dirent;
277#line 182 "include/linux/sysfs.h"
278struct kref {
279 atomic_t refcount ;
280};
281#line 49 "include/linux/kobject.h"
282struct kset;
283#line 49
284struct kobj_type;
285#line 49 "include/linux/kobject.h"
286struct kobject {
287 char const *name ;
288 struct list_head entry ;
289 struct kobject *parent ;
290 struct kset *kset ;
291 struct kobj_type *ktype ;
292 struct sysfs_dirent *sd ;
293 struct kref kref ;
294 unsigned char state_initialized : 1 ;
295 unsigned char state_in_sysfs : 1 ;
296 unsigned char state_add_uevent_sent : 1 ;
297 unsigned char state_remove_uevent_sent : 1 ;
298 unsigned char uevent_suppress : 1 ;
299};
300#line 107 "include/linux/kobject.h"
301struct kobj_type {
302 void (*release)(struct kobject * ) ;
303 struct sysfs_ops const *sysfs_ops ;
304 struct attribute **default_attrs ;
305 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
306 void const *(*namespace)(struct kobject * ) ;
307};
308#line 115 "include/linux/kobject.h"
309struct kobj_uevent_env {
310 char *envp[32U] ;
311 int envp_idx ;
312 char buf[2048U] ;
313 int buflen ;
314};
315#line 122 "include/linux/kobject.h"
316struct kset_uevent_ops {
317 int (* const filter)(struct kset * , struct kobject * ) ;
318 char const *(* const name)(struct kset * , struct kobject * ) ;
319 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
320};
321#line 139 "include/linux/kobject.h"
322struct kset {
323 struct list_head list ;
324 spinlock_t list_lock ;
325 struct kobject kobj ;
326 struct kset_uevent_ops const *uevent_ops ;
327};
328#line 215
329struct kernel_param;
330#line 215
331struct kernel_param;
332#line 216 "include/linux/kobject.h"
333struct kernel_param_ops {
334 int (*set)(char const * , struct kernel_param const * ) ;
335 int (*get)(char * , struct kernel_param const * ) ;
336 void (*free)(void * ) ;
337};
338#line 49 "include/linux/moduleparam.h"
339struct kparam_string;
340#line 49
341struct kparam_array;
342#line 49 "include/linux/moduleparam.h"
343union __anonunion_ldv_13363_134 {
344 void *arg ;
345 struct kparam_string const *str ;
346 struct kparam_array const *arr ;
347};
348#line 49 "include/linux/moduleparam.h"
349struct kernel_param {
350 char const *name ;
351 struct kernel_param_ops const *ops ;
352 u16 perm ;
353 s16 level ;
354 union __anonunion_ldv_13363_134 ldv_13363 ;
355};
356#line 61 "include/linux/moduleparam.h"
357struct kparam_string {
358 unsigned int maxlen ;
359 char *string ;
360};
361#line 67 "include/linux/moduleparam.h"
362struct kparam_array {
363 unsigned int max ;
364 unsigned int elemsize ;
365 unsigned int *num ;
366 struct kernel_param_ops const *ops ;
367 void *elem ;
368};
369#line 458 "include/linux/moduleparam.h"
370struct static_key {
371 atomic_t enabled ;
372};
373#line 225 "include/linux/jump_label.h"
374struct tracepoint;
375#line 225
376struct tracepoint;
377#line 226 "include/linux/jump_label.h"
378struct tracepoint_func {
379 void *func ;
380 void *data ;
381};
382#line 29 "include/linux/tracepoint.h"
383struct tracepoint {
384 char const *name ;
385 struct static_key key ;
386 void (*regfunc)(void) ;
387 void (*unregfunc)(void) ;
388 struct tracepoint_func *funcs ;
389};
390#line 86 "include/linux/tracepoint.h"
391struct kernel_symbol {
392 unsigned long value ;
393 char const *name ;
394};
395#line 27 "include/linux/export.h"
396struct mod_arch_specific {
397
398};
399#line 34 "include/linux/module.h"
400struct module_param_attrs;
401#line 34 "include/linux/module.h"
402struct module_kobject {
403 struct kobject kobj ;
404 struct module *mod ;
405 struct kobject *drivers_dir ;
406 struct module_param_attrs *mp ;
407};
408#line 43 "include/linux/module.h"
409struct module_attribute {
410 struct attribute attr ;
411 ssize_t (*show)(struct module_attribute * , struct module_kobject * , char * ) ;
412 ssize_t (*store)(struct module_attribute * , struct module_kobject * , char const * ,
413 size_t ) ;
414 void (*setup)(struct module * , char const * ) ;
415 int (*test)(struct module * ) ;
416 void (*free)(struct module * ) ;
417};
418#line 69
419struct exception_table_entry;
420#line 69
421struct exception_table_entry;
422#line 198
423enum module_state {
424 MODULE_STATE_LIVE = 0,
425 MODULE_STATE_COMING = 1,
426 MODULE_STATE_GOING = 2
427} ;
428#line 204 "include/linux/module.h"
429struct module_ref {
430 unsigned long incs ;
431 unsigned long decs ;
432};
433#line 219
434struct module_sect_attrs;
435#line 219
436struct module_notes_attrs;
437#line 219
438struct ftrace_event_call;
439#line 219 "include/linux/module.h"
440struct module {
441 enum module_state state ;
442 struct list_head list ;
443 char name[56U] ;
444 struct module_kobject mkobj ;
445 struct module_attribute *modinfo_attrs ;
446 char const *version ;
447 char const *srcversion ;
448 struct kobject *holders_dir ;
449 struct kernel_symbol const *syms ;
450 unsigned long const *crcs ;
451 unsigned int num_syms ;
452 struct kernel_param *kp ;
453 unsigned int num_kp ;
454 unsigned int num_gpl_syms ;
455 struct kernel_symbol const *gpl_syms ;
456 unsigned long const *gpl_crcs ;
457 struct kernel_symbol const *unused_syms ;
458 unsigned long const *unused_crcs ;
459 unsigned int num_unused_syms ;
460 unsigned int num_unused_gpl_syms ;
461 struct kernel_symbol const *unused_gpl_syms ;
462 unsigned long const *unused_gpl_crcs ;
463 struct kernel_symbol const *gpl_future_syms ;
464 unsigned long const *gpl_future_crcs ;
465 unsigned int num_gpl_future_syms ;
466 unsigned int num_exentries ;
467 struct exception_table_entry *extable ;
468 int (*init)(void) ;
469 void *module_init ;
470 void *module_core ;
471 unsigned int init_size ;
472 unsigned int core_size ;
473 unsigned int init_text_size ;
474 unsigned int core_text_size ;
475 unsigned int init_ro_size ;
476 unsigned int core_ro_size ;
477 struct mod_arch_specific arch ;
478 unsigned int taints ;
479 unsigned int num_bugs ;
480 struct list_head bug_list ;
481 struct bug_entry *bug_table ;
482 Elf64_Sym *symtab ;
483 Elf64_Sym *core_symtab ;
484 unsigned int num_symtab ;
485 unsigned int core_num_syms ;
486 char *strtab ;
487 char *core_strtab ;
488 struct module_sect_attrs *sect_attrs ;
489 struct module_notes_attrs *notes_attrs ;
490 char *args ;
491 void *percpu ;
492 unsigned int percpu_size ;
493 unsigned int num_tracepoints ;
494 struct tracepoint * const *tracepoints_ptrs ;
495 unsigned int num_trace_bprintk_fmt ;
496 char const **trace_bprintk_fmt_start ;
497 struct ftrace_event_call **trace_events ;
498 unsigned int num_trace_events ;
499 struct list_head source_list ;
500 struct list_head target_list ;
501 struct task_struct *waiter ;
502 void (*exit)(void) ;
503 struct module_ref *refptr ;
504 ctor_fn_t (**ctors)(void) ;
505 unsigned int num_ctors ;
506};
507#line 88 "include/linux/kmemleak.h"
508struct kmem_cache_cpu {
509 void **freelist ;
510 unsigned long tid ;
511 struct page *page ;
512 struct page *partial ;
513 int node ;
514 unsigned int stat[26U] ;
515};
516#line 55 "include/linux/slub_def.h"
517struct kmem_cache_node {
518 spinlock_t list_lock ;
519 unsigned long nr_partial ;
520 struct list_head partial ;
521 atomic_long_t nr_slabs ;
522 atomic_long_t total_objects ;
523 struct list_head full ;
524};
525#line 66 "include/linux/slub_def.h"
526struct kmem_cache_order_objects {
527 unsigned long x ;
528};
529#line 76 "include/linux/slub_def.h"
530struct kmem_cache {
531 struct kmem_cache_cpu *cpu_slab ;
532 unsigned long flags ;
533 unsigned long min_partial ;
534 int size ;
535 int objsize ;
536 int offset ;
537 int cpu_partial ;
538 struct kmem_cache_order_objects oo ;
539 struct kmem_cache_order_objects max ;
540 struct kmem_cache_order_objects min ;
541 gfp_t allocflags ;
542 int refcount ;
543 void (*ctor)(void * ) ;
544 int inuse ;
545 int align ;
546 int reserved ;
547 char const *name ;
548 struct list_head list ;
549 struct kobject kobj ;
550 int remote_node_defrag_ratio ;
551 struct kmem_cache_node *node[1024U] ;
552};
553#line 38 "include/linux/cpufreq.h"
554struct cpufreq_governor;
555#line 38
556struct cpufreq_governor;
557#line 71 "include/linux/cpufreq.h"
558struct cpufreq_cpuinfo {
559 unsigned int max_freq ;
560 unsigned int min_freq ;
561 unsigned int transition_latency ;
562};
563#line 80 "include/linux/cpufreq.h"
564struct cpufreq_real_policy {
565 unsigned int min ;
566 unsigned int max ;
567 unsigned int policy ;
568 struct cpufreq_governor *governor ;
569};
570#line 87 "include/linux/cpufreq.h"
571struct cpufreq_policy {
572 cpumask_var_t cpus ;
573 cpumask_var_t related_cpus ;
574 unsigned int shared_type ;
575 unsigned int cpu ;
576 struct cpufreq_cpuinfo cpuinfo ;
577 unsigned int min ;
578 unsigned int max ;
579 unsigned int cur ;
580 unsigned int policy ;
581 struct cpufreq_governor *governor ;
582 struct work_struct update ;
583 struct cpufreq_real_policy user_policy ;
584 struct kobject kobj ;
585 struct completion kobj_unregister ;
586};
587#line 160 "include/linux/cpufreq.h"
588struct cpufreq_governor {
589 char name[16U] ;
590 int (*governor)(struct cpufreq_policy * , unsigned int ) ;
591 ssize_t (*show_setspeed)(struct cpufreq_policy * , char * ) ;
592 int (*store_setspeed)(struct cpufreq_policy * , unsigned int ) ;
593 unsigned int max_transition_latency ;
594 struct list_head governor_list ;
595 struct module *owner ;
596};
597#line 1 "<compiler builtins>"
598long __builtin_expect(long , long ) ;
599#line 2 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
600void ldv_spin_lock(void) ;
601#line 3
602void ldv_spin_unlock(void) ;
603#line 4
604int ldv_spin_trylock(void) ;
605#line 45 "include/linux/dynamic_debug.h"
606extern int __dynamic_pr_debug(struct _ddebug * , char const * , ...) ;
607#line 26 "include/linux/export.h"
608extern struct module __this_module ;
609#line 220 "include/linux/slub_def.h"
610extern void *kmem_cache_alloc(struct kmem_cache * , gfp_t ) ;
611#line 223
612void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 ) ;
613#line 11 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
614void ldv_check_alloc_flags(gfp_t flags ) ;
615#line 12
616void ldv_check_alloc_nonatomic(void) ;
617#line 14
618struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags ) ;
619#line 192 "include/linux/cpufreq.h"
620extern int __cpufreq_driver_target(struct cpufreq_policy * , unsigned int , unsigned int ) ;
621#line 200
622extern int cpufreq_register_governor(struct cpufreq_governor * ) ;
623#line 201
624extern void cpufreq_unregister_governor(struct cpufreq_governor * ) ;
625#line 33 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
626static int cpufreq_governor_powersave(struct cpufreq_policy *policy , unsigned int event )
627{ struct _ddebug descriptor ;
628 long tmp ;
629 struct _ddebug *__cil_tmp5 ;
630 unsigned long __cil_tmp6 ;
631 unsigned long __cil_tmp7 ;
632 unsigned long __cil_tmp8 ;
633 unsigned long __cil_tmp9 ;
634 unsigned long __cil_tmp10 ;
635 unsigned long __cil_tmp11 ;
636 unsigned char __cil_tmp12 ;
637 long __cil_tmp13 ;
638 long __cil_tmp14 ;
639 unsigned long __cil_tmp15 ;
640 unsigned long __cil_tmp16 ;
641 unsigned int __cil_tmp17 ;
642 unsigned long __cil_tmp18 ;
643 unsigned long __cil_tmp19 ;
644 unsigned int __cil_tmp20 ;
645
646 {
647#line 37
648 if ((int )event == 1) {
649#line 37
650 goto case_1;
651 } else
652#line 38
653 if ((int )event == 3) {
654#line 38
655 goto case_3;
656 } else {
657 {
658#line 44
659 goto switch_default;
660#line 36
661 if (0) {
662 case_1: ;
663 case_3:
664 {
665#line 39
666 __cil_tmp5 = & descriptor;
667#line 39
668 *((char const **)__cil_tmp5) = "cpufreq_powersave";
669#line 39
670 __cil_tmp6 = (unsigned long )(& descriptor) + 8;
671#line 39
672 *((char const **)__cil_tmp6) = "cpufreq_governor_powersave";
673#line 39
674 __cil_tmp7 = (unsigned long )(& descriptor) + 16;
675#line 39
676 *((char const **)__cil_tmp7) = "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p";
677#line 39
678 __cil_tmp8 = (unsigned long )(& descriptor) + 24;
679#line 39
680 *((char const **)__cil_tmp8) = "setting to %u kHz because of event %u\n";
681#line 39
682 __cil_tmp9 = (unsigned long )(& descriptor) + 32;
683#line 39
684 *((unsigned int *)__cil_tmp9) = 40U;
685#line 39
686 __cil_tmp10 = (unsigned long )(& descriptor) + 35;
687#line 39
688 *((unsigned char *)__cil_tmp10) = (unsigned char)0;
689#line 39
690 __cil_tmp11 = (unsigned long )(& descriptor) + 35;
691#line 39
692 __cil_tmp12 = *((unsigned char *)__cil_tmp11);
693#line 39
694 __cil_tmp13 = (long )__cil_tmp12;
695#line 39
696 __cil_tmp14 = __cil_tmp13 & 1L;
697#line 39
698 tmp = __builtin_expect(__cil_tmp14, 0L);
699 }
700#line 39
701 if (tmp != 0L) {
702 {
703#line 39
704 __cil_tmp15 = (unsigned long )policy;
705#line 39
706 __cil_tmp16 = __cil_tmp15 + 36;
707#line 39
708 __cil_tmp17 = *((unsigned int *)__cil_tmp16);
709#line 39
710 __dynamic_pr_debug(& descriptor, "setting to %u kHz because of event %u\n",
711 __cil_tmp17, event);
712 }
713 } else {
714
715 }
716 {
717#line 41
718 __cil_tmp18 = (unsigned long )policy;
719#line 41
720 __cil_tmp19 = __cil_tmp18 + 36;
721#line 41
722 __cil_tmp20 = *((unsigned int *)__cil_tmp19);
723#line 41
724 __cpufreq_driver_target(policy, __cil_tmp20, 0U);
725 }
726#line 43
727 goto ldv_14335;
728 switch_default: ;
729#line 45
730 goto ldv_14335;
731 } else {
732 switch_break: ;
733 }
734 }
735 }
736 ldv_14335: ;
737#line 47
738 return (0);
739}
740}
741#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
742static struct cpufreq_governor cpufreq_gov_powersave = {{(char )'p', (char )'o', (char )'w', (char )'e', (char )'r', (char )'s', (char )'a',
743 (char )'v', (char )'e', (char )'\000', (char)0, (char)0, (char)0, (char)0, (char)0,
744 (char)0}, & cpufreq_governor_powersave, (ssize_t (*)(struct cpufreq_policy * ,
745 char * ))0, (int (*)(struct cpufreq_policy * ,
746 unsigned int ))0,
747 0U, {(struct list_head *)0, (struct list_head *)0}, & __this_module};
748#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
749static int cpufreq_gov_powersave_init(void)
750{ int tmp ;
751
752 {
753 {
754#line 61
755 tmp = cpufreq_register_governor(& cpufreq_gov_powersave);
756 }
757#line 61
758 return (tmp);
759}
760}
761#line 65 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
762static void cpufreq_gov_powersave_exit(void)
763{
764
765 {
766 {
767#line 67
768 cpufreq_unregister_governor(& cpufreq_gov_powersave);
769 }
770#line 68
771 return;
772}
773}
774#line 98
775extern void ldv_check_final_state(void) ;
776#line 104
777extern void ldv_initialize(void) ;
778#line 107
779extern int __VERIFIER_nondet_int(void) ;
780#line 110 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
781int LDV_IN_INTERRUPT ;
782#line 113 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
783void main(void)
784{ struct cpufreq_policy *var_group1 ;
785 unsigned int var_cpufreq_governor_powersave_0_p1 ;
786 int tmp ;
787 int tmp___0 ;
788 int tmp___1 ;
789
790 {
791 {
792#line 140
793 LDV_IN_INTERRUPT = 1;
794#line 149
795 ldv_initialize();
796#line 158
797 tmp = cpufreq_gov_powersave_init();
798 }
799#line 158
800 if (tmp != 0) {
801#line 159
802 goto ldv_final;
803 } else {
804
805 }
806#line 168
807 goto ldv_14376;
808 ldv_14375:
809 {
810#line 171
811 tmp___0 = __VERIFIER_nondet_int();
812 }
813#line 173
814 if (tmp___0 == 0) {
815#line 173
816 goto case_0;
817 } else {
818 {
819#line 196
820 goto switch_default;
821#line 171
822 if (0) {
823 case_0:
824 {
825#line 181
826 cpufreq_governor_powersave(var_group1, var_cpufreq_governor_powersave_0_p1);
827 }
828#line 195
829 goto ldv_14373;
830 switch_default: ;
831#line 196
832 goto ldv_14373;
833 } else {
834 switch_break: ;
835 }
836 }
837 }
838 ldv_14373: ;
839 ldv_14376:
840 {
841#line 168
842 tmp___1 = __VERIFIER_nondet_int();
843 }
844#line 168
845 if (tmp___1 != 0) {
846#line 169
847 goto ldv_14375;
848 } else {
849#line 171
850 goto ldv_14377;
851 }
852 ldv_14377: ;
853 {
854#line 211
855 cpufreq_gov_powersave_exit();
856 }
857 ldv_final:
858 {
859#line 219
860 ldv_check_final_state();
861 }
862#line 222
863 return;
864}
865}
866#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast-assert.h"
867void ldv_blast_assert(void)
868{
869
870 {
871 ERROR: ;
872#line 6
873 goto ERROR;
874}
875}
876#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/kernel-rules/files/engine-blast.h"
877extern int __VERIFIER_nondet_int(void) ;
878#line 243 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
879int ldv_spin = 0;
880#line 247 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
881void ldv_check_alloc_flags(gfp_t flags )
882{
883
884 {
885#line 250
886 if (ldv_spin != 0) {
887#line 250
888 if (flags != 32U) {
889 {
890#line 250
891 ldv_blast_assert();
892 }
893 } else {
894
895 }
896 } else {
897
898 }
899#line 253
900 return;
901}
902}
903#line 253
904extern struct page *ldv_some_page(void) ;
905#line 256 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
906struct page *ldv_check_alloc_flags_and_return_some_page(gfp_t flags )
907{ struct page *tmp ;
908
909 {
910#line 259
911 if (ldv_spin != 0) {
912#line 259
913 if (flags != 32U) {
914 {
915#line 259
916 ldv_blast_assert();
917 }
918 } else {
919
920 }
921 } else {
922
923 }
924 {
925#line 261
926 tmp = ldv_some_page();
927 }
928#line 261
929 return (tmp);
930}
931}
932#line 265 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
933void ldv_check_alloc_nonatomic(void)
934{
935
936 {
937#line 268
938 if (ldv_spin != 0) {
939 {
940#line 268
941 ldv_blast_assert();
942 }
943 } else {
944
945 }
946#line 271
947 return;
948}
949}
950#line 272 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
951void ldv_spin_lock(void)
952{
953
954 {
955#line 275
956 ldv_spin = 1;
957#line 276
958 return;
959}
960}
961#line 279 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
962void ldv_spin_unlock(void)
963{
964
965 {
966#line 282
967 ldv_spin = 0;
968#line 283
969 return;
970}
971}
972#line 286 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
973int ldv_spin_trylock(void)
974{ int is_lock ;
975
976 {
977 {
978#line 291
979 is_lock = __VERIFIER_nondet_int();
980 }
981#line 293
982 if (is_lock != 0) {
983#line 296
984 return (0);
985 } else {
986#line 301
987 ldv_spin = 1;
988#line 303
989 return (1);
990 }
991}
992}
993#line 470 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--43_1a--X--cpachecker/linux-3.4/csd_deg_dscv/11153/dscv_tempdir/dscv/ri/43_1a/drivers/cpufreq/cpufreq_powersave.c.p"
994void *ldv_kmem_cache_alloc_16(struct kmem_cache *ldv_func_arg1 , gfp_t ldv_func_arg2 )
995{
996
997 {
998 {
999#line 476
1000 ldv_check_alloc_flags(ldv_func_arg2);
1001#line 478
1002 kmem_cache_alloc(ldv_func_arg1, ldv_func_arg2);
1003 }
1004#line 479
1005 return ((void *)0);
1006}
1007}