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