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 33 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
428static struct var_t vars[8] =
429#line 33 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
430 { {(enum var_id_t )37, {.s = {(char *)"\005P8"}}},
431 {(enum var_id_t )38, {.s = {(char *)"\005P5"}}},
432 {(enum var_id_t )28, {{(char *)"\005R%d", 5, 0, 9, (short)0, (short)0, (char *)((void *)0),
433 0}}},
434 {(enum var_id_t )29, {{(char *)"\005P%d", 5, 0, 9, (short)0, (short)0, (char *)((void *)0),
435 0}}},
436 {(enum var_id_t )30, {{(char *)"\005V%d", 5, 0, 9, (short)0, (short)0, (char *)((void *)0),
437 0}}},
438 {(enum var_id_t )31, {{(char *)"\005T%c", 12, 0, 25, (short)61, (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 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
444static struct kobj_attribute caps_start_attribute = {{"caps_start", (umode_t )33206}, & spk_var_show, & spk_var_store};
445#line 49 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
446static struct kobj_attribute caps_stop_attribute = {{"caps_stop", (umode_t )33206}, & spk_var_show, & spk_var_store};
447#line 51 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
448static struct kobj_attribute pitch_attribute = {{"pitch", (umode_t )33206}, & spk_var_show, & spk_var_store};
449#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
450static struct kobj_attribute rate_attribute = {{"rate", (umode_t )33206}, & spk_var_show, & spk_var_store};
451#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
452static struct kobj_attribute tone_attribute = {{"tone", (umode_t )33206}, & spk_var_show, & spk_var_store};
453#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
454static struct kobj_attribute vol_attribute = {{"vol", (umode_t )33206}, & spk_var_show, & spk_var_store};
455#line 60 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
456static struct kobj_attribute delay_time_attribute = {{"delay_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
457#line 62 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
458static struct kobj_attribute direct_attribute = {{"direct", (umode_t )33206}, & spk_var_show, & spk_var_store};
459#line 64 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
460static struct kobj_attribute full_time_attribute = {{"full_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
461#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
462static struct kobj_attribute jiffy_delta_attribute = {{"jiffy_delta", (umode_t )33188}, & spk_var_show, & spk_var_store};
463#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
464static struct kobj_attribute trigger_time_attribute = {{"trigger_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
465#line 75 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
466static struct attribute *synth_attrs[12] =
467#line 75
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 90 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
472static struct spk_synth synth_txprt =
473#line 90
474 {"txprt", "2.11", "Transport", "\005N1", (char )'\r', (char)24, 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, {"txprt", (umode_t (*)(struct kobject * , struct attribute * , int ))0, synth_attrs}};
483#line 125 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
484static char const __param_str_ser[4] = { (char const )'s', (char const )'e', (char const )'r', (char const )'\000'};
485#line 125 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.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_txprt.ser)}};
489#line 125 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
490static char const __mod_sertype125[17] __attribute__((__used__, __unused__, __section__(".modinfo"),
491__aligned__(1))) =
492#line 125
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 126 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.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 126 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.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_txprt.startup)}};
505#line 126 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
506static char const __mod_starttype126[21] __attribute__((__used__, __unused__, __section__(".modinfo"),
507__aligned__(1))) =
508#line 126
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 128 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
516static char const __mod_ser128[60] __attribute__((__used__, __unused__, __section__(".modinfo"),
517__aligned__(1))) =
518#line 128
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 129 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
535static char const __mod_start129[52] __attribute__((__used__, __unused__, __section__(".modinfo"),
536__aligned__(1))) =
537#line 129
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 131
552static int txprt_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
553#line 131 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
554static int txprt_init(void)
555{ int tmp ;
556
557 {
558 {
559#line 133
560 tmp = synth_add(& synth_txprt);
561 }
562#line 133
563 return (tmp);
564}
565}
566#line 136
567static void txprt_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
568#line 136 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
569static void txprt_exit(void)
570{
571
572 {
573 {
574#line 138
575 synth_remove(& synth_txprt);
576 }
577#line 139
578 return;
579}
580}
581#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
582int init_module(void)
583{ int tmp ;
584
585 {
586 {
587#line 141
588 tmp = txprt_init();
589 }
590#line 141
591 return (tmp);
592}
593}
594#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
595void cleanup_module(void)
596{
597
598 {
599 {
600#line 142
601 txprt_exit();
602 }
603#line 142
604 return;
605}
606}
607#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
608static char const __mod_author143[41] __attribute__((__used__, __unused__, __section__(".modinfo"),
609__aligned__(1))) =
610#line 143
611 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
612 (char const )'o', (char const )'r', (char const )'=', (char const )'K',
613 (char const )'i', (char const )'r', (char const )'k', (char const )' ',
614 (char const )'R', (char const )'e', (char const )'i', (char const )'s',
615 (char const )'e', (char const )'r', (char const )' ', (char const )'<',
616 (char const )'k', (char const )'i', (char const )'r', (char const )'k',
617 (char const )'@', (char const )'b', (char const )'r', (char const )'a',
618 (char const )'i', (char const )'l', (char const )'l', (char const )'e',
619 (char const )'.', (char const )'u', (char const )'w', (char const )'o',
620 (char const )'.', (char const )'c', (char const )'a', (char const )'>',
621 (char const )'\000'};
622#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
623static char const __mod_author144[22] __attribute__((__used__, __unused__, __section__(".modinfo"),
624__aligned__(1))) =
625#line 144
626 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
627 (char const )'o', (char const )'r', (char const )'=', (char const )'D',
628 (char const )'a', (char const )'v', (char const )'i', (char const )'d',
629 (char const )' ', (char const )'B', (char const )'o', (char const )'r',
630 (char const )'o', (char const )'w', (char const )'s', (char const )'k',
631 (char const )'i', (char const )'\000'};
632#line 145 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
633static char const __mod_description145[55] __attribute__((__used__, __unused__,
634__section__(".modinfo"), __aligned__(1))) =
635#line 145
636 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
637 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
638 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
639 (char const )'S', (char const )'p', (char const )'e', (char const )'a',
640 (char const )'k', (char const )'u', (char const )'p', (char const )' ',
641 (char const )'s', (char const )'u', (char const )'p', (char const )'p',
642 (char const )'o', (char const )'r', (char const )'t', (char const )' ',
643 (char const )'f', (char const )'o', (char const )'r', (char const )' ',
644 (char const )'T', (char const )'r', (char const )'a', (char const )'n',
645 (char const )'s', (char const )'p', (char const )'o', (char const )'r',
646 (char const )'t', (char const )' ', (char const )'s', (char const )'y',
647 (char const )'n', (char const )'t', (char const )'h', (char const )'e',
648 (char const )'s', (char const )'i', (char const )'z', (char const )'e',
649 (char const )'r', (char const )'s', (char const )'\000'};
650#line 146 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
651static char const __mod_license146[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
652__aligned__(1))) =
653#line 146
654 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
655 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
656 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
657#line 147 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
658static char const __mod_version147[13] __attribute__((__used__, __unused__, __section__(".modinfo"),
659__aligned__(1))) =
660#line 147
661 { (char const )'v', (char const )'e', (char const )'r', (char const )'s',
662 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
663 (char const )'2', (char const )'.', (char const )'1', (char const )'1',
664 (char const )'\000'};
665#line 166
666void ldv_check_final_state(void) ;
667#line 172
668extern void ldv_initialize(void) ;
669#line 175
670extern int __VERIFIER_nondet_int(void) ;
671#line 178 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
672int LDV_IN_INTERRUPT ;
673#line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
674void main(void)
675{ int tmp ;
676 int tmp___0 ;
677 int tmp___1 ;
678
679 {
680 {
681#line 193
682 LDV_IN_INTERRUPT = 1;
683#line 202
684 ldv_initialize();
685#line 212
686 tmp = txprt_init();
687 }
688#line 212
689 if (tmp) {
690#line 213
691 goto ldv_final;
692 } else {
693
694 }
695 {
696#line 215
697 while (1) {
698 while_continue: ;
699 {
700#line 215
701 tmp___1 = __VERIFIER_nondet_int();
702 }
703#line 215
704 if (tmp___1) {
705
706 } else {
707#line 215
708 goto while_break;
709 }
710 {
711#line 218
712 tmp___0 = __VERIFIER_nondet_int();
713 }
714 {
715#line 220
716 goto switch_default;
717#line 218
718 if (0) {
719 switch_default:
720#line 220
721 goto switch_break;
722 } else {
723 switch_break: ;
724 }
725 }
726 }
727 while_break: ;
728 }
729 {
730#line 236
731 txprt_exit();
732 }
733 ldv_final:
734 {
735#line 239
736 ldv_check_final_state();
737 }
738#line 242
739 return;
740}
741}
742#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
743void ldv_blast_assert(void)
744{
745
746 {
747 ERROR:
748#line 6
749 goto ERROR;
750}
751}
752#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
753extern int __VERIFIER_nondet_int(void) ;
754#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
755int ldv_mutex = 1;
756#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
757int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
758{ int nondetermined ;
759
760 {
761#line 29
762 if (ldv_mutex == 1) {
763
764 } else {
765 {
766#line 29
767 ldv_blast_assert();
768 }
769 }
770 {
771#line 32
772 nondetermined = __VERIFIER_nondet_int();
773 }
774#line 35
775 if (nondetermined) {
776#line 38
777 ldv_mutex = 2;
778#line 40
779 return (0);
780 } else {
781#line 45
782 return (-4);
783 }
784}
785}
786#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
787int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
788{ int nondetermined ;
789
790 {
791#line 57
792 if (ldv_mutex == 1) {
793
794 } else {
795 {
796#line 57
797 ldv_blast_assert();
798 }
799 }
800 {
801#line 60
802 nondetermined = __VERIFIER_nondet_int();
803 }
804#line 63
805 if (nondetermined) {
806#line 66
807 ldv_mutex = 2;
808#line 68
809 return (0);
810 } else {
811#line 73
812 return (-4);
813 }
814}
815}
816#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
817int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
818{ int atomic_value_after_dec ;
819
820 {
821#line 83
822 if (ldv_mutex == 1) {
823
824 } else {
825 {
826#line 83
827 ldv_blast_assert();
828 }
829 }
830 {
831#line 86
832 atomic_value_after_dec = __VERIFIER_nondet_int();
833 }
834#line 89
835 if (atomic_value_after_dec == 0) {
836#line 92
837 ldv_mutex = 2;
838#line 94
839 return (1);
840 } else {
841
842 }
843#line 98
844 return (0);
845}
846}
847#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
848void mutex_lock(struct mutex *lock )
849{
850
851 {
852#line 108
853 if (ldv_mutex == 1) {
854
855 } else {
856 {
857#line 108
858 ldv_blast_assert();
859 }
860 }
861#line 110
862 ldv_mutex = 2;
863#line 111
864 return;
865}
866}
867#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
868int mutex_trylock(struct mutex *lock )
869{ int nondetermined ;
870
871 {
872#line 121
873 if (ldv_mutex == 1) {
874
875 } else {
876 {
877#line 121
878 ldv_blast_assert();
879 }
880 }
881 {
882#line 124
883 nondetermined = __VERIFIER_nondet_int();
884 }
885#line 127
886 if (nondetermined) {
887#line 130
888 ldv_mutex = 2;
889#line 132
890 return (1);
891 } else {
892#line 137
893 return (0);
894 }
895}
896}
897#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
898void mutex_unlock(struct mutex *lock )
899{
900
901 {
902#line 147
903 if (ldv_mutex == 2) {
904
905 } else {
906 {
907#line 147
908 ldv_blast_assert();
909 }
910 }
911#line 149
912 ldv_mutex = 1;
913#line 150
914 return;
915}
916}
917#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
918void ldv_check_final_state(void)
919{
920
921 {
922#line 156
923 if (ldv_mutex == 1) {
924
925 } else {
926 {
927#line 156
928 ldv_blast_assert();
929 }
930 }
931#line 157
932 return;
933}
934}
935#line 251 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1179/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_txprt.c.common.c"
936long s__builtin_expect(long val , long res )
937{
938
939 {
940#line 252
941 return (val);
942}
943}