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