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 182 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_types.h"
385struct speakup_info_t {
386 spinlock_t spinlock ;
387 int port_tts ;
388 int flushing ;
389};
390#line 1 "<compiler builtins>"
391long __builtin_expect(long val , long res ) ;
392#line 152 "include/linux/mutex.h"
393void mutex_lock(struct mutex *lock ) ;
394#line 153
395int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
396#line 154
397int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
398#line 168
399int mutex_trylock(struct mutex *lock ) ;
400#line 169
401void mutex_unlock(struct mutex *lock ) ;
402#line 170
403int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
404#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
405__inline static void outb(unsigned char value , int port ) __attribute__((__no_instrument_function__)) ;
406#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
407__inline static void outb(unsigned char value , int port )
408{
409
410 {
411#line 308
412 __asm__ volatile ("out"
413 "b"
414 " %"
415 "b"
416 "0, %w1": : "a" (value), "Nd" (port));
417#line 308
418 return;
419}
420}
421#line 308
422__inline static unsigned char inb(int port ) __attribute__((__no_instrument_function__)) ;
423#line 308 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/arch/x86/include/asm/io.h"
424__inline static unsigned char inb(int port )
425{ unsigned char value ;
426
427 {
428#line 308
429 __asm__ volatile ("in"
430 "b"
431 " %w1, %"
432 "b"
433 "0": "=a" (value): "Nd" (port));
434#line 308
435 return (value);
436}
437}
438#line 10 "include/asm-generic/delay.h"
439extern void __const_udelay(unsigned long xloops ) ;
440#line 346 "include/linux/moduleparam.h"
441extern struct kernel_param_ops param_ops_short ;
442#line 356
443extern struct kernel_param_ops param_ops_int ;
444#line 67 "include/linux/module.h"
445int init_module(void) ;
446#line 68
447void cleanup_module(void) ;
448#line 51 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_priv.h"
449extern unsigned char spk_serial_in_nowait(void) ;
450#line 53
451extern void spk_serial_release(void) ;
452#line 59
453extern ssize_t spk_var_show(struct kobject *kobj , struct kobj_attribute *attr , char *buf ) ;
454#line 61
455extern ssize_t spk_var_store(struct kobject *kobj , struct kobj_attribute *attr ,
456 char const *buf , size_t count ) ;
457#line 64
458extern int serial_synth_probe(struct spk_synth *synth ) ;
459#line 65
460extern char const *spk_synth_immediate(struct spk_synth *synth , char const *buff ) ;
461#line 66
462extern void spk_do_catch_up(struct spk_synth *synth ) ;
463#line 69
464extern int spk_synth_is_alive_restart(struct spk_synth *synth ) ;
465#line 73
466extern int synth_add(struct spk_synth *in_synth ) ;
467#line 74
468extern void synth_remove(struct spk_synth *in_synth ) ;
469#line 76
470extern struct speakup_info_t speakup_info ;
471#line 34 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
472static void synth_flush(struct spk_synth *synth___0 ) ;
473#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
474static struct var_t vars[9] =
475#line 36
476 { {(enum var_id_t )37, {.s = {(char *)"\005P+"}}},
477 {(enum var_id_t )38, {.s = {(char *)"\005P-"}}},
478 {(enum var_id_t )28, {{(char *)"\005R%d", 7, 0, 9, (short)0, (short)0, (char *)((void *)0),
479 0}}},
480 {(enum var_id_t )29, {{(char *)"\005P%d", 3, 0, 9, (short)0, (short)0, (char *)((void *)0),
481 0}}},
482 {(enum var_id_t )30, {{(char *)"\005V%d", 9, 0, 9, (short)0, (short)0, (char *)((void *)0),
483 0}}},
484 {(enum var_id_t )31, {{(char *)"\005T%c", 8, 0, 25, (short)65, (short)0, (char *)((void *)0),
485 0}}},
486 {(enum var_id_t )32, {{(char *)"\005M%c", 0, 0, 3, (short)0, (short)0, (char *)"nsma",
487 0}}},
488 {(enum var_id_t )36, {{(char *)((void *)0), 0, 0, 1, (short)0, (short)0, (char *)((void *)0),
489 0}}},
490 {(enum var_id_t )40, {{(char *)0, 0, 0, 0, (short)0, (short)0, (char *)0, 0}}}};
491#line 51 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
492static struct kobj_attribute caps_start_attribute = {{"caps_start", (umode_t )33206}, & spk_var_show, & spk_var_store};
493#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
494static struct kobj_attribute caps_stop_attribute = {{"caps_stop", (umode_t )33206}, & spk_var_show, & spk_var_store};
495#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
496static struct kobj_attribute pitch_attribute = {{"pitch", (umode_t )33206}, & spk_var_show, & spk_var_store};
497#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
498static struct kobj_attribute punct_attribute = {{"punct", (umode_t )33206}, & spk_var_show, & spk_var_store};
499#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
500static struct kobj_attribute rate_attribute = {{"rate", (umode_t )33206}, & spk_var_show, & spk_var_store};
501#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
502static struct kobj_attribute tone_attribute = {{"tone", (umode_t )33206}, & spk_var_show, & spk_var_store};
503#line 63 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
504static struct kobj_attribute vol_attribute = {{"vol", (umode_t )33206}, & spk_var_show, & spk_var_store};
505#line 66 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
506static struct kobj_attribute delay_time_attribute = {{"delay_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
507#line 68 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
508static struct kobj_attribute direct_attribute = {{"direct", (umode_t )33206}, & spk_var_show, & spk_var_store};
509#line 70 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
510static struct kobj_attribute full_time_attribute = {{"full_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
511#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
512static struct kobj_attribute jiffy_delta_attribute = {{"jiffy_delta", (umode_t )33188}, & spk_var_show, & spk_var_store};
513#line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
514static struct kobj_attribute trigger_time_attribute = {{"trigger_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
515#line 81 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
516static struct attribute *synth_attrs[13] =
517#line 81
518 { & caps_start_attribute.attr, & caps_stop_attribute.attr, & pitch_attribute.attr, & punct_attribute.attr,
519 & rate_attribute.attr, & tone_attribute.attr, & vol_attribute.attr, & delay_time_attribute.attr,
520 & direct_attribute.attr, & full_time_attribute.attr, & jiffy_delta_attribute.attr, & trigger_time_attribute.attr,
521 (struct attribute *)((void *)0)};
522#line 97 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
523static struct spk_synth synth_spkout =
524#line 97
525 {"spkout", "2.11", "Speakout", "\005W1\005I2\005C3", (char )'\r', (char)24, 500,
526 50, 50, 40000, 0, (short)0, (short)1, (int const )20030716, vars, (int *)0,
527 (int *)0, & serial_synth_probe, & spk_serial_release, & spk_synth_immediate, & spk_do_catch_up,
528 & synth_flush, & spk_synth_is_alive_restart, (int (*)(struct st_var_header *var ))((void *)0),
529 (void (*)(u_char ))((void *)0), & spk_serial_in_nowait, {(char *)"\005[%c", (unsigned char)1,
530 (unsigned char)5, (unsigned char)1},
531 0, {"spkout", (umode_t (*)(struct kobject * , struct attribute * , int ))0, synth_attrs}};
532#line 132 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
533static void synth_flush(struct spk_synth *synth___0 )
534{ int timeout ;
535 unsigned char tmp ;
536 int __cil_tmp4 ;
537 int __cil_tmp5 ;
538 int __cil_tmp6 ;
539
540 {
541#line 134
542 timeout = 100000;
543 {
544#line 135
545 while (1) {
546 while_continue: ;
547 {
548#line 135
549 __cil_tmp4 = speakup_info.port_tts + 5;
550#line 135
551 tmp = inb(__cil_tmp4);
552 }
553 {
554#line 135
555 __cil_tmp5 = (int )tmp;
556#line 135
557 __cil_tmp6 = __cil_tmp5 & 96;
558#line 135
559 if (__cil_tmp6 != 96) {
560
561 } else {
562#line 135
563 goto while_break;
564 }
565 }
566#line 136
567 timeout = timeout - 1;
568#line 136
569 if (timeout) {
570
571 } else {
572#line 137
573 goto while_break;
574 }
575 {
576#line 138
577 __const_udelay(4295UL);
578 }
579 }
580 while_break: ;
581 }
582 {
583#line 140
584 outb((unsigned char)24, speakup_info.port_tts);
585 }
586#line 141
587 return;
588}
589}
590#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
591static char const __param_str_ser[4] = { (char const )'s', (char const )'e', (char const )'r', (char const )'\000'};
592#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
593static struct kernel_param const __param_ser __attribute__((__used__, __unused__,
594__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_ser, (struct kernel_param_ops const *)(& param_ops_int), (u16 )292,
595 (s16 )0, {(void *)(& synth_spkout.ser)}};
596#line 143 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
597static char const __mod_sertype143[17] __attribute__((__used__, __unused__, __section__(".modinfo"),
598__aligned__(1))) =
599#line 143
600 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
601 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
602 (char const )'=', (char const )'s', (char const )'e', (char const )'r',
603 (char const )':', (char const )'i', (char const )'n', (char const )'t',
604 (char const )'\000'};
605#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
606static char const __param_str_start[6] = { (char const )'s', (char const )'t', (char const )'a', (char const )'r',
607 (char const )'t', (char const )'\000'};
608#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
609static struct kernel_param const __param_start __attribute__((__used__, __unused__,
610__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_start, (struct kernel_param_ops const *)(& param_ops_short), (u16 )292,
611 (s16 )0, {(void *)(& synth_spkout.startup)}};
612#line 144 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
613static char const __mod_starttype144[21] __attribute__((__used__, __unused__, __section__(".modinfo"),
614__aligned__(1))) =
615#line 144
616 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
617 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
618 (char const )'=', (char const )'s', (char const )'t', (char const )'a',
619 (char const )'r', (char const )'t', (char const )':', (char const )'s',
620 (char const )'h', (char const )'o', (char const )'r', (char const )'t',
621 (char const )'\000'};
622#line 146 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
623static char const __mod_ser146[60] __attribute__((__used__, __unused__, __section__(".modinfo"),
624__aligned__(1))) =
625#line 146
626 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
627 (char const )'=', (char const )'s', (char const )'e', (char const )'r',
628 (char const )':', (char const )'S', (char const )'e', (char const )'t',
629 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
630 (char const )' ', (char const )'s', (char const )'e', (char const )'r',
631 (char const )'i', (char const )'a', (char const )'l', (char const )' ',
632 (char const )'p', (char const )'o', (char const )'r', (char const )'t',
633 (char const )' ', (char const )'f', (char const )'o', (char const )'r',
634 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
635 (char const )' ', (char const )'s', (char const )'y', (char const )'n',
636 (char const )'t', (char const )'h', (char const )'e', (char const )'s',
637 (char const )'i', (char const )'z', (char const )'e', (char const )'r',
638 (char const )' ', (char const )'(', (char const )'0', (char const )'-',
639 (char const )'b', (char const )'a', (char const )'s', (char const )'e',
640 (char const )'d', (char const )')', (char const )'.', (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/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
642static char const __mod_start147[52] __attribute__((__used__, __unused__, __section__(".modinfo"),
643__aligned__(1))) =
644#line 147
645 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
646 (char const )'=', (char const )'s', (char const )'t', (char const )'a',
647 (char const )'r', (char const )'t', (char const )':', (char const )'S',
648 (char const )'t', (char const )'a', (char const )'r', (char const )'t',
649 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
650 (char const )' ', (char const )'s', (char const )'y', (char const )'n',
651 (char const )'t', (char const )'h', (char const )'e', (char const )'s',
652 (char const )'i', (char const )'z', (char const )'e', (char const )'r',
653 (char const )' ', (char const )'o', (char const )'n', (char const )'c',
654 (char const )'e', (char const )' ', (char const )'i', (char const )'t',
655 (char const )' ', (char const )'i', (char const )'s', (char const )' ',
656 (char const )'l', (char const )'o', (char const )'a', (char const )'d',
657 (char const )'e', (char const )'d', (char const )'.', (char const )'\000'};
658#line 149
659static int spkout_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
660#line 149 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
661static int spkout_init(void)
662{ int tmp ;
663
664 {
665 {
666#line 151
667 tmp = synth_add(& synth_spkout);
668 }
669#line 151
670 return (tmp);
671}
672}
673#line 154
674static void spkout_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
675#line 154 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
676static void spkout_exit(void)
677{
678
679 {
680 {
681#line 156
682 synth_remove(& synth_spkout);
683 }
684#line 157
685 return;
686}
687}
688#line 159 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
689int init_module(void)
690{ int tmp ;
691
692 {
693 {
694#line 159
695 tmp = spkout_init();
696 }
697#line 159
698 return (tmp);
699}
700}
701#line 160 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
702void cleanup_module(void)
703{
704
705 {
706 {
707#line 160
708 spkout_exit();
709 }
710#line 160
711 return;
712}
713}
714#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
715static char const __mod_author161[41] __attribute__((__used__, __unused__, __section__(".modinfo"),
716__aligned__(1))) =
717#line 161
718 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
719 (char const )'o', (char const )'r', (char const )'=', (char const )'K',
720 (char const )'i', (char const )'r', (char const )'k', (char const )' ',
721 (char const )'R', (char const )'e', (char const )'i', (char const )'s',
722 (char const )'e', (char const )'r', (char const )' ', (char const )'<',
723 (char const )'k', (char const )'i', (char const )'r', (char const )'k',
724 (char const )'@', (char const )'b', (char const )'r', (char const )'a',
725 (char const )'i', (char const )'l', (char const )'l', (char const )'e',
726 (char const )'.', (char const )'u', (char const )'w', (char const )'o',
727 (char const )'.', (char const )'c', (char const )'a', (char const )'>',
728 (char const )'\000'};
729#line 162 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
730static char const __mod_author162[22] __attribute__((__used__, __unused__, __section__(".modinfo"),
731__aligned__(1))) =
732#line 162
733 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
734 (char const )'o', (char const )'r', (char const )'=', (char const )'D',
735 (char const )'a', (char const )'v', (char const )'i', (char const )'d',
736 (char const )' ', (char const )'B', (char const )'o', (char const )'r',
737 (char const )'o', (char const )'w', (char const )'s', (char const )'k',
738 (char const )'i', (char const )'\000'};
739#line 163 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
740static char const __mod_description163[55] __attribute__((__used__, __unused__,
741__section__(".modinfo"), __aligned__(1))) =
742#line 163
743 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
744 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
745 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
746 (char const )'S', (char const )'p', (char const )'e', (char const )'a',
747 (char const )'k', (char const )'u', (char const )'p', (char const )' ',
748 (char const )'s', (char const )'u', (char const )'p', (char const )'p',
749 (char const )'o', (char const )'r', (char const )'t', (char const )' ',
750 (char const )'f', (char const )'o', (char const )'r', (char const )' ',
751 (char const )'S', (char const )'p', (char const )'e', (char const )'a',
752 (char const )'k', (char const )' ', (char const )'O', (char const )'u',
753 (char const )'t', (char const )' ', (char const )'s', (char const )'y',
754 (char const )'n', (char const )'t', (char const )'h', (char const )'e',
755 (char const )'s', (char const )'i', (char const )'z', (char const )'e',
756 (char const )'r', (char const )'s', (char const )'\000'};
757#line 164 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
758static char const __mod_license164[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
759__aligned__(1))) =
760#line 164
761 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
762 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
763 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
764#line 165 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
765static char const __mod_version165[13] __attribute__((__used__, __unused__, __section__(".modinfo"),
766__aligned__(1))) =
767#line 165
768 { (char const )'v', (char const )'e', (char const )'r', (char const )'s',
769 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
770 (char const )'2', (char const )'.', (char const )'1', (char const )'1',
771 (char const )'\000'};
772#line 184
773void ldv_check_final_state(void) ;
774#line 190
775extern void ldv_initialize(void) ;
776#line 193
777extern int __VERIFIER_nondet_int(void) ;
778#line 196 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
779int LDV_IN_INTERRUPT ;
780#line 199 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
781void main(void)
782{ struct spk_synth *var_group1 ;
783 int tmp ;
784 int tmp___0 ;
785 int tmp___1 ;
786
787 {
788 {
789#line 221
790 LDV_IN_INTERRUPT = 1;
791#line 230
792 ldv_initialize();
793#line 240
794 tmp = spkout_init();
795 }
796#line 240
797 if (tmp) {
798#line 241
799 goto ldv_final;
800 } else {
801
802 }
803 {
804#line 245
805 while (1) {
806 while_continue: ;
807 {
808#line 245
809 tmp___1 = __VERIFIER_nondet_int();
810 }
811#line 245
812 if (tmp___1) {
813
814 } else {
815#line 245
816 goto while_break;
817 }
818 {
819#line 248
820 tmp___0 = __VERIFIER_nondet_int();
821 }
822#line 250
823 if (tmp___0 == 0) {
824#line 250
825 goto case_0;
826 } else {
827 {
828#line 270
829 goto switch_default;
830#line 248
831 if (0) {
832 case_0:
833 {
834#line 262
835 synth_flush(var_group1);
836 }
837#line 269
838 goto switch_break;
839 switch_default:
840#line 270
841 goto switch_break;
842 } else {
843 switch_break: ;
844 }
845 }
846 }
847 }
848 while_break: ;
849 }
850 {
851#line 286
852 spkout_exit();
853 }
854 ldv_final:
855 {
856#line 289
857 ldv_check_final_state();
858 }
859#line 292
860 return;
861}
862}
863#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
864void ldv_blast_assert(void)
865{
866
867 {
868 ERROR:
869#line 6
870 goto ERROR;
871}
872}
873#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
874extern int __VERIFIER_nondet_int(void) ;
875#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
876int ldv_mutex = 1;
877#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
878int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
879{ int nondetermined ;
880
881 {
882#line 29
883 if (ldv_mutex == 1) {
884
885 } else {
886 {
887#line 29
888 ldv_blast_assert();
889 }
890 }
891 {
892#line 32
893 nondetermined = __VERIFIER_nondet_int();
894 }
895#line 35
896 if (nondetermined) {
897#line 38
898 ldv_mutex = 2;
899#line 40
900 return (0);
901 } else {
902#line 45
903 return (-4);
904 }
905}
906}
907#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
908int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
909{ int nondetermined ;
910
911 {
912#line 57
913 if (ldv_mutex == 1) {
914
915 } else {
916 {
917#line 57
918 ldv_blast_assert();
919 }
920 }
921 {
922#line 60
923 nondetermined = __VERIFIER_nondet_int();
924 }
925#line 63
926 if (nondetermined) {
927#line 66
928 ldv_mutex = 2;
929#line 68
930 return (0);
931 } else {
932#line 73
933 return (-4);
934 }
935}
936}
937#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
938int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
939{ int atomic_value_after_dec ;
940
941 {
942#line 83
943 if (ldv_mutex == 1) {
944
945 } else {
946 {
947#line 83
948 ldv_blast_assert();
949 }
950 }
951 {
952#line 86
953 atomic_value_after_dec = __VERIFIER_nondet_int();
954 }
955#line 89
956 if (atomic_value_after_dec == 0) {
957#line 92
958 ldv_mutex = 2;
959#line 94
960 return (1);
961 } else {
962
963 }
964#line 98
965 return (0);
966}
967}
968#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
969void mutex_lock(struct mutex *lock )
970{
971
972 {
973#line 108
974 if (ldv_mutex == 1) {
975
976 } else {
977 {
978#line 108
979 ldv_blast_assert();
980 }
981 }
982#line 110
983 ldv_mutex = 2;
984#line 111
985 return;
986}
987}
988#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
989int mutex_trylock(struct mutex *lock )
990{ int nondetermined ;
991
992 {
993#line 121
994 if (ldv_mutex == 1) {
995
996 } else {
997 {
998#line 121
999 ldv_blast_assert();
1000 }
1001 }
1002 {
1003#line 124
1004 nondetermined = __VERIFIER_nondet_int();
1005 }
1006#line 127
1007 if (nondetermined) {
1008#line 130
1009 ldv_mutex = 2;
1010#line 132
1011 return (1);
1012 } else {
1013#line 137
1014 return (0);
1015 }
1016}
1017}
1018#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1019void mutex_unlock(struct mutex *lock )
1020{
1021
1022 {
1023#line 147
1024 if (ldv_mutex == 2) {
1025
1026 } else {
1027 {
1028#line 147
1029 ldv_blast_assert();
1030 }
1031 }
1032#line 149
1033 ldv_mutex = 1;
1034#line 150
1035 return;
1036}
1037}
1038#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1039void ldv_check_final_state(void)
1040{
1041
1042 {
1043#line 156
1044 if (ldv_mutex == 1) {
1045
1046 } else {
1047 {
1048#line 156
1049 ldv_blast_assert();
1050 }
1051 }
1052#line 157
1053 return;
1054}
1055}
1056#line 301 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1178/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_spkout.c.common.c"
1057long s__builtin_expect(long val , long res )
1058{
1059
1060 {
1061#line 302
1062 return (val);
1063}
1064}