1
2
3
4#line 45 "include/asm-generic/int-ll64.h"
5typedef short s16;
6#line 46 "include/asm-generic/int-ll64.h"
7typedef unsigned short u16;
8#line 49 "include/asm-generic/int-ll64.h"
9typedef unsigned int u32;
10#line 14 "include/asm-generic/posix_types.h"
11typedef long __kernel_long_t;
12#line 15 "include/asm-generic/posix_types.h"
13typedef unsigned long __kernel_ulong_t;
14#line 75 "include/asm-generic/posix_types.h"
15typedef __kernel_ulong_t __kernel_size_t;
16#line 76 "include/asm-generic/posix_types.h"
17typedef __kernel_long_t __kernel_ssize_t;
18#line 27 "include/linux/types.h"
19typedef unsigned short umode_t;
20#line 63 "include/linux/types.h"
21typedef __kernel_size_t size_t;
22#line 68 "include/linux/types.h"
23typedef __kernel_ssize_t ssize_t;
24#line 92 "include/linux/types.h"
25typedef unsigned char u_char;
26#line 219 "include/linux/types.h"
27struct __anonstruct_atomic_t_7 {
28 int counter ;
29};
30#line 219 "include/linux/types.h"
31typedef struct __anonstruct_atomic_t_7 atomic_t;
32#line 229 "include/linux/types.h"
33struct list_head {
34 struct list_head *next ;
35 struct list_head *prev ;
36};
37#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/thread_info.h"
38struct task_struct;
39#line 20
40struct task_struct;
41#line 7 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/processor.h"
42struct task_struct;
43#line 52 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/paravirt_types.h"
44struct task_struct;
45#line 329
46struct arch_spinlock;
47#line 329
48struct arch_spinlock;
49#line 139 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/ptrace.h"
50struct task_struct;
51#line 8 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/current.h"
52struct task_struct;
53#line 14 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
54typedef u16 __ticket_t;
55#line 15 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
56typedef u32 __ticketpair_t;
57#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
58struct __raw_tickets {
59 __ticket_t head ;
60 __ticket_t tail ;
61};
62#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
63union __anonunion____missing_field_name_36 {
64 __ticketpair_t head_tail ;
65 struct __raw_tickets tickets ;
66};
67#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
68struct arch_spinlock {
69 union __anonunion____missing_field_name_36 __annonCompField17 ;
70};
71#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/spinlock_types.h"
72typedef struct arch_spinlock arch_spinlock_t;
73#line 12 "include/linux/lockdep.h"
74struct task_struct;
75#line 20 "include/linux/spinlock_types.h"
76struct raw_spinlock {
77 arch_spinlock_t raw_lock ;
78 unsigned int magic ;
79 unsigned int owner_cpu ;
80 void *owner ;
81};
82#line 64 "include/linux/spinlock_types.h"
83union __anonunion____missing_field_name_39 {
84 struct raw_spinlock rlock ;
85};
86#line 64 "include/linux/spinlock_types.h"
87struct spinlock {
88 union __anonunion____missing_field_name_39 __annonCompField19 ;
89};
90#line 64 "include/linux/spinlock_types.h"
91typedef struct spinlock spinlock_t;
92#line 55 "include/linux/wait.h"
93struct task_struct;
94#line 48 "include/linux/mutex.h"
95struct mutex {
96 atomic_t count ;
97 spinlock_t wait_lock ;
98 struct list_head wait_list ;
99 struct task_struct *owner ;
100 char const *name ;
101 void *magic ;
102};
103#line 18 "include/linux/capability.h"
104struct task_struct;
105#line 413 "include/linux/fs.h"
106struct kobject;
107#line 413
108struct kobject;
109#line 270 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/elf.h"
110struct task_struct;
111#line 20 "include/linux/kobject_ns.h"
112struct sock;
113#line 20
114struct sock;
115#line 21
116struct kobject;
117#line 27
118enum kobj_ns_type {
119 KOBJ_NS_TYPE_NONE = 0,
120 KOBJ_NS_TYPE_NET = 1,
121 KOBJ_NS_TYPES = 2
122} ;
123#line 40 "include/linux/kobject_ns.h"
124struct kobj_ns_type_operations {
125 enum kobj_ns_type type ;
126 void *(*grab_current_ns)(void) ;
127 void const *(*netlink_ns)(struct sock *sk ) ;
128 void const *(*initial_ns)(void) ;
129 void (*drop_ns)(void * ) ;
130};
131#line 22 "include/linux/sysfs.h"
132struct kobject;
133#line 24
134enum kobj_ns_type;
135#line 26 "include/linux/sysfs.h"
136struct attribute {
137 char const *name ;
138 umode_t mode ;
139};
140#line 56 "include/linux/sysfs.h"
141struct attribute_group {
142 char const *name ;
143 umode_t (*is_visible)(struct kobject * , struct attribute * , int ) ;
144 struct attribute **attrs ;
145};
146#line 112 "include/linux/sysfs.h"
147struct sysfs_ops {
148 ssize_t (*show)(struct kobject * , struct attribute * , char * ) ;
149 ssize_t (*store)(struct kobject * , struct attribute * , char const * , size_t ) ;
150 void const *(*namespace)(struct kobject * , struct attribute const * ) ;
151};
152#line 118
153struct sysfs_dirent;
154#line 118
155struct sysfs_dirent;
156#line 22 "include/linux/kref.h"
157struct kref {
158 atomic_t refcount ;
159};
160#line 60 "include/linux/kobject.h"
161struct kset;
162#line 60
163struct kobj_type;
164#line 60 "include/linux/kobject.h"
165struct kobject {
166 char const *name ;
167 struct list_head entry ;
168 struct kobject *parent ;
169 struct kset *kset ;
170 struct kobj_type *ktype ;
171 struct sysfs_dirent *sd ;
172 struct kref kref ;
173 unsigned int state_initialized : 1 ;
174 unsigned int state_in_sysfs : 1 ;
175 unsigned int state_add_uevent_sent : 1 ;
176 unsigned int state_remove_uevent_sent : 1 ;
177 unsigned int uevent_suppress : 1 ;
178};
179#line 108 "include/linux/kobject.h"
180struct kobj_type {
181 void (*release)(struct kobject *kobj ) ;
182 struct sysfs_ops const *sysfs_ops ;
183 struct attribute **default_attrs ;
184 struct kobj_ns_type_operations const *(*child_ns_type)(struct kobject *kobj ) ;
185 void const *(*namespace)(struct kobject *kobj ) ;
186};
187#line 116 "include/linux/kobject.h"
188struct kobj_uevent_env {
189 char *envp[32] ;
190 int envp_idx ;
191 char buf[2048] ;
192 int buflen ;
193};
194#line 123 "include/linux/kobject.h"
195struct kset_uevent_ops {
196 int (* const filter)(struct kset *kset , struct kobject *kobj ) ;
197 char const *(* const name)(struct kset *kset , struct kobject *kobj ) ;
198 int (* const uevent)(struct kset *kset , struct kobject *kobj , struct kobj_uevent_env *env ) ;
199};
200#line 130 "include/linux/kobject.h"
201struct kobj_attribute {
202 struct attribute attr ;
203 ssize_t (*show)(struct kobject *kobj , struct kobj_attribute *attr , char *buf ) ;
204 ssize_t (*store)(struct kobject *kobj , struct kobj_attribute *attr , char const *buf ,
205 size_t count ) ;
206};
207#line 140
208struct sock;
209#line 159 "include/linux/kobject.h"
210struct kset {
211 struct list_head list ;
212 spinlock_t list_lock ;
213 struct kobject kobj ;
214 struct kset_uevent_ops const *uevent_ops ;
215};
216#line 39 "include/linux/moduleparam.h"
217struct kernel_param;
218#line 39
219struct kernel_param;
220#line 41 "include/linux/moduleparam.h"
221struct kernel_param_ops {
222 int (*set)(char const *val , struct kernel_param const *kp ) ;
223 int (*get)(char *buffer , struct kernel_param const *kp ) ;
224 void (*free)(void *arg ) ;
225};
226#line 50
227struct kparam_string;
228#line 50
229struct kparam_array;
230#line 50 "include/linux/moduleparam.h"
231union __anonunion____missing_field_name_216 {
232 void *arg ;
233 struct kparam_string const *str ;
234 struct kparam_array const *arr ;
235};
236#line 50 "include/linux/moduleparam.h"
237struct kernel_param {
238 char const *name ;
239 struct kernel_param_ops const *ops ;
240 u16 perm ;
241 s16 level ;
242 union __anonunion____missing_field_name_216 __annonCompField35 ;
243};
244#line 63 "include/linux/moduleparam.h"
245struct kparam_string {
246 unsigned int maxlen ;
247 char *string ;
248};
249#line 69 "include/linux/moduleparam.h"
250struct kparam_array {
251 unsigned int max ;
252 unsigned int elemsize ;
253 unsigned int *num ;
254 struct kernel_param_ops const *ops ;
255 void *elem ;
256};
257#line 8 "include/linux/debug_locks.h"
258struct task_struct;
259#line 48
260struct task_struct;
261#line 20 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
262enum var_type_t {
263 VAR_NUM = 0,
264 VAR_TIME = 1,
265 VAR_STRING = 2,
266 VAR_PROC = 3
267} ;
268#line 35
269enum var_id_t {
270 VERSION = 0,
271 SYNTH = 1,
272 SILENT = 2,
273 SYNTH_DIRECT = 3,
274 KEYMAP = 4,
275 CHARS = 5,
276 PUNC_SOME = 6,
277 PUNC_MOST = 7,
278 PUNC_ALL = 8,
279 DELIM = 9,
280 REPEATS = 10,
281 EXNUMBER = 11,
282 DELAY = 12,
283 TRIGGER = 13,
284 JIFFY = 14,
285 FULL = 15,
286 BLEEP_TIME = 16,
287 CURSOR_TIME = 17,
288 BELL_POS = 18,
289 SAY_CONTROL = 19,
290 SAY_WORD_CTL = 20,
291 NO_INTERRUPT = 21,
292 KEY_ECHO = 22,
293 SPELL_DELAY = 23,
294 PUNC_LEVEL = 24,
295 READING_PUNC = 25,
296 ATTRIB_BLEEP = 26,
297 BLEEPS = 27,
298 RATE = 28,
299 PITCH = 29,
300 VOL = 30,
301 TONE = 31,
302 PUNCT = 32,
303 VOICE = 33,
304 FREQUENCY = 34,
305 LANG = 35,
306 DIRECT = 36,
307 CAPS_START = 37,
308 CAPS_STOP = 38,
309 CHARTAB = 39,
310 MAXVARS = 40
311} ;
312#line 102 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
313struct st_var_header {
314 char *name ;
315 enum var_id_t var_id ;
316 enum var_type_t var_type ;
317 void *p_val ;
318 void *data ;
319};
320#line 110 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
321struct num_var_t {
322 char *synth_fmt ;
323 int default_val ;
324 int low ;
325 int high ;
326 short offset ;
327 short multiplier ;
328 char *out_str ;
329 int value ;
330};
331#line 125 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
332struct string_var_t {
333 char *default_val ;
334};
335#line 129 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
336union __anonunion_u_231 {
337 struct num_var_t n ;
338 struct string_var_t s ;
339};
340#line 129 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
341struct var_t {
342 enum var_id_t var_id ;
343 union __anonunion_u_231 u ;
344};
345#line 143 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
346struct synth_indexing {
347 char *command ;
348 unsigned char lowindex ;
349 unsigned char highindex ;
350 unsigned char currindex ;
351};
352#line 150 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
353struct spk_synth {
354 char const *name ;
355 char const *version ;
356 char const *long_name ;
357 char const *init ;
358 char procspeech ;
359 char clear ;
360 int delay ;
361 int trigger ;
362 int jiffies ;
363 int full ;
364 int ser ;
365 short flags ;
366 short startup ;
367 int const checkval ;
368 struct var_t *vars ;
369 int *default_pitch ;
370 int *default_vol ;
371 int (*probe)(struct spk_synth *synth ) ;
372 void (*release)(void) ;
373 char const *(*synth_immediate)(struct spk_synth *synth , char const *buff ) ;
374 void (*catch_up)(struct spk_synth *synth ) ;
375 void (*flush)(struct spk_synth *synth ) ;
376 int (*is_alive)(struct spk_synth *synth ) ;
377 int (*synth_adjust)(struct st_var_header *var ) ;
378 void (*read_buff_add)(u_char ) ;
379 unsigned char (*get_index)(void) ;
380 struct synth_indexing indexing ;
381 int alive ;
382 struct attribute_group attributes ;
383};
384#line 1 "<compiler builtins>"
385long __builtin_expect(long val , long res ) ;
386#line 152 "include/linux/mutex.h"
387void mutex_lock(struct mutex *lock ) ;
388#line 153
389int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
390#line 154
391int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
392#line 168
393int mutex_trylock(struct mutex *lock ) ;
394#line 169
395void mutex_unlock(struct mutex *lock ) ;
396#line 170
397int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
398#line 346 "include/linux/moduleparam.h"
399extern struct kernel_param_ops param_ops_short ;
400#line 356
401extern struct kernel_param_ops param_ops_int ;
402#line 67 "include/linux/module.h"
403int init_module(void) ;
404#line 68
405void cleanup_module(void) ;
406#line 53 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_priv.h"
407extern void spk_serial_release(void) ;
408#line 59
409extern ssize_t spk_var_show(struct kobject *kobj , struct kobj_attribute *attr , char *buf ) ;
410#line 61
411extern ssize_t spk_var_store(struct kobject *kobj , struct kobj_attribute *attr ,
412 char const *buf , size_t count ) ;
413#line 64
414extern int serial_synth_probe(struct spk_synth *synth ) ;
415#line 65
416extern char const *spk_synth_immediate(struct spk_synth *synth , char const *buff ) ;
417#line 66
418extern void spk_do_catch_up(struct spk_synth *synth ) ;
419#line 67
420extern void spk_synth_flush(struct spk_synth *synth ) ;
421#line 69
422extern int spk_synth_is_alive_restart(struct spk_synth *synth ) ;
423#line 73
424extern int synth_add(struct spk_synth *in_synth ) ;
425#line 74
426extern void synth_remove(struct spk_synth *in_synth ) ;
427#line 35 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
428static struct var_t vars[8] =
429#line 35 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
430 { {(enum var_id_t )37, {.s = {(char *)"CAPS_START\n"}}},
431 {(enum var_id_t )38, {.s = {(char *)"CAPS_STOP\n"}}},
432 {(enum var_id_t )28, {{(char *)"RATE %d\n", 8, 1, 16, (short)0, (short)0, (char *)((void *)0),
433 0}}},
434 {(enum var_id_t )29, {{(char *)"PITCH %d\n", 8, 0, 16, (short)0, (short)0, (char *)((void *)0),
435 0}}},
436 {(enum var_id_t )30, {{(char *)"VOL %d\n", 8, 0, 16, (short)0, (short)0, (char *)((void *)0),
437 0}}},
438 {(enum var_id_t )31, {{(char *)"TONE %d\n", 8, 0, 16, (short)0, (short)0, (char *)((void *)0),
439 0}}},
440 {(enum var_id_t )36, {{(char *)((void *)0), 0, 0, 1, (short)0, (short)0, (char *)((void *)0),
441 0}}},
442 {(enum var_id_t )40, {{(char *)0, 0, 0, 0, (short)0, (short)0, (char *)0, 0}}}};
443#line 49 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
444static struct kobj_attribute caps_start_attribute = {{"caps_start", (umode_t )33206}, & spk_var_show, & spk_var_store};
445#line 51 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
446static struct kobj_attribute caps_stop_attribute = {{"caps_stop", (umode_t )33206}, & spk_var_show, & spk_var_store};
447#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
448static struct kobj_attribute pitch_attribute = {{"pitch", (umode_t )33206}, & spk_var_show, & spk_var_store};
449#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
450static struct kobj_attribute rate_attribute = {{"rate", (umode_t )33206}, & spk_var_show, & spk_var_store};
451#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
452static struct kobj_attribute tone_attribute = {{"tone", (umode_t )33206}, & spk_var_show, & spk_var_store};
453#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
454static struct kobj_attribute vol_attribute = {{"vol", (umode_t )33206}, & spk_var_show, & spk_var_store};
455#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
456static struct kobj_attribute delay_time_attribute = {{"delay_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
457#line 64 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
458static struct kobj_attribute direct_attribute = {{"direct", (umode_t )33206}, & spk_var_show, & spk_var_store};
459#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
460static struct kobj_attribute full_time_attribute = {{"full_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
461#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
462static struct kobj_attribute jiffy_delta_attribute = {{"jiffy_delta", (umode_t )33188}, & spk_var_show, & spk_var_store};
463#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
464static struct kobj_attribute trigger_time_attribute = {{"trigger_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
465#line 77 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
466static struct attribute *synth_attrs[12] =
467#line 77
468 { & caps_start_attribute.attr, & caps_stop_attribute.attr, & pitch_attribute.attr, & rate_attribute.attr,
469 & tone_attribute.attr, & vol_attribute.attr, & delay_time_attribute.attr, & direct_attribute.attr,
470 & full_time_attribute.attr, & jiffy_delta_attribute.attr, & trigger_time_attribute.attr, (struct attribute *)((void *)0)};
471#line 92 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
472static struct spk_synth synth_dummy =
473#line 92
474 {"dummy", "2.11", "Dummy", "Speakup\n", (char )'\n', (char )'!', 500, 50, 50, 40000,
475 0, (short)0, (short)1, (int const )20030716, vars, (int *)0, (int *)0, & serial_synth_probe,
476 & spk_serial_release, & spk_synth_immediate, & spk_do_catch_up, & spk_synth_flush,
477 & spk_synth_is_alive_restart, (int (*)(struct st_var_header *var ))((void *)0),
478 (void (*)(u_char ))((void *)0), (unsigned char (*)(void))((void *)0), {(char *)((void *)0),
479 (unsigned char)0,
480 (unsigned char)0,
481 (unsigned char)0},
482 0, {"dummy", (umode_t (*)(struct kobject * , struct attribute * , int ))0, synth_attrs}};
483#line 127 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
484static char const __param_str_ser[4] = { (char const )'s', (char const )'e', (char const )'r', (char const )'\000'};
485#line 127 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
486static struct kernel_param const __param_ser __attribute__((__used__, __unused__,
487__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_ser, (struct kernel_param_ops const *)(& param_ops_int), (u16 )292,
488 (s16 )0, {(void *)(& synth_dummy.ser)}};
489#line 127 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
490static char const __mod_sertype127[17] __attribute__((__used__, __unused__, __section__(".modinfo"),
491__aligned__(1))) =
492#line 127
493 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
494 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
495 (char const )'=', (char const )'s', (char const )'e', (char const )'r',
496 (char const )':', (char const )'i', (char const )'n', (char const )'t',
497 (char const )'\000'};
498#line 128 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
499static char const __param_str_start[6] = { (char const )'s', (char const )'t', (char const )'a', (char const )'r',
500 (char const )'t', (char const )'\000'};
501#line 128 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
502static struct kernel_param const __param_start __attribute__((__used__, __unused__,
503__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_start, (struct kernel_param_ops const *)(& param_ops_short), (u16 )292,
504 (s16 )0, {(void *)(& synth_dummy.startup)}};
505#line 128 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
506static char const __mod_starttype128[21] __attribute__((__used__, __unused__, __section__(".modinfo"),
507__aligned__(1))) =
508#line 128
509 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
510 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
511 (char const )'=', (char const )'s', (char const )'t', (char const )'a',
512 (char const )'r', (char const )'t', (char const )':', (char const )'s',
513 (char const )'h', (char const )'o', (char const )'r', (char const )'t',
514 (char const )'\000'};
515#line 130 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
516static char const __mod_ser130[60] __attribute__((__used__, __unused__, __section__(".modinfo"),
517__aligned__(1))) =
518#line 130
519 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
520 (char const )'=', (char const )'s', (char const )'e', (char const )'r',
521 (char const )':', (char const )'S', (char const )'e', (char const )'t',
522 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
523 (char const )' ', (char const )'s', (char const )'e', (char const )'r',
524 (char const )'i', (char const )'a', (char const )'l', (char const )' ',
525 (char const )'p', (char const )'o', (char const )'r', (char const )'t',
526 (char const )' ', (char const )'f', (char const )'o', (char const )'r',
527 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
528 (char const )' ', (char const )'s', (char const )'y', (char const )'n',
529 (char const )'t', (char const )'h', (char const )'e', (char const )'s',
530 (char const )'i', (char const )'z', (char const )'e', (char const )'r',
531 (char const )' ', (char const )'(', (char const )'0', (char const )'-',
532 (char const )'b', (char const )'a', (char const )'s', (char const )'e',
533 (char const )'d', (char const )')', (char const )'.', (char const )'\000'};
534#line 131 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
535static char const __mod_start131[52] __attribute__((__used__, __unused__, __section__(".modinfo"),
536__aligned__(1))) =
537#line 131
538 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
539 (char const )'=', (char const )'s', (char const )'t', (char const )'a',
540 (char const )'r', (char const )'t', (char const )':', (char const )'S',
541 (char const )'t', (char const )'a', (char const )'r', (char const )'t',
542 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
543 (char const )' ', (char const )'s', (char const )'y', (char const )'n',
544 (char const )'t', (char const )'h', (char const )'e', (char const )'s',
545 (char const )'i', (char const )'z', (char const )'e', (char const )'r',
546 (char const )' ', (char const )'o', (char const )'n', (char const )'c',
547 (char const )'e', (char const )' ', (char const )'i', (char const )'t',
548 (char const )' ', (char const )'i', (char const )'s', (char const )' ',
549 (char const )'l', (char const )'o', (char const )'a', (char const )'d',
550 (char const )'e', (char const )'d', (char const )'.', (char const )'\000'};
551#line 133
552static int dummy_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
553#line 133 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
554static int dummy_init(void)
555{ int tmp ;
556
557 {
558 {
559#line 135
560 tmp = synth_add(& synth_dummy);
561 }
562#line 135
563 return (tmp);
564}
565}
566#line 138
567static void dummy_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
568#line 138 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
569static void dummy_exit(void)
570{
571
572 {
573 {
574#line 140
575 synth_remove(& synth_dummy);
576 }
577#line 141
578 return;
579}
580}
581#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
582int init_module(void)
583{ int tmp ;
584
585 {
586 {
587#line 143
588 tmp = dummy_init();
589 }
590#line 143
591 return (tmp);
592}
593}
594#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
595void cleanup_module(void)
596{
597
598 {
599 {
600#line 144
601 dummy_exit();
602 }
603#line 144
604 return;
605}
606}
607#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
608static char const __mod_author145[54] __attribute__((__used__, __unused__, __section__(".modinfo"),
609__aligned__(1))) =
610#line 145
611 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
612 (char const )'o', (char const )'r', (char const )'=', (char const )'S',
613 (char const )'a', (char const )'m', (char const )'u', (char const )'e',
614 (char const )'l', (char const )' ', (char const )'T', (char const )'h',
615 (char const )'i', (char const )'b', (char const )'a', (char const )'u',
616 (char const )'l', (char const )'t', (char const )' ', (char const )'<',
617 (char const )'s', (char const )'a', (char const )'m', (char const )'u',
618 (char const )'e', (char const )'l', (char const )'.', (char const )'t',
619 (char const )'h', (char const )'i', (char const )'b', (char const )'a',
620 (char const )'u', (char const )'l', (char const )'t', (char const )'@',
621 (char const )'e', (char const )'n', (char const )'s', (char const )'-',
622 (char const )'l', (char const )'y', (char const )'o', (char const )'n',
623 (char const )'.', (char const )'o', (char const )'r', (char const )'g',
624 (char const )'>', (char const )'\000'};
625#line 146 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
626static char const __mod_description146[45] __attribute__((__used__, __unused__,
627__section__(".modinfo"), __aligned__(1))) =
628#line 146
629 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
630 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
631 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
632 (char const )'S', (char const )'p', (char const )'e', (char const )'a',
633 (char const )'k', (char const )'u', (char const )'p', (char const )' ',
634 (char const )'s', (char const )'u', (char const )'p', (char const )'p',
635 (char const )'o', (char const )'r', (char const )'t', (char const )' ',
636 (char const )'f', (char const )'o', (char const )'r', (char const )' ',
637 (char const )'t', (char const )'e', (char const )'x', (char const )'t',
638 (char const )' ', (char const )'c', (char const )'o', (char const )'n',
639 (char const )'s', (char const )'o', (char const )'l', (char const )'e',
640 (char const )'\000'};
641#line 147 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
642static char const __mod_license147[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
643__aligned__(1))) =
644#line 147
645 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
646 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
647 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
648#line 148 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
649static char const __mod_version148[13] __attribute__((__used__, __unused__, __section__(".modinfo"),
650__aligned__(1))) =
651#line 148
652 { (char const )'v', (char const )'e', (char const )'r', (char const )'s',
653 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
654 (char const )'2', (char const )'.', (char const )'1', (char const )'1',
655 (char const )'\000'};
656#line 167
657void ldv_check_final_state(void) ;
658#line 173
659extern void ldv_initialize(void) ;
660#line 176
661extern int __VERIFIER_nondet_int(void) ;
662#line 179 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
663int LDV_IN_INTERRUPT ;
664#line 182 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
665void main(void)
666{ int tmp ;
667 int tmp___0 ;
668 int tmp___1 ;
669
670 {
671 {
672#line 194
673 LDV_IN_INTERRUPT = 1;
674#line 203
675 ldv_initialize();
676#line 213
677 tmp = dummy_init();
678 }
679#line 213
680 if (tmp) {
681#line 214
682 goto ldv_final;
683 } else {
684
685 }
686 {
687#line 216
688 while (1) {
689 while_continue: ;
690 {
691#line 216
692 tmp___1 = __VERIFIER_nondet_int();
693 }
694#line 216
695 if (tmp___1) {
696
697 } else {
698#line 216
699 goto while_break;
700 }
701 {
702#line 219
703 tmp___0 = __VERIFIER_nondet_int();
704 }
705 {
706#line 221
707 goto switch_default;
708#line 219
709 if (0) {
710 switch_default:
711#line 221
712 goto switch_break;
713 } else {
714 switch_break: ;
715 }
716 }
717 }
718 while_break: ;
719 }
720 {
721#line 237
722 dummy_exit();
723 }
724 ldv_final:
725 {
726#line 240
727 ldv_check_final_state();
728 }
729#line 243
730 return;
731}
732}
733#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
734void ldv_blast_assert(void)
735{
736
737 {
738 ERROR:
739#line 6
740 goto ERROR;
741}
742}
743#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
744extern int __VERIFIER_nondet_int(void) ;
745#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
746int ldv_mutex = 1;
747#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
748int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
749{ int nondetermined ;
750
751 {
752#line 29
753 if (ldv_mutex == 1) {
754
755 } else {
756 {
757#line 29
758 ldv_blast_assert();
759 }
760 }
761 {
762#line 32
763 nondetermined = __VERIFIER_nondet_int();
764 }
765#line 35
766 if (nondetermined) {
767#line 38
768 ldv_mutex = 2;
769#line 40
770 return (0);
771 } else {
772#line 45
773 return (-4);
774 }
775}
776}
777#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
778int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
779{ int nondetermined ;
780
781 {
782#line 57
783 if (ldv_mutex == 1) {
784
785 } else {
786 {
787#line 57
788 ldv_blast_assert();
789 }
790 }
791 {
792#line 60
793 nondetermined = __VERIFIER_nondet_int();
794 }
795#line 63
796 if (nondetermined) {
797#line 66
798 ldv_mutex = 2;
799#line 68
800 return (0);
801 } else {
802#line 73
803 return (-4);
804 }
805}
806}
807#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
808int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
809{ int atomic_value_after_dec ;
810
811 {
812#line 83
813 if (ldv_mutex == 1) {
814
815 } else {
816 {
817#line 83
818 ldv_blast_assert();
819 }
820 }
821 {
822#line 86
823 atomic_value_after_dec = __VERIFIER_nondet_int();
824 }
825#line 89
826 if (atomic_value_after_dec == 0) {
827#line 92
828 ldv_mutex = 2;
829#line 94
830 return (1);
831 } else {
832
833 }
834#line 98
835 return (0);
836}
837}
838#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
839void mutex_lock(struct mutex *lock )
840{
841
842 {
843#line 108
844 if (ldv_mutex == 1) {
845
846 } else {
847 {
848#line 108
849 ldv_blast_assert();
850 }
851 }
852#line 110
853 ldv_mutex = 2;
854#line 111
855 return;
856}
857}
858#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
859int mutex_trylock(struct mutex *lock )
860{ int nondetermined ;
861
862 {
863#line 121
864 if (ldv_mutex == 1) {
865
866 } else {
867 {
868#line 121
869 ldv_blast_assert();
870 }
871 }
872 {
873#line 124
874 nondetermined = __VERIFIER_nondet_int();
875 }
876#line 127
877 if (nondetermined) {
878#line 130
879 ldv_mutex = 2;
880#line 132
881 return (1);
882 } else {
883#line 137
884 return (0);
885 }
886}
887}
888#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
889void mutex_unlock(struct mutex *lock )
890{
891
892 {
893#line 147
894 if (ldv_mutex == 2) {
895
896 } else {
897 {
898#line 147
899 ldv_blast_assert();
900 }
901 }
902#line 149
903 ldv_mutex = 1;
904#line 150
905 return;
906}
907}
908#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
909void ldv_check_final_state(void)
910{
911
912 {
913#line 156
914 if (ldv_mutex == 1) {
915
916 } else {
917 {
918#line 156
919 ldv_blast_assert();
920 }
921 }
922#line 157
923 return;
924}
925}
926#line 252 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1174/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_dummy.c.common.c"
927long s__builtin_expect(long val , long res )
928{
929
930 {
931#line 253
932 return (val);
933}
934}