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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
430 { {(enum var_id_t )37, {.s = {(char *)"\00512P"}}},
431 {(enum var_id_t )38, {.s = {(char *)"\0058P"}}},
432 {(enum var_id_t )28, {{(char *)"\005%dE", 8, 1, 16, (short)0, (short)0, (char *)((void *)0),
433 0}}},
434 {(enum var_id_t )29, {{(char *)"\005%dP", 8, 0, 16, (short)0, (short)0, (char *)((void *)0),
435 0}}},
436 {(enum var_id_t )30, {{(char *)"\005%dV", 8, 0, 16, (short)0, (short)0, (char *)((void *)0),
437 0}}},
438 {(enum var_id_t )31, {{(char *)"\005%dT", 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 47 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
472static struct spk_synth synth_bns =
473#line 90
474 {"bns", "2.11", "Braille \'N Speak", "\005Z\005C", (char )'\r', (char)24, 500,
475 50, 50, 40000, 0, (short)0, (short)1, (int const )20030716, vars, (int *)0,
476 (int *)0, & serial_synth_probe, & spk_serial_release, & spk_synth_immediate, & spk_do_catch_up,
477 & spk_synth_flush, & 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, {"bns", (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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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 bns_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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
554static int bns_init(void)
555{ int tmp ;
556
557 {
558 {
559#line 133
560 tmp = synth_add(& synth_bns);
561 }
562#line 133
563 return (tmp);
564}
565}
566#line 136
567static void bns_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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
569static void bns_exit(void)
570{
571
572 {
573 {
574#line 138
575 synth_remove(& synth_bns);
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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
582int init_module(void)
583{ int tmp ;
584
585 {
586 {
587#line 141
588 tmp = bns_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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
595void cleanup_module(void)
596{
597
598 {
599 {
600#line 142
601 bns_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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.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/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
633static char const __mod_description145[62] __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 )'B', (char const )'r', (char const )'a', (char const )'i',
645 (char const )'l', (char const )'l', (char const )'e', (char const )' ',
646 (char const )'\'', (char const )'n', (char const )' ', (char const )'S',
647 (char const )'p', (char const )'e', (char const )'a', (char const )'k',
648 (char const )' ', (char const )'s', (char const )'y', (char const )'n',
649 (char const )'t', (char const )'h', (char const )'e', (char const )'s',
650 (char const )'i', (char const )'z', (char const )'e', (char const )'r',
651 (char const )'s', (char const )'\000'};
652#line 146 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
653static char const __mod_license146[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
654__aligned__(1))) =
655#line 146
656 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
657 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
658 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
659#line 147 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
660static char const __mod_version147[13] __attribute__((__used__, __unused__, __section__(".modinfo"),
661__aligned__(1))) =
662#line 147
663 { (char const )'v', (char const )'e', (char const )'r', (char const )'s',
664 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
665 (char const )'2', (char const )'.', (char const )'1', (char const )'1',
666 (char const )'\000'};
667#line 166
668void ldv_check_final_state(void) ;
669#line 172
670extern void ldv_initialize(void) ;
671#line 175
672extern int __VERIFIER_nondet_int(void) ;
673#line 178 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
674int LDV_IN_INTERRUPT ;
675#line 181 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
676void main(void)
677{ int tmp ;
678 int tmp___0 ;
679 int tmp___1 ;
680
681 {
682 {
683#line 193
684 LDV_IN_INTERRUPT = 1;
685#line 202
686 ldv_initialize();
687#line 212
688 tmp = bns_init();
689 }
690#line 212
691 if (tmp) {
692#line 213
693 goto ldv_final;
694 } else {
695
696 }
697 {
698#line 215
699 while (1) {
700 while_continue: ;
701 {
702#line 215
703 tmp___1 = __VERIFIER_nondet_int();
704 }
705#line 215
706 if (tmp___1) {
707
708 } else {
709#line 215
710 goto while_break;
711 }
712 {
713#line 218
714 tmp___0 = __VERIFIER_nondet_int();
715 }
716 {
717#line 220
718 goto switch_default;
719#line 218
720 if (0) {
721 switch_default:
722#line 220
723 goto switch_break;
724 } else {
725 switch_break: ;
726 }
727 }
728 }
729 while_break: ;
730 }
731 {
732#line 236
733 bns_exit();
734 }
735 ldv_final:
736 {
737#line 239
738 ldv_check_final_state();
739 }
740#line 242
741 return;
742}
743}
744#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
745void ldv_blast_assert(void)
746{
747
748 {
749 ERROR:
750#line 6
751 goto ERROR;
752}
753}
754#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
755extern int __VERIFIER_nondet_int(void) ;
756#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
757int ldv_mutex = 1;
758#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
759int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
760{ int nondetermined ;
761
762 {
763#line 29
764 if (ldv_mutex == 1) {
765
766 } else {
767 {
768#line 29
769 ldv_blast_assert();
770 }
771 }
772 {
773#line 32
774 nondetermined = __VERIFIER_nondet_int();
775 }
776#line 35
777 if (nondetermined) {
778#line 38
779 ldv_mutex = 2;
780#line 40
781 return (0);
782 } else {
783#line 45
784 return (-4);
785 }
786}
787}
788#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
789int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
790{ int nondetermined ;
791
792 {
793#line 57
794 if (ldv_mutex == 1) {
795
796 } else {
797 {
798#line 57
799 ldv_blast_assert();
800 }
801 }
802 {
803#line 60
804 nondetermined = __VERIFIER_nondet_int();
805 }
806#line 63
807 if (nondetermined) {
808#line 66
809 ldv_mutex = 2;
810#line 68
811 return (0);
812 } else {
813#line 73
814 return (-4);
815 }
816}
817}
818#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
819int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
820{ int atomic_value_after_dec ;
821
822 {
823#line 83
824 if (ldv_mutex == 1) {
825
826 } else {
827 {
828#line 83
829 ldv_blast_assert();
830 }
831 }
832 {
833#line 86
834 atomic_value_after_dec = __VERIFIER_nondet_int();
835 }
836#line 89
837 if (atomic_value_after_dec == 0) {
838#line 92
839 ldv_mutex = 2;
840#line 94
841 return (1);
842 } else {
843
844 }
845#line 98
846 return (0);
847}
848}
849#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
850void mutex_lock(struct mutex *lock )
851{
852
853 {
854#line 108
855 if (ldv_mutex == 1) {
856
857 } else {
858 {
859#line 108
860 ldv_blast_assert();
861 }
862 }
863#line 110
864 ldv_mutex = 2;
865#line 111
866 return;
867}
868}
869#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
870int mutex_trylock(struct mutex *lock )
871{ int nondetermined ;
872
873 {
874#line 121
875 if (ldv_mutex == 1) {
876
877 } else {
878 {
879#line 121
880 ldv_blast_assert();
881 }
882 }
883 {
884#line 124
885 nondetermined = __VERIFIER_nondet_int();
886 }
887#line 127
888 if (nondetermined) {
889#line 130
890 ldv_mutex = 2;
891#line 132
892 return (1);
893 } else {
894#line 137
895 return (0);
896 }
897}
898}
899#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
900void mutex_unlock(struct mutex *lock )
901{
902
903 {
904#line 147
905 if (ldv_mutex == 2) {
906
907 } else {
908 {
909#line 147
910 ldv_blast_assert();
911 }
912 }
913#line 149
914 ldv_mutex = 1;
915#line 150
916 return;
917}
918}
919#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
920void ldv_check_final_state(void)
921{
922
923 {
924#line 156
925 if (ldv_mutex == 1) {
926
927 } else {
928 {
929#line 156
930 ldv_blast_assert();
931 }
932 }
933#line 157
934 return;
935}
936}
937#line 251 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1169/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_bns.c.common.c"
938long s__builtin_expect(long val , long res )
939{
940
941 {
942#line 252
943 return (val);
944}
945}