source: CIVL/examples/svcomp17/linux-stable-af3071a-1-130_7a-drivers--hwmon--s3c-hwmon.ko-entry_point_false-unreach-call.cil.out.c@ 02876df

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since 02876df was 6cc72ad, checked in by Manchun Zheng <zmanchun@…>, 11 years ago

added tests for SVCOMP 2017 experiments.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@2874 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 36.7 KB
Line 
1extern void __VERIFIER_error() __attribute__ ((__noreturn__));
2/* Generated by CIL v. 1.5.1 */
3/* print_CIL_Input is false */
4
5typedef unsigned char __u8;
6typedef unsigned short __u16;
7typedef unsigned int __u32;
8typedef unsigned long long __u64;
9typedef unsigned char u8;
10typedef unsigned short u16;
11typedef unsigned int u32;
12typedef long long s64;
13typedef unsigned long long u64;
14typedef unsigned short __kernel_mode_t;
15typedef unsigned int __kernel_size_t;
16typedef int __kernel_ssize_t;
17typedef long __kernel_time_t;
18typedef int __kernel_clockid_t;
19typedef long long __kernel_loff_t;
20typedef __u32 __kernel_dev_t;
21typedef __kernel_dev_t dev_t;
22typedef __kernel_mode_t mode_t;
23typedef __kernel_clockid_t clockid_t;
24typedef _Bool bool;
25typedef __kernel_loff_t loff_t;
26typedef __kernel_size_t size_t;
27typedef __kernel_ssize_t ssize_t;
28typedef unsigned int gfp_t;
29typedef u32 phys_addr_t;
30typedef phys_addr_t resource_size_t;
31struct __anonstruct_atomic_t_6 {
32 int counter ;
33};
34typedef struct __anonstruct_atomic_t_6 atomic_t;
35struct list_head {
36 struct list_head *next ;
37 struct list_head *prev ;
38};
39struct thread_info;
40struct task_struct;
41struct module;
42struct completion;
43struct resource {
44 resource_size_t start ;
45 resource_size_t end ;
46 char const *name ;
47 unsigned long flags ;
48 struct resource *parent ;
49 struct resource *sibling ;
50 struct resource *child ;
51};
52struct device;
53struct lockdep_map;
54typedef atomic_t atomic_long_t;
55struct stack_trace {
56 unsigned int nr_entries ;
57 unsigned int max_entries ;
58 unsigned long *entries ;
59 int skip ;
60};
61struct lockdep_subclass_key {
62 char __one_byte ;
63};
64struct lock_class_key {
65 struct lockdep_subclass_key subkeys[8U] ;
66};
67struct lock_class {
68 struct list_head hash_entry ;
69 struct list_head lock_entry ;
70 struct lockdep_subclass_key *key ;
71 unsigned int subclass ;
72 unsigned int dep_gen_id ;
73 unsigned long usage_mask ;
74 struct stack_trace usage_traces[13U] ;
75 struct list_head locks_after ;
76 struct list_head locks_before ;
77 unsigned int version ;
78 unsigned long ops ;
79 char const *name ;
80 int name_version ;
81 unsigned long contention_point[4U] ;
82 unsigned long contending_point[4U] ;
83};
84struct lockdep_map {
85 struct lock_class_key *key ;
86 struct lock_class *class_cache[2U] ;
87 char const *name ;
88 int cpu ;
89 unsigned long ip ;
90};
91struct sock;
92struct kobject;
93enum kobj_ns_type {
94 KOBJ_NS_TYPE_NONE = 0,
95 KOBJ_NS_TYPE_NET = 1,
96 KOBJ_NS_TYPES = 2
97} ;
98struct kobj_ns_type_operations {
99 enum kobj_ns_type type ;
100 void const *(*current_ns)(void) ;
101 void const *(*netlink_ns)(struct sock * ) ;
102 void const *(*initial_ns)(void) ;
103};
104struct attribute {
105 char const *name ;
106 mode_t mode ;
107 struct lock_class_key *key ;
108 struct lock_class_key skey ;
109};
110struct attribute_group {
111 char const *name ;
112 mode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
113 struct attribute **attrs ;
114};
115struct file;
116struct vm_area_struct;
117struct bin_attribute {
118 struct attribute attr ;
119 size_t size ;
120 void *private ;
121 ssize_t (*read)(struct file * , struct kobject * , struct bin_attribute * , char * ,
122 loff_t , size_t ) ;
123 ssize_t (*write)(struct file * , struct kobject * , struct bin_attribute * , char * ,
124 loff_t , size_t ) ;
125 int (*mmap)(struct file * , struct kobject * , struct bin_attribute * , struct vm_area_struct * ) ;
126};
127struct sysfs_ops {
128 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
129 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
130};
131struct sysfs_dirent;
132struct timespec;
133struct __anonstruct_futex_9 {
134 u32 *uaddr ;
135 u32 val ;
136 u32 flags ;
137 u32 bitset ;
138 u64 time ;
139 u32 *uaddr2 ;
140};
141struct __anonstruct_nanosleep_10 {
142 clockid_t index ;
143 struct timespec *rmtp ;
144 u64 expires ;
145};
146struct pollfd;
147struct __anonstruct_poll_11 {
148 struct pollfd *ufds ;
149 int nfds ;
150 int has_timeout ;
151 unsigned long tv_sec ;
152 unsigned long tv_nsec ;
153};
154union __anonunion_ldv_2945_8 {
155 struct __anonstruct_futex_9 futex ;
156 struct __anonstruct_nanosleep_10 nanosleep ;
157 struct __anonstruct_poll_11 poll ;
158};
159struct restart_block {
160 long (*fn)(struct restart_block * ) ;
161 union __anonunion_ldv_2945_8 ldv_2945 ;
162};
163struct vfp_hard_struct {
164 __u64 fpregs[16U] ;
165 __u32 fpexc ;
166 __u32 fpscr ;
167 __u32 fpinst ;
168 __u32 fpinst2 ;
169};
170union vfp_state {
171 struct vfp_hard_struct hard ;
172};
173struct fp_hard_struct {
174 unsigned int save[35U] ;
175};
176struct fp_soft_struct {
177 unsigned int save[35U] ;
178};
179union fp_state {
180 struct fp_hard_struct hard ;
181 struct fp_soft_struct soft ;
182};
183struct crunch_state {
184 unsigned int mvdx[16U][2U] ;
185 unsigned int mvax[4U][3U] ;
186 unsigned int dspsc[2U] ;
187};
188struct exec_domain;
189typedef unsigned long mm_segment_t;
190struct cpu_context_save {
191 __u32 r4 ;
192 __u32 r5 ;
193 __u32 r6 ;
194 __u32 r7 ;
195 __u32 r8 ;
196 __u32 r9 ;
197 __u32 sl ;
198 __u32 fp ;
199 __u32 sp ;
200 __u32 pc ;
201 __u32 extra[2U] ;
202};
203struct thread_info {
204 unsigned long flags ;
205 int preempt_count ;
206 mm_segment_t addr_limit ;
207 struct task_struct *task ;
208 struct exec_domain *exec_domain ;
209 __u32 cpu ;
210 __u32 cpu_domain ;
211 struct cpu_context_save cpu_context ;
212 __u32 syscall ;
213 __u8 used_cp[16U] ;
214 unsigned long tp_value ;
215 struct crunch_state crunchstate ;
216 union fp_state fpstate ;
217 union vfp_state vfpstate ;
218 struct restart_block restart_block ;
219};
220struct __anonstruct_arch_spinlock_t_12 {
221 unsigned int volatile slock ;
222};
223typedef struct __anonstruct_arch_spinlock_t_12 arch_spinlock_t;
224struct raw_spinlock {
225 arch_spinlock_t raw_lock ;
226 unsigned int magic ;
227 unsigned int owner_cpu ;
228 void *owner ;
229 struct lockdep_map dep_map ;
230};
231struct __anonstruct_ldv_3083_15 {
232 u8 __padding[1U] ;
233 struct lockdep_map dep_map ;
234};
235union __anonunion_ldv_3084_14 {
236 struct raw_spinlock rlock ;
237 struct __anonstruct_ldv_3083_15 ldv_3083 ;
238};
239struct spinlock {
240 union __anonunion_ldv_3084_14 ldv_3084 ;
241};
242typedef struct spinlock spinlock_t;
243struct kref {
244 atomic_t refcount ;
245};
246struct __wait_queue_head {
247 spinlock_t lock ;
248 struct list_head task_list ;
249};
250typedef struct __wait_queue_head wait_queue_head_t;
251struct kset;
252struct kobj_type;
253struct kobject {
254 char const *name ;
255 struct list_head entry ;
256 struct kobject *parent ;
257 struct kset *kset ;
258 struct kobj_type *ktype ;
259 struct sysfs_dirent *sd ;
260 struct kref kref ;
261 unsigned char state_initialized : 1 ;
262 unsigned char state_in_sysfs : 1 ;
263 unsigned char state_add_uevent_sent : 1 ;
264 unsigned char state_remove_uevent_sent : 1 ;
265 unsigned char uevent_suppress : 1 ;
266};
267struct kobj_type {
268 void (*release)(struct kobject * ) ;
269 struct sysfs_ops const *sysfs_ops ;
270 struct attribute **default_attrs ;
271 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject * ) ;
272 void const *(*namespace)(struct kobject * ) ;
273};
274struct kobj_uevent_env {
275 char *envp[32U] ;
276 int envp_idx ;
277 char buf[2048U] ;
278 int buflen ;
279};
280struct kset_uevent_ops {
281 int (* const filter)(struct kset * , struct kobject * ) ;
282 char const *(* const name)(struct kset * , struct kobject * ) ;
283 int (* const uevent)(struct kset * , struct kobject * , struct kobj_uevent_env * ) ;
284};
285struct kset {
286 struct list_head list ;
287 spinlock_t list_lock ;
288 struct kobject kobj ;
289 struct kset_uevent_ops const *uevent_ops ;
290};
291struct klist_node;
292struct klist_node {
293 void *n_klist ;
294 struct list_head n_node ;
295 struct kref n_ref ;
296};
297struct timespec {
298 __kernel_time_t tv_sec ;
299 long tv_nsec ;
300};
301typedef void (*ctor_fn_t)(void);
302struct mutex {
303 atomic_t count ;
304 spinlock_t wait_lock ;
305 struct list_head wait_list ;
306 struct thread_info *owner ;
307 char const *name ;
308 void *magic ;
309 struct lockdep_map dep_map ;
310};
311union ktime {
312 s64 tv64 ;
313};
314typedef union ktime ktime_t;
315struct tvec_base;
316struct timer_list {
317 struct list_head entry ;
318 unsigned long expires ;
319 struct tvec_base *base ;
320 void (*function)(unsigned long ) ;
321 unsigned long data ;
322 int slack ;
323 int start_pid ;
324 void *start_site ;
325 char start_comm[16U] ;
326 struct lockdep_map lockdep_map ;
327};
328struct work_struct;
329struct work_struct {
330 atomic_long_t data ;
331 struct list_head entry ;
332 void (*func)(struct work_struct * ) ;
333 struct lockdep_map lockdep_map ;
334};
335typedef __u32 Elf32_Addr;
336typedef __u16 Elf32_Half;
337typedef __u32 Elf32_Word;
338struct elf32_sym {
339 Elf32_Word st_name ;
340 Elf32_Addr st_value ;
341 Elf32_Word st_size ;
342 unsigned char st_info ;
343 unsigned char st_other ;
344 Elf32_Half st_shndx ;
345};
346typedef struct elf32_sym Elf32_Sym;
347struct kernel_param;
348struct kernel_param_ops {
349 int (*set)(char const * , struct kernel_param const * ) ;
350 int (*get)(char * , struct kernel_param const * ) ;
351 void (*free)(void * ) ;
352};
353struct kparam_string;
354struct kparam_array;
355union __anonunion_ldv_6605_22 {
356 void *arg ;
357 struct kparam_string const *str ;
358 struct kparam_array const *arr ;
359};
360struct kernel_param {
361 char const *name ;
362 struct kernel_param_ops const *ops ;
363 u16 perm ;
364 u16 flags ;
365 union __anonunion_ldv_6605_22 ldv_6605 ;
366};
367struct kparam_string {
368 unsigned int maxlen ;
369 char *string ;
370};
371struct kparam_array {
372 unsigned int max ;
373 unsigned int *num ;
374 struct kernel_param_ops const *ops ;
375 unsigned int elemsize ;
376 void *elem ;
377};
378struct completion {
379 unsigned int done ;
380 wait_queue_head_t wait ;
381};
382struct tracepoint;
383struct tracepoint_func {
384 void *func ;
385 void *data ;
386};
387struct tracepoint {
388 char const *name ;
389 int state ;
390 void (*regfunc)(void) ;
391 void (*unregfunc)(void) ;
392 struct tracepoint_func *funcs ;
393};
394struct unwind_table;
395struct mod_arch_specific {
396 struct unwind_table *unwind[5U] ;
397};
398struct kernel_symbol {
399 unsigned long value ;
400 char const *name ;
401};
402struct module_attribute {
403 struct attribute attr ;
404 ssize_t (*show)(struct module_attribute * , struct module * , char * ) ;
405 ssize_t (*store)(struct module_attribute * , struct module * , char const * ,
406 size_t ) ;
407 void (*setup)(struct module * , char const * ) ;
408 int (*test)(struct module * ) ;
409 void (*free)(struct module * ) ;
410};
411struct module_param_attrs;
412struct module_kobject {
413 struct kobject kobj ;
414 struct module *mod ;
415 struct kobject *drivers_dir ;
416 struct module_param_attrs *mp ;
417};
418struct exception_table_entry;
419enum module_state {
420 MODULE_STATE_LIVE = 0,
421 MODULE_STATE_COMING = 1,
422 MODULE_STATE_GOING = 2
423} ;
424struct module_ref {
425 unsigned int incs ;
426 unsigned int decs ;
427};
428struct module_sect_attrs;
429struct module_notes_attrs;
430struct ftrace_event_call;
431struct module {
432 enum module_state state ;
433 struct list_head list ;
434 char name[60U] ;
435 struct module_kobject mkobj ;
436 struct module_attribute *modinfo_attrs ;
437 char const *version ;
438 char const *srcversion ;
439 struct kobject *holders_dir ;
440 struct kernel_symbol const *syms ;
441 unsigned long const *crcs ;
442 unsigned int num_syms ;
443 struct kernel_param *kp ;
444 unsigned int num_kp ;
445 unsigned int num_gpl_syms ;
446 struct kernel_symbol const *gpl_syms ;
447 unsigned long const *gpl_crcs ;
448 struct kernel_symbol const *unused_syms ;
449 unsigned long const *unused_crcs ;
450 unsigned int num_unused_syms ;
451 unsigned int num_unused_gpl_syms ;
452 struct kernel_symbol const *unused_gpl_syms ;
453 unsigned long const *unused_gpl_crcs ;
454 struct kernel_symbol const *gpl_future_syms ;
455 unsigned long const *gpl_future_crcs ;
456 unsigned int num_gpl_future_syms ;
457 unsigned int num_exentries ;
458 struct exception_table_entry *extable ;
459 int (*init)(void) ;
460 void *module_init ;
461 void *module_core ;
462 unsigned int init_size ;
463 unsigned int core_size ;
464 unsigned int init_text_size ;
465 unsigned int core_text_size ;
466 unsigned int init_ro_size ;
467 unsigned int core_ro_size ;
468 struct mod_arch_specific arch ;
469 unsigned int taints ;
470 Elf32_Sym *symtab ;
471 Elf32_Sym *core_symtab ;
472 unsigned int num_symtab ;
473 unsigned int core_num_syms ;
474 char *strtab ;
475 char *core_strtab ;
476 struct module_sect_attrs *sect_attrs ;
477 struct module_notes_attrs *notes_attrs ;
478 char *args ;
479 struct tracepoint * const *tracepoints_ptrs ;
480 unsigned int num_tracepoints ;
481 char const **trace_bprintk_fmt_start ;
482 unsigned int num_trace_bprintk_fmt ;
483 struct ftrace_event_call **trace_events ;
484 unsigned int num_trace_events ;
485 struct list_head source_list ;
486 struct list_head target_list ;
487 struct task_struct *waiter ;
488 void (*exit)(void) ;
489 struct module_ref *refptr ;
490 ctor_fn_t (**ctors)(void) ;
491 unsigned int num_ctors ;
492};
493struct pm_message {
494 int event ;
495};
496typedef struct pm_message pm_message_t;
497struct dev_pm_ops {
498 int (*prepare)(struct device * ) ;
499 void (*complete)(struct device * ) ;
500 int (*suspend)(struct device * ) ;
501 int (*resume)(struct device * ) ;
502 int (*freeze)(struct device * ) ;
503 int (*thaw)(struct device * ) ;
504 int (*poweroff)(struct device * ) ;
505 int (*restore)(struct device * ) ;
506 int (*suspend_noirq)(struct device * ) ;
507 int (*resume_noirq)(struct device * ) ;
508 int (*freeze_noirq)(struct device * ) ;
509 int (*thaw_noirq)(struct device * ) ;
510 int (*poweroff_noirq)(struct device * ) ;
511 int (*restore_noirq)(struct device * ) ;
512 int (*runtime_suspend)(struct device * ) ;
513 int (*runtime_resume)(struct device * ) ;
514 int (*runtime_idle)(struct device * ) ;
515};
516enum rpm_status {
517 RPM_ACTIVE = 0,
518 RPM_RESUMING = 1,
519 RPM_SUSPENDED = 2,
520 RPM_SUSPENDING = 3
521} ;
522enum rpm_request {
523 RPM_REQ_NONE = 0,
524 RPM_REQ_IDLE = 1,
525 RPM_REQ_SUSPEND = 2,
526 RPM_REQ_AUTOSUSPEND = 3,
527 RPM_REQ_RESUME = 4
528} ;
529struct wakeup_source;
530struct dev_pm_info {
531 pm_message_t power_state ;
532 unsigned char can_wakeup : 1 ;
533 unsigned char async_suspend : 1 ;
534 unsigned char in_suspend : 1 ;
535 spinlock_t lock ;
536 struct list_head entry ;
537 struct completion completion ;
538 struct wakeup_source *wakeup ;
539 struct timer_list suspend_timer ;
540 unsigned long timer_expires ;
541 struct work_struct work ;
542 wait_queue_head_t wait_queue ;
543 atomic_t usage_count ;
544 atomic_t child_count ;
545 unsigned char disable_depth : 3 ;
546 unsigned char ignore_children : 1 ;
547 unsigned char idle_notification : 1 ;
548 unsigned char request_pending : 1 ;
549 unsigned char deferred_resume : 1 ;
550 unsigned char run_wake : 1 ;
551 unsigned char runtime_auto : 1 ;
552 unsigned char no_callbacks : 1 ;
553 unsigned char irq_safe : 1 ;
554 unsigned char use_autosuspend : 1 ;
555 unsigned char timer_autosuspends : 1 ;
556 enum rpm_request request ;
557 enum rpm_status runtime_status ;
558 int runtime_error ;
559 int autosuspend_delay ;
560 unsigned long last_busy ;
561 unsigned long active_jiffies ;
562 unsigned long suspended_jiffies ;
563 unsigned long accounting_timestamp ;
564};
565struct dev_power_domain {
566 struct dev_pm_ops ops ;
567};
568struct dev_archdata {
569
570};
571struct pdev_archdata {
572
573};
574struct device_private;
575struct device_driver;
576struct driver_private;
577struct class;
578struct subsys_private;
579struct bus_type;
580struct device_node;
581struct bus_attribute {
582 struct attribute attr ;
583 ssize_t (*show)(struct bus_type * , char * ) ;
584 ssize_t (*store)(struct bus_type * , char const * , size_t ) ;
585};
586struct device_attribute;
587struct driver_attribute;
588struct bus_type {
589 char const *name ;
590 struct bus_attribute *bus_attrs ;
591 struct device_attribute *dev_attrs ;
592 struct driver_attribute *drv_attrs ;
593 int (*match)(struct device * , struct device_driver * ) ;
594 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
595 int (*probe)(struct device * ) ;
596 int (*remove)(struct device * ) ;
597 void (*shutdown)(struct device * ) ;
598 int (*suspend)(struct device * , pm_message_t ) ;
599 int (*resume)(struct device * ) ;
600 struct dev_pm_ops const *pm ;
601 struct subsys_private *p ;
602};
603struct of_device_id;
604struct device_driver {
605 char const *name ;
606 struct bus_type *bus ;
607 struct module *owner ;
608 char const *mod_name ;
609 bool suppress_bind_attrs ;
610 struct of_device_id const *of_match_table ;
611 int (*probe)(struct device * ) ;
612 int (*remove)(struct device * ) ;
613 void (*shutdown)(struct device * ) ;
614 int (*suspend)(struct device * , pm_message_t ) ;
615 int (*resume)(struct device * ) ;
616 struct attribute_group const **groups ;
617 struct dev_pm_ops const *pm ;
618 struct driver_private *p ;
619};
620struct driver_attribute {
621 struct attribute attr ;
622 ssize_t (*show)(struct device_driver * , char * ) ;
623 ssize_t (*store)(struct device_driver * , char const * , size_t ) ;
624};
625struct class_attribute;
626struct class {
627 char const *name ;
628 struct module *owner ;
629 struct class_attribute *class_attrs ;
630 struct device_attribute *dev_attrs ;
631 struct bin_attribute *dev_bin_attrs ;
632 struct kobject *dev_kobj ;
633 int (*dev_uevent)(struct device * , struct kobj_uevent_env * ) ;
634 char *(*devnode)(struct device * , mode_t * ) ;
635 void (*class_release)(struct class * ) ;
636 void (*dev_release)(struct device * ) ;
637 int (*suspend)(struct device * , pm_message_t ) ;
638 int (*resume)(struct device * ) ;
639 struct kobj_ns_type_operations const *ns_type ;
640 void const *(*namespace)(struct device * ) ;
641 struct dev_pm_ops const *pm ;
642 struct subsys_private *p ;
643};
644struct device_type;
645struct class_attribute {
646 struct attribute attr ;
647 ssize_t (*show)(struct class * , struct class_attribute * , char * ) ;
648 ssize_t (*store)(struct class * , struct class_attribute * , char const * , size_t ) ;
649};
650struct device_type {
651 char const *name ;
652 struct attribute_group const **groups ;
653 int (*uevent)(struct device * , struct kobj_uevent_env * ) ;
654 char *(*devnode)(struct device * , mode_t * ) ;
655 void (*release)(struct device * ) ;
656 struct dev_pm_ops const *pm ;
657};
658struct device_attribute {
659 struct attribute attr ;
660 ssize_t (*show)(struct device * , struct device_attribute * , char * ) ;
661 ssize_t (*store)(struct device * , struct device_attribute * , char const * ,
662 size_t ) ;
663};
664struct device_dma_parameters {
665 unsigned int max_segment_size ;
666 unsigned long segment_boundary_mask ;
667};
668struct dma_coherent_mem;
669struct device {
670 struct device *parent ;
671 struct device_private *p ;
672 struct kobject kobj ;
673 char const *init_name ;
674 struct device_type *type ;
675 struct mutex mutex ;
676 struct bus_type *bus ;
677 struct device_driver *driver ;
678 void *platform_data ;
679 struct dev_pm_info power ;
680 struct dev_power_domain *pwr_domain ;
681 u64 *dma_mask ;
682 u64 coherent_dma_mask ;
683 struct device_dma_parameters *dma_parms ;
684 struct list_head dma_pools ;
685 struct dma_coherent_mem *dma_mem ;
686 struct dev_archdata archdata ;
687 struct device_node *of_node ;
688 dev_t devt ;
689 spinlock_t devres_lock ;
690 struct list_head devres_head ;
691 struct klist_node knode_class ;
692 struct class *class ;
693 struct attribute_group const **groups ;
694 void (*release)(struct device * ) ;
695};
696struct wakeup_source {
697 char *name ;
698 struct list_head entry ;
699 spinlock_t lock ;
700 struct timer_list timer ;
701 unsigned long timer_expires ;
702 ktime_t total_time ;
703 ktime_t max_time ;
704 ktime_t last_time ;
705 unsigned long event_count ;
706 unsigned long active_count ;
707 unsigned long relax_count ;
708 unsigned long hit_count ;
709 unsigned char active : 1 ;
710};
711struct platform_device;
712typedef unsigned long kernel_ulong_t;
713struct of_device_id {
714 char name[32U] ;
715 char type[32U] ;
716 char compatible[128U] ;
717 void *data ;
718};
719struct platform_device_id {
720 char name[20U] ;
721 kernel_ulong_t driver_data ;
722};
723struct mfd_cell;
724struct platform_device {
725 char const *name ;
726 int id ;
727 struct device dev ;
728 u32 num_resources ;
729 struct resource *resource ;
730 struct platform_device_id const *id_entry ;
731 struct mfd_cell *mfd_cell ;
732 struct pdev_archdata archdata ;
733};
734struct platform_driver {
735 int (*probe)(struct platform_device * ) ;
736 int (*remove)(struct platform_device * ) ;
737 void (*shutdown)(struct platform_device * ) ;
738 int (*suspend)(struct platform_device * , pm_message_t ) ;
739 int (*resume)(struct platform_device * ) ;
740 struct device_driver driver ;
741 struct platform_device_id const *id_table ;
742};
743struct sensor_device_attribute {
744 struct device_attribute dev_attr ;
745 int index ;
746};
747struct s3c_adc_client;
748struct s3c_hwmon_chcfg {
749 char const *name ;
750 unsigned int mult ;
751 unsigned int div ;
752};
753struct s3c_hwmon_pdata {
754 struct s3c_hwmon_chcfg *in[8U] ;
755};
756struct s3c_hwmon_attr {
757 struct sensor_device_attribute in ;
758 struct sensor_device_attribute label ;
759 char in_name[12U] ;
760 char label_name[12U] ;
761};
762struct s3c_hwmon {
763 struct mutex lock ;
764 struct s3c_adc_client *client ;
765 struct device *hwmon_dev ;
766 struct s3c_hwmon_attr attrs[8U] ;
767};
768long ldv__builtin_expect(long exp , long c ) ;
769long ldv_is_err(void const *ptr ) ;
770long ldv_ptr_err(void const *ptr ) ;
771extern int snprintf(char * , size_t , char const * , ...) ;
772void *ldv_malloc(size_t size ) ;
773void *ldv_zalloc(size_t size ) ;
774extern void __mutex_init(struct mutex * , char const * , struct lock_class_key * ) ;
775extern int mutex_lock_interruptible_nested(struct mutex * , unsigned int ) ;
776extern void mutex_unlock(struct mutex * ) ;
777extern struct module __this_module ;
778int ldv_device_create_file_7(struct device *ldv_func_arg1 , struct device_attribute const *ldv_func_arg2 ) ;
779int ldv_device_create_file_8(struct device *ldv_func_arg1 , struct device_attribute const *ldv_func_arg2 ) ;
780extern void device_remove_file(struct device * , struct device_attribute const * ) ;
781extern void *dev_get_drvdata(struct device const * ) ;
782extern void dev_set_drvdata(struct device * , void * ) ;
783extern int dev_printk(char const * , struct device const * , char const * , ...) ;
784extern int dev_err(struct device const * , char const * , ...) ;
785extern int dev_warn(struct device const * , char const * , ...) ;
786int ldv_device_create_file_dev_attr_of_sensor_device_attribute(void) ;
787extern void kfree(void const * ) ;
788__inline static void *ldv_kzalloc_9(size_t size , gfp_t flags ) ;
789extern void *malloc(size_t size ) ;
790extern void *calloc(size_t nmemb , size_t size ) ;
791extern int __VERIFIER_nondet_int(void) ;
792extern unsigned long __VERIFIER_nondet_ulong(void) ;
793extern void *__VERIFIER_nondet_pointer(void) ;
794extern void __VERIFIER_assume(int expression ) ;
795void *ldv_malloc(size_t size )
796{
797 void *p ;
798 void *tmp ;
799 int tmp___0 ;
800
801 {
802 tmp___0 = __VERIFIER_nondet_int();
803 if (tmp___0 != 0) {
804 return (0);
805 } else {
806 tmp = malloc(size);
807 p = tmp;
808 __VERIFIER_assume((unsigned long )p != (unsigned long )((void *)0));
809 return (p);
810 }
811}
812}
813void *ldv_zalloc(size_t size )
814{
815 void *p ;
816 void *tmp ;
817 int tmp___0 ;
818
819 {
820 tmp___0 = __VERIFIER_nondet_int();
821 if (tmp___0 != 0) {
822 return (0);
823 } else {
824 tmp = calloc(1U, size);
825 p = tmp;
826 __VERIFIER_assume((unsigned long )p != (unsigned long )((void *)0));
827 return (p);
828 }
829}
830}
831int ldv_undef_int(void)
832{
833 int tmp ;
834
835 {
836 tmp = __VERIFIER_nondet_int();
837 return (tmp);
838}
839}
840void *ldv_undef_ptr(void)
841{
842 void *tmp ;
843
844 {
845 tmp = __VERIFIER_nondet_pointer();
846 return (tmp);
847}
848}
849unsigned long ldv_undef_ulong(void)
850{
851 unsigned long tmp ;
852
853 {
854 tmp = __VERIFIER_nondet_ulong();
855 return (tmp);
856}
857}
858__inline static void ldv_error(void)
859{
860
861
862 {
863 ERROR: ;
864 __VERIFIER_error();
865}
866}
867__inline static void ldv_stop(void)
868{
869
870
871 {
872 LDV_STOP: ;
873 goto LDV_STOP;
874}
875}
876long ldv__builtin_expect(long exp , long c )
877{
878
879
880 {
881 return (exp);
882}
883}
884void ldv__builtin_trap(void)
885{
886
887
888 {
889 ldv_error();
890 return;
891}
892}
893int ldv_state_variable_1 ;
894struct platform_device *s3c_hwmon_driver_group0 ;
895int LDV_IN_INTERRUPT = 1;
896int ref_cnt ;
897int ldv_state_variable_0 ;
898void ldv_initialize_platform_driver_1(void) ;
899__inline static long PTR_ERR(void const *ptr ) ;
900__inline static long IS_ERR(void const *ptr ) ;
901extern int platform_driver_register(struct platform_driver * ) ;
902extern void platform_driver_unregister(struct platform_driver * ) ;
903__inline static void *platform_get_drvdata(struct platform_device const *pdev )
904{
905 void *tmp ;
906
907 {
908 tmp = dev_get_drvdata(& pdev->dev);
909 return (tmp);
910}
911}
912__inline static void platform_set_drvdata(struct platform_device *pdev , void *data )
913{
914
915
916 {
917 dev_set_drvdata(& pdev->dev, data);
918 return;
919}
920}
921extern struct device *hwmon_device_register(struct device * ) ;
922extern void hwmon_device_unregister(struct device * ) ;
923extern int s3c_adc_read(struct s3c_adc_client * , unsigned int ) ;
924extern struct s3c_adc_client *s3c_adc_register(struct platform_device * , void (*)(struct s3c_adc_client * ,
925 unsigned int ) ,
926 void (*)(struct s3c_adc_client * ,
927 unsigned int , unsigned int ,
928 unsigned int * ) , unsigned int ) ;
929extern void s3c_adc_release(struct s3c_adc_client * ) ;
930static int s3c_hwmon_read_ch(struct device *dev , struct s3c_hwmon *hwmon , int channel )
931{
932 int ret ;
933
934 {
935 ret = mutex_lock_interruptible_nested(& hwmon->lock, 0U);
936 if (ret < 0) {
937 return (ret);
938 } else {
939
940 }
941 dev_printk("<7>", (struct device const *)dev, "reading channel %d\n", channel);
942 ret = s3c_adc_read(hwmon->client, (unsigned int )channel);
943 mutex_unlock(& hwmon->lock);
944 return (ret);
945}
946}
947__inline static int s3c_hwmon_add_raw(struct device *dev )
948{
949
950
951 {
952 return (0);
953}
954}
955__inline static void s3c_hwmon_remove_raw(struct device *dev )
956{
957
958
959 {
960 return;
961}
962}
963static ssize_t s3c_hwmon_ch_show(struct device *dev , struct device_attribute *attr ,
964 char *buf )
965{
966 struct sensor_device_attribute *sen_attr ;
967 struct device_attribute const *__mptr ;
968 struct s3c_hwmon *hwmon ;
969 struct device const *__mptr___0 ;
970 void *tmp ;
971 struct s3c_hwmon_pdata *pdata ;
972 struct s3c_hwmon_chcfg *cfg ;
973 int ret ;
974 unsigned int __divisor ;
975 int tmp___0 ;
976
977 {
978 __mptr = (struct device_attribute const *)attr;
979 sen_attr = (struct sensor_device_attribute *)__mptr;
980 __mptr___0 = (struct device const *)dev;
981 tmp = platform_get_drvdata((struct platform_device const *)((struct platform_device *)__mptr___0 + 0xfffffffffffffff8UL));
982 hwmon = (struct s3c_hwmon *)tmp;
983 pdata = (struct s3c_hwmon_pdata *)dev->platform_data;
984 cfg = pdata->in[sen_attr->index];
985 ret = s3c_hwmon_read_ch(dev, hwmon, sen_attr->index);
986 if (ret < 0) {
987 return (ret);
988 } else {
989
990 }
991 ret = (int )(cfg->mult * (unsigned int )ret);
992 __divisor = cfg->div;
993 ret = (int )((__divisor / 2U + (unsigned int )ret) / __divisor);
994 tmp___0 = snprintf(buf, 4096U, "%d\n", ret);
995 return (tmp___0);
996}
997}
998static ssize_t s3c_hwmon_label_show(struct device *dev , struct device_attribute *attr ,
999 char *buf )
1000{
1001 struct sensor_device_attribute *sen_attr ;
1002 struct device_attribute const *__mptr ;
1003 struct s3c_hwmon_pdata *pdata ;
1004 struct s3c_hwmon_chcfg *cfg ;
1005 int tmp ;
1006
1007 {
1008 __mptr = (struct device_attribute const *)attr;
1009 sen_attr = (struct sensor_device_attribute *)__mptr;
1010 pdata = (struct s3c_hwmon_pdata *)dev->platform_data;
1011 cfg = pdata->in[sen_attr->index];
1012 tmp = snprintf(buf, 4096U, "%s\n", cfg->name);
1013 return (tmp);
1014}
1015}
1016static int s3c_hwmon_create_attr(struct device *dev , struct s3c_hwmon_chcfg *cfg ,
1017 struct s3c_hwmon_attr *attrs , int channel )
1018{
1019 struct sensor_device_attribute *attr ;
1020 int ret ;
1021
1022 {
1023 snprintf((char *)(& attrs->in_name), 12U, "in%d_input", channel);
1024 attr = & attrs->in;
1025 attr->index = channel;
1026 attr->dev_attr.attr.name = (char const *)(& attrs->in_name);
1027 attr->dev_attr.attr.mode = 292U;
1028 attr->dev_attr.show = & s3c_hwmon_ch_show;
1029 ret = ldv_device_create_file_7(dev, (struct device_attribute const *)(& attr->dev_attr));
1030 if (ret < 0) {
1031 dev_err((struct device const *)dev, "failed to create input attribute\n");
1032 return (ret);
1033 } else {
1034
1035 }
1036 if ((unsigned long )cfg->name != (unsigned long )((char const *)0)) {
1037 snprintf((char *)(& attrs->label_name), 12U, "in%d_label", channel);
1038 attr = & attrs->label;
1039 attr->index = channel;
1040 attr->dev_attr.attr.name = (char const *)(& attrs->label_name);
1041 attr->dev_attr.attr.mode = 292U;
1042 attr->dev_attr.show = & s3c_hwmon_label_show;
1043 ret = ldv_device_create_file_8(dev, (struct device_attribute const *)(& attr->dev_attr));
1044 if (ret < 0) {
1045 device_remove_file(dev, (struct device_attribute const *)(& attrs->in.dev_attr));
1046 dev_err((struct device const *)dev, "failed to create label attribute\n");
1047 } else {
1048
1049 }
1050 } else {
1051
1052 }
1053 return (ret);
1054}
1055}
1056static void s3c_hwmon_remove_attr(struct device *dev , struct s3c_hwmon_attr *attrs )
1057{
1058
1059
1060 {
1061 device_remove_file(dev, (struct device_attribute const *)(& attrs->in.dev_attr));
1062 device_remove_file(dev, (struct device_attribute const *)(& attrs->label.dev_attr));
1063 return;
1064}
1065}
1066static int s3c_hwmon_probe(struct platform_device *dev )
1067{
1068 struct s3c_hwmon_pdata *pdata ;
1069 struct s3c_hwmon *hwmon ;
1070 int ret ;
1071 int i ;
1072 void *tmp ;
1073 struct lock_class_key __key ;
1074 long tmp___0 ;
1075 long tmp___1 ;
1076 long tmp___2 ;
1077 long tmp___3 ;
1078 struct s3c_hwmon_chcfg *cfg ;
1079
1080 {
1081 pdata = (struct s3c_hwmon_pdata *)dev->dev.platform_data;
1082 ret = 0;
1083 if ((unsigned long )pdata == (unsigned long )((struct s3c_hwmon_pdata *)0)) {
1084 dev_err((struct device const *)(& dev->dev), "no platform data supplied\n");
1085 return (-22);
1086 } else {
1087
1088 }
1089 tmp = ldv_kzalloc_9(800U, 208U);
1090 hwmon = (struct s3c_hwmon *)tmp;
1091 if ((unsigned long )hwmon == (unsigned long )((struct s3c_hwmon *)0)) {
1092 dev_err((struct device const *)(& dev->dev), "no memory\n");
1093 return (-12);
1094 } else {
1095
1096 }
1097 platform_set_drvdata(dev, (void *)hwmon);
1098 __mutex_init(& hwmon->lock, "&hwmon->lock", & __key);
1099 hwmon->client = s3c_adc_register(dev, 0, 0, 0U);
1100 tmp___1 = IS_ERR((void const *)hwmon->client);
1101 if (tmp___1 != 0L) {
1102 dev_err((struct device const *)(& dev->dev), "cannot register adc\n");
1103 tmp___0 = PTR_ERR((void const *)hwmon->client);
1104 ret = (int )tmp___0;
1105 goto err_mem;
1106 } else {
1107
1108 }
1109 ret = s3c_hwmon_add_raw(& dev->dev);
1110 if (ret != 0) {
1111 goto err_registered;
1112 } else {
1113
1114 }
1115 hwmon->hwmon_dev = hwmon_device_register(& dev->dev);
1116 tmp___3 = IS_ERR((void const *)hwmon->hwmon_dev);
1117 if (tmp___3 != 0L) {
1118 dev_err((struct device const *)(& dev->dev), "error registering with hwmon\n");
1119 tmp___2 = PTR_ERR((void const *)hwmon->hwmon_dev);
1120 ret = (int )tmp___2;
1121 goto err_raw_attribute;
1122 } else {
1123
1124 }
1125 i = 0;
1126 goto ldv_10018;
1127 ldv_10017:
1128 cfg = pdata->in[i];
1129 if ((unsigned long )cfg == (unsigned long )((struct s3c_hwmon_chcfg *)0)) {
1130 goto ldv_10012;
1131 } else {
1132
1133 }
1134 if (cfg->mult > 65535U) {
1135 dev_warn((struct device const *)(& dev->dev), "channel %d multiplier too large\n",
1136 i);
1137 } else {
1138
1139 }
1140 if (cfg->div == 0U) {
1141 dev_err((struct device const *)(& dev->dev), "channel %d divider zero\n", i);
1142 goto ldv_10012;
1143 } else {
1144
1145 }
1146 ret = s3c_hwmon_create_attr(& dev->dev, pdata->in[i], (struct s3c_hwmon_attr *)(& hwmon->attrs) + (unsigned int )i,
1147 i);
1148 if (ret != 0) {
1149 dev_err((struct device const *)(& dev->dev), "error creating channel %d\n",
1150 i);
1151 i = i - 1;
1152 goto ldv_10014;
1153 ldv_10013:
1154 s3c_hwmon_remove_attr(& dev->dev, (struct s3c_hwmon_attr *)(& hwmon->attrs) + (unsigned int )i);
1155 i = i - 1;
1156 ldv_10014: ;
1157 if (i >= 0) {
1158 goto ldv_10013;
1159 } else {
1160
1161 }
1162
1163 goto err_hwmon_register;
1164 } else {
1165
1166 }
1167 ldv_10012:
1168 i = i + 1;
1169 ldv_10018: ;
1170 if ((unsigned int )i <= 7U) {
1171 goto ldv_10017;
1172 } else {
1173
1174 }
1175
1176 return (0);
1177 err_hwmon_register:
1178 hwmon_device_unregister(hwmon->hwmon_dev);
1179 err_raw_attribute:
1180 s3c_hwmon_remove_raw(& dev->dev);
1181 err_registered:
1182 s3c_adc_release(hwmon->client);
1183 err_mem:
1184 kfree((void const *)hwmon);
1185 return (ret);
1186}
1187}
1188static int s3c_hwmon_remove(struct platform_device *dev )
1189{
1190 struct s3c_hwmon *hwmon ;
1191 void *tmp ;
1192 int i ;
1193
1194 {
1195 tmp = platform_get_drvdata((struct platform_device const *)dev);
1196 hwmon = (struct s3c_hwmon *)tmp;
1197 s3c_hwmon_remove_raw(& dev->dev);
1198 i = 0;
1199 goto ldv_10028;
1200 ldv_10027:
1201 s3c_hwmon_remove_attr(& dev->dev, (struct s3c_hwmon_attr *)(& hwmon->attrs) + (unsigned int )i);
1202 i = i + 1;
1203 ldv_10028: ;
1204 if ((unsigned int )i <= 7U) {
1205 goto ldv_10027;
1206 } else {
1207
1208 }
1209 hwmon_device_unregister(hwmon->hwmon_dev);
1210 s3c_adc_release(hwmon->client);
1211 return (0);
1212}
1213}
1214static struct platform_driver s3c_hwmon_driver = {& s3c_hwmon_probe, & s3c_hwmon_remove, 0, 0, 0, {"s3c-hwmon", 0, & __this_module,
1215 0, (_Bool)0, 0, 0, 0, 0, 0, 0,
1216 0, 0, 0}, 0};
1217static int s3c_hwmon_init(void)
1218{
1219 int tmp ;
1220
1221 {
1222 tmp = platform_driver_register(& s3c_hwmon_driver);
1223 return (tmp);
1224}
1225}
1226static void s3c_hwmon_exit(void)
1227{
1228
1229
1230 {
1231 platform_driver_unregister(& s3c_hwmon_driver);
1232 return;
1233}
1234}
1235int ldv_retval_0 ;
1236int ldv_retval_1 ;
1237void ldv_initialize(void) ;
1238extern void ldv_check_final_state(void) ;
1239void ldv_initialize_platform_driver_1(void)
1240{
1241 void *tmp ;
1242
1243 {
1244 tmp = ldv_zalloc(624U);
1245 s3c_hwmon_driver_group0 = (struct platform_device *)tmp;
1246 return;
1247}
1248}
1249int main(void)
1250{
1251 int tmp ;
1252 int tmp___0 ;
1253 int tmp___1 ;
1254
1255 {
1256 ldv_initialize();
1257 ldv_state_variable_1 = 0;
1258 ref_cnt = 0;
1259 ldv_state_variable_0 = 1;
1260 ldv_10082:
1261 tmp = __VERIFIER_nondet_int();
1262 switch (tmp) {
1263 case 0: ;
1264 if (ldv_state_variable_1 != 0) {
1265 tmp___0 = __VERIFIER_nondet_int();
1266 switch (tmp___0) {
1267 case 0: ;
1268 if (ldv_state_variable_1 == 1) {
1269 ldv_retval_0 = s3c_hwmon_probe(s3c_hwmon_driver_group0);
1270 if (ldv_retval_0 == 0) {
1271 ldv_state_variable_1 = 2;
1272 ref_cnt = ref_cnt + 1;
1273 } else {
1274
1275 }
1276 } else {
1277
1278 }
1279 goto ldv_10071;
1280 case 1: ;
1281 if (ldv_state_variable_1 == 2) {
1282 s3c_hwmon_remove(s3c_hwmon_driver_group0);
1283 ldv_state_variable_1 = 1;
1284 ref_cnt = ref_cnt - 1;
1285 } else {
1286
1287 }
1288 goto ldv_10071;
1289 default:
1290 ldv_stop();
1291 }
1292 ldv_10071: ;
1293 } else {
1294
1295 }
1296 goto ldv_10074;
1297 case 1: ;
1298 if (ldv_state_variable_0 != 0) {
1299 tmp___1 = __VERIFIER_nondet_int();
1300 switch (tmp___1) {
1301 case 0: ;
1302 if (ldv_state_variable_0 == 3 && ref_cnt == 0) {
1303 s3c_hwmon_exit();
1304 ldv_state_variable_0 = 2;
1305 goto ldv_final;
1306 } else {
1307
1308 }
1309 goto ldv_10078;
1310 case 1: ;
1311 if (ldv_state_variable_0 == 1) {
1312 ldv_retval_1 = s3c_hwmon_init();
1313 if (ldv_retval_1 == 0) {
1314 ldv_state_variable_0 = 3;
1315 ldv_state_variable_1 = 1;
1316 ldv_initialize_platform_driver_1();
1317 } else {
1318
1319 }
1320 if (ldv_retval_1 != 0) {
1321 ldv_state_variable_0 = 2;
1322 goto ldv_final;
1323 } else {
1324
1325 }
1326 } else {
1327
1328 }
1329 goto ldv_10078;
1330 default:
1331 ldv_stop();
1332 }
1333 ldv_10078: ;
1334 } else {
1335
1336 }
1337 goto ldv_10074;
1338 default:
1339 ldv_stop();
1340 }
1341 ldv_10074: ;
1342 goto ldv_10082;
1343 ldv_final:
1344 ldv_check_final_state();
1345 return 0;
1346}
1347}
1348__inline static long PTR_ERR(void const *ptr )
1349{
1350 long tmp ;
1351
1352 {
1353 tmp = ldv_ptr_err(ptr);
1354 return (tmp);
1355}
1356}
1357__inline static long IS_ERR(void const *ptr )
1358{
1359 long tmp ;
1360
1361 {
1362 tmp = ldv_is_err(ptr);
1363 return (tmp);
1364}
1365}
1366int ldv_device_create_file_7(struct device *ldv_func_arg1 , struct device_attribute const *ldv_func_arg2 )
1367{
1368 int tmp ;
1369
1370 {
1371 tmp = ldv_device_create_file_dev_attr_of_sensor_device_attribute();
1372 return (tmp);
1373}
1374}
1375int ldv_device_create_file_8(struct device *ldv_func_arg1 , struct device_attribute const *ldv_func_arg2 )
1376{
1377 int tmp ;
1378
1379 {
1380 tmp = ldv_device_create_file_dev_attr_of_sensor_device_attribute();
1381 return (tmp);
1382}
1383}
1384__inline static void *ldv_kzalloc_9(size_t size , gfp_t flags )
1385{
1386 void *tmp ;
1387
1388 {
1389 tmp = ldv_zalloc(size);
1390 return (tmp);
1391}
1392}
1393long ldv_is_err(void const *ptr )
1394{
1395
1396
1397 {
1398 return ((unsigned long )ptr > 2012UL);
1399}
1400}
1401void *ldv_err_ptr(long error )
1402{
1403
1404
1405 {
1406 return ((void *)(2012L - error));
1407}
1408}
1409long ldv_ptr_err(void const *ptr )
1410{
1411
1412
1413 {
1414 return ((long )(2012UL - (unsigned long )ptr));
1415}
1416}
1417long ldv_is_err_or_null(void const *ptr )
1418{
1419 long tmp ;
1420 int tmp___0 ;
1421
1422 {
1423 if (! ptr) {
1424 tmp___0 = 1;
1425 } else {
1426 tmp = ldv_is_err((unsigned long )ptr);
1427 if (tmp) {
1428 tmp___0 = 1;
1429 } else {
1430 tmp___0 = 0;
1431 }
1432 }
1433 return (tmp___0);
1434}
1435}
1436int ldv_count_1 = 0;
1437int ldv_count_2 = 0;
1438void ldv_sysfs(void)
1439{
1440
1441
1442 {
1443 ldv_count_1 = ldv_count_1 + 1;
1444 return;
1445}
1446}
1447int ldv_call_dev_attr_of_sensor_device_attribute = 0;
1448int ldv_device_create_file_dev_attr_of_sensor_device_attribute(void)
1449{
1450 int tmp ;
1451
1452 {
1453 if (ldv_call_dev_attr_of_sensor_device_attribute == 0) {
1454 ldv_count_2 = ldv_count_2 + 1;
1455 ldv_call_dev_attr_of_sensor_device_attribute = 1;
1456 if (ldv_count_1 >= ldv_count_2) {
1457
1458 } else {
1459 ldv_error();
1460 }
1461 } else {
1462
1463 }
1464 tmp = ldv_undef_int();
1465 return (tmp);
1466}
1467}
1468void ldv_initialize(void)
1469{
1470
1471
1472 {
1473 return;
1474}
1475}
Note: See TracBrowser for help on using the repository browser.