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 100 "include/linux/printk.h"
387extern int ( printk)(char const *fmt , ...) ;
388#line 152 "include/linux/mutex.h"
389void mutex_lock(struct mutex *lock ) ;
390#line 153
391int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock ) ;
392#line 154
393int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock ) ;
394#line 168
395int mutex_trylock(struct mutex *lock ) ;
396#line 169
397void mutex_unlock(struct mutex *lock ) ;
398#line 170
399int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock ) ;
400#line 346 "include/linux/moduleparam.h"
401extern struct kernel_param_ops param_ops_short ;
402#line 356
403extern struct kernel_param_ops param_ops_int ;
404#line 67 "include/linux/module.h"
405int init_module(void) ;
406#line 68
407void cleanup_module(void) ;
408#line 50 "/home/zakharov/launch/inst/current/envs/linux-3.4/linux-3.4/drivers/staging/speakup/spk_priv.h"
409extern unsigned char spk_serial_in(void) ;
410#line 51
411extern unsigned char spk_serial_in_nowait(void) ;
412#line 53
413extern void spk_serial_release(void) ;
414#line 59
415extern ssize_t spk_var_show(struct kobject *kobj , struct kobj_attribute *attr , char *buf ) ;
416#line 61
417extern ssize_t spk_var_store(struct kobject *kobj , struct kobj_attribute *attr ,
418 char const *buf , size_t count ) ;
419#line 64
420extern int serial_synth_probe(struct spk_synth *synth ) ;
421#line 65
422extern char const *spk_synth_immediate(struct spk_synth *synth , char const *buff ) ;
423#line 66
424extern void spk_do_catch_up(struct spk_synth *synth ) ;
425#line 67
426extern void spk_synth_flush(struct spk_synth *synth ) ;
427#line 69
428extern int spk_synth_is_alive_restart(struct spk_synth *synth ) ;
429#line 73
430extern int synth_add(struct spk_synth *in_synth ) ;
431#line 74
432extern void synth_remove(struct spk_synth *in_synth ) ;
433#line 34 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
434static int synth_probe(struct spk_synth *synth___0 ) ;
435#line 36 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
436static struct var_t vars[11] =
437#line 36
438 { {(enum var_id_t )37, {.s = {(char *)"\001+35p"}}},
439 {(enum var_id_t )38, {.s = {(char *)"\001-35p"}}},
440 {(enum var_id_t )28, {{(char *)"\001%ds", 8, 0, 9, (short)0, (short)0, (char *)((void *)0),
441 0}}},
442 {(enum var_id_t )29, {{(char *)"\001%dp", 50, 0, 99, (short)0, (short)0, (char *)((void *)0),
443 0}}},
444 {(enum var_id_t )30, {{(char *)"\001%dv", 5, 0, 9, (short)0, (short)0, (char *)((void *)0),
445 0}}},
446 {(enum var_id_t )31, {{(char *)"\001%dx", 1, 0, 2, (short)0, (short)0, (char *)((void *)0),
447 0}}},
448 {(enum var_id_t )32, {{(char *)"\001%db", 7, 0, 15, (short)0, (short)0, (char *)((void *)0),
449 0}}},
450 {(enum var_id_t )33, {{(char *)"\001%do", 0, 0, 7, (short)0, (short)0, (char *)((void *)0),
451 0}}},
452 {(enum var_id_t )34, {{(char *)"\001%df", 5, 0, 9, (short)0, (short)0, (char *)((void *)0),
453 0}}},
454 {(enum var_id_t )36, {{(char *)((void *)0), 0, 0, 1, (short)0, (short)0, (char *)((void *)0),
455 0}}},
456 {(enum var_id_t )40, {{(char *)0, 0, 0, 0, (short)0, (short)0, (char *)0, 0}}}};
457#line 53 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
458static struct kobj_attribute caps_start_attribute = {{"caps_start", (umode_t )33206}, & spk_var_show, & spk_var_store};
459#line 55 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
460static struct kobj_attribute caps_stop_attribute = {{"caps_stop", (umode_t )33206}, & spk_var_show, & spk_var_store};
461#line 57 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
462static struct kobj_attribute freq_attribute = {{"freq", (umode_t )33206}, & spk_var_show, & spk_var_store};
463#line 59 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
464static struct kobj_attribute pitch_attribute = {{"pitch", (umode_t )33206}, & spk_var_show, & spk_var_store};
465#line 61 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
466static struct kobj_attribute punct_attribute = {{"punct", (umode_t )33206}, & spk_var_show, & spk_var_store};
467#line 63 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
468static struct kobj_attribute rate_attribute = {{"rate", (umode_t )33206}, & spk_var_show, & spk_var_store};
469#line 65 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
470static struct kobj_attribute tone_attribute = {{"tone", (umode_t )33206}, & spk_var_show, & spk_var_store};
471#line 67 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
472static struct kobj_attribute voice_attribute = {{"voice", (umode_t )33206}, & spk_var_show, & spk_var_store};
473#line 69 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
474static struct kobj_attribute vol_attribute = {{"vol", (umode_t )33206}, & spk_var_show, & spk_var_store};
475#line 72 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
476static struct kobj_attribute delay_time_attribute = {{"delay_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
477#line 74 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
478static struct kobj_attribute direct_attribute = {{"direct", (umode_t )33206}, & spk_var_show, & spk_var_store};
479#line 76 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
480static struct kobj_attribute full_time_attribute = {{"full_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
481#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
482static struct kobj_attribute jiffy_delta_attribute = {{"jiffy_delta", (umode_t )33188}, & spk_var_show, & spk_var_store};
483#line 80 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
484static struct kobj_attribute trigger_time_attribute = {{"trigger_time", (umode_t )33188}, & spk_var_show, & spk_var_store};
485#line 87 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
486static struct attribute *synth_attrs[15] =
487#line 87
488 { & caps_start_attribute.attr, & caps_stop_attribute.attr, & freq_attribute.attr, & pitch_attribute.attr,
489 & punct_attribute.attr, & rate_attribute.attr, & tone_attribute.attr, & voice_attribute.attr,
490 & vol_attribute.attr, & delay_time_attribute.attr, & direct_attribute.attr, & full_time_attribute.attr,
491 & jiffy_delta_attribute.attr, & trigger_time_attribute.attr, (struct attribute *)((void *)0)};
492#line 105 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
493static struct spk_synth synth_ltlk =
494#line 105
495 {"ltlk", "2.11", "LiteTalk", "\001@\0011y\n\000", (char)13, (char)24, 500, 50,
496 50, 40000, 0, (short)0, (short)1, (int const )20030716, vars, (int *)0, (int *)0,
497 & synth_probe, & spk_serial_release, & spk_synth_immediate, & spk_do_catch_up,
498 & spk_synth_flush, & spk_synth_is_alive_restart, (int (*)(struct st_var_header *var ))((void *)0),
499 (void (*)(u_char ))((void *)0), & spk_serial_in_nowait, {(char *)"\001%di", (unsigned char)1,
500 (unsigned char)5, (unsigned char)1},
501 0, {"ltlk", (umode_t (*)(struct kobject * , struct attribute * , int ))0, synth_attrs}};
502#line 141 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
503static void synth_interrogate(struct spk_synth *synth___0 )
504{ unsigned char *t ;
505 unsigned char i ;
506 unsigned char buf[50] ;
507 unsigned char rom_v[20] ;
508 int __cil_tmp6 ;
509 unsigned long __cil_tmp7 ;
510 unsigned long __cil_tmp8 ;
511 int __cil_tmp9 ;
512 unsigned long __cil_tmp10 ;
513 unsigned long __cil_tmp11 ;
514 unsigned char __cil_tmp12 ;
515 int __cil_tmp13 ;
516 int __cil_tmp14 ;
517 int __cil_tmp15 ;
518 unsigned long __cil_tmp16 ;
519 unsigned long __cil_tmp17 ;
520 unsigned char *__cil_tmp18 ;
521 unsigned char __cil_tmp19 ;
522 int __cil_tmp20 ;
523 unsigned long __cil_tmp21 ;
524 unsigned long __cil_tmp22 ;
525 int __cil_tmp23 ;
526 int __cil_tmp24 ;
527 unsigned long __cil_tmp25 ;
528 unsigned long __cil_tmp26 ;
529 unsigned long __cil_tmp27 ;
530 unsigned long __cil_tmp28 ;
531 char const *__cil_tmp29 ;
532 unsigned long __cil_tmp30 ;
533 unsigned long __cil_tmp31 ;
534 unsigned char *__cil_tmp32 ;
535
536 {
537 {
538#line 145
539 spk_synth_immediate(synth___0, "\030\001?");
540#line 146
541 i = (unsigned char)0;
542 }
543 {
544#line 146
545 while (1) {
546 while_continue: ;
547 {
548#line 146
549 __cil_tmp6 = (int )i;
550#line 146
551 if (__cil_tmp6 < 50) {
552
553 } else {
554#line 146
555 goto while_break;
556 }
557 }
558 {
559#line 147
560 __cil_tmp7 = i * 1UL;
561#line 147
562 __cil_tmp8 = (unsigned long )(buf) + __cil_tmp7;
563#line 147
564 *((unsigned char *)__cil_tmp8) = spk_serial_in();
565 }
566 {
567#line 148
568 __cil_tmp9 = (int )i;
569#line 148
570 if (__cil_tmp9 > 2) {
571 {
572#line 148
573 __cil_tmp10 = i * 1UL;
574#line 148
575 __cil_tmp11 = (unsigned long )(buf) + __cil_tmp10;
576#line 148
577 __cil_tmp12 = *((unsigned char *)__cil_tmp11);
578#line 148
579 __cil_tmp13 = (int )__cil_tmp12;
580#line 148
581 if (__cil_tmp13 == 127) {
582#line 149
583 goto while_break;
584 } else {
585
586 }
587 }
588 } else {
589
590 }
591 }
592#line 146
593 __cil_tmp14 = (int )i;
594#line 146
595 __cil_tmp15 = __cil_tmp14 + 1;
596#line 146
597 i = (unsigned char )__cil_tmp15;
598 }
599 while_break: ;
600 }
601#line 151
602 __cil_tmp16 = 0 * 1UL;
603#line 151
604 __cil_tmp17 = (unsigned long )(buf) + __cil_tmp16;
605#line 151
606 __cil_tmp18 = (unsigned char *)__cil_tmp17;
607#line 151
608 t = __cil_tmp18 + 2;
609#line 152
610 i = (unsigned char)0;
611 {
612#line 152
613 while (1) {
614 while_continue___0: ;
615 {
616#line 152
617 __cil_tmp19 = *t;
618#line 152
619 __cil_tmp20 = (int )__cil_tmp19;
620#line 152
621 if (__cil_tmp20 != 13) {
622
623 } else {
624#line 152
625 goto while_break___0;
626 }
627 }
628#line 153
629 __cil_tmp21 = i * 1UL;
630#line 153
631 __cil_tmp22 = (unsigned long )(rom_v) + __cil_tmp21;
632#line 153
633 *((unsigned char *)__cil_tmp22) = *t;
634#line 154
635 __cil_tmp23 = (int )i;
636#line 154
637 __cil_tmp24 = __cil_tmp23 + 1;
638#line 154
639 i = (unsigned char )__cil_tmp24;
640#line 154
641 if (i >= 19) {
642#line 155
643 goto while_break___0;
644 } else {
645
646 }
647#line 152
648 t = t + 1;
649 }
650 while_break___0: ;
651 }
652 {
653#line 157
654 __cil_tmp25 = i * 1UL;
655#line 157
656 __cil_tmp26 = (unsigned long )(rom_v) + __cil_tmp25;
657#line 157
658 *((unsigned char *)__cil_tmp26) = (unsigned char)0;
659#line 158
660 __cil_tmp27 = (unsigned long )synth___0;
661#line 158
662 __cil_tmp28 = __cil_tmp27 + 16;
663#line 158
664 __cil_tmp29 = *((char const **)__cil_tmp28);
665#line 158
666 __cil_tmp30 = 0 * 1UL;
667#line 158
668 __cil_tmp31 = (unsigned long )(rom_v) + __cil_tmp30;
669#line 158
670 __cil_tmp32 = (unsigned char *)__cil_tmp31;
671#line 158
672 printk("<6>%s: ROM version: %s\n", __cil_tmp29, __cil_tmp32);
673 }
674#line 159
675 return;
676}
677}
678#line 161 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
679static int synth_probe(struct spk_synth *synth___0 )
680{ int failed ;
681 unsigned long __cil_tmp3 ;
682 unsigned long __cil_tmp4 ;
683
684 {
685 {
686#line 163
687 failed = 0;
688#line 165
689 failed = serial_synth_probe(synth___0);
690 }
691#line 166
692 if (failed == 0) {
693 {
694#line 167
695 synth_interrogate(synth___0);
696 }
697 } else {
698
699 }
700#line 168
701 __cil_tmp3 = (unsigned long )synth___0;
702#line 168
703 __cil_tmp4 = __cil_tmp3 + 176;
704#line 168
705 *((int *)__cil_tmp4) = ! failed;
706#line 169
707 return (failed);
708}
709}
710#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
711static char const __param_str_ser[4] = { (char const )'s', (char const )'e', (char const )'r', (char const )'\000'};
712#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
713static struct kernel_param const __param_ser __attribute__((__used__, __unused__,
714__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_ser, (struct kernel_param_ops const *)(& param_ops_int), (u16 )292,
715 (s16 )0, {(void *)(& synth_ltlk.ser)}};
716#line 172 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
717static char const __mod_sertype172[17] __attribute__((__used__, __unused__, __section__(".modinfo"),
718__aligned__(1))) =
719#line 172
720 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
721 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
722 (char const )'=', (char const )'s', (char const )'e', (char const )'r',
723 (char const )':', (char const )'i', (char const )'n', (char const )'t',
724 (char const )'\000'};
725#line 173 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
726static char const __param_str_start[6] = { (char const )'s', (char const )'t', (char const )'a', (char const )'r',
727 (char const )'t', (char const )'\000'};
728#line 173 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
729static struct kernel_param const __param_start __attribute__((__used__, __unused__,
730__section__("__param"), __aligned__(sizeof(void *)))) = {__param_str_start, (struct kernel_param_ops const *)(& param_ops_short), (u16 )292,
731 (s16 )0, {(void *)(& synth_ltlk.startup)}};
732#line 173 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
733static char const __mod_starttype173[21] __attribute__((__used__, __unused__, __section__(".modinfo"),
734__aligned__(1))) =
735#line 173
736 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
737 (char const )'t', (char const )'y', (char const )'p', (char const )'e',
738 (char const )'=', (char const )'s', (char const )'t', (char const )'a',
739 (char const )'r', (char const )'t', (char const )':', (char const )'s',
740 (char const )'h', (char const )'o', (char const )'r', (char const )'t',
741 (char const )'\000'};
742#line 175 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
743static char const __mod_ser175[60] __attribute__((__used__, __unused__, __section__(".modinfo"),
744__aligned__(1))) =
745#line 175
746 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
747 (char const )'=', (char const )'s', (char const )'e', (char const )'r',
748 (char const )':', (char const )'S', (char const )'e', (char const )'t',
749 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
750 (char const )' ', (char const )'s', (char const )'e', (char const )'r',
751 (char const )'i', (char const )'a', (char const )'l', (char const )' ',
752 (char const )'p', (char const )'o', (char const )'r', (char const )'t',
753 (char const )' ', (char const )'f', (char const )'o', (char const )'r',
754 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
755 (char const )' ', (char const )'s', (char const )'y', (char const )'n',
756 (char const )'t', (char const )'h', (char const )'e', (char const )'s',
757 (char const )'i', (char const )'z', (char const )'e', (char const )'r',
758 (char const )' ', (char const )'(', (char const )'0', (char const )'-',
759 (char const )'b', (char const )'a', (char const )'s', (char const )'e',
760 (char const )'d', (char const )')', (char const )'.', (char const )'\000'};
761#line 176 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
762static char const __mod_start176[52] __attribute__((__used__, __unused__, __section__(".modinfo"),
763__aligned__(1))) =
764#line 176
765 { (char const )'p', (char const )'a', (char const )'r', (char const )'m',
766 (char const )'=', (char const )'s', (char const )'t', (char const )'a',
767 (char const )'r', (char const )'t', (char const )':', (char const )'S',
768 (char const )'t', (char const )'a', (char const )'r', (char const )'t',
769 (char const )' ', (char const )'t', (char const )'h', (char const )'e',
770 (char const )' ', (char const )'s', (char const )'y', (char const )'n',
771 (char const )'t', (char const )'h', (char const )'e', (char const )'s',
772 (char const )'i', (char const )'z', (char const )'e', (char const )'r',
773 (char const )' ', (char const )'o', (char const )'n', (char const )'c',
774 (char const )'e', (char const )' ', (char const )'i', (char const )'t',
775 (char const )' ', (char const )'i', (char const )'s', (char const )' ',
776 (char const )'l', (char const )'o', (char const )'a', (char const )'d',
777 (char const )'e', (char const )'d', (char const )'.', (char const )'\000'};
778#line 178
779static int ltlk_init(void) __attribute__((__section__(".init.text"), __no_instrument_function__)) ;
780#line 178 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
781static int ltlk_init(void)
782{ int tmp ;
783
784 {
785 {
786#line 180
787 tmp = synth_add(& synth_ltlk);
788 }
789#line 180
790 return (tmp);
791}
792}
793#line 183
794static void ltlk_exit(void) __attribute__((__section__(".exit.text"), __no_instrument_function__)) ;
795#line 183 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
796static void ltlk_exit(void)
797{
798
799 {
800 {
801#line 185
802 synth_remove(& synth_ltlk);
803 }
804#line 186
805 return;
806}
807}
808#line 188 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
809int init_module(void)
810{ int tmp ;
811
812 {
813 {
814#line 188
815 tmp = ltlk_init();
816 }
817#line 188
818 return (tmp);
819}
820}
821#line 189 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
822void cleanup_module(void)
823{
824
825 {
826 {
827#line 189
828 ltlk_exit();
829 }
830#line 189
831 return;
832}
833}
834#line 190 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
835static char const __mod_author190[41] __attribute__((__used__, __unused__, __section__(".modinfo"),
836__aligned__(1))) =
837#line 190
838 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
839 (char const )'o', (char const )'r', (char const )'=', (char const )'K',
840 (char const )'i', (char const )'r', (char const )'k', (char const )' ',
841 (char const )'R', (char const )'e', (char const )'i', (char const )'s',
842 (char const )'e', (char const )'r', (char const )' ', (char const )'<',
843 (char const )'k', (char const )'i', (char const )'r', (char const )'k',
844 (char const )'@', (char const )'b', (char const )'r', (char const )'a',
845 (char const )'i', (char const )'l', (char const )'l', (char const )'e',
846 (char const )'.', (char const )'u', (char const )'w', (char const )'o',
847 (char const )'.', (char const )'c', (char const )'a', (char const )'>',
848 (char const )'\000'};
849#line 191 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
850static char const __mod_author191[22] __attribute__((__used__, __unused__, __section__(".modinfo"),
851__aligned__(1))) =
852#line 191
853 { (char const )'a', (char const )'u', (char const )'t', (char const )'h',
854 (char const )'o', (char const )'r', (char const )'=', (char const )'D',
855 (char const )'a', (char const )'v', (char const )'i', (char const )'d',
856 (char const )' ', (char const )'B', (char const )'o', (char const )'r',
857 (char const )'o', (char const )'w', (char const )'s', (char const )'k',
858 (char const )'i', (char const )'\000'};
859#line 192 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
860static char const __mod_description192[68] __attribute__((__used__, __unused__,
861__section__(".modinfo"), __aligned__(1))) =
862#line 192
863 { (char const )'d', (char const )'e', (char const )'s', (char const )'c',
864 (char const )'r', (char const )'i', (char const )'p', (char const )'t',
865 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
866 (char const )'S', (char const )'p', (char const )'e', (char const )'a',
867 (char const )'k', (char const )'u', (char const )'p', (char const )' ',
868 (char const )'s', (char const )'u', (char const )'p', (char const )'p',
869 (char const )'o', (char const )'r', (char const )'t', (char const )' ',
870 (char const )'f', (char const )'o', (char const )'r', (char const )' ',
871 (char const )'D', (char const )'o', (char const )'u', (char const )'b',
872 (char const )'l', (char const )'e', (char const )'T', (char const )'a',
873 (char const )'l', (char const )'k', (char const )' ', (char const )'L',
874 (char const )'T', (char const )'/', (char const )'L', (char const )'i',
875 (char const )'t', (char const )'e', (char const )'T', (char const )'a',
876 (char const )'l', (char const )'k', (char const )' ', (char const )'s',
877 (char const )'y', (char const )'n', (char const )'t', (char const )'h',
878 (char const )'e', (char const )'s', (char const )'i', (char const )'z',
879 (char const )'e', (char const )'r', (char const )'s', (char const )'\000'};
880#line 193 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
881static char const __mod_license193[12] __attribute__((__used__, __unused__, __section__(".modinfo"),
882__aligned__(1))) =
883#line 193
884 { (char const )'l', (char const )'i', (char const )'c', (char const )'e',
885 (char const )'n', (char const )'s', (char const )'e', (char const )'=',
886 (char const )'G', (char const )'P', (char const )'L', (char const )'\000'};
887#line 194 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
888static char const __mod_version194[13] __attribute__((__used__, __unused__, __section__(".modinfo"),
889__aligned__(1))) =
890#line 194
891 { (char const )'v', (char const )'e', (char const )'r', (char const )'s',
892 (char const )'i', (char const )'o', (char const )'n', (char const )'=',
893 (char const )'2', (char const )'.', (char const )'1', (char const )'1',
894 (char const )'\000'};
895#line 213
896void ldv_check_final_state(void) ;
897#line 216
898extern void ldv_check_return_value(int res ) ;
899#line 219
900extern void ldv_initialize(void) ;
901#line 222
902extern int __VERIFIER_nondet_int(void) ;
903#line 225 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
904int LDV_IN_INTERRUPT ;
905#line 243 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
906static int res_synth_probe_1 ;
907#line 228 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
908void main(void)
909{ struct spk_synth *var_group1 ;
910 int tmp ;
911 int ldv_s_synth_ltlk_spk_synth ;
912 int tmp___0 ;
913 int tmp___1 ;
914 int __cil_tmp6 ;
915
916 {
917 {
918#line 251
919 LDV_IN_INTERRUPT = 1;
920#line 260
921 ldv_initialize();
922#line 269
923 tmp = ltlk_init();
924 }
925#line 269
926 if (tmp) {
927#line 270
928 goto ldv_final;
929 } else {
930
931 }
932#line 271
933 ldv_s_synth_ltlk_spk_synth = 0;
934 {
935#line 274
936 while (1) {
937 while_continue: ;
938 {
939#line 274
940 tmp___1 = __VERIFIER_nondet_int();
941 }
942#line 274
943 if (tmp___1) {
944
945 } else {
946 {
947#line 274
948 __cil_tmp6 = ldv_s_synth_ltlk_spk_synth == 0;
949#line 274
950 if (! __cil_tmp6) {
951
952 } else {
953#line 274
954 goto while_break;
955 }
956 }
957 }
958 {
959#line 278
960 tmp___0 = __VERIFIER_nondet_int();
961 }
962#line 280
963 if (tmp___0 == 0) {
964#line 280
965 goto case_0;
966 } else {
967 {
968#line 302
969 goto switch_default;
970#line 278
971 if (0) {
972 case_0:
973#line 283
974 if (ldv_s_synth_ltlk_spk_synth == 0) {
975 {
976#line 291
977 res_synth_probe_1 = synth_probe(var_group1);
978#line 292
979 ldv_check_return_value(res_synth_probe_1);
980 }
981#line 293
982 if (res_synth_probe_1) {
983#line 294
984 goto ldv_module_exit;
985 } else {
986
987 }
988#line 295
989 ldv_s_synth_ltlk_spk_synth = 0;
990 } else {
991
992 }
993#line 301
994 goto switch_break;
995 switch_default:
996#line 302
997 goto switch_break;
998 } else {
999 switch_break: ;
1000 }
1001 }
1002 }
1003 }
1004 while_break: ;
1005 }
1006 ldv_module_exit:
1007 {
1008#line 317
1009 ltlk_exit();
1010 }
1011 ldv_final:
1012 {
1013#line 320
1014 ldv_check_final_state();
1015 }
1016#line 323
1017 return;
1018}
1019}
1020#line 5 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast-assert.h"
1021void ldv_blast_assert(void)
1022{
1023
1024 {
1025 ERROR:
1026#line 6
1027 goto ERROR;
1028}
1029}
1030#line 6 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/engine-blast.h"
1031extern int __VERIFIER_nondet_int(void) ;
1032#line 19 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1033int ldv_mutex = 1;
1034#line 22 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1035int __attribute__((__warn_unused_result__)) mutex_lock_interruptible(struct mutex *lock )
1036{ int nondetermined ;
1037
1038 {
1039#line 29
1040 if (ldv_mutex == 1) {
1041
1042 } else {
1043 {
1044#line 29
1045 ldv_blast_assert();
1046 }
1047 }
1048 {
1049#line 32
1050 nondetermined = __VERIFIER_nondet_int();
1051 }
1052#line 35
1053 if (nondetermined) {
1054#line 38
1055 ldv_mutex = 2;
1056#line 40
1057 return (0);
1058 } else {
1059#line 45
1060 return (-4);
1061 }
1062}
1063}
1064#line 50 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1065int __attribute__((__warn_unused_result__)) mutex_lock_killable(struct mutex *lock )
1066{ int nondetermined ;
1067
1068 {
1069#line 57
1070 if (ldv_mutex == 1) {
1071
1072 } else {
1073 {
1074#line 57
1075 ldv_blast_assert();
1076 }
1077 }
1078 {
1079#line 60
1080 nondetermined = __VERIFIER_nondet_int();
1081 }
1082#line 63
1083 if (nondetermined) {
1084#line 66
1085 ldv_mutex = 2;
1086#line 68
1087 return (0);
1088 } else {
1089#line 73
1090 return (-4);
1091 }
1092}
1093}
1094#line 78 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1095int atomic_dec_and_mutex_lock(atomic_t *cnt , struct mutex *lock )
1096{ int atomic_value_after_dec ;
1097
1098 {
1099#line 83
1100 if (ldv_mutex == 1) {
1101
1102 } else {
1103 {
1104#line 83
1105 ldv_blast_assert();
1106 }
1107 }
1108 {
1109#line 86
1110 atomic_value_after_dec = __VERIFIER_nondet_int();
1111 }
1112#line 89
1113 if (atomic_value_after_dec == 0) {
1114#line 92
1115 ldv_mutex = 2;
1116#line 94
1117 return (1);
1118 } else {
1119
1120 }
1121#line 98
1122 return (0);
1123}
1124}
1125#line 103 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1126void mutex_lock(struct mutex *lock )
1127{
1128
1129 {
1130#line 108
1131 if (ldv_mutex == 1) {
1132
1133 } else {
1134 {
1135#line 108
1136 ldv_blast_assert();
1137 }
1138 }
1139#line 110
1140 ldv_mutex = 2;
1141#line 111
1142 return;
1143}
1144}
1145#line 114 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1146int mutex_trylock(struct mutex *lock )
1147{ int nondetermined ;
1148
1149 {
1150#line 121
1151 if (ldv_mutex == 1) {
1152
1153 } else {
1154 {
1155#line 121
1156 ldv_blast_assert();
1157 }
1158 }
1159 {
1160#line 124
1161 nondetermined = __VERIFIER_nondet_int();
1162 }
1163#line 127
1164 if (nondetermined) {
1165#line 130
1166 ldv_mutex = 2;
1167#line 132
1168 return (1);
1169 } else {
1170#line 137
1171 return (0);
1172 }
1173}
1174}
1175#line 142 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1176void mutex_unlock(struct mutex *lock )
1177{
1178
1179 {
1180#line 147
1181 if (ldv_mutex == 2) {
1182
1183 } else {
1184 {
1185#line 147
1186 ldv_blast_assert();
1187 }
1188 }
1189#line 149
1190 ldv_mutex = 1;
1191#line 150
1192 return;
1193}
1194}
1195#line 153 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/kernel-rules/files/model0032.c"
1196void ldv_check_final_state(void)
1197{
1198
1199 {
1200#line 156
1201 if (ldv_mutex == 1) {
1202
1203 } else {
1204 {
1205#line 156
1206 ldv_blast_assert();
1207 }
1208 }
1209#line 157
1210 return;
1211}
1212}
1213#line 332 "/home/zakharov/launch/work/current--X--drivers/--X--defaultlinux-3.4--X--32_1--X--cpachecker/linux-3.4/csd_deg_dscv/1176/dscv_tempdir/dscv/ri/32_1/drivers/staging/speakup/speakup_ltlk.c.common.c"
1214long s__builtin_expect(long val , long res )
1215{
1216
1217 {
1218#line 333
1219 return (val);
1220}
1221}