1
2
3
4#line 4 "/ddverify-2010-04-30/models/seq1/include/asm/posix_types.h"
5typedef unsigned long __kernel_ino_t;
6#line 5 "/ddverify-2010-04-30/models/seq1/include/asm/posix_types.h"
7typedef unsigned short __kernel_mode_t;
8#line 7 "/ddverify-2010-04-30/models/seq1/include/asm/posix_types.h"
9typedef long __kernel_off_t;
10#line 12 "/ddverify-2010-04-30/models/seq1/include/asm/posix_types.h"
11typedef unsigned int __kernel_size_t;
12#line 13 "/ddverify-2010-04-30/models/seq1/include/asm/posix_types.h"
13typedef int __kernel_ssize_t;
14#line 4 "/ddverify-2010-04-30/models/seq1/include/asm/types.h"
15typedef unsigned short umode_t;
16#line 7 "/ddverify-2010-04-30/models/seq1/include/asm/types.h"
17typedef unsigned char __u8;
18#line 13 "/ddverify-2010-04-30/models/seq1/include/asm/types.h"
19typedef unsigned int __u32;
20#line 30 "/ddverify-2010-04-30/models/seq1/include/asm/types.h"
21typedef unsigned long long u64;
22#line 9 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
23typedef __u32 __kernel_dev_t;
24#line 11 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
25typedef __kernel_dev_t dev_t;
26#line 12 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
27typedef __kernel_ino_t ino_t;
28#line 13 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
29typedef __kernel_mode_t mode_t;
30#line 15 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
31typedef __kernel_off_t off_t;
32#line 30 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
33typedef long long loff_t;
34#line 38 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
35typedef __kernel_size_t size_t;
36#line 43 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
37typedef __kernel_ssize_t ssize_t;
38#line 88 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
39typedef unsigned int gfp_t;
40#line 91 "/ddverify-2010-04-30/models/seq1/include/linux/types.h"
41typedef unsigned long sector_t;
42#line 4 "/ddverify-2010-04-30/models/seq1/include/linux/timer.h"
43struct timer_list {
44 unsigned long expires ;
45 void (*function)(unsigned long ) ;
46 unsigned long data ;
47 short __ddv_active ;
48 short __ddv_init ;
49};
50#line 4 "/ddverify-2010-04-30/models/seq1/include/linux/spinlock_types.h"
51struct __anonstruct_spinlock_t_1 {
52 int init ;
53 int locked ;
54};
55#line 4 "/ddverify-2010-04-30/models/seq1/include/linux/spinlock_types.h"
56typedef struct __anonstruct_spinlock_t_1 spinlock_t;
57#line 9 "/ddverify-2010-04-30/models/seq1/include/linux/list.h"
58struct list_head {
59 struct list_head *next ;
60 struct list_head *prev ;
61};
62#line 16 "/ddverify-2010-04-30/models/seq1/include/linux/wait.h"
63struct __wait_queue_head {
64 int number_process_waiting ;
65 int wakeup ;
66 int init ;
67};
68#line 22 "/ddverify-2010-04-30/models/seq1/include/linux/wait.h"
69typedef struct __wait_queue_head wait_queue_head_t;
70#line 25 "/ddverify-2010-04-30/models/seq1/include/ddverify/pthread.h"
71struct __pthread_mutex_t_struct {
72 _Bool locked ;
73};
74#line 30 "/ddverify-2010-04-30/models/seq1/include/ddverify/pthread.h"
75struct __pthread_mutexattr_t_struct {
76 int dummy ;
77};
78#line 52 "/ddverify-2010-04-30/models/seq1/include/ddverify/pthread.h"
79typedef struct __pthread_mutex_t_struct pthread_mutex_t;
80#line 53 "/ddverify-2010-04-30/models/seq1/include/ddverify/pthread.h"
81typedef struct __pthread_mutexattr_t_struct pthread_mutexattr_t;
82#line 6 "/ddverify-2010-04-30/models/seq1/include/asm/atomic.h"
83typedef int atomic_t;
84#line 67 "/ddverify-2010-04-30/models/seq1/include/linux/gfp.h"
85struct page;
86#line 24 "/ddverify-2010-04-30/models/seq1/include/linux/module.h"
87struct module {
88 int something ;
89};
90#line 34 "/ddverify-2010-04-30/models/seq1/include/linux/miscdevice.h"
91struct file_operations;
92#line 34 "/ddverify-2010-04-30/models/seq1/include/linux/miscdevice.h"
93struct miscdevice {
94 int minor ;
95 char const *name ;
96 struct file_operations *fops ;
97};
98#line 9 "/ddverify-2010-04-30/models/seq1/include/linux/watchdog.h"
99struct watchdog_info {
100 __u32 options ;
101 __u32 firmware_version ;
102 __u8 identity[32] ;
103};
104#line 4 "/ddverify-2010-04-30/models/seq1/include/linux/dcache.h"
105struct inode;
106#line 4 "/ddverify-2010-04-30/models/seq1/include/linux/dcache.h"
107struct dentry {
108 struct inode *d_inode ;
109};
110#line 4 "/ddverify-2010-04-30/models/seq1/include/asm/semaphore.h"
111struct semaphore {
112 int init ;
113 int locked ;
114};
115#line 82 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
116struct hd_geometry;
117#line 82
118struct hd_geometry;
119#line 83
120struct iovec;
121#line 83
122struct iovec;
123#line 84
124struct poll_table_struct;
125#line 84
126struct poll_table_struct;
127#line 85
128struct vm_area_struct;
129#line 85
130struct vm_area_struct;
131#line 87
132struct page;
133#line 90 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
134struct address_space {
135 struct inode *host ;
136};
137#line 94 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
138struct file {
139 struct dentry *f_dentry ;
140 struct file_operations *f_op ;
141 atomic_t f_count ;
142 unsigned int f_flags ;
143 mode_t f_mode ;
144 loff_t f_pos ;
145 void *private_data ;
146 struct address_space *f_mapping ;
147};
148#line 105
149struct gendisk;
150#line 105 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
151struct block_device {
152 struct inode *bd_inode ;
153 struct gendisk *bd_disk ;
154 struct block_device *bd_contains ;
155 unsigned int bd_block_size ;
156};
157#line 113
158struct cdev;
159#line 113 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
160struct inode {
161 umode_t i_mode ;
162 struct block_device *i_bdev ;
163 dev_t i_rdev ;
164 loff_t i_size ;
165 struct cdev *i_cdev ;
166};
167#line 122 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
168struct __anonstruct_read_descriptor_t_12 {
169 size_t written ;
170 size_t count ;
171};
172#line 122 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
173typedef struct __anonstruct_read_descriptor_t_12 read_descriptor_t;
174#line 130 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
175struct file_lock {
176 int something ;
177};
178#line 134 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
179struct file_operations {
180 struct module *owner ;
181 loff_t (*llseek)(struct file * , loff_t , int ) ;
182 ssize_t (*read)(struct file * , char * , size_t , loff_t * ) ;
183 ssize_t (*write)(struct file * , char const * , size_t , loff_t * ) ;
184 int (*readdir)(struct file * , void * , int (*)(void * , char const * , int ,
185 loff_t , ino_t , unsigned int ) ) ;
186 unsigned int (*poll)(struct file * , struct poll_table_struct * ) ;
187 int (*ioctl)(struct inode * , struct file * , unsigned int , unsigned long ) ;
188 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
189 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
190 int (*mmap)(struct file * , struct vm_area_struct * ) ;
191 int (*open)(struct inode * , struct file * ) ;
192 int (*flush)(struct file * ) ;
193 int (*release)(struct inode * , struct file * ) ;
194 int (*fsync)(struct file * , struct dentry * , int datasync ) ;
195 int (*fasync)(int , struct file * , int ) ;
196 int (*lock)(struct file * , int , struct file_lock * ) ;
197 ssize_t (*readv)(struct file * , struct iovec const * , unsigned long , loff_t * ) ;
198 ssize_t (*writev)(struct file * , struct iovec const * , unsigned long , loff_t * ) ;
199 ssize_t (*sendfile)(struct file * , loff_t * , size_t , int (*)(read_descriptor_t * ,
200 struct page * ,
201 unsigned long ,
202 unsigned long ) ,
203 void * ) ;
204 ssize_t (*sendpage)(struct file * , struct page * , int , size_t , loff_t * ,
205 int ) ;
206 unsigned long (*get_unmapped_area)(struct file * , unsigned long , unsigned long ,
207 unsigned long , unsigned long ) ;
208 int (*check_flags)(int ) ;
209 int (*dir_notify)(struct file *filp , unsigned long arg ) ;
210 int (*flock)(struct file * , int , struct file_lock * ) ;
211 int (*open_exec)(struct inode * ) ;
212};
213#line 168 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
214struct block_device_operations {
215 int (*open)(struct inode * , struct file * ) ;
216 int (*release)(struct inode * , struct file * ) ;
217 int (*ioctl)(struct inode * , struct file * , unsigned int , unsigned long ) ;
218 long (*unlocked_ioctl)(struct file * , unsigned int , unsigned long ) ;
219 long (*compat_ioctl)(struct file * , unsigned int , unsigned long ) ;
220 int (*direct_access)(struct block_device * , sector_t , unsigned long * ) ;
221 int (*media_changed)(struct gendisk * ) ;
222 int (*revalidate_disk)(struct gendisk * ) ;
223 int (*getgeo)(struct block_device * , struct hd_geometry * ) ;
224 struct module *owner ;
225};
226#line 18 "/ddverify-2010-04-30/models/seq1/include/linux/ioport.h"
227struct resource {
228 char const *name ;
229 unsigned long start ;
230 unsigned long end ;
231 unsigned long flags ;
232};
233#line 15 "/ddverify-2010-04-30/models/seq1/include/linux/notifier.h"
234struct notifier_block {
235 int (*notifier_call)(struct notifier_block *self , unsigned long , void * ) ;
236 struct notifier_block *next ;
237 int priority ;
238};
239#line 53 "/ddverify-2010-04-30/models/seq1/include/linux/reboot.h"
240struct pt_regs;
241#line 53
242struct pt_regs;
243#line 4 "/ddverify-2010-04-30/models/seq1/include/linux/cdev.h"
244struct cdev {
245 struct module *owner ;
246 struct file_operations *ops ;
247 dev_t dev ;
248 unsigned int count ;
249};
250#line 13 "/ddverify-2010-04-30/models/seq1/include/ddverify/cdev.h"
251struct ddv_cdev {
252 struct cdev *cdevp ;
253 struct file filp ;
254 struct inode inode ;
255 int open ;
256};
257#line 8 "/ddverify-2010-04-30/models/seq1/include/linux/sysfs.h"
258struct module;
259#line 8 "/ddverify-2010-04-30/models/seq1/include/linux/pm.h"
260struct pm_message {
261 int event ;
262};
263#line 8 "/ddverify-2010-04-30/models/seq1/include/linux/pm.h"
264typedef struct pm_message pm_message_t;
265#line 25 "/ddverify-2010-04-30/models/seq1/include/linux/device.h"
266struct device {
267 void *driver_data ;
268 void (*release)(struct device *dev ) ;
269};
270#line 17 "/ddverify-2010-04-30/models/seq1/include/linux/genhd.h"
271struct request_queue;
272#line 17 "/ddverify-2010-04-30/models/seq1/include/linux/genhd.h"
273struct gendisk {
274 int major ;
275 int first_minor ;
276 int minors ;
277 char disk_name[32] ;
278 struct block_device_operations *fops ;
279 struct request_queue *queue ;
280 void *private_data ;
281 int flags ;
282 struct device *driverfs_dev ;
283 char devfs_name[64] ;
284};
285#line 12 "/ddverify-2010-04-30/models/seq1/include/linux/workqueue.h"
286struct work_struct {
287 unsigned long pending ;
288 void (*func)(void * ) ;
289 void *data ;
290 int init ;
291};
292#line 20 "/ddverify-2010-04-30/models/seq1/include/linux/mutex.h"
293struct mutex {
294 int locked ;
295 int init ;
296};
297#line 9 "/ddverify-2010-04-30/models/seq1/include/linux/mm_types.h"
298struct page {
299 int something ;
300};
301#line 4 "/ddverify-2010-04-30/models/seq1/include/asm/ptrace.h"
302struct pt_regs {
303 int something ;
304};
305#line 28 "/ddverify-2010-04-30/models/seq1/include/linux/interrupt.h"
306typedef int irqreturn_t;
307#line 34 "/ddverify-2010-04-30/models/seq1/include/linux/interrupt.h"
308struct tasklet_struct {
309 atomic_t count ;
310 void (*func)(unsigned long ) ;
311 unsigned long data ;
312 int init ;
313};
314#line 11 "/ddverify-2010-04-30/models/seq1/include/linux/backing-dev.h"
315struct backing_dev_info {
316 unsigned long ra_pages ;
317 unsigned long state ;
318 unsigned int capabilities ;
319};
320#line 6 "/ddverify-2010-04-30/models/seq1/include/linux/bio.h"
321struct bio_vec {
322 struct page *bv_page ;
323 unsigned int bv_len ;
324 unsigned int bv_offset ;
325};
326#line 13
327struct bio;
328#line 13
329struct bio;
330#line 14 "/ddverify-2010-04-30/models/seq1/include/linux/bio.h"
331typedef int bio_end_io_t(struct bio * , unsigned int , int );
332#line 17 "/ddverify-2010-04-30/models/seq1/include/linux/bio.h"
333struct bio {
334 sector_t bi_sector ;
335 struct bio *bi_next ;
336 struct block_device *bi_bdev ;
337 unsigned long bi_flags ;
338 unsigned long bi_rw ;
339 unsigned short bi_vcnt ;
340 unsigned short bi_idx ;
341 unsigned short bi_phys_segments ;
342 unsigned int bi_size ;
343 struct bio_vec *bi_io_vec ;
344 bio_end_io_t *bi_end_io ;
345 void *bi_private ;
346};
347#line 4 "/ddverify-2010-04-30/models/seq1/include/linux/elevator.h"
348struct request;
349#line 22 "/ddverify-2010-04-30/models/seq1/include/linux/blkdev.h"
350struct request_queue;
351#line 23 "/ddverify-2010-04-30/models/seq1/include/linux/blkdev.h"
352typedef struct request_queue request_queue_t;
353#line 25 "/ddverify-2010-04-30/models/seq1/include/linux/blkdev.h"
354typedef void request_fn_proc(request_queue_t *q );
355#line 26 "/ddverify-2010-04-30/models/seq1/include/linux/blkdev.h"
356typedef int make_request_fn(request_queue_t *q , struct bio *bio );
357#line 27 "/ddverify-2010-04-30/models/seq1/include/linux/blkdev.h"
358typedef void unplug_fn(request_queue_t * );
359#line 32
360enum rq_cmd_type_bits {
361 REQ_TYPE_FS = 1,
362 REQ_TYPE_BLOCK_PC = 2,
363 REQ_TYPE_SENSE = 3,
364 REQ_TYPE_PM_SUSPEND = 4,
365 REQ_TYPE_PM_RESUME = 5,
366 REQ_TYPE_PM_SHUTDOWN = 6,
367 REQ_TYPE_FLUSH = 7,
368 REQ_TYPE_SPECIAL = 8,
369 REQ_TYPE_LINUX_BLOCK = 9,
370 REQ_TYPE_ATA_CMD = 10,
371 REQ_TYPE_ATA_TASK = 11,
372 REQ_TYPE_ATA_TASKFILE = 12,
373 REQ_TYPE_ATA_PC = 13
374} ;
375#line 54 "/ddverify-2010-04-30/models/seq1/include/linux/blkdev.h"
376struct request_queue {
377 request_fn_proc *request_fn ;
378 make_request_fn *make_request_fn ;
379 unplug_fn *unplug_fn ;
380 struct backing_dev_info backing_dev_info ;
381 void *queuedata ;
382 unsigned long queue_flags ;
383 spinlock_t *queue_lock ;
384 unsigned short hardsect_size ;
385 int __ddv_genhd_no ;
386 int __ddv_queue_alive ;
387};
388#line 90 "/ddverify-2010-04-30/models/seq1/include/linux/blkdev.h"
389struct request {
390 struct list_head queuelist ;
391 struct list_head donelist ;
392 request_queue_t *q ;
393 unsigned long flags ;
394 unsigned int cmd_flags ;
395 enum rq_cmd_type_bits cmd_type ;
396 struct bio *bio ;
397 void *completion_data ;
398 struct gendisk *rq_disk ;
399 sector_t sector ;
400 unsigned long nr_sectors ;
401 unsigned int current_nr_sectors ;
402 char *buffer ;
403 int errors ;
404 unsigned short nr_phys_segments ;
405 unsigned char cmd[16] ;
406};
407#line 15 "/ddverify-2010-04-30/models/seq1/include/ddverify/genhd.h"
408struct ddv_genhd {
409 struct gendisk *gd ;
410 struct inode inode ;
411 struct file file ;
412 struct request current_request ;
413 int requests_open ;
414};
415#line 6 "/ddverify-2010-04-30/models/seq1/include/linux/mod_devicetable.h"
416typedef unsigned long kernel_ulong_t;
417#line 10 "/ddverify-2010-04-30/models/seq1/include/linux/mod_devicetable.h"
418struct pci_device_id {
419 __u32 vendor ;
420 __u32 device ;
421 __u32 subvendor ;
422 __u32 subdevice ;
423 __u32 class ;
424 __u32 class_mask ;
425 kernel_ulong_t driver_data ;
426};
427#line 40 "/ddverify-2010-04-30/models/seq1/include/linux/pci.h"
428typedef int pci_power_t;
429#line 43
430struct pci_bus;
431#line 43 "/ddverify-2010-04-30/models/seq1/include/linux/pci.h"
432struct pci_dev {
433 struct pci_bus *bus ;
434 unsigned int devfn ;
435 unsigned short vendor ;
436 unsigned short device ;
437 u64 dma_mask ;
438 struct device dev ;
439 unsigned int irq ;
440 struct resource resource[12] ;
441};
442#line 62 "/ddverify-2010-04-30/models/seq1/include/linux/pci.h"
443struct pci_bus {
444 unsigned char number ;
445};
446#line 67 "/ddverify-2010-04-30/models/seq1/include/linux/pci.h"
447struct pci_driver {
448 char *name ;
449 struct pci_device_id const *id_table ;
450 int (*probe)(struct pci_dev *dev , struct pci_device_id const *id ) ;
451 void (*remove)(struct pci_dev *dev ) ;
452 int (*suspend)(struct pci_dev *dev , pm_message_t state ) ;
453 int (*resume)(struct pci_dev *dev ) ;
454 int (*enable_wake)(struct pci_dev *dev , pci_power_t state , int enable ) ;
455 void (*shutdown)(struct pci_dev *dev ) ;
456};
457#line 6 "/ddverify-2010-04-30/models/seq1/include/ddverify/pci.h"
458struct ddv_pci_driver {
459 struct pci_driver *pci_driver ;
460 struct pci_dev pci_dev ;
461 unsigned int no_pci_device_id ;
462 int dev_initialized ;
463};
464#line 9 "/ddverify-2010-04-30/models/seq1/include/ddverify/interrupt.h"
465struct registered_irq {
466 irqreturn_t (*handler)(int , void * , struct pt_regs * ) ;
467 void *dev_id ;
468};
469#line 10 "/ddverify-2010-04-30/models/seq1/include/ddverify/tasklet.h"
470struct ddv_tasklet {
471 struct tasklet_struct *tasklet ;
472 unsigned short is_running ;
473};
474#line 10 "/ddverify-2010-04-30/models/seq1/include/ddverify/timer.h"
475struct ddv_timer {
476 struct timer_list *timer ;
477};
478#line 4 "/ddverify-2010-04-30/models/seq1/include/linux/hdreg.h"
479struct hd_geometry {
480 unsigned char heads ;
481 unsigned char sectors ;
482 unsigned short cylinders ;
483 unsigned long start ;
484};
485#line 7 "/ddverify-2010-04-30/models/seq1/include/linux/proc_fs.h"
486struct proc_dir_entry {
487 int something ;
488};
489#line 9 "/ddverify-2010-04-30/models/seq1/include/linux/seq_file.h"
490struct file;
491#line 11
492struct dentry;
493#line 12
494struct inode;
495#line 6 "/ddverify-2010-04-30/models/seq1/include/asm/termbits.h"
496typedef unsigned char cc_t;
497#line 8 "/ddverify-2010-04-30/models/seq1/include/asm/termbits.h"
498typedef unsigned int tcflag_t;
499#line 11 "/ddverify-2010-04-30/models/seq1/include/asm/termbits.h"
500struct termios {
501 tcflag_t c_iflag ;
502 tcflag_t c_oflag ;
503 tcflag_t c_cflag ;
504 tcflag_t c_lflag ;
505 cc_t c_line ;
506 cc_t c_cc[19] ;
507};
508#line 9 "/ddverify-2010-04-30/models/seq1/include/linux/tty_driver.h"
509struct tty_struct;
510#line 9
511struct tty_struct;
512#line 12 "/ddverify-2010-04-30/models/seq1/include/linux/tty_driver.h"
513struct tty_operations {
514 int (*open)(struct tty_struct *tty , struct file *filp ) ;
515 void (*close)(struct tty_struct *tty , struct file *filp ) ;
516 int (*write)(struct tty_struct *tty , unsigned char const *buf , int count ) ;
517 void (*put_char)(struct tty_struct *tty , unsigned char ch ) ;
518 void (*flush_chars)(struct tty_struct *tty ) ;
519 int (*write_room)(struct tty_struct *tty ) ;
520 int (*chars_in_buffer)(struct tty_struct *tty ) ;
521 int (*ioctl)(struct tty_struct *tty , struct file *file , unsigned int cmd , unsigned long arg ) ;
522 void (*set_termios)(struct tty_struct *tty , struct termios *old ) ;
523 void (*throttle)(struct tty_struct *tty ) ;
524 void (*unthrottle)(struct tty_struct *tty ) ;
525 void (*stop)(struct tty_struct *tty ) ;
526 void (*start)(struct tty_struct *tty ) ;
527 void (*hangup)(struct tty_struct *tty ) ;
528 void (*break_ctl)(struct tty_struct *tty , int state ) ;
529 void (*flush_buffer)(struct tty_struct *tty ) ;
530 void (*set_ldisc)(struct tty_struct *tty ) ;
531 void (*wait_until_sent)(struct tty_struct *tty , int timeout ) ;
532 void (*send_xchar)(struct tty_struct *tty , char ch ) ;
533 int (*read_proc)(char *page , char **start , off_t off , int count , int *eof ,
534 void *data ) ;
535 int (*write_proc)(struct file *file , char const *buffer , unsigned long count ,
536 void *data ) ;
537 int (*tiocmget)(struct tty_struct *tty , struct file *file ) ;
538 int (*tiocmset)(struct tty_struct *tty , struct file *file , unsigned int set ,
539 unsigned int clear ) ;
540};
541#line 43 "/ddverify-2010-04-30/models/seq1/include/linux/tty_driver.h"
542struct tty_driver {
543 int magic ;
544 struct cdev cdev ;
545 struct module *owner ;
546 char const *driver_name ;
547 char const *name ;
548 int name_base ;
549 int major ;
550 int minor_start ;
551 int minor_num ;
552 int num ;
553 short type ;
554 short subtype ;
555 struct termios init_termios ;
556 int flags ;
557 int refcount ;
558 struct proc_dir_entry *proc_entry ;
559 int (*open)(struct tty_struct *tty , struct file *filp ) ;
560 void (*close)(struct tty_struct *tty , struct file *filp ) ;
561 int (*write)(struct tty_struct *tty , unsigned char const *buf , int count ) ;
562 void (*put_char)(struct tty_struct *tty , unsigned char ch ) ;
563 void (*flush_chars)(struct tty_struct *tty ) ;
564 int (*write_room)(struct tty_struct *tty ) ;
565 int (*chars_in_buffer)(struct tty_struct *tty ) ;
566 int (*ioctl)(struct tty_struct *tty , struct file *file , unsigned int cmd , unsigned long arg ) ;
567 void (*set_termios)(struct tty_struct *tty , struct termios *old ) ;
568 void (*throttle)(struct tty_struct *tty ) ;
569 void (*unthrottle)(struct tty_struct *tty ) ;
570 void (*stop)(struct tty_struct *tty ) ;
571 void (*start)(struct tty_struct *tty ) ;
572 void (*hangup)(struct tty_struct *tty ) ;
573 void (*break_ctl)(struct tty_struct *tty , int state ) ;
574 void (*flush_buffer)(struct tty_struct *tty ) ;
575 void (*set_ldisc)(struct tty_struct *tty ) ;
576 void (*wait_until_sent)(struct tty_struct *tty , int timeout ) ;
577 void (*send_xchar)(struct tty_struct *tty , char ch ) ;
578 int (*read_proc)(char *page , char **start , off_t off , int count , int *eof ,
579 void *data ) ;
580 int (*write_proc)(struct file *file , char const *buffer , unsigned long count ,
581 void *data ) ;
582 int (*tiocmget)(struct tty_struct *tty , struct file *file ) ;
583 int (*tiocmset)(struct tty_struct *tty , struct file *file , unsigned int set ,
584 unsigned int clear ) ;
585};
586#line 113 "/ddverify-2010-04-30/models/seq1/include/linux/tty.h"
587struct tty_struct {
588 int magic ;
589 struct tty_driver *driver ;
590 int index ;
591 struct termios *termios ;
592 struct termios *termios_locked ;
593 char name[64] ;
594 unsigned long flags ;
595 int count ;
596 unsigned char stopped : 1 ;
597 unsigned char hw_stopped : 1 ;
598 unsigned char flow_stopped : 1 ;
599 unsigned char packet : 1 ;
600 unsigned int receive_room ;
601 wait_queue_head_t write_wait ;
602 wait_queue_head_t read_wait ;
603 void *disc_data ;
604 void *driver_data ;
605 unsigned char closing : 1 ;
606};
607#line 7 "/ddverify-2010-04-30/models/seq1/include/ddverify/tty.h"
608struct ddv_tty_driver {
609 struct tty_driver driver ;
610 unsigned short allocated ;
611 unsigned short registered ;
612};
613#line 2 "/ddverify-2010-04-30/models/seq1/include/ddverify/ddverify.h"
614void __VERIFIER_assume(int phi ) ;
615#line 3
616void __VERIFIER_assert(int phi , char *txt ) ;
617#line 12 "/ddverify-2010-04-30/models/seq1/include/ddverify/ddverify.h"
618int current_execution_context ;
619#line 32 "/ddverify-2010-04-30/models/seq1/include/ddverify/ddverify.h"
620__inline static int assert_context_process(void)
621{
622
623 {
624#line 34
625 return (0);
626}
627}
628#line 42 "/ddverify-2010-04-30/models/seq1/include/ddverify/ddverify.h"
629int (*_ddv_module_init)(void) ;
630#line 43 "/ddverify-2010-04-30/models/seq1/include/ddverify/ddverify.h"
631void (*_ddv_module_exit)(void) ;
632#line 45
633int call_ddv(void) ;
634#line 7 "/ddverify-2010-04-30/models/seq1/include/linux/jiffies.h"
635unsigned long jiffies ;
636#line 26 "/ddverify-2010-04-30/models/seq1/include/linux/timer.h"
637__inline void init_timer(struct timer_list *timer ) ;
638#line 27
639__inline void add_timer_on(struct timer_list *timer , int cpu ) ;
640#line 28
641__inline void add_timer(struct timer_list *timer ) ;
642#line 29
643__inline int del_timer(struct timer_list *timer ) ;
644#line 30
645__inline int mod_timer(struct timer_list *timer , unsigned long expires ) ;
646#line 9 "/ddverify-2010-04-30/models/seq1/include/linux/spinlock.h"
647__inline void spin_lock_init(spinlock_t *lock ) ;
648#line 10
649__inline void spin_lock(spinlock_t *lock ) ;
650#line 11
651__inline void spin_lock_irqsave(spinlock_t *lock , unsigned long flags ) ;
652#line 12
653__inline void spin_lock_irq(spinlock_t *lock ) ;
654#line 13
655__inline void spin_lock_bh(spinlock_t *lock ) ;
656#line 15
657__inline void spin_unlock(spinlock_t *lock ) ;
658#line 16
659__inline void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags ) ;
660#line 17
661__inline void spin_unlock_irq(spinlock_t *lock ) ;
662#line 18
663__inline void spin_unlock_bh(spinlock_t *lock ) ;
664#line 62 "/ddverify-2010-04-30/models/seq1/include/linux/wait.h"
665__inline void init_waitqueue_head(wait_queue_head_t *q ) ;
666#line 69
667__inline void wake_up(wait_queue_head_t *q ) ;
668#line 71
669__inline void wake_up_all(wait_queue_head_t *q ) ;
670#line 73
671__inline void wake_up_interruptible(wait_queue_head_t *q ) ;
672#line 86
673__inline void sleep_on(wait_queue_head_t *q ) ;
674#line 88
675__inline void interruptible_sleep_on(wait_queue_head_t *q ) ;
676#line 186 "/ddverify-2010-04-30/models/seq1/include/ddverify/pthread.h"
677__inline extern int pthread_mutex_init(pthread_mutex_t *__mutex , pthread_mutexattr_t const *__mutex_attr )
678{ pthread_mutex_t i ;
679
680 {
681#line 190
682 i.locked = (_Bool)0;
683#line 191
684 *__mutex = i;
685#line 192
686 return (0);
687}
688}
689#line 194 "/ddverify-2010-04-30/models/seq1/include/ddverify/pthread.h"
690__inline extern int pthread_mutex_destroy(pthread_mutex_t *__mutex )
691{
692
693 {
694#line 196
695 return (0);
696}
697}
698#line 200
699void __VERIFIER_atomic_begin(void) ;
700#line 201
701void __VERIFIER_atomic_end(void) ;
702#line 203 "/ddverify-2010-04-30/models/seq1/include/ddverify/pthread.h"
703__inline extern int pthread_mutex_lock(pthread_mutex_t *__mutex )
704{ _Bool __cil_tmp2 ;
705 int __cil_tmp3 ;
706
707 {
708 {
709#line 206
710 __VERIFIER_atomic_begin();
711#line 207
712 __cil_tmp2 = __mutex->locked;
713#line 207
714 __cil_tmp3 = ! __cil_tmp2;
715#line 207
716 __VERIFIER_assume(__cil_tmp3);
717#line 208
718 __mutex->locked = (_Bool)1;
719#line 209
720 __VERIFIER_atomic_end();
721 }
722#line 210
723 return (0);
724}
725}
726#line 213 "/ddverify-2010-04-30/models/seq1/include/ddverify/pthread.h"
727__inline extern int pthread_mutex_unlock(pthread_mutex_t *__mutex )
728{
729
730 {
731#line 215
732 __mutex->locked = (_Bool)0;
733#line 216
734 return (0);
735}
736}
737#line 10 "/ddverify-2010-04-30/models/seq1/include/ddverify/satabs.h"
738extern void *malloc(size_t size ) ;
739#line 15
740short __VERIFIER_nondet_short(void) ;
741#line 16
742unsigned short __VERIFIER_nondet_ushort(void) ;
743#line 17
744int __VERIFIER_nondet_int(void) ;
745#line 18
746unsigned int __VERIFIER_nondet_uint(void) ;
747#line 19
748long __VERIFIER_nondet_long(void) ;
749#line 20
750unsigned long __VERIFIER_nondet_ulong(void) ;
751#line 21
752char __VERIFIER_nondet_char(void) ;
753#line 22
754unsigned char __VERIFIER_nondet_uchar(void) ;
755#line 23
756unsigned int __VERIFIER_nondet_unsigned(void) ;
757#line 24
758loff_t __VERIFIER_nondet_loff_t(void) ;
759#line 25
760size_t __VERIFIER_nondet_size_t(void) ;
761#line 26
762sector_t __VERIFIER_nondet_sector_t(void) ;
763#line 28
764char *__VERIFIER_nondet_pchar(void) ;
765#line 55 "/ddverify-2010-04-30/models/seq1/include/linux/gfp.h"
766__inline unsigned long __get_free_pages(gfp_t gfp_mask , unsigned int order ) ;
767#line 57
768__inline unsigned long __get_free_page(gfp_t gfp_mask ) ;
769#line 59
770__inline unsigned long get_zeroed_page(gfp_t gfp_mask ) ;
771#line 70
772__inline struct page *alloc_pages(gfp_t gfp_mask , unsigned int order ) ;
773#line 72
774__inline struct page *alloc_page(gfp_t gfp_mask ) ;
775#line 8 "/ddverify-2010-04-30/models/seq1/include/linux/slab.h"
776void kfree(void const *addr ) ;
777#line 10
778void *kmalloc(size_t size , gfp_t flags ) ;
779#line 12
780void *kzalloc(size_t size , gfp_t flags ) ;
781#line 6 "/ddverify-2010-04-30/models/seq1/include/asm/bitops.h"
782int test_and_set_bit(int nr , unsigned long *addr ) ;
783#line 10
784void clear_bit(int nr , unsigned long volatile *addr ) ;
785#line 43 "/ddverify-2010-04-30/models/seq1/include/linux/sched.h"
786void schedule(void) ;
787#line 45
788long schedule_timeout(long timeout ) ;
789#line 34 "/ddverify-2010-04-30/models/seq1/include/linux/kernel.h"
790int printk(char const *fmt , ...) ;
791#line 30 "/ddverify-2010-04-30/models/seq1/include/linux/module.h"
792void __module_get(struct module *module ) ;
793#line 40 "/ddverify-2010-04-30/models/seq1/include/linux/miscdevice.h"
794int misc_register(struct miscdevice *misc ) ;
795#line 41
796int misc_deregister(struct miscdevice *misc ) ;
797#line 23 "/ddverify-2010-04-30/models/seq1/include/asm/semaphore.h"
798__inline void sema_init(struct semaphore *sem , int val ) ;
799#line 25
800__inline void init_MUTEX(struct semaphore *sem ) ;
801#line 27
802__inline void init_MUTEX_LOCKED(struct semaphore *sem ) ;
803#line 29
804__inline void down(struct semaphore *sem ) ;
805#line 31
806__inline int down_interruptible(struct semaphore *sem ) ;
807#line 33
808__inline int down_trylock(struct semaphore *sem ) ;
809#line 35
810__inline void up(struct semaphore *sem ) ;
811#line 195 "/ddverify-2010-04-30/models/seq1/include/linux/fs.h"
812__inline int alloc_chrdev_region(dev_t *dev , unsigned int baseminor , unsigned int count ,
813 char const *name ) ;
814#line 196
815__inline int register_chrdev_region(dev_t from , unsigned int count , char const *name ) ;
816#line 199
817__inline int register_chrdev(unsigned int major , char const *name , struct file_operations *fops ) ;
818#line 200
819__inline int unregister_chrdev(unsigned int major , char const *name ) ;
820#line 207
821int register_blkdev(unsigned int major , char const *name ) ;
822#line 208
823int unregister_blkdev(unsigned int major , char const *name ) ;
824#line 223
825loff_t no_llseek(struct file *file , loff_t offset , int origin ) ;
826#line 233
827int nonseekable_open(struct inode *inode , struct file *filp ) ;
828#line 90 "/ddverify-2010-04-30/models/seq1/include/linux/ioport.h"
829__inline struct resource *request_region(unsigned long start , unsigned long len ,
830 char const *name ) ;
831#line 92
832__inline void release_region(unsigned long start , unsigned long len ) ;
833#line 96
834struct resource *request_mem_region(unsigned long start , unsigned long len , char const *name ) ;
835#line 98
836void release_mem_region(unsigned long start , unsigned long len ) ;
837#line 40 "/ddverify-2010-04-30/models/seq1/include/linux/reboot.h"
838int register_reboot_notifier(struct notifier_block *dummy ) ;
839#line 41
840int unregister_reboot_notifier(struct notifier_block *dummy ) ;
841#line 14 "/ddverify-2010-04-30/models/seq1/include/asm/io.h"
842__inline unsigned char inb(unsigned int port ) ;
843#line 15
844__inline void outb(unsigned char byte , unsigned int port ) ;
845#line 16
846__inline unsigned short inw(unsigned int port ) ;
847#line 17
848__inline void outw(unsigned short word , unsigned int port ) ;
849#line 18
850__inline unsigned int inl(unsigned int port ) ;
851#line 19
852__inline void outl(unsigned int doubleword , unsigned int port ) ;
853#line 23
854__inline unsigned char inb_p(unsigned int port ) ;
855#line 24
856__inline void outb_p(unsigned char byte , unsigned int port ) ;
857#line 25
858__inline unsigned short inw_p(unsigned int port ) ;
859#line 26
860__inline void outw_p(unsigned short word , unsigned int port ) ;
861#line 27
862__inline unsigned int inl_p(unsigned int port ) ;
863#line 28
864__inline void outl_p(unsigned int doubleword , unsigned int port ) ;
865#line 41 "/ddverify-2010-04-30/models/seq1/include/asm/uaccess.h"
866__inline int __get_user(int size , void *ptr ) ;
867#line 43
868__inline int get_user(int size , void *ptr ) ;
869#line 46
870__inline int __put_user(int size , void *ptr ) ;
871#line 48
872__inline int put_user(int size , void *ptr ) ;
873#line 51
874__inline unsigned long copy_to_user(void *to , void const *from , unsigned long n ) ;
875#line 53
876__inline unsigned long copy_from_user(void *to , void *from , unsigned long n ) ;
877#line 84 "machzwd.c"
878static unsigned short zf_readw(unsigned char port )
879{ unsigned short tmp ;
880
881 {
882 {
883#line 86
884 outb(port, 536U);
885#line 87
886 tmp = inw(538U);
887 }
888#line 87
889 return (tmp);
890}
891}
892#line 91 "machzwd.c"
893char _ddv_module_author[44] =
894#line 91
895 { (char )'F', (char )'e', (char )'r', (char )'n',
896 (char )'a', (char )'n', (char )'d', (char )'o',
897 (char )' ', (char )'F', (char )'u', (char )'g',
898 (char )'a', (char )'n', (char )'t', (char )'i',
899 (char )' ', (char )'<', (char )'f', (char )'u',
900 (char )'g', (char )'a', (char )'n', (char )'t',
901 (char )'i', (char )'@', (char )'c', (char )'o',
902 (char )'n', (char )'e', (char )'c', (char )'t',
903 (char )'i', (char )'v', (char )'a', (char )'.',
904 (char )'c', (char )'o', (char )'m', (char )'.',
905 (char )'b', (char )'r', (char )'>', (char )'\000'};
906#line 92 "machzwd.c"
907char _ddv_module_description[31] =
908#line 92
909 { (char )'M', (char )'a', (char )'c', (char )'h',
910 (char )'Z', (char )' ', (char )'Z', (char )'F',
911 (char )'-', (char )'L', (char )'o', (char )'g',
912 (char )'i', (char )'c', (char )' ', (char )'W',
913 (char )'a', (char )'t', (char )'c', (char )'h',
914 (char )'d', (char )'o', (char )'g', (char )' ',
915 (char )'d', (char )'r', (char )'i', (char )'v',
916 (char )'e', (char )'r', (char )'\000'};
917#line 93 "machzwd.c"
918char _ddv_module_license[4] = { (char )'G', (char )'P', (char )'L', (char )'\000'};
919#line 96 "machzwd.c"
920static int nowayout = 0;
921#line 98 "machzwd.c"
922char _ddv_module_param_nowayout[75] =
923#line 98
924 { (char )'W', (char )'a', (char )'t', (char )'c',
925 (char )'h', (char )'d', (char )'o', (char )'g',
926 (char )' ', (char )'c', (char )'a', (char )'n',
927 (char )'n', (char )'o', (char )'t', (char )' ',
928 (char )'b', (char )'e', (char )' ', (char )'s',
929 (char )'t', (char )'o', (char )'p', (char )'p',
930 (char )'e', (char )'d', (char )' ', (char )'o',
931 (char )'n', (char )'c', (char )'e', (char )' ',
932 (char )'s', (char )'t', (char )'a', (char )'r',
933 (char )'t', (char )'e', (char )'d', (char )' ',
934 (char )'(', (char )'d', (char )'e', (char )'f',
935 (char )'a', (char )'u', (char )'l', (char )'t',
936 (char )'=', (char )'C', (char )'O', (char )'N',
937 (char )'F', (char )'I', (char )'G', (char )'_',
938 (char )'W', (char )'A', (char )'T', (char )'C',
939 (char )'H', (char )'D', (char )'O', (char )'G',
940 (char )'_', (char )'N', (char )'O', (char )'W',
941 (char )'A', (char )'Y', (char )'O', (char )'U',
942 (char )'T', (char )')', (char )'\000'};
943#line 102 "machzwd.c"
944static struct watchdog_info zf_info = {(__u32 )33024, (__u32 )1, {(__u8 )'Z', (__u8 )'F', (__u8 )'-', (__u8 )'L', (__u8 )'o',
945 (__u8 )'g', (__u8 )'i', (__u8 )'c', (__u8 )' ', (__u8 )'w',
946 (__u8 )'a', (__u8 )'t', (__u8 )'c', (__u8 )'h', (__u8 )'d',
947 (__u8 )'o', (__u8 )'g', (__u8 )'\000', (unsigned char)0,
948 (unsigned char)0, (unsigned char)0, (unsigned char)0,
949 (unsigned char)0, (unsigned char)0, (unsigned char)0,
950 (unsigned char)0, (unsigned char)0, (unsigned char)0,
951 (unsigned char)0, (unsigned char)0, (unsigned char)0,
952 (unsigned char)0}};
953#line 117 "machzwd.c"
954static int action = 0;
955#line 119 "machzwd.c"
956char _ddv_module_param_action[73] =
957#line 119
958 { (char )'a', (char )'f', (char )'t', (char )'e',
959 (char )'r', (char )' ', (char )'w', (char )'a',
960 (char )'t', (char )'c', (char )'h', (char )'d',
961 (char )'o', (char )'g', (char )' ', (char )'r',
962 (char )'e', (char )'s', (char )'e', (char )'t',
963 (char )'s', (char )',', (char )' ', (char )'g',
964 (char )'e', (char )'n', (char )'e', (char )'r',
965 (char )'a', (char )'t', (char )'e', (char )':',
966 (char )' ', (char )'0', (char )' ', (char )'=',
967 (char )' ', (char )'R', (char )'E', (char )'S',
968 (char )'E', (char )'T', (char )'(', (char )'*',
969 (char )')', (char )' ', (char )' ', (char )'1',
970 (char )' ', (char )'=', (char )' ', (char )'S',
971 (char )'M', (char )'I', (char )' ', (char )' ',
972 (char )'2', (char )' ', (char )'=', (char )' ',
973 (char )'N', (char )'M', (char )'I', (char )' ',
974 (char )' ', (char )'3', (char )' ', (char )'=',
975 (char )' ', (char )'S', (char )'C', (char )'I',
976 (char )'\000'};
977#line 121 "machzwd.c"
978static int zf_action = 2048;
979#line 122 "machzwd.c"
980static unsigned long zf_is_open ;
981#line 123 "machzwd.c"
982static char zf_expect_close ;
983#line 124 "machzwd.c"
984static spinlock_t zf_lock ;
985#line 125 "machzwd.c"
986static spinlock_t zf_port_lock ;
987#line 126 "machzwd.c"
988static struct timer_list zf_timer ;
989#line 127 "machzwd.c"
990static unsigned long next_heartbeat = 0UL;
991#line 146 "machzwd.c"
992__inline static void zf_set_status(unsigned char new )
993{
994
995 {
996 {
997#line 148
998 outb((unsigned char)18, 536U);
999#line 148
1000 outb(new, 537U);
1001 }
1002#line 149
1003 return;
1004}
1005}
1006#line 154 "machzwd.c"
1007__inline static unsigned short zf_get_control(void)
1008{ unsigned short tmp ;
1009
1010 {
1011 {
1012#line 156
1013 tmp = zf_readw((unsigned char)16);
1014 }
1015#line 156
1016 return (tmp);
1017}
1018}
1019#line 159 "machzwd.c"
1020__inline static void zf_set_control(unsigned short new )
1021{
1022
1023 {
1024 {
1025#line 161
1026 outb((unsigned char)16, 536U);
1027#line 161
1028 outw(new, 538U);
1029 }
1030#line 162
1031 return;
1032}
1033}
1034#line 170 "machzwd.c"
1035__inline static void zf_set_timer(unsigned short new , unsigned char n )
1036{ int tmp ;
1037 int __cil_tmp4 ;
1038 unsigned char __cil_tmp5 ;
1039
1040 {
1041#line 173
1042 if ((int )n == 0) {
1043 goto switch_0_0;
1044 } else {
1045#line 175
1046 if ((int )n == 1) {
1047 goto switch_0_1;
1048 } else {
1049 {
1050 goto switch_0_default;
1051#line 172
1052 if (0) {
1053 switch_0_0:
1054 {
1055#line 174
1056 outb((unsigned char)12, 536U);
1057#line 174
1058 outw(new, 538U);
1059 }
1060 switch_0_1:
1061 {
1062#line 176
1063 outb((unsigned char)14, 536U);
1064 }
1065 {
1066#line 176
1067 __cil_tmp4 = (int )new;
1068#line 176
1069 if (__cil_tmp4 > 255) {
1070#line 176
1071 tmp = 255;
1072 } else {
1073#line 176
1074 tmp = (int )new;
1075 }
1076 }
1077 {
1078#line 176
1079 __cil_tmp5 = (unsigned char )tmp;
1080#line 176
1081 outb(__cil_tmp5, 537U);
1082 }
1083 switch_0_default: ;
1084#line 178
1085 return;
1086 } else {
1087 switch_0_break: ;
1088 }
1089 }
1090 }
1091 }
1092}
1093}
1094#line 185 "machzwd.c"
1095static void zf_timer_off(void)
1096{ unsigned int ctrl_reg ;
1097 unsigned long flags ;
1098 unsigned short tmp ;
1099 unsigned short __cil_tmp4 ;
1100
1101 {
1102 {
1103#line 187
1104 ctrl_reg = 0U;
1105#line 191
1106 del_timer(& zf_timer);
1107#line 193
1108 spin_lock_irqsave(& zf_port_lock, flags);
1109#line 195
1110 tmp = zf_get_control();
1111#line 195
1112 ctrl_reg = (unsigned int )tmp;
1113#line 196
1114 ctrl_reg = ctrl_reg | 3U;
1115#line 197
1116 ctrl_reg = ctrl_reg & 4294967292U;
1117#line 198
1118 __cil_tmp4 = (unsigned short )ctrl_reg;
1119#line 198
1120 zf_set_control(__cil_tmp4);
1121#line 199
1122 spin_unlock_irqrestore(& zf_port_lock, flags);
1123#line 201
1124 printk("<6>machzwd: Watchdog timer is now disabled\n");
1125 }
1126#line 202
1127 return;
1128}
1129}
1130#line 208 "machzwd.c"
1131static void zf_timer_on(void)
1132{ unsigned int ctrl_reg ;
1133 unsigned long flags ;
1134 unsigned short tmp ;
1135 int __cil_tmp4 ;
1136 unsigned int __cil_tmp5 ;
1137 unsigned short __cil_tmp6 ;
1138
1139 {
1140 {
1141#line 210
1142 ctrl_reg = 0U;
1143#line 213
1144 spin_lock_irqsave(& zf_port_lock, flags);
1145#line 215
1146 outb((unsigned char)15, 536U);
1147#line 215
1148 outb((unsigned char)255, 537U);
1149#line 217
1150 zf_set_timer((unsigned short)65535, (unsigned char)0);
1151#line 220
1152 next_heartbeat = jiffies + 1000UL;
1153#line 223
1154 zf_timer.expires = jiffies + 50UL;
1155#line 225
1156 add_timer(& zf_timer);
1157#line 228
1158 tmp = zf_get_control();
1159#line 228
1160 ctrl_reg = (unsigned int )tmp;
1161#line 229
1162 __cil_tmp4 = 1 | zf_action;
1163#line 229
1164 __cil_tmp5 = (unsigned int )__cil_tmp4;
1165#line 229
1166 ctrl_reg = ctrl_reg | __cil_tmp5;
1167#line 230
1168 __cil_tmp6 = (unsigned short )ctrl_reg;
1169#line 230
1170 zf_set_control(__cil_tmp6);
1171#line 231
1172 spin_unlock_irqrestore(& zf_port_lock, flags);
1173#line 233
1174 printk("<6>machzwd: Watchdog timer is now enabled\n");
1175 }
1176#line 234
1177 return;
1178}
1179}
1180#line 237 "machzwd.c"
1181static void zf_ping(unsigned long data )
1182{ unsigned int ctrl_reg ;
1183 unsigned long flags ;
1184 unsigned short tmp ;
1185 long __cil_tmp5 ;
1186 long __cil_tmp6 ;
1187 long __cil_tmp7 ;
1188 unsigned short __cil_tmp8 ;
1189 unsigned short __cil_tmp9 ;
1190
1191 {
1192 {
1193#line 239
1194 ctrl_reg = 0U;
1195#line 242
1196 outb((unsigned char)14, 536U);
1197#line 242
1198 outb((unsigned char)255, 537U);
1199 }
1200 {
1201#line 244
1202 __cil_tmp5 = (long )next_heartbeat;
1203#line 244
1204 __cil_tmp6 = (long )jiffies;
1205#line 244
1206 __cil_tmp7 = __cil_tmp6 - __cil_tmp5;
1207#line 244
1208 if (__cil_tmp7 < 0L) {
1209 {
1210#line 253
1211 spin_lock_irqsave(& zf_port_lock, flags);
1212#line 254
1213 tmp = zf_get_control();
1214#line 254
1215 ctrl_reg = (unsigned int )tmp;
1216#line 255
1217 ctrl_reg = ctrl_reg | 16U;
1218#line 256
1219 __cil_tmp8 = (unsigned short )ctrl_reg;
1220#line 256
1221 zf_set_control(__cil_tmp8);
1222#line 259
1223 ctrl_reg = ctrl_reg & 4294967279U;
1224#line 260
1225 __cil_tmp9 = (unsigned short )ctrl_reg;
1226#line 260
1227 zf_set_control(__cil_tmp9);
1228#line 261
1229 spin_unlock_irqrestore(& zf_port_lock, flags);
1230#line 263
1231 zf_timer.expires = jiffies + 50UL;
1232#line 264
1233 add_timer(& zf_timer);
1234 }
1235 } else {
1236 {
1237#line 266
1238 printk("<2>machzwd: I will reset your machine\n");
1239 }
1240 }
1241 }
1242#line 268
1243 return;
1244}
1245}
1246#line 270 "machzwd.c"
1247static ssize_t zf_write(struct file *file , char const *buf , size_t count , loff_t *ppos )
1248{ size_t ofs ;
1249 char c ;
1250 int tmp ;
1251 int __cil_tmp8 ;
1252 char const *__cil_tmp9 ;
1253 void *__cil_tmp10 ;
1254 int __cil_tmp11 ;
1255
1256 {
1257#line 274
1258 if (count) {
1259#line 280
1260 if (! nowayout) {
1261#line 287
1262 zf_expect_close = (char)0;
1263#line 290
1264 ofs = 0U;
1265 {
1266#line 290
1267 while (1) {
1268 while_1_continue: ;
1269#line 290
1270 if (ofs != count) {
1271
1272 } else {
1273 goto while_1_break;
1274 }
1275 {
1276#line 292
1277 __cil_tmp8 = (int )c;
1278#line 292
1279 __cil_tmp9 = buf + ofs;
1280#line 292
1281 __cil_tmp10 = (void *)__cil_tmp9;
1282#line 292
1283 tmp = get_user(__cil_tmp8, __cil_tmp10);
1284 }
1285#line 292
1286 if (tmp) {
1287#line 293
1288 return (-14);
1289 } else {
1290
1291 }
1292 {
1293#line 294
1294 __cil_tmp11 = (int )c;
1295#line 294
1296 if (__cil_tmp11 == 86) {
1297#line 295
1298 zf_expect_close = (char)42;
1299 } else {
1300
1301 }
1302 }
1303#line 290
1304 ofs = ofs + 1U;
1305 }
1306 while_1_break: ;
1307 }
1308 } else {
1309
1310 }
1311#line 305
1312 next_heartbeat = jiffies + 1000UL;
1313 } else {
1314
1315 }
1316#line 310
1317 return ((int )count);
1318}
1319}
1320#line 313 "machzwd.c"
1321static int zf_ioctl(struct inode *inode , struct file *file , unsigned int cmd , unsigned long arg )
1322{ void *argp ;
1323 int *p ;
1324 unsigned long tmp ;
1325 int tmp___0 ;
1326 void const *__cil_tmp9 ;
1327 unsigned long __cil_tmp10 ;
1328 int __cil_tmp11 ;
1329 unsigned int __cil_tmp12 ;
1330 unsigned int __cil_tmp13 ;
1331 unsigned int __cil_tmp14 ;
1332 unsigned long __cil_tmp15 ;
1333 void *__cil_tmp16 ;
1334 unsigned long __cil_tmp17 ;
1335 int __cil_tmp18 ;
1336 unsigned int __cil_tmp19 ;
1337 unsigned int __cil_tmp20 ;
1338 unsigned int __cil_tmp21 ;
1339 unsigned int __cil_tmp22 ;
1340 unsigned long __cil_tmp23 ;
1341 unsigned long __cil_tmp24 ;
1342 int __cil_tmp25 ;
1343 unsigned int __cil_tmp26 ;
1344 unsigned int __cil_tmp27 ;
1345 unsigned int __cil_tmp28 ;
1346 unsigned int __cil_tmp29 ;
1347 unsigned long __cil_tmp30 ;
1348
1349 {
1350#line 316
1351 argp = (void *)arg;
1352#line 317
1353 p = (int *)argp;
1354#line 319
1355 if ((int )cmd == (__cil_tmp15 | __cil_tmp10)) {
1356 goto switch_2_exp_0;
1357 } else {
1358#line 324
1359 if ((int )cmd == (__cil_tmp23 | __cil_tmp17)) {
1360 goto switch_2_exp_1;
1361 } else {
1362#line 327
1363 if ((int )cmd == (__cil_tmp30 | __cil_tmp24)) {
1364 goto switch_2_exp_2;
1365 } else {
1366 {
1367 goto switch_2_default;
1368#line 318
1369 if (0) {
1370 switch_2_exp_0:
1371 {
1372#line 320
1373 __cil_tmp10 = 40UL << 16;
1374#line 320
1375 __cil_tmp11 = 87 << 8;
1376#line 320
1377 __cil_tmp12 = (unsigned int )__cil_tmp11;
1378#line 320
1379 __cil_tmp13 = 2U << 30;
1380#line 320
1381 __cil_tmp14 = __cil_tmp13 | __cil_tmp12;
1382#line 320
1383 __cil_tmp15 = (unsigned long )__cil_tmp14;
1384 {
1385#line 320
1386 __cil_tmp9 = (void const *)(& zf_info);
1387#line 320
1388 tmp = copy_to_user(argp, __cil_tmp9, 40UL);
1389 }
1390 }
1391#line 320
1392 if (tmp) {
1393#line 321
1394 return (-14);
1395 } else {
1396
1397 }
1398 goto switch_2_break;
1399 switch_2_exp_1:
1400 {
1401#line 325
1402 __cil_tmp17 = 4UL << 16;
1403#line 325
1404 __cil_tmp18 = 87 << 8;
1405#line 325
1406 __cil_tmp19 = (unsigned int )__cil_tmp18;
1407#line 325
1408 __cil_tmp20 = 2U << 30;
1409#line 325
1410 __cil_tmp21 = __cil_tmp20 | __cil_tmp19;
1411#line 325
1412 __cil_tmp22 = __cil_tmp21 | 1U;
1413#line 325
1414 __cil_tmp23 = (unsigned long )__cil_tmp22;
1415 {
1416#line 325
1417 __cil_tmp16 = (void *)p;
1418#line 325
1419 tmp___0 = put_user(0, __cil_tmp16);
1420 }
1421 }
1422#line 325
1423 return (tmp___0);
1424 switch_2_exp_2:
1425 {
1426#line 328
1427 __cil_tmp24 = 4UL << 16;
1428#line 328
1429 __cil_tmp25 = 87 << 8;
1430#line 328
1431 __cil_tmp26 = (unsigned int )__cil_tmp25;
1432#line 328
1433 __cil_tmp27 = 2U << 30;
1434#line 328
1435 __cil_tmp28 = __cil_tmp27 | __cil_tmp26;
1436#line 328
1437 __cil_tmp29 = __cil_tmp28 | 5U;
1438#line 328
1439 __cil_tmp30 = (unsigned long )__cil_tmp29;
1440 {
1441#line 328
1442 zf_ping(0UL);
1443 }
1444 }
1445 goto switch_2_break;
1446 switch_2_default: ;
1447#line 332
1448 return (-25);
1449 } else {
1450 switch_2_break: ;
1451 }
1452 }
1453 }
1454 }
1455 }
1456#line 335
1457 return (0);
1458}
1459}
1460#line 338 "machzwd.c"
1461static int zf_open(struct inode *inode , struct file *file )
1462{ int tmp ;
1463 int tmp___0 ;
1464 struct module *__cil_tmp5 ;
1465
1466 {
1467 {
1468#line 340
1469 spin_lock(& zf_lock);
1470#line 341
1471 tmp = test_and_set_bit(0, & zf_is_open);
1472 }
1473#line 341
1474 if (tmp) {
1475 {
1476#line 342
1477 spin_unlock(& zf_lock);
1478 }
1479#line 343
1480 return (-16);
1481 } else {
1482
1483 }
1484#line 346
1485 if (nowayout) {
1486 {
1487#line 347
1488 __cil_tmp5 = (struct module *)0;
1489#line 347
1490 __module_get(__cil_tmp5);
1491 }
1492 } else {
1493
1494 }
1495 {
1496#line 349
1497 spin_unlock(& zf_lock);
1498#line 351
1499 zf_timer_on();
1500#line 353
1501 tmp___0 = nonseekable_open(inode, file);
1502 }
1503#line 353
1504 return (tmp___0);
1505}
1506}
1507#line 356 "machzwd.c"
1508static int zf_close(struct inode *inode , struct file *file )
1509{ int __cil_tmp3 ;
1510 unsigned long volatile *__cil_tmp4 ;
1511
1512 {
1513 {
1514#line 358
1515 __cil_tmp3 = (int )zf_expect_close;
1516#line 358
1517 if (__cil_tmp3 == 42) {
1518 {
1519#line 359
1520 zf_timer_off();
1521 }
1522 } else {
1523 {
1524#line 361
1525 del_timer(& zf_timer);
1526#line 362
1527 printk("<3>machzwd: device file closed unexpectedly. Will not stop the WDT!\n");
1528 }
1529 }
1530 }
1531 {
1532#line 365
1533 spin_lock(& zf_lock);
1534#line 366
1535 __cil_tmp4 = (unsigned long volatile *)(& zf_is_open);
1536#line 366
1537 clear_bit(0, __cil_tmp4);
1538#line 367
1539 spin_unlock(& zf_lock);
1540#line 369
1541 zf_expect_close = (char)0;
1542 }
1543#line 371
1544 return (0);
1545}
1546}
1547#line 378 "machzwd.c"
1548static int zf_notify_sys(struct notifier_block *this , unsigned long code , void *unused )
1549{
1550
1551 {
1552#line 381
1553 if (code == 1UL) {
1554 {
1555#line 382
1556 zf_timer_off();
1557 }
1558 } else {
1559#line 381
1560 if (code == 2UL) {
1561 {
1562#line 382
1563 zf_timer_off();
1564 }
1565 } else {
1566
1567 }
1568 }
1569#line 385
1570 return (0);
1571}
1572}
1573#line 391 "machzwd.c"
1574static struct file_operations const zf_fops =
1575#line 391
1576 {(struct module *)0, & no_llseek, (ssize_t (*)(struct file * , char * , size_t ,
1577 loff_t * ))0, & zf_write, (int (*)(struct file * ,
1578 void * ,
1579 int (*)(void * ,
1580 char const * ,
1581 int ,
1582 loff_t ,
1583 ino_t ,
1584 unsigned int ) ))0,
1585 (unsigned int (*)(struct file * , struct poll_table_struct * ))0, & zf_ioctl,
1586 (long (*)(struct file * , unsigned int , unsigned long ))0, (long (*)(struct file * ,
1587 unsigned int ,
1588 unsigned long ))0,
1589 (int (*)(struct file * , struct vm_area_struct * ))0, & zf_open, (int (*)(struct file * ))0,
1590 & zf_close, (int (*)(struct file * , struct dentry * , int datasync ))0, (int (*)(int ,
1591 struct file * ,
1592 int ))0,
1593 (int (*)(struct file * , int , struct file_lock * ))0, (ssize_t (*)(struct file * ,
1594 struct iovec const * ,
1595 unsigned long ,
1596 loff_t * ))0,
1597 (ssize_t (*)(struct file * , struct iovec const * , unsigned long , loff_t * ))0,
1598 (ssize_t (*)(struct file * , loff_t * , size_t , int (*)(read_descriptor_t * ,
1599 struct page * , unsigned long ,
1600 unsigned long ) , void * ))0,
1601 (ssize_t (*)(struct file * , struct page * , int , size_t , loff_t * , int ))0,
1602 (unsigned long (*)(struct file * , unsigned long , unsigned long , unsigned long ,
1603 unsigned long ))0, (int (*)(int ))0, (int (*)(struct file *filp ,
1604 unsigned long arg ))0,
1605 (int (*)(struct file * , int , struct file_lock * ))0, (int (*)(struct inode * ))0};
1606#line 400 "machzwd.c"
1607static struct miscdevice zf_miscdev = {130, "watchdog", (struct file_operations *)(& zf_fops)};
1608#line 411 "machzwd.c"
1609static struct notifier_block zf_notifier = {& zf_notify_sys, (struct notifier_block *)0, 0};
1610#line 415 "machzwd.c"
1611static void zf_show_action(int act )
1612{ char *str[4] ;
1613
1614 {
1615 {
1616#line 417
1617 str[0] = (char *)"RESET";
1618#line 417
1619 str[1] = (char *)"SMI";
1620#line 417
1621 str[2] = (char *)"NMI";
1622#line 417
1623 str[3] = (char *)"SCI";
1624#line 419
1625 printk("<6>machzwd: Watchdog using action = %s\n", str[act]);
1626 }
1627#line 420
1628 return;
1629}
1630}
1631#line 422 "machzwd.c"
1632static int zf_init(void)
1633{ int ret ;
1634 unsigned short tmp ;
1635 struct resource *tmp___0 ;
1636
1637 {
1638 {
1639#line 426
1640 printk("<6>machzwd: MachZ ZF-Logic Watchdog driver initializing.\n");
1641#line 428
1642 tmp = zf_readw((unsigned char)2);
1643#line 428
1644 ret = (int )tmp;
1645 }
1646#line 429
1647 if (! ret) {
1648 {
1649#line 430
1650 printk("<4>machzwd: no ZF-Logic found\n");
1651 }
1652#line 431
1653 return (-19);
1654 } else {
1655#line 429
1656 if (ret == 65535) {
1657 {
1658#line 430
1659 printk("<4>machzwd: no ZF-Logic found\n");
1660 }
1661#line 431
1662 return (-19);
1663 } else {
1664
1665 }
1666 }
1667#line 434
1668 if (action <= 3) {
1669#line 434
1670 if (action >= 0) {
1671#line 435
1672 zf_action = zf_action >> action;
1673 } else {
1674#line 437
1675 action = 0;
1676 }
1677 } else {
1678#line 437
1679 action = 0;
1680 }
1681 {
1682#line 439
1683 zf_show_action(action);
1684#line 441
1685 spin_lock_init(& zf_lock);
1686#line 442
1687 spin_lock_init(& zf_port_lock);
1688#line 444
1689 ret = misc_register(& zf_miscdev);
1690 }
1691#line 445
1692 if (ret) {
1693 {
1694#line 446
1695 printk("<3>can\'t misc_register on minor=%d\n", 130);
1696 }
1697 goto out;
1698 } else {
1699
1700 }
1701 {
1702#line 451
1703 tmp___0 = request_region(536UL, 3UL, "MachZ ZFL WDT");
1704 }
1705#line 451
1706 if (tmp___0) {
1707
1708 } else {
1709 {
1710#line 452
1711 printk("<3>cannot reserve I/O ports at %d\n", 536);
1712#line 454
1713 ret = -16;
1714 }
1715 goto no_region;
1716 }
1717 {
1718#line 458
1719 ret = register_reboot_notifier(& zf_notifier);
1720 }
1721#line 459
1722 if (ret) {
1723 {
1724#line 460
1725 printk("<3>can\'t register reboot notifier (err=%d)\n", ret);
1726 }
1727 goto no_reboot;
1728 } else {
1729
1730 }
1731 {
1732#line 465
1733 zf_set_status((unsigned char)0);
1734#line 466
1735 zf_set_control((unsigned short)0);
1736#line 469
1737 init_timer(& zf_timer);
1738#line 470
1739 zf_timer.function = & zf_ping;
1740#line 471
1741 zf_timer.data = 0UL;
1742 }
1743#line 473
1744 return (0);
1745 no_reboot:
1746 {
1747#line 476
1748 release_region(536UL, 3UL);
1749 }
1750 no_region:
1751 {
1752#line 478
1753 misc_deregister(& zf_miscdev);
1754 }
1755 out:
1756#line 480
1757 return (ret);
1758}
1759}
1760#line 484 "machzwd.c"
1761static void zf_exit(void)
1762{
1763
1764 {
1765 {
1766#line 486
1767 zf_timer_off();
1768#line 488
1769 misc_deregister(& zf_miscdev);
1770#line 489
1771 unregister_reboot_notifier(& zf_notifier);
1772#line 490
1773 release_region(536UL, 3UL);
1774 }
1775#line 491
1776 return;
1777}
1778}
1779#line 493 "machzwd.c"
1780int (*_ddv_tmp_init)(void) = & zf_init;
1781#line 494 "machzwd.c"
1782void (*_ddv_tmp_exit)(void) = & zf_exit;
1783#line 4 "concatenated.c"
1784int main(void)
1785{
1786
1787 {
1788 {
1789#line 6
1790 _ddv_module_init = & zf_init;
1791#line 7
1792 _ddv_module_exit = & zf_exit;
1793#line 8
1794 call_ddv();
1795 }
1796#line 10
1797 return (0);
1798}
1799}
1800#line 11 "/ddverify-2010-04-30/models/seq1/include/linux/cdev.h"
1801__inline void cdev_init(struct cdev *cdev , struct file_operations *fops ) ;
1802#line 13
1803__inline struct cdev *cdev_alloc(void) ;
1804#line 17
1805__inline int cdev_add(struct cdev *p , dev_t dev , unsigned int count ) ;
1806#line 19
1807__inline void cdev_del(struct cdev *p ) ;
1808#line 12 "/ddverify-2010-04-30/models/seq1/include/ddverify/fixed_cdev.h"
1809struct cdev fixed_cdev[1] ;
1810#line 13 "/ddverify-2010-04-30/models/seq1/include/ddverify/fixed_cdev.h"
1811int fixed_cdev_used = 0;
1812#line 11 "/ddverify-2010-04-30/models/seq1/include/ddverify/cdev.h"
1813short number_cdev_registered = (short)0;
1814#line 22 "/ddverify-2010-04-30/models/seq1/include/ddverify/cdev.h"
1815struct ddv_cdev cdev_registered[1] ;
1816#line 24
1817void call_cdev_functions(void) ;
1818#line 33 "/ddverify-2010-04-30/models/seq1/include/linux/genhd.h"
1819void add_disk(struct gendisk *disk ) ;
1820#line 35
1821void del_gendisk(struct gendisk *gp ) ;
1822#line 37
1823struct gendisk *alloc_disk(int minors ) ;
1824#line 46 "/ddverify-2010-04-30/models/seq1/include/linux/workqueue.h"
1825__inline int schedule_work(struct work_struct *work ) ;
1826#line 32 "/ddverify-2010-04-30/models/seq1/include/linux/mutex.h"
1827__inline void mutex_init(struct mutex *lock ) ;
1828#line 34
1829__inline void mutex_lock(struct mutex *lock ) ;
1830#line 36
1831__inline void mutex_unlock(struct mutex *lock ) ;
1832#line 50 "/ddverify-2010-04-30/models/seq1/include/linux/interrupt.h"
1833__inline void tasklet_schedule(struct tasklet_struct *t ) ;
1834#line 65
1835__inline void tasklet_init(struct tasklet_struct *t , void (*func)(unsigned long ) ,
1836 unsigned long data ) ;
1837#line 75
1838int request_irq(unsigned int irq , irqreturn_t (*handler)(int , void * , struct pt_regs * ) ,
1839 unsigned long irqflags , char const *devname , void *dev_id ) ;
1840#line 78
1841void free_irq(unsigned int irq , void *dev_id ) ;
1842#line 192 "/ddverify-2010-04-30/models/seq1/include/linux/blkdev.h"
1843request_queue_t *blk_alloc_queue(gfp_t gfp_mask ) ;
1844#line 194
1845request_queue_t *blk_init_queue(request_fn_proc *rfn , spinlock_t *lock ) ;
1846#line 196
1847void blk_queue_make_request(request_queue_t *q , make_request_fn *mfn ) ;
1848#line 198
1849void blk_queue_hardsect_size(request_queue_t *q , unsigned short size ) ;
1850#line 200
1851void blk_cleanup_queue(request_queue_t *q ) ;
1852#line 220
1853void end_request(struct request *req , int uptodate ) ;
1854#line 12 "/ddverify-2010-04-30/models/seq1/include/ddverify/genhd.h"
1855short number_genhd_registered = (short)0;
1856#line 13 "/ddverify-2010-04-30/models/seq1/include/ddverify/genhd.h"
1857short number_fixed_genhd_used = (short)0;
1858#line 24 "/ddverify-2010-04-30/models/seq1/include/ddverify/genhd.h"
1859struct gendisk fixed_gendisk[10] ;
1860#line 25 "/ddverify-2010-04-30/models/seq1/include/ddverify/genhd.h"
1861struct ddv_genhd genhd_registered[10] ;
1862#line 27
1863void call_genhd_functions(void) ;
1864#line 87 "/ddverify-2010-04-30/models/seq1/include/linux/pci.h"
1865__inline struct pci_dev *pci_get_class(unsigned int class , struct pci_dev *from ) ;
1866#line 141
1867__inline int pci_register_driver(struct pci_driver *driver ) ;
1868#line 143
1869__inline void pci_unregister_driver(struct pci_driver *driver ) ;
1870#line 145
1871__inline int pci_enable_device(struct pci_dev *dev ) ;
1872#line 152
1873__inline int pci_request_regions(struct pci_dev *pdev , char const *res_name ) ;
1874#line 154
1875__inline void pci_release_regions(struct pci_dev *pdev ) ;
1876#line 156
1877__inline int pci_request_region(struct pci_dev *pdev , int bar , char const *res_name ) ;
1878#line 158
1879__inline void pci_release_region(struct pci_dev *pdev , int bar ) ;
1880#line 14 "/ddverify-2010-04-30/models/seq1/include/ddverify/pci.h"
1881struct ddv_pci_driver registered_pci_driver ;
1882#line 16
1883int pci_probe_device(void) ;
1884#line 17
1885void pci_remove_device(void) ;
1886#line 19
1887void call_pci_functions(void) ;
1888#line 14 "/ddverify-2010-04-30/models/seq1/include/ddverify/interrupt.h"
1889struct registered_irq registered_irq[16] ;
1890#line 16
1891void call_interrupt_handler(void) ;
1892#line 8 "/ddverify-2010-04-30/models/seq1/include/ddverify/tasklet.h"
1893short number_tasklet_registered = (short)0;
1894#line 15 "/ddverify-2010-04-30/models/seq1/include/ddverify/tasklet.h"
1895struct ddv_tasklet tasklet_registered[1] ;
1896#line 17
1897void call_tasklet_functions(void) ;
1898#line 8 "/ddverify-2010-04-30/models/seq1/include/ddverify/timer.h"
1899short number_timer_registered = (short)0;
1900#line 14 "/ddverify-2010-04-30/models/seq1/include/ddverify/timer.h"
1901struct ddv_timer timer_registered[1] ;
1902#line 16
1903void call_timer_functions(void) ;
1904#line 8 "/ddverify-2010-04-30/models/seq1/include/ddverify/workqueue.h"
1905struct work_struct *shared_workqueue[10] ;
1906#line 10
1907__inline void call_shared_workqueue_functions(void) ;
1908#line 7 "/ddverify-2010-04-30/models/seq1/include/linux/smp_lock.h"
1909spinlock_t kernel_lock ;
1910#line 26 "concatenated.c"
1911void init_kernel(void)
1912{ int i ;
1913 void *__cil_tmp2 ;
1914 void *__cil_tmp3 ;
1915
1916 {
1917 {
1918#line 30
1919 spin_lock_init(& kernel_lock);
1920#line 32
1921 i = 0;
1922 }
1923 {
1924#line 32
1925 while (1) {
1926 while_3_continue: ;
1927#line 32
1928 if (i < 10) {
1929
1930 } else {
1931 goto while_3_break;
1932 }
1933#line 33
1934 __cil_tmp2 = (void *)0;
1935#line 33
1936 shared_workqueue[i] = (struct work_struct *)__cil_tmp2;
1937#line 32
1938 i = i + 1;
1939 }
1940 while_3_break: ;
1941 }
1942#line 36
1943 i = 0;
1944 {
1945#line 36
1946 while (1) {
1947 while_4_continue: ;
1948#line 36
1949 if (i < 1) {
1950
1951 } else {
1952 goto while_4_break;
1953 }
1954#line 37
1955 __cil_tmp3 = (void *)0;
1956#line 37
1957 tasklet_registered[i].tasklet = (struct tasklet_struct *)__cil_tmp3;
1958#line 38
1959 tasklet_registered[i].is_running = (unsigned short)0;
1960#line 36
1961 i = i + 1;
1962 }
1963 while_4_break: ;
1964 }
1965#line 40
1966 return;
1967}
1968}
1969#line 42 "concatenated.c"
1970void ddv(void)
1971{ unsigned short random ;
1972
1973 {
1974 {
1975#line 46
1976 while (1) {
1977 while_5_continue: ;
1978 {
1979#line 47
1980 random = __VERIFIER_nondet_ushort();
1981 }
1982#line 50
1983 if ((int )random == 1) {
1984 goto switch_6_1;
1985 } else {
1986#line 61
1987 if ((int )random == 2) {
1988 goto switch_6_2;
1989 } else {
1990#line 66
1991 if ((int )random == 3) {
1992 goto switch_6_3;
1993 } else {
1994#line 71
1995 if ((int )random == 4) {
1996 goto switch_6_4;
1997 } else {
1998#line 76
1999 if ((int )random == 5) {
2000 goto switch_6_5;
2001 } else {
2002 {
2003 goto switch_6_default;
2004#line 49
2005 if (0) {
2006 switch_6_1:
2007 {
2008#line 51
2009 current_execution_context = 1;
2010#line 53
2011 call_cdev_functions();
2012 }
2013 goto switch_6_break;
2014 switch_6_2:
2015 {
2016#line 62
2017 current_execution_context = 2;
2018#line 63
2019 call_timer_functions();
2020 }
2021 goto switch_6_break;
2022 switch_6_3:
2023 {
2024#line 67
2025 current_execution_context = 2;
2026#line 68
2027 call_interrupt_handler();
2028 }
2029 goto switch_6_break;
2030 switch_6_4:
2031 {
2032#line 72
2033 current_execution_context = 1;
2034#line 73
2035 call_shared_workqueue_functions();
2036 }
2037 goto switch_6_break;
2038 switch_6_5:
2039 {
2040#line 77
2041 current_execution_context = 2;
2042#line 78
2043 call_tasklet_functions();
2044 }
2045 goto switch_6_break;
2046 switch_6_default: ;
2047 goto switch_6_break;
2048 } else {
2049 switch_6_break: ;
2050 }
2051 }
2052 }
2053 }
2054 }
2055 }
2056 }
2057#line 46
2058 if (random) {
2059
2060 } else {
2061 goto while_5_break;
2062 }
2063 }
2064 while_5_break: ;
2065 }
2066#line 92
2067 return;
2068}
2069}
2070#line 94 "concatenated.c"
2071int call_ddv(void)
2072{ int err ;
2073
2074 {
2075 {
2076#line 98
2077 current_execution_context = 1;
2078#line 100
2079 init_kernel();
2080#line 102
2081 err = (*_ddv_module_init)();
2082 }
2083#line 104
2084 if (err) {
2085#line 105
2086 return (-1);
2087 } else {
2088
2089 }
2090 {
2091#line 108
2092 ddv();
2093#line 110
2094 current_execution_context = 1;
2095#line 111
2096 (*_ddv_module_exit)();
2097 }
2098#line 113
2099 return (0);
2100}
2101}
2102#line 119 "concatenated.c"
2103void call_cdev_functions(void)
2104{ int cdev_no ;
2105 int result ;
2106 loff_t loff_t_value ;
2107 int int_value ;
2108 unsigned int uint_value ;
2109 unsigned long ulong_value ;
2110 char char_value ;
2111 size_t size_t_value ;
2112 unsigned short tmp ;
2113 int tmp___0 ;
2114 unsigned short tmp___1 ;
2115 int __cil_tmp13 ;
2116 int __cil_tmp14 ;
2117 struct file_operations *__cil_tmp15 ;
2118 struct file_operations *__cil_tmp16 ;
2119 loff_t (*__cil_tmp17)(struct file * , loff_t , int ) ;
2120 struct file *__cil_tmp18 ;
2121 struct file_operations *__cil_tmp19 ;
2122 struct file_operations *__cil_tmp20 ;
2123 ssize_t (*__cil_tmp21)(struct file * , char * , size_t , loff_t * ) ;
2124 struct file *__cil_tmp22 ;
2125 struct file_operations *__cil_tmp23 ;
2126 struct file_operations *__cil_tmp24 ;
2127 ssize_t (*__cil_tmp25)(struct file * , char const * , size_t , loff_t * ) ;
2128 struct file *__cil_tmp26 ;
2129 char const *__cil_tmp27 ;
2130 struct file_operations *__cil_tmp28 ;
2131 struct file_operations *__cil_tmp29 ;
2132 int (*__cil_tmp30)(struct inode * , struct file * , unsigned int , unsigned long ) ;
2133 struct inode *__cil_tmp31 ;
2134 struct file *__cil_tmp32 ;
2135 struct file_operations *__cil_tmp33 ;
2136 struct file_operations *__cil_tmp34 ;
2137 int (*__cil_tmp35)(struct inode * , struct file * ) ;
2138 struct inode *__cil_tmp36 ;
2139 struct file *__cil_tmp37 ;
2140 struct file_operations *__cil_tmp38 ;
2141 struct file_operations *__cil_tmp39 ;
2142 int (*__cil_tmp40)(struct inode * , struct file * ) ;
2143 struct inode *__cil_tmp41 ;
2144 struct file *__cil_tmp42 ;
2145
2146 {
2147 {
2148#line 130
2149 __cil_tmp13 = (int )number_cdev_registered;
2150#line 130
2151 if (__cil_tmp13 == 0) {
2152#line 131
2153 return;
2154 } else {
2155
2156 }
2157 }
2158 {
2159#line 134
2160 tmp = __VERIFIER_nondet_ushort();
2161#line 134
2162 cdev_no = (int )tmp;
2163 }
2164#line 135
2165 if (0 <= cdev_no) {
2166 {
2167#line 135
2168 __cil_tmp14 = (int )number_cdev_registered;
2169#line 135
2170 if (cdev_no < __cil_tmp14) {
2171#line 135
2172 tmp___0 = 1;
2173 } else {
2174#line 135
2175 tmp___0 = 0;
2176 }
2177 }
2178 } else {
2179#line 135
2180 tmp___0 = 0;
2181 }
2182 {
2183#line 135
2184 __VERIFIER_assume(tmp___0);
2185#line 137
2186 tmp___1 = __VERIFIER_nondet_ushort();
2187 }
2188#line 138
2189 if ((int )tmp___1 == 0) {
2190 goto switch_7_0;
2191 } else {
2192#line 148
2193 if ((int )tmp___1 == 1) {
2194 goto switch_7_1;
2195 } else {
2196#line 159
2197 if ((int )tmp___1 == 2) {
2198 goto switch_7_2;
2199 } else {
2200#line 162
2201 if ((int )tmp___1 == 3) {
2202 goto switch_7_3;
2203 } else {
2204#line 173
2205 if ((int )tmp___1 == 4) {
2206 goto switch_7_4;
2207 } else {
2208#line 176
2209 if ((int )tmp___1 == 5) {
2210 goto switch_7_5;
2211 } else {
2212#line 179
2213 if ((int )tmp___1 == 6) {
2214 goto switch_7_6;
2215 } else {
2216#line 182
2217 if ((int )tmp___1 == 7) {
2218 goto switch_7_7;
2219 } else {
2220#line 194
2221 if ((int )tmp___1 == 8) {
2222 goto switch_7_8;
2223 } else {
2224#line 197
2225 if ((int )tmp___1 == 9) {
2226 goto switch_7_9;
2227 } else {
2228#line 200
2229 if ((int )tmp___1 == 10) {
2230 goto switch_7_10;
2231 } else {
2232#line 203
2233 if ((int )tmp___1 == 11) {
2234 goto switch_7_11;
2235 } else {
2236#line 214
2237 if ((int )tmp___1 == 12) {
2238 goto switch_7_12;
2239 } else {
2240#line 217
2241 if ((int )tmp___1 == 13) {
2242 goto switch_7_13;
2243 } else {
2244#line 228
2245 if ((int )tmp___1 == 14) {
2246 goto switch_7_14;
2247 } else {
2248#line 231
2249 if ((int )tmp___1 == 15) {
2250 goto switch_7_15;
2251 } else {
2252#line 234
2253 if ((int )tmp___1 == 16) {
2254 goto switch_7_16;
2255 } else {
2256#line 237
2257 if ((int )tmp___1 == 17) {
2258 goto switch_7_17;
2259 } else {
2260#line 240
2261 if ((int )tmp___1 == 18) {
2262 goto switch_7_18;
2263 } else {
2264#line 243
2265 if ((int )tmp___1 == 19) {
2266 goto switch_7_19;
2267 } else {
2268#line 246
2269 if ((int )tmp___1 == 20) {
2270 goto switch_7_20;
2271 } else {
2272#line 249
2273 if ((int )tmp___1 == 21) {
2274 goto switch_7_21;
2275 } else {
2276#line 252
2277 if ((int )tmp___1 == 22) {
2278 goto switch_7_22;
2279 } else {
2280#line 255
2281 if ((int )tmp___1 == 23) {
2282 goto switch_7_23;
2283 } else {
2284#line 258
2285 if ((int )tmp___1 == 24) {
2286 goto switch_7_24;
2287 } else {
2288#line 261
2289 if ((int )tmp___1 == 25) {
2290 goto switch_7_25;
2291 } else {
2292#line 264
2293 if ((int )tmp___1 == 26) {
2294 goto switch_7_26;
2295 } else {
2296 {
2297 goto switch_7_default;
2298#line 137
2299 if (0) {
2300 switch_7_0:
2301 {
2302#line 139
2303 __cil_tmp15 = (cdev_registered[cdev_no].cdevp)->ops;
2304#line 139
2305 if (__cil_tmp15->llseek) {
2306 {
2307#line 140
2308 loff_t_value = __VERIFIER_nondet_loff_t();
2309#line 141
2310 int_value = __VERIFIER_nondet_int();
2311#line 143
2312 __cil_tmp16 = (cdev_registered[cdev_no].cdevp)->ops;
2313#line 143
2314 __cil_tmp17 = __cil_tmp16->llseek;
2315#line 143
2316 __cil_tmp18 = & cdev_registered[cdev_no].filp;
2317#line 143
2318 (*__cil_tmp17)(__cil_tmp18,
2319 loff_t_value,
2320 int_value);
2321 }
2322 } else {
2323
2324 }
2325 }
2326 goto switch_7_break;
2327 switch_7_1:
2328 {
2329#line 149
2330 __cil_tmp19 = (cdev_registered[cdev_no].cdevp)->ops;
2331#line 149
2332 if (__cil_tmp19->read) {
2333 {
2334#line 150
2335 char_value = __VERIFIER_nondet_char();
2336#line 151
2337 size_t_value = __VERIFIER_nondet_size_t();
2338#line 153
2339 __cil_tmp20 = (cdev_registered[cdev_no].cdevp)->ops;
2340#line 153
2341 __cil_tmp21 = __cil_tmp20->read;
2342#line 153
2343 __cil_tmp22 = & cdev_registered[cdev_no].filp;
2344#line 153
2345 (*__cil_tmp21)(__cil_tmp22,
2346 & char_value,
2347 size_t_value,
2348 & loff_t_value);
2349 }
2350 } else {
2351
2352 }
2353 }
2354 goto switch_7_break;
2355 switch_7_2:
2356 goto switch_7_break;
2357 switch_7_3:
2358 {
2359#line 163
2360 __cil_tmp23 = (cdev_registered[cdev_no].cdevp)->ops;
2361#line 163
2362 if (__cil_tmp23->write) {
2363 {
2364#line 164
2365 char_value = __VERIFIER_nondet_char();
2366#line 165
2367 size_t_value = __VERIFIER_nondet_size_t();
2368#line 167
2369 __cil_tmp24 = (cdev_registered[cdev_no].cdevp)->ops;
2370#line 167
2371 __cil_tmp25 = __cil_tmp24->write;
2372#line 167
2373 __cil_tmp26 = & cdev_registered[cdev_no].filp;
2374#line 167
2375 __cil_tmp27 = (char const *)(& char_value);
2376#line 167
2377 (*__cil_tmp25)(__cil_tmp26,
2378 __cil_tmp27,
2379 size_t_value,
2380 & loff_t_value);
2381 }
2382 } else {
2383
2384 }
2385 }
2386 goto switch_7_break;
2387 switch_7_4:
2388 goto switch_7_break;
2389 switch_7_5:
2390 goto switch_7_break;
2391 switch_7_6:
2392 goto switch_7_break;
2393 switch_7_7:
2394 {
2395#line 183
2396 __cil_tmp28 = (cdev_registered[cdev_no].cdevp)->ops;
2397#line 183
2398 if (__cil_tmp28->ioctl) {
2399 {
2400#line 184
2401 uint_value = __VERIFIER_nondet_uint();
2402#line 185
2403 ulong_value = __VERIFIER_nondet_ulong();
2404#line 187
2405 __cil_tmp29 = (cdev_registered[cdev_no].cdevp)->ops;
2406#line 187
2407 __cil_tmp30 = __cil_tmp29->ioctl;
2408#line 187
2409 __cil_tmp31 = & cdev_registered[cdev_no].inode;
2410#line 187
2411 __cil_tmp32 = & cdev_registered[cdev_no].filp;
2412#line 187
2413 (*__cil_tmp30)(__cil_tmp31,
2414 __cil_tmp32,
2415 uint_value,
2416 ulong_value);
2417 }
2418 } else {
2419
2420 }
2421 }
2422 goto switch_7_break;
2423 switch_7_8:
2424 goto switch_7_break;
2425 switch_7_9:
2426 goto switch_7_break;
2427 switch_7_10:
2428 goto switch_7_break;
2429 switch_7_11:
2430 {
2431#line 204
2432 __cil_tmp33 = (cdev_registered[cdev_no].cdevp)->ops;
2433#line 204
2434 if (__cil_tmp33->open) {
2435#line 204
2436 if (! cdev_registered[cdev_no].open) {
2437 {
2438#line 206
2439 __cil_tmp34 = (cdev_registered[cdev_no].cdevp)->ops;
2440#line 206
2441 __cil_tmp35 = __cil_tmp34->open;
2442#line 206
2443 __cil_tmp36 = & cdev_registered[cdev_no].inode;
2444#line 206
2445 __cil_tmp37 = & cdev_registered[cdev_no].filp;
2446#line 206
2447 result = (*__cil_tmp35)(__cil_tmp36,
2448 __cil_tmp37);
2449 }
2450#line 209
2451 if (! result) {
2452#line 210
2453 cdev_registered[cdev_no].open = 1;
2454 } else {
2455
2456 }
2457 } else {
2458
2459 }
2460 } else {
2461
2462 }
2463 }
2464 goto switch_7_break;
2465 switch_7_12:
2466 goto switch_7_break;
2467 switch_7_13:
2468 {
2469#line 218
2470 __cil_tmp38 = (cdev_registered[cdev_no].cdevp)->ops;
2471#line 218
2472 if (__cil_tmp38->release) {
2473#line 218
2474 if (cdev_registered[cdev_no].open) {
2475 {
2476#line 220
2477 __cil_tmp39 = (cdev_registered[cdev_no].cdevp)->ops;
2478#line 220
2479 __cil_tmp40 = __cil_tmp39->release;
2480#line 220
2481 __cil_tmp41 = & cdev_registered[cdev_no].inode;
2482#line 220
2483 __cil_tmp42 = & cdev_registered[cdev_no].filp;
2484#line 220
2485 result = (*__cil_tmp40)(__cil_tmp41,
2486 __cil_tmp42);
2487 }
2488#line 223
2489 if (! result) {
2490#line 224
2491 cdev_registered[cdev_no].open = 0;
2492 } else {
2493
2494 }
2495 } else {
2496
2497 }
2498 } else {
2499
2500 }
2501 }
2502 goto switch_7_break;
2503 switch_7_14:
2504 goto switch_7_break;
2505 switch_7_15:
2506 goto switch_7_break;
2507 switch_7_16:
2508 goto switch_7_break;
2509 switch_7_17:
2510 goto switch_7_break;
2511 switch_7_18:
2512 goto switch_7_break;
2513 switch_7_19:
2514 goto switch_7_break;
2515 switch_7_20:
2516 goto switch_7_break;
2517 switch_7_21:
2518 goto switch_7_break;
2519 switch_7_22:
2520 goto switch_7_break;
2521 switch_7_23:
2522 goto switch_7_break;
2523 switch_7_24:
2524 goto switch_7_break;
2525 switch_7_25:
2526 goto switch_7_break;
2527 switch_7_26:
2528 goto switch_7_break;
2529 switch_7_default: ;
2530 goto switch_7_break;
2531 } else {
2532 switch_7_break: ;
2533 }
2534 }
2535 }
2536 }
2537 }
2538 }
2539 }
2540 }
2541 }
2542 }
2543 }
2544 }
2545 }
2546 }
2547 }
2548 }
2549 }
2550 }
2551 }
2552 }
2553 }
2554 }
2555 }
2556 }
2557 }
2558 }
2559 }
2560 }
2561 }
2562#line 270
2563 return;
2564}
2565}
2566#line 277 "concatenated.c"
2567int create_request(int genhd_no )
2568{ struct request rq ;
2569
2570 {
2571 {
2572#line 281
2573 rq.cmd_type = (enum rq_cmd_type_bits )1;
2574#line 282
2575 rq.rq_disk = genhd_registered[genhd_no].gd;
2576#line 283
2577 rq.sector = __VERIFIER_nondet_sector_t();
2578#line 284
2579 rq.current_nr_sectors = __VERIFIER_nondet_uint();
2580#line 285
2581 rq.buffer = __VERIFIER_nondet_pchar();
2582#line 287
2583 genhd_registered[genhd_no].current_request = rq;
2584#line 288
2585 genhd_registered[genhd_no].requests_open = 1;
2586 }
2587#line 289
2588 return (0);
2589}
2590}
2591#line 291 "concatenated.c"
2592void call_rq_function(int genhd_no )
2593{ void *__cil_tmp2 ;
2594 unsigned long __cil_tmp3 ;
2595 struct request_queue *__cil_tmp4 ;
2596 request_fn_proc *__cil_tmp5 ;
2597 unsigned long __cil_tmp6 ;
2598 struct request_queue *__cil_tmp7 ;
2599 struct request_queue *__cil_tmp8 ;
2600 spinlock_t *__cil_tmp9 ;
2601 struct request_queue *__cil_tmp10 ;
2602 struct request_queue *__cil_tmp11 ;
2603 request_fn_proc *__cil_tmp12 ;
2604 struct request_queue *__cil_tmp13 ;
2605 struct request_queue *__cil_tmp14 ;
2606 spinlock_t *__cil_tmp15 ;
2607 struct request_queue *__cil_tmp16 ;
2608
2609 {
2610 {
2611#line 293
2612 __cil_tmp2 = (void *)0;
2613#line 293
2614 __cil_tmp3 = (unsigned long )__cil_tmp2;
2615#line 293
2616 __cil_tmp4 = (genhd_registered[genhd_no].gd)->queue;
2617#line 293
2618 __cil_tmp5 = __cil_tmp4->request_fn;
2619#line 293
2620 __cil_tmp6 = (unsigned long )__cil_tmp5;
2621#line 293
2622 if (__cil_tmp6 != __cil_tmp3) {
2623 {
2624#line 293
2625 __cil_tmp7 = (genhd_registered[genhd_no].gd)->queue;
2626#line 293
2627 if (__cil_tmp7->__ddv_queue_alive) {
2628 {
2629#line 296
2630 __cil_tmp8 = (genhd_registered[genhd_no].gd)->queue;
2631#line 296
2632 __cil_tmp9 = __cil_tmp8->queue_lock;
2633#line 296
2634 spin_lock(__cil_tmp9);
2635#line 298
2636 create_request(genhd_no);
2637#line 299
2638 __cil_tmp10 = (genhd_registered[genhd_no].gd)->queue;
2639#line 299
2640 __cil_tmp10->__ddv_genhd_no = genhd_no;
2641#line 301
2642 __cil_tmp11 = (genhd_registered[genhd_no].gd)->queue;
2643#line 301
2644 __cil_tmp12 = __cil_tmp11->request_fn;
2645#line 301
2646 __cil_tmp13 = (genhd_registered[genhd_no].gd)->queue;
2647#line 301
2648 (*__cil_tmp12)(__cil_tmp13);
2649#line 304
2650 __cil_tmp14 = (genhd_registered[genhd_no].gd)->queue;
2651#line 304
2652 __cil_tmp15 = __cil_tmp14->queue_lock;
2653#line 304
2654 spin_unlock(__cil_tmp15);
2655 }
2656#line 306
2657 return;
2658 } else {
2659
2660 }
2661 }
2662 } else {
2663
2664 }
2665 }
2666 {
2667#line 309
2668 __cil_tmp16 = (genhd_registered[genhd_no].gd)->queue;
2669#line 309
2670 if (__cil_tmp16->make_request_fn) {
2671#line 310
2672 return;
2673 } else {
2674
2675 }
2676 }
2677#line 312
2678 return;
2679}
2680}
2681#line 314 "concatenated.c"
2682void call_genhd_functions(void)
2683{ unsigned short genhd_no ;
2684 unsigned short function_no ;
2685 unsigned int uint_value ;
2686 unsigned long ulong_value ;
2687 void *tmp ;
2688 struct hd_geometry hdg ;
2689 struct block_device blk_dev ;
2690 int __cil_tmp9 ;
2691 int __cil_tmp10 ;
2692 int __cil_tmp11 ;
2693 int __cil_tmp12 ;
2694 int __cil_tmp13 ;
2695 struct block_device_operations *__cil_tmp14 ;
2696 unsigned int __cil_tmp15 ;
2697 struct block_device_operations *__cil_tmp16 ;
2698 int (*__cil_tmp17)(struct inode * , struct file * ) ;
2699 struct inode *__cil_tmp18 ;
2700 struct file *__cil_tmp19 ;
2701 struct block_device_operations *__cil_tmp20 ;
2702 struct block_device_operations *__cil_tmp21 ;
2703 int (*__cil_tmp22)(struct inode * , struct file * ) ;
2704 struct inode *__cil_tmp23 ;
2705 struct file *__cil_tmp24 ;
2706 struct block_device_operations *__cil_tmp25 ;
2707 struct block_device_operations *__cil_tmp26 ;
2708 int (*__cil_tmp27)(struct inode * , struct file * , unsigned int , unsigned long ) ;
2709 struct inode *__cil_tmp28 ;
2710 struct file *__cil_tmp29 ;
2711 struct block_device_operations *__cil_tmp30 ;
2712 struct block_device_operations *__cil_tmp31 ;
2713 int (*__cil_tmp32)(struct gendisk * ) ;
2714 struct block_device_operations *__cil_tmp33 ;
2715 struct block_device_operations *__cil_tmp34 ;
2716 int (*__cil_tmp35)(struct gendisk * ) ;
2717 struct block_device_operations *__cil_tmp36 ;
2718 struct block_device_operations *__cil_tmp37 ;
2719 int (*__cil_tmp38)(struct block_device * , struct hd_geometry * ) ;
2720
2721 {
2722 {
2723#line 321
2724 __cil_tmp9 = (int )number_genhd_registered;
2725#line 321
2726 if (__cil_tmp9 == 0) {
2727#line 322
2728 return;
2729 } else {
2730
2731 }
2732 }
2733 {
2734#line 325
2735 genhd_no = __VERIFIER_nondet_ushort();
2736#line 326
2737 __cil_tmp10 = (int )number_genhd_registered;
2738#line 326
2739 __cil_tmp11 = (int )genhd_no;
2740#line 326
2741 __cil_tmp12 = __cil_tmp11 < __cil_tmp10;
2742#line 326
2743 __VERIFIER_assume(__cil_tmp12);
2744#line 329
2745 function_no = __VERIFIER_nondet_ushort();
2746 }
2747#line 332
2748 if ((int )function_no == 0) {
2749 goto switch_8_0;
2750 } else {
2751#line 336
2752 if ((int )function_no == 1) {
2753 goto switch_8_1;
2754 } else {
2755#line 346
2756 if ((int )function_no == 2) {
2757 goto switch_8_2;
2758 } else {
2759#line 353
2760 if ((int )function_no == 3) {
2761 goto switch_8_3;
2762 } else {
2763#line 364
2764 if ((int )function_no == 4) {
2765 goto switch_8_4;
2766 } else {
2767#line 370
2768 if ((int )function_no == 5) {
2769 goto switch_8_5;
2770 } else {
2771#line 376
2772 if ((int )function_no == 6) {
2773 goto switch_8_6;
2774 } else {
2775 {
2776 goto switch_8_default;
2777#line 331
2778 if (0) {
2779 switch_8_0:
2780 {
2781#line 333
2782 __cil_tmp13 = (int )genhd_no;
2783#line 333
2784 call_rq_function(__cil_tmp13);
2785 }
2786 goto switch_8_break;
2787 switch_8_1:
2788 {
2789#line 337
2790 __cil_tmp14 = (genhd_registered[genhd_no].gd)->fops;
2791#line 337
2792 if (__cil_tmp14->open) {
2793 {
2794#line 338
2795 __cil_tmp15 = (unsigned int )32UL;
2796#line 338
2797 tmp = malloc(__cil_tmp15);
2798#line 338
2799 genhd_registered[genhd_no].inode.i_bdev = (struct block_device *)tmp;
2800#line 339
2801 (genhd_registered[genhd_no].inode.i_bdev)->bd_disk = genhd_registered[genhd_no].gd;
2802#line 341
2803 __cil_tmp16 = (genhd_registered[genhd_no].gd)->fops;
2804#line 341
2805 __cil_tmp17 = __cil_tmp16->open;
2806#line 341
2807 __cil_tmp18 = & genhd_registered[genhd_no].inode;
2808#line 341
2809 __cil_tmp19 = & genhd_registered[genhd_no].file;
2810#line 341
2811 (*__cil_tmp17)(__cil_tmp18, __cil_tmp19);
2812 }
2813 } else {
2814
2815 }
2816 }
2817 goto switch_8_break;
2818 switch_8_2:
2819 {
2820#line 347
2821 __cil_tmp20 = (genhd_registered[genhd_no].gd)->fops;
2822#line 347
2823 if (__cil_tmp20->release) {
2824 {
2825#line 348
2826 __cil_tmp21 = (genhd_registered[genhd_no].gd)->fops;
2827#line 348
2828 __cil_tmp22 = __cil_tmp21->release;
2829#line 348
2830 __cil_tmp23 = & genhd_registered[genhd_no].inode;
2831#line 348
2832 __cil_tmp24 = & genhd_registered[genhd_no].file;
2833#line 348
2834 (*__cil_tmp22)(__cil_tmp23, __cil_tmp24);
2835 }
2836 } else {
2837
2838 }
2839 }
2840 goto switch_8_break;
2841 switch_8_3:
2842 {
2843#line 354
2844 __cil_tmp25 = (genhd_registered[genhd_no].gd)->fops;
2845#line 354
2846 if (__cil_tmp25->ioctl) {
2847 {
2848#line 355
2849 uint_value = __VERIFIER_nondet_uint();
2850#line 356
2851 ulong_value = __VERIFIER_nondet_ulong();
2852#line 357
2853 __cil_tmp26 = (genhd_registered[genhd_no].gd)->fops;
2854#line 357
2855 __cil_tmp27 = __cil_tmp26->ioctl;
2856#line 357
2857 __cil_tmp28 = & genhd_registered[genhd_no].inode;
2858#line 357
2859 __cil_tmp29 = & genhd_registered[genhd_no].file;
2860#line 357
2861 (*__cil_tmp27)(__cil_tmp28, __cil_tmp29, uint_value, ulong_value);
2862 }
2863 } else {
2864
2865 }
2866 }
2867 goto switch_8_break;
2868 switch_8_4:
2869 {
2870#line 365
2871 __cil_tmp30 = (genhd_registered[genhd_no].gd)->fops;
2872#line 365
2873 if (__cil_tmp30->media_changed) {
2874 {
2875#line 366
2876 __cil_tmp31 = (genhd_registered[genhd_no].gd)->fops;
2877#line 366
2878 __cil_tmp32 = __cil_tmp31->media_changed;
2879#line 366
2880 (*__cil_tmp32)(genhd_registered[genhd_no].gd);
2881 }
2882 } else {
2883
2884 }
2885 }
2886 goto switch_8_break;
2887 switch_8_5:
2888 {
2889#line 371
2890 __cil_tmp33 = (genhd_registered[genhd_no].gd)->fops;
2891#line 371
2892 if (__cil_tmp33->revalidate_disk) {
2893 {
2894#line 372
2895 __cil_tmp34 = (genhd_registered[genhd_no].gd)->fops;
2896#line 372
2897 __cil_tmp35 = __cil_tmp34->revalidate_disk;
2898#line 372
2899 (*__cil_tmp35)(genhd_registered[genhd_no].gd);
2900 }
2901 } else {
2902
2903 }
2904 }
2905 goto switch_8_break;
2906 switch_8_6:
2907 {
2908#line 377
2909 __cil_tmp36 = (genhd_registered[genhd_no].gd)->fops;
2910#line 377
2911 if (__cil_tmp36->getgeo) {
2912 {
2913#line 381
2914 blk_dev.bd_disk = genhd_registered[genhd_no].gd;
2915#line 383
2916 __cil_tmp37 = (genhd_registered[genhd_no].gd)->fops;
2917#line 383
2918 __cil_tmp38 = __cil_tmp37->getgeo;
2919#line 383
2920 (*__cil_tmp38)(& blk_dev, & hdg);
2921 }
2922 } else {
2923
2924 }
2925 }
2926 goto switch_8_break;
2927 switch_8_default: ;
2928 goto switch_8_break;
2929 } else {
2930 switch_8_break: ;
2931 }
2932 }
2933 }
2934 }
2935 }
2936 }
2937 }
2938 }
2939 }
2940#line 390
2941 return;
2942}
2943}
2944#line 400 "concatenated.c"
2945void call_interrupt_handler(void)
2946{ unsigned short i ;
2947 struct pt_regs regs ;
2948 int tmp ;
2949 int __cil_tmp4 ;
2950 int __cil_tmp5 ;
2951 int __cil_tmp6 ;
2952
2953 {
2954 {
2955#line 405
2956 tmp = __VERIFIER_nondet_int();
2957#line 405
2958 i = (unsigned short )tmp;
2959#line 406
2960 __cil_tmp4 = (int )i;
2961#line 406
2962 __cil_tmp5 = __cil_tmp4 < 16;
2963#line 406
2964 __VERIFIER_assume(__cil_tmp5);
2965 }
2966#line 408
2967 if (registered_irq[i].handler) {
2968 {
2969#line 409
2970 __cil_tmp6 = (int )i;
2971#line 409
2972 (*(registered_irq[i].handler))(__cil_tmp6, registered_irq[i].dev_id, & regs);
2973 }
2974 } else {
2975
2976 }
2977#line 412
2978 return;
2979}
2980}
2981#line 438 "concatenated.c"
2982void create_pci_dev(void)
2983{
2984
2985 {
2986#line 440
2987 return;
2988}
2989}
2990#line 442 "concatenated.c"
2991int pci_probe_device(void)
2992{ int err ;
2993 unsigned int dev_id ;
2994 int __cil_tmp3 ;
2995 int (*__cil_tmp4)(struct pci_dev *dev , struct pci_device_id const *id ) ;
2996 struct pci_dev *__cil_tmp5 ;
2997 struct pci_device_id const *__cil_tmp6 ;
2998 struct pci_device_id const *__cil_tmp7 ;
2999
3000 {
3001 {
3002#line 447
3003 registered_pci_driver.no_pci_device_id = 1U;
3004#line 449
3005 dev_id = __VERIFIER_nondet_uint();
3006#line 450
3007 __cil_tmp3 = dev_id < registered_pci_driver.no_pci_device_id;
3008#line 450
3009 __VERIFIER_assume(__cil_tmp3);
3010#line 452
3011 __cil_tmp4 = (registered_pci_driver.pci_driver)->probe;
3012#line 452
3013 __cil_tmp5 = & registered_pci_driver.pci_dev;
3014#line 452
3015 __cil_tmp6 = (registered_pci_driver.pci_driver)->id_table;
3016#line 452
3017 __cil_tmp7 = __cil_tmp6 + dev_id;
3018#line 452
3019 err = (*__cil_tmp4)(__cil_tmp5, __cil_tmp7);
3020 }
3021#line 455
3022 if (! err) {
3023#line 456
3024 registered_pci_driver.dev_initialized = 1;
3025 } else {
3026
3027 }
3028#line 459
3029 return (err);
3030}
3031}
3032#line 462 "concatenated.c"
3033void pci_remove_device(void)
3034{ void (*__cil_tmp1)(struct pci_dev *dev ) ;
3035 struct pci_dev *__cil_tmp2 ;
3036
3037 {
3038 {
3039#line 464
3040 __cil_tmp1 = (registered_pci_driver.pci_driver)->remove;
3041#line 464
3042 __cil_tmp2 = & registered_pci_driver.pci_dev;
3043#line 464
3044 (*__cil_tmp1)(__cil_tmp2);
3045#line 466
3046 registered_pci_driver.dev_initialized = 0;
3047 }
3048#line 467
3049 return;
3050}
3051}
3052#line 469 "concatenated.c"
3053void call_pci_functions(void)
3054{ unsigned int tmp ;
3055
3056 {
3057 {
3058#line 471
3059 tmp = __VERIFIER_nondet_uint();
3060 }
3061#line 472
3062 if ((int )tmp == 0) {
3063 goto switch_9_0;
3064 } else {
3065#line 478
3066 if ((int )tmp == 1) {
3067 goto switch_9_1;
3068 } else {
3069 {
3070 goto switch_9_default;
3071#line 471
3072 if (0) {
3073 switch_9_0:
3074#line 473
3075 if (! registered_pci_driver.dev_initialized) {
3076 {
3077#line 474
3078 pci_probe_device();
3079 }
3080 } else {
3081
3082 }
3083 goto switch_9_break;
3084 switch_9_1:
3085#line 479
3086 if (registered_pci_driver.dev_initialized) {
3087 {
3088#line 480
3089 pci_remove_device();
3090 }
3091 } else {
3092
3093 }
3094 goto switch_9_break;
3095 switch_9_default: ;
3096 goto switch_9_break;
3097 } else {
3098 switch_9_break: ;
3099 }
3100 }
3101 }
3102 }
3103#line 487
3104 return;
3105}
3106}
3107#line 490 "concatenated.c"
3108void call_tasklet_functions(void)
3109{ unsigned int i ;
3110 int __cil_tmp2 ;
3111 void *__cil_tmp3 ;
3112 unsigned long __cil_tmp4 ;
3113 unsigned long __cil_tmp5 ;
3114 atomic_t __cil_tmp6 ;
3115 void (*__cil_tmp7)(unsigned long ) ;
3116 unsigned long __cil_tmp8 ;
3117 void *__cil_tmp9 ;
3118
3119 {
3120 {
3121#line 493
3122 __cil_tmp2 = i < 1U;
3123#line 493
3124 __VERIFIER_assume(__cil_tmp2);
3125 }
3126 {
3127#line 495
3128 __cil_tmp3 = (void *)0;
3129#line 495
3130 __cil_tmp4 = (unsigned long )__cil_tmp3;
3131#line 495
3132 __cil_tmp5 = (unsigned long )tasklet_registered[i].tasklet;
3133#line 495
3134 if (__cil_tmp5 != __cil_tmp4) {
3135 {
3136#line 495
3137 __cil_tmp6 = (tasklet_registered[i].tasklet)->count;
3138#line 495
3139 if (__cil_tmp6 == 0) {
3140 {
3141#line 497
3142 tasklet_registered[i].is_running = (unsigned short)1;
3143#line 498
3144 __cil_tmp7 = (tasklet_registered[i].tasklet)->func;
3145#line 498
3146 __cil_tmp8 = (tasklet_registered[i].tasklet)->data;
3147#line 498
3148 (*__cil_tmp7)(__cil_tmp8);
3149#line 499
3150 tasklet_registered[i].is_running = (unsigned short)0;
3151#line 500
3152 __cil_tmp9 = (void *)0;
3153#line 500
3154 tasklet_registered[i].tasklet = (struct tasklet_struct *)__cil_tmp9;
3155 }
3156 } else {
3157
3158 }
3159 }
3160 } else {
3161
3162 }
3163 }
3164#line 502
3165 return;
3166}
3167}
3168#line 506 "concatenated.c"
3169void call_timer_functions(void)
3170{ unsigned short i ;
3171 unsigned short tmp ;
3172 int __cil_tmp3 ;
3173 int __cil_tmp4 ;
3174 int __cil_tmp5 ;
3175 void (*__cil_tmp6)(unsigned long ) ;
3176 unsigned long __cil_tmp7 ;
3177
3178 {
3179 {
3180#line 508
3181 tmp = __VERIFIER_nondet_ushort();
3182#line 508
3183 i = tmp;
3184#line 510
3185 __cil_tmp3 = (int )number_timer_registered;
3186#line 510
3187 __cil_tmp4 = (int )i;
3188#line 510
3189 __cil_tmp5 = __cil_tmp4 < __cil_tmp3;
3190#line 510
3191 __VERIFIER_assume(__cil_tmp5);
3192 }
3193#line 512
3194 if ((timer_registered[i].timer)->__ddv_active) {
3195 {
3196#line 513
3197 __cil_tmp6 = (timer_registered[i].timer)->function;
3198#line 513
3199 __cil_tmp7 = (timer_registered[i].timer)->data;
3200#line 513
3201 (*__cil_tmp6)(__cil_tmp7);
3202 }
3203 } else {
3204
3205 }
3206#line 515
3207 return;
3208}
3209}
3210#line 523 "concatenated.c"
3211__inline int pci_enable_device(struct pci_dev *dev )
3212{ int i ;
3213 unsigned int tmp ;
3214 unsigned short tmp___0 ;
3215 unsigned long __cil_tmp5 ;
3216 unsigned long __cil_tmp6 ;
3217
3218 {
3219#line 527
3220 i = 0;
3221 {
3222#line 527
3223 while (1) {
3224 while_10_continue: ;
3225#line 527
3226 if (i < 12) {
3227
3228 } else {
3229 goto while_10_break;
3230 }
3231 {
3232#line 528
3233 dev->resource[i].flags = 256UL;
3234#line 529
3235 tmp = __VERIFIER_nondet_uint();
3236#line 529
3237 dev->resource[i].start = (unsigned long )tmp;
3238#line 530
3239 tmp___0 = __VERIFIER_nondet_ushort();
3240#line 530
3241 __cil_tmp5 = (unsigned long )tmp___0;
3242#line 530
3243 __cil_tmp6 = dev->resource[i].start;
3244#line 530
3245 dev->resource[i].end = __cil_tmp6 + __cil_tmp5;
3246#line 527
3247 i = i + 1;
3248 }
3249 }
3250 while_10_break: ;
3251 }
3252#line 532
3253 return (0);
3254}
3255}
3256#line 534 "concatenated.c"
3257__inline struct pci_dev *pci_get_class(unsigned int class , struct pci_dev *from )
3258{ void *tmp ;
3259 int tmp___0 ;
3260 void *__cil_tmp5 ;
3261 unsigned long __cil_tmp6 ;
3262 unsigned long __cil_tmp7 ;
3263 unsigned int __cil_tmp8 ;
3264 unsigned int __cil_tmp9 ;
3265 int __cil_tmp10 ;
3266 void *__cil_tmp11 ;
3267
3268 {
3269 {
3270#line 536
3271 __cil_tmp5 = (void *)0;
3272#line 536
3273 __cil_tmp6 = (unsigned long )__cil_tmp5;
3274#line 536
3275 __cil_tmp7 = (unsigned long )from;
3276#line 536
3277 if (__cil_tmp7 == __cil_tmp6) {
3278 {
3279#line 537
3280 __cil_tmp8 = (unsigned int )432UL;
3281#line 537
3282 tmp = malloc(__cil_tmp8);
3283#line 537
3284 from = (struct pci_dev *)tmp;
3285 }
3286 } else {
3287
3288 }
3289 }
3290 {
3291#line 540
3292 tmp___0 = __VERIFIER_nondet_int();
3293 }
3294#line 540
3295 if (tmp___0) {
3296 {
3297#line 541
3298 from->vendor = __VERIFIER_nondet_ushort();
3299#line 542
3300 from->device = __VERIFIER_nondet_ushort();
3301#line 543
3302 from->irq = __VERIFIER_nondet_uint();
3303#line 544
3304 __cil_tmp9 = from->irq;
3305#line 544
3306 __cil_tmp10 = __cil_tmp9 < 16U;
3307#line 544
3308 __VERIFIER_assume(__cil_tmp10);
3309 }
3310#line 546
3311 return (from);
3312 } else {
3313 {
3314#line 548
3315 __cil_tmp11 = (void *)0;
3316#line 548
3317 return ((struct pci_dev *)__cil_tmp11);
3318 }
3319 }
3320}
3321}
3322#line 552 "concatenated.c"
3323__inline int pci_register_driver(struct pci_driver *driver )
3324{ int tmp ;
3325 unsigned long __cil_tmp3 ;
3326
3327 {
3328 {
3329#line 554
3330 tmp = __VERIFIER_nondet_int();
3331 }
3332#line 554
3333 if (tmp) {
3334#line 555
3335 registered_pci_driver.pci_driver = driver;
3336#line 556
3337 __cil_tmp3 = 8UL / 32UL;
3338#line 556
3339 registered_pci_driver.no_pci_device_id = (unsigned int )__cil_tmp3;
3340#line 557
3341 registered_pci_driver.dev_initialized = 0;
3342#line 559
3343 return (0);
3344 } else {
3345#line 561
3346 return (-1);
3347 }
3348}
3349}
3350#line 565 "concatenated.c"
3351__inline void pci_unregister_driver(struct pci_driver *driver )
3352{ void *__cil_tmp2 ;
3353
3354 {
3355#line 567
3356 __cil_tmp2 = (void *)0;
3357#line 567
3358 registered_pci_driver.pci_driver = (struct pci_driver *)__cil_tmp2;
3359#line 568
3360 registered_pci_driver.no_pci_device_id = 0U;
3361#line 569
3362 return;
3363}
3364}
3365#line 571 "concatenated.c"
3366__inline void pci_release_region(struct pci_dev *pdev , int bar )
3367{ unsigned long tmp ;
3368 unsigned long tmp___0 ;
3369 unsigned long tmp___1 ;
3370 unsigned long __cil_tmp6 ;
3371 unsigned long __cil_tmp7 ;
3372 unsigned long __cil_tmp8 ;
3373 unsigned long __cil_tmp9 ;
3374 unsigned long __cil_tmp10 ;
3375 unsigned long __cil_tmp11 ;
3376 unsigned long __cil_tmp12 ;
3377 unsigned long __cil_tmp13 ;
3378 unsigned long __cil_tmp14 ;
3379 unsigned long __cil_tmp15 ;
3380 unsigned long __cil_tmp16 ;
3381 unsigned long __cil_tmp17 ;
3382 unsigned long __cil_tmp18 ;
3383 unsigned long __cil_tmp19 ;
3384 unsigned long __cil_tmp20 ;
3385 unsigned long __cil_tmp21 ;
3386 unsigned long __cil_tmp22 ;
3387 unsigned long __cil_tmp23 ;
3388 unsigned long __cil_tmp24 ;
3389 unsigned long __cil_tmp25 ;
3390 unsigned long __cil_tmp26 ;
3391 unsigned long __cil_tmp27 ;
3392 unsigned long __cil_tmp28 ;
3393 unsigned long __cil_tmp29 ;
3394 unsigned long __cil_tmp30 ;
3395 unsigned long __cil_tmp31 ;
3396 unsigned long __cil_tmp32 ;
3397 unsigned long __cil_tmp33 ;
3398 unsigned long __cil_tmp34 ;
3399 unsigned long __cil_tmp35 ;
3400 unsigned long __cil_tmp36 ;
3401
3402 {
3403 {
3404#line 573
3405 __cil_tmp6 = pdev->resource[bar].start;
3406#line 573
3407 if (__cil_tmp6 == 0UL) {
3408 {
3409#line 573
3410 __cil_tmp7 = pdev->resource[bar].start;
3411#line 573
3412 __cil_tmp8 = pdev->resource[bar].end;
3413#line 573
3414 if (__cil_tmp8 == __cil_tmp7) {
3415#line 573
3416 tmp = 0UL;
3417 } else {
3418#line 573
3419 __cil_tmp9 = pdev->resource[bar].start;
3420#line 573
3421 __cil_tmp10 = pdev->resource[bar].end;
3422#line 573
3423 __cil_tmp11 = __cil_tmp10 - __cil_tmp9;
3424#line 573
3425 tmp = __cil_tmp11 + 1UL;
3426 }
3427 }
3428 } else {
3429#line 573
3430 __cil_tmp12 = pdev->resource[bar].start;
3431#line 573
3432 __cil_tmp13 = pdev->resource[bar].end;
3433#line 573
3434 __cil_tmp14 = __cil_tmp13 - __cil_tmp12;
3435#line 573
3436 tmp = __cil_tmp14 + 1UL;
3437 }
3438 }
3439#line 573
3440 if (tmp == 0UL) {
3441#line 574
3442 return;
3443 } else {
3444
3445 }
3446 {
3447#line 575
3448 __cil_tmp15 = pdev->resource[bar].flags;
3449#line 575
3450 if (__cil_tmp15 & 256UL) {
3451 {
3452#line 576
3453 __cil_tmp16 = pdev->resource[bar].start;
3454#line 576
3455 if (__cil_tmp16 == 0UL) {
3456 {
3457#line 576
3458 __cil_tmp17 = pdev->resource[bar].start;
3459#line 576
3460 __cil_tmp18 = pdev->resource[bar].end;
3461#line 576
3462 if (__cil_tmp18 == __cil_tmp17) {
3463#line 576
3464 tmp___0 = 0UL;
3465 } else {
3466#line 576
3467 __cil_tmp19 = pdev->resource[bar].start;
3468#line 576
3469 __cil_tmp20 = pdev->resource[bar].end;
3470#line 576
3471 __cil_tmp21 = __cil_tmp20 - __cil_tmp19;
3472#line 576
3473 tmp___0 = __cil_tmp21 + 1UL;
3474 }
3475 }
3476 } else {
3477#line 576
3478 __cil_tmp22 = pdev->resource[bar].start;
3479#line 576
3480 __cil_tmp23 = pdev->resource[bar].end;
3481#line 576
3482 __cil_tmp24 = __cil_tmp23 - __cil_tmp22;
3483#line 576
3484 tmp___0 = __cil_tmp24 + 1UL;
3485 }
3486 }
3487 {
3488#line 576
3489 __cil_tmp25 = pdev->resource[bar].start;
3490#line 576
3491 release_region(__cil_tmp25, tmp___0);
3492 }
3493 } else {
3494 {
3495#line 578
3496 __cil_tmp26 = pdev->resource[bar].flags;
3497#line 578
3498 if (__cil_tmp26 & 512UL) {
3499 {
3500#line 579
3501 __cil_tmp27 = pdev->resource[bar].start;
3502#line 579
3503 if (__cil_tmp27 == 0UL) {
3504 {
3505#line 579
3506 __cil_tmp28 = pdev->resource[bar].start;
3507#line 579
3508 __cil_tmp29 = pdev->resource[bar].end;
3509#line 579
3510 if (__cil_tmp29 == __cil_tmp28) {
3511#line 579
3512 tmp___1 = 0UL;
3513 } else {
3514#line 579
3515 __cil_tmp30 = pdev->resource[bar].start;
3516#line 579
3517 __cil_tmp31 = pdev->resource[bar].end;
3518#line 579
3519 __cil_tmp32 = __cil_tmp31 - __cil_tmp30;
3520#line 579
3521 tmp___1 = __cil_tmp32 + 1UL;
3522 }
3523 }
3524 } else {
3525#line 579
3526 __cil_tmp33 = pdev->resource[bar].start;
3527#line 579
3528 __cil_tmp34 = pdev->resource[bar].end;
3529#line 579
3530 __cil_tmp35 = __cil_tmp34 - __cil_tmp33;
3531#line 579
3532 tmp___1 = __cil_tmp35 + 1UL;
3533 }
3534 }
3535 {
3536#line 579
3537 __cil_tmp36 = pdev->resource[bar].start;
3538#line 579
3539 release_mem_region(__cil_tmp36, tmp___1);
3540 }
3541 } else {
3542
3543 }
3544 }
3545 }
3546 }
3547#line 581
3548 return;
3549}
3550}
3551#line 583 "concatenated.c"
3552__inline int pci_request_region(struct pci_dev *pdev , int bar , char const *res_name )
3553{ unsigned long tmp ;
3554 unsigned long tmp___0 ;
3555 struct resource *tmp___1 ;
3556 unsigned long tmp___2 ;
3557 struct resource *tmp___3 ;
3558 unsigned long __cil_tmp9 ;
3559 unsigned long __cil_tmp10 ;
3560 unsigned long __cil_tmp11 ;
3561 unsigned long __cil_tmp12 ;
3562 unsigned long __cil_tmp13 ;
3563 unsigned long __cil_tmp14 ;
3564 unsigned long __cil_tmp15 ;
3565 unsigned long __cil_tmp16 ;
3566 unsigned long __cil_tmp17 ;
3567 unsigned long __cil_tmp18 ;
3568 unsigned long __cil_tmp19 ;
3569 unsigned long __cil_tmp20 ;
3570 unsigned long __cil_tmp21 ;
3571 unsigned long __cil_tmp22 ;
3572 unsigned long __cil_tmp23 ;
3573 unsigned long __cil_tmp24 ;
3574 unsigned long __cil_tmp25 ;
3575 unsigned long __cil_tmp26 ;
3576 unsigned long __cil_tmp27 ;
3577 unsigned long __cil_tmp28 ;
3578 unsigned long __cil_tmp29 ;
3579 unsigned long __cil_tmp30 ;
3580 unsigned long __cil_tmp31 ;
3581 unsigned long __cil_tmp32 ;
3582 unsigned long __cil_tmp33 ;
3583 unsigned long __cil_tmp34 ;
3584 unsigned long __cil_tmp35 ;
3585 unsigned long __cil_tmp36 ;
3586 unsigned long __cil_tmp37 ;
3587 unsigned long __cil_tmp38 ;
3588 unsigned long __cil_tmp39 ;
3589
3590 {
3591 {
3592#line 585
3593 __cil_tmp9 = pdev->resource[bar].start;
3594#line 585
3595 if (__cil_tmp9 == 0UL) {
3596 {
3597#line 585
3598 __cil_tmp10 = pdev->resource[bar].start;
3599#line 585
3600 __cil_tmp11 = pdev->resource[bar].end;
3601#line 585
3602 if (__cil_tmp11 == __cil_tmp10) {
3603#line 585
3604 tmp = 0UL;
3605 } else {
3606#line 585
3607 __cil_tmp12 = pdev->resource[bar].start;
3608#line 585
3609 __cil_tmp13 = pdev->resource[bar].end;
3610#line 585
3611 __cil_tmp14 = __cil_tmp13 - __cil_tmp12;
3612#line 585
3613 tmp = __cil_tmp14 + 1UL;
3614 }
3615 }
3616 } else {
3617#line 585
3618 __cil_tmp15 = pdev->resource[bar].start;
3619#line 585
3620 __cil_tmp16 = pdev->resource[bar].end;
3621#line 585
3622 __cil_tmp17 = __cil_tmp16 - __cil_tmp15;
3623#line 585
3624 tmp = __cil_tmp17 + 1UL;
3625 }
3626 }
3627#line 585
3628 if (tmp == 0UL) {
3629#line 586
3630 return (0);
3631 } else {
3632
3633 }
3634 {
3635#line 588
3636 __cil_tmp18 = pdev->resource[bar].flags;
3637#line 588
3638 if (__cil_tmp18 & 256UL) {
3639 {
3640#line 589
3641 __cil_tmp19 = pdev->resource[bar].start;
3642#line 589
3643 if (__cil_tmp19 == 0UL) {
3644 {
3645#line 589
3646 __cil_tmp20 = pdev->resource[bar].start;
3647#line 589
3648 __cil_tmp21 = pdev->resource[bar].end;
3649#line 589
3650 if (__cil_tmp21 == __cil_tmp20) {
3651#line 589
3652 tmp___0 = 0UL;
3653 } else {
3654#line 589
3655 __cil_tmp22 = pdev->resource[bar].start;
3656#line 589
3657 __cil_tmp23 = pdev->resource[bar].end;
3658#line 589
3659 __cil_tmp24 = __cil_tmp23 - __cil_tmp22;
3660#line 589
3661 tmp___0 = __cil_tmp24 + 1UL;
3662 }
3663 }
3664 } else {
3665#line 589
3666 __cil_tmp25 = pdev->resource[bar].start;
3667#line 589
3668 __cil_tmp26 = pdev->resource[bar].end;
3669#line 589
3670 __cil_tmp27 = __cil_tmp26 - __cil_tmp25;
3671#line 589
3672 tmp___0 = __cil_tmp27 + 1UL;
3673 }
3674 }
3675 {
3676#line 589
3677 __cil_tmp28 = pdev->resource[bar].start;
3678#line 589
3679 tmp___1 = request_region(__cil_tmp28, tmp___0, res_name);
3680 }
3681#line 589
3682 if (tmp___1) {
3683
3684 } else {
3685#line 591
3686 return (-16);
3687 }
3688 } else {
3689 {
3690#line 593
3691 __cil_tmp29 = pdev->resource[bar].flags;
3692#line 593
3693 if (__cil_tmp29 & 512UL) {
3694 {
3695#line 594
3696 __cil_tmp30 = pdev->resource[bar].start;
3697#line 594
3698 if (__cil_tmp30 == 0UL) {
3699 {
3700#line 594
3701 __cil_tmp31 = pdev->resource[bar].start;
3702#line 594
3703 __cil_tmp32 = pdev->resource[bar].end;
3704#line 594
3705 if (__cil_tmp32 == __cil_tmp31) {
3706#line 594
3707 tmp___2 = 0UL;
3708 } else {
3709#line 594
3710 __cil_tmp33 = pdev->resource[bar].start;
3711#line 594
3712 __cil_tmp34 = pdev->resource[bar].end;
3713#line 594
3714 __cil_tmp35 = __cil_tmp34 - __cil_tmp33;
3715#line 594
3716 tmp___2 = __cil_tmp35 + 1UL;
3717 }
3718 }
3719 } else {
3720#line 594
3721 __cil_tmp36 = pdev->resource[bar].start;
3722#line 594
3723 __cil_tmp37 = pdev->resource[bar].end;
3724#line 594
3725 __cil_tmp38 = __cil_tmp37 - __cil_tmp36;
3726#line 594
3727 tmp___2 = __cil_tmp38 + 1UL;
3728 }
3729 }
3730 {
3731#line 594
3732 __cil_tmp39 = pdev->resource[bar].start;
3733#line 594
3734 tmp___3 = request_mem_region(__cil_tmp39, tmp___2, res_name);
3735 }
3736#line 594
3737 if (tmp___3) {
3738
3739 } else {
3740#line 596
3741 return (-16);
3742 }
3743 } else {
3744
3745 }
3746 }
3747 }
3748 }
3749#line 599
3750 return (0);
3751}
3752}
3753#line 602 "concatenated.c"
3754__inline void pci_release_regions(struct pci_dev *pdev )
3755{ int i ;
3756
3757 {
3758#line 606
3759 i = 0;
3760 {
3761#line 606
3762 while (1) {
3763 while_11_continue: ;
3764#line 606
3765 if (i < 6) {
3766
3767 } else {
3768 goto while_11_break;
3769 }
3770 {
3771#line 607
3772 pci_release_region(pdev, i);
3773#line 606
3774 i = i + 1;
3775 }
3776 }
3777 while_11_break: ;
3778 }
3779#line 608
3780 return;
3781}
3782}
3783#line 610 "concatenated.c"
3784__inline int pci_request_regions(struct pci_dev *pdev , char const *res_name )
3785{ int i ;
3786 int tmp ;
3787
3788 {
3789#line 614
3790 i = 0;
3791 {
3792#line 614
3793 while (1) {
3794 while_12_continue: ;
3795#line 614
3796 if (i < 6) {
3797
3798 } else {
3799 goto while_12_break;
3800 }
3801 {
3802#line 615
3803 tmp = pci_request_region(pdev, i, res_name);
3804 }
3805#line 615
3806 if (tmp) {
3807 goto err_out;
3808 } else {
3809
3810 }
3811#line 614
3812 i = i + 1;
3813 }
3814 while_12_break: ;
3815 }
3816#line 617
3817 return (0);
3818 err_out:
3819 {
3820#line 620
3821 while (1) {
3822 while_13_continue: ;
3823#line 620
3824 i = i - 1;
3825#line 620
3826 if (i >= 0) {
3827
3828 } else {
3829 goto while_13_break;
3830 }
3831 {
3832#line 621
3833 pci_release_region(pdev, i);
3834 }
3835 }
3836 while_13_break: ;
3837 }
3838#line 623
3839 return (-16);
3840}
3841}
3842#line 629 "concatenated.c"
3843__inline int __get_user(int size , void *ptr )
3844{ int tmp ;
3845
3846 {
3847 {
3848#line 632
3849 assert_context_process();
3850#line 634
3851 tmp = __VERIFIER_nondet_int();
3852 }
3853#line 634
3854 return (tmp);
3855}
3856}
3857#line 637 "concatenated.c"
3858__inline int get_user(int size , void *ptr )
3859{ int tmp ;
3860
3861 {
3862 {
3863#line 640
3864 assert_context_process();
3865#line 642
3866 tmp = __VERIFIER_nondet_int();
3867 }
3868#line 642
3869 return (tmp);
3870}
3871}
3872#line 645 "concatenated.c"
3873__inline int __put_user(int size , void *ptr )
3874{ int tmp ;
3875
3876 {
3877 {
3878#line 648
3879 assert_context_process();
3880#line 650
3881 tmp = __VERIFIER_nondet_int();
3882 }
3883#line 650
3884 return (tmp);
3885}
3886}
3887#line 653 "concatenated.c"
3888__inline int put_user(int size , void *ptr )
3889{ int tmp ;
3890
3891 {
3892 {
3893#line 656
3894 assert_context_process();
3895#line 658
3896 tmp = __VERIFIER_nondet_int();
3897 }
3898#line 658
3899 return (tmp);
3900}
3901}
3902#line 661 "concatenated.c"
3903__inline unsigned long copy_to_user(void *to , void const *from , unsigned long n )
3904{ unsigned long tmp ;
3905
3906 {
3907 {
3908#line 664
3909 assert_context_process();
3910#line 666
3911 tmp = __VERIFIER_nondet_ulong();
3912 }
3913#line 666
3914 return (tmp);
3915}
3916}
3917#line 669 "concatenated.c"
3918__inline unsigned long copy_from_user(void *to , void *from , unsigned long n )
3919{ unsigned long tmp ;
3920
3921 {
3922 {
3923#line 672
3924 assert_context_process();
3925#line 674
3926 tmp = __VERIFIER_nondet_ulong();
3927 }
3928#line 674
3929 return (tmp);
3930}
3931}
3932#line 681 "concatenated.c"
3933int register_blkdev(unsigned int major , char const *name )
3934{ int result ;
3935 int tmp ;
3936
3937 {
3938 {
3939#line 683
3940 tmp = __VERIFIER_nondet_int();
3941#line 683
3942 result = tmp;
3943 }
3944#line 689
3945 return (result);
3946}
3947}
3948#line 692 "concatenated.c"
3949int unregister_blkdev(unsigned int major , char const *name )
3950{
3951
3952 {
3953#line 694
3954 return (0);
3955}
3956}
3957#line 697 "concatenated.c"
3958struct gendisk *alloc_disk(int minors )
3959{ struct gendisk *gd ;
3960 int __cil_tmp3 ;
3961 int __cil_tmp4 ;
3962 int __cil_tmp5 ;
3963 void *__cil_tmp6 ;
3964
3965 {
3966 {
3967#line 701
3968 __cil_tmp3 = (int )number_fixed_genhd_used;
3969#line 701
3970 if (__cil_tmp3 < 10) {
3971#line 702
3972 gd = & fixed_gendisk[number_fixed_genhd_used];
3973#line 703
3974 gd->minors = minors;
3975#line 705
3976 __cil_tmp4 = (int )number_fixed_genhd_used;
3977#line 705
3978 __cil_tmp5 = __cil_tmp4 + 1;
3979#line 705
3980 number_fixed_genhd_used = (short )__cil_tmp5;
3981#line 707
3982 return (gd);
3983 } else {
3984 {
3985#line 709
3986 __cil_tmp6 = (void *)0;
3987#line 709
3988 return ((struct gendisk *)__cil_tmp6);
3989 }
3990 }
3991 }
3992}
3993}
3994#line 713 "concatenated.c"
3995void add_disk(struct gendisk *disk )
3996{ void *tmp ;
3997 int __cil_tmp3 ;
3998 unsigned int __cil_tmp4 ;
3999 int __cil_tmp5 ;
4000 int __cil_tmp6 ;
4001
4002 {
4003 {
4004#line 715
4005 __cil_tmp3 = (int )number_genhd_registered;
4006#line 715
4007 if (__cil_tmp3 < 10) {
4008 {
4009#line 716
4010 genhd_registered[number_genhd_registered].gd = disk;
4011#line 717
4012 __cil_tmp4 = (unsigned int )32UL;
4013#line 717
4014 tmp = malloc(__cil_tmp4);
4015#line 717
4016 genhd_registered[number_genhd_registered].inode.i_bdev = (struct block_device *)tmp;
4017#line 718
4018 (genhd_registered[number_genhd_registered].inode.i_bdev)->bd_disk = disk;
4019#line 720
4020 __cil_tmp5 = (int )number_genhd_registered;
4021#line 720
4022 __cil_tmp6 = __cil_tmp5 + 1;
4023#line 720
4024 number_genhd_registered = (short )__cil_tmp6;
4025 }
4026 } else {
4027
4028 }
4029 }
4030#line 722
4031 return;
4032}
4033}
4034#line 724 "concatenated.c"
4035void del_gendisk(struct gendisk *gp )
4036{ int i ;
4037 int __cil_tmp3 ;
4038 unsigned long __cil_tmp4 ;
4039 unsigned long __cil_tmp5 ;
4040 void *__cil_tmp6 ;
4041
4042 {
4043#line 728
4044 i = 0;
4045 {
4046#line 728
4047 while (1) {
4048 while_14_continue: ;
4049 {
4050#line 728
4051 __cil_tmp3 = (int )number_genhd_registered;
4052#line 728
4053 if (i < __cil_tmp3) {
4054
4055 } else {
4056 goto while_14_break;
4057 }
4058 }
4059 {
4060#line 729
4061 __cil_tmp4 = (unsigned long )gp;
4062#line 729
4063 __cil_tmp5 = (unsigned long )genhd_registered[i].gd;
4064#line 729
4065 if (__cil_tmp5 == __cil_tmp4) {
4066#line 730
4067 __cil_tmp6 = (void *)0;
4068#line 730
4069 genhd_registered[i].gd = (struct gendisk *)__cil_tmp6;
4070 } else {
4071
4072 }
4073 }
4074#line 728
4075 i = i + 1;
4076 }
4077 while_14_break: ;
4078 }
4079#line 733
4080 return;
4081}
4082}
4083#line 6 "/ddverify-2010-04-30/models/seq1/include/ddverify/blkdev.h"
4084request_queue_t fixed_request_queue[10] ;
4085#line 8 "/ddverify-2010-04-30/models/seq1/include/ddverify/blkdev.h"
4086int number_request_queue_used = 0;
4087#line 740 "concatenated.c"
4088request_queue_t *get_fixed_request_queue(void)
4089{ int tmp ;
4090 void *__cil_tmp2 ;
4091
4092 {
4093#line 742
4094 if (number_request_queue_used < 10) {
4095#line 743
4096 tmp = number_request_queue_used;
4097#line 743
4098 number_request_queue_used = number_request_queue_used + 1;
4099#line 743
4100 return (& fixed_request_queue[tmp]);
4101 } else {
4102 {
4103#line 745
4104 __cil_tmp2 = (void *)0;
4105#line 745
4106 return ((request_queue_t *)__cil_tmp2);
4107 }
4108 }
4109}
4110}
4111#line 749 "concatenated.c"
4112request_queue_t *blk_init_queue(request_fn_proc *rfn , spinlock_t *lock )
4113{ request_queue_t *queue ;
4114 int tmp ;
4115 void *__cil_tmp5 ;
4116 void *__cil_tmp6 ;
4117
4118 {
4119 {
4120#line 753
4121 tmp = __VERIFIER_nondet_int();
4122 }
4123#line 753
4124 if (tmp) {
4125 {
4126#line 754
4127 queue = get_fixed_request_queue();
4128#line 756
4129 queue->queue_lock = lock;
4130#line 757
4131 queue->request_fn = rfn;
4132#line 758
4133 __cil_tmp5 = (void *)0;
4134#line 758
4135 queue->make_request_fn = (make_request_fn *)__cil_tmp5;
4136#line 759
4137 queue->__ddv_queue_alive = 1;
4138 }
4139#line 761
4140 return (queue);
4141 } else {
4142 {
4143#line 763
4144 __cil_tmp6 = (void *)0;
4145#line 763
4146 return ((request_queue_t *)__cil_tmp6);
4147 }
4148 }
4149}
4150}
4151#line 767 "concatenated.c"
4152request_queue_t *blk_alloc_queue(gfp_t gfp_mask )
4153{ request_queue_t *queue ;
4154 int tmp ;
4155 void *__cil_tmp4 ;
4156 void *__cil_tmp5 ;
4157 void *__cil_tmp6 ;
4158
4159 {
4160 {
4161#line 771
4162 tmp = __VERIFIER_nondet_int();
4163 }
4164#line 771
4165 if (tmp) {
4166 {
4167#line 772
4168 queue = get_fixed_request_queue();
4169#line 774
4170 __cil_tmp4 = (void *)0;
4171#line 774
4172 queue->request_fn = (request_fn_proc *)__cil_tmp4;
4173#line 775
4174 __cil_tmp5 = (void *)0;
4175#line 775
4176 queue->make_request_fn = (make_request_fn *)__cil_tmp5;
4177#line 776
4178 queue->__ddv_queue_alive = 1;
4179 }
4180#line 778
4181 return (queue);
4182 } else {
4183 {
4184#line 780
4185 __cil_tmp6 = (void *)0;
4186#line 780
4187 return ((request_queue_t *)__cil_tmp6);
4188 }
4189 }
4190}
4191}
4192#line 784 "concatenated.c"
4193void blk_queue_make_request(request_queue_t *q , make_request_fn *mfn )
4194{
4195
4196 {
4197#line 786
4198 q->make_request_fn = mfn;
4199#line 787
4200 return;
4201}
4202}
4203#line 789 "concatenated.c"
4204void end_request(struct request *req , int uptodate )
4205{ int genhd_no ;
4206 struct gendisk *__cil_tmp4 ;
4207 struct request_queue *__cil_tmp5 ;
4208
4209 {
4210#line 791
4211 __cil_tmp4 = req->rq_disk;
4212#line 791
4213 __cil_tmp5 = __cil_tmp4->queue;
4214#line 791
4215 genhd_no = __cil_tmp5->__ddv_genhd_no;
4216#line 793
4217 genhd_registered[genhd_no].requests_open = 0;
4218#line 794
4219 return;
4220}
4221}
4222#line 797 "concatenated.c"
4223void blk_queue_hardsect_size(request_queue_t *q , unsigned short size )
4224{
4225
4226 {
4227#line 799
4228 q->hardsect_size = size;
4229#line 800
4230 return;
4231}
4232}
4233#line 802 "concatenated.c"
4234void blk_cleanup_queue(request_queue_t *q )
4235{
4236
4237 {
4238#line 804
4239 q->__ddv_queue_alive = 0;
4240#line 805
4241 return;
4242}
4243}
4244#line 11 "/ddverify-2010-04-30/models/seq1/include/linux/proc_fs.h"
4245struct proc_dir_entry *proc_root_driver ;
4246#line 823 "concatenated.c"
4247int misc_register(struct miscdevice *misc )
4248{ int i ;
4249 dev_t dev ;
4250 int tmp ;
4251 int __cil_tmp5 ;
4252 int __cil_tmp6 ;
4253 int __cil_tmp7 ;
4254 struct cdev *__cil_tmp8 ;
4255
4256 {
4257#line 828
4258 if (fixed_cdev_used < 1) {
4259 {
4260#line 829
4261 i = fixed_cdev_used;
4262#line 830
4263 fixed_cdev_used = fixed_cdev_used + 1;
4264#line 832
4265 fixed_cdev[i].owner = (struct module *)0;
4266#line 833
4267 fixed_cdev[i].ops = misc->fops;
4268#line 835
4269 __cil_tmp5 = misc->minor;
4270#line 835
4271 __cil_tmp6 = 10 << 20;
4272#line 835
4273 __cil_tmp7 = __cil_tmp6 | __cil_tmp5;
4274#line 835
4275 dev = (unsigned int )__cil_tmp7;
4276#line 837
4277 __cil_tmp8 = & fixed_cdev[i];
4278#line 837
4279 tmp = cdev_add(__cil_tmp8, dev, 0U);
4280 }
4281#line 837
4282 return (tmp);
4283 } else {
4284#line 839
4285 return (-1);
4286 }
4287}
4288}
4289#line 97 "/ddverify-2010-04-30/models/seq1/include/linux/tty_driver.h"
4290struct tty_driver *alloc_tty_driver(int lines ) ;
4291#line 101
4292void tty_set_operations(struct tty_driver *driver , struct tty_operations const *op ) ;
4293#line 13 "/ddverify-2010-04-30/models/seq1/include/ddverify/tty.h"
4294struct ddv_tty_driver global_tty_driver ;
4295#line 845 "concatenated.c"
4296struct tty_driver *alloc_tty_driver(int lines )
4297{ void *__cil_tmp2 ;
4298
4299 {
4300#line 847
4301 if (! global_tty_driver.allocated) {
4302#line 848
4303 global_tty_driver.driver.magic = 21506;
4304#line 849
4305 global_tty_driver.driver.num = lines;
4306 } else {
4307 {
4308#line 851
4309 __cil_tmp2 = (void *)0;
4310#line 851
4311 return ((struct tty_driver *)__cil_tmp2);
4312 }
4313 }
4314#line 853
4315 return ((struct tty_driver *)0);
4316}
4317}
4318#line 855 "concatenated.c"
4319void tty_set_operations(struct tty_driver *driver , struct tty_operations const *op )
4320{ int (*__cil_tmp3)(struct tty_struct *tty , struct file *filp ) ;
4321 void (*__cil_tmp4)(struct tty_struct *tty , struct file *filp ) ;
4322 int (*__cil_tmp5)(struct tty_struct *tty , unsigned char const *buf , int count ) ;
4323 void (*__cil_tmp6)(struct tty_struct *tty , unsigned char ch ) ;
4324 void (*__cil_tmp7)(struct tty_struct *tty ) ;
4325 int (*__cil_tmp8)(struct tty_struct *tty ) ;
4326 int (*__cil_tmp9)(struct tty_struct *tty ) ;
4327 int (*__cil_tmp10)(struct tty_struct *tty , struct file *file , unsigned int cmd ,
4328 unsigned long arg ) ;
4329 void (*__cil_tmp11)(struct tty_struct *tty , struct termios *old ) ;
4330 void (*__cil_tmp12)(struct tty_struct *tty ) ;
4331 void (*__cil_tmp13)(struct tty_struct *tty ) ;
4332 void (*__cil_tmp14)(struct tty_struct *tty ) ;
4333 void (*__cil_tmp15)(struct tty_struct *tty ) ;
4334 void (*__cil_tmp16)(struct tty_struct *tty ) ;
4335 void (*__cil_tmp17)(struct tty_struct *tty , int state ) ;
4336 void (*__cil_tmp18)(struct tty_struct *tty ) ;
4337 void (*__cil_tmp19)(struct tty_struct *tty ) ;
4338 void (*__cil_tmp20)(struct tty_struct *tty , int timeout ) ;
4339 void (*__cil_tmp21)(struct tty_struct *tty , char ch ) ;
4340 int (*__cil_tmp22)(char *page , char **start , off_t off , int count , int *eof ,
4341 void *data ) ;
4342 int (*__cil_tmp23)(struct file *file , char const *buffer , unsigned long count ,
4343 void *data ) ;
4344 int (*__cil_tmp24)(struct tty_struct *tty , struct file *file ) ;
4345 int (*__cil_tmp25)(struct tty_struct *tty , struct file *file , unsigned int set ,
4346 unsigned int clear ) ;
4347
4348 {
4349#line 858
4350 __cil_tmp3 = op->open;
4351#line 858
4352 driver->open = (int (*)(struct tty_struct *tty , struct file *filp ))__cil_tmp3;
4353#line 859
4354 __cil_tmp4 = op->close;
4355#line 859
4356 driver->close = (void (*)(struct tty_struct *tty , struct file *filp ))__cil_tmp4;
4357#line 860
4358 __cil_tmp5 = op->write;
4359#line 860
4360 driver->write = (int (*)(struct tty_struct *tty , unsigned char const *buf , int count ))__cil_tmp5;
4361#line 861
4362 __cil_tmp6 = op->put_char;
4363#line 861
4364 driver->put_char = (void (*)(struct tty_struct *tty , unsigned char ch ))__cil_tmp6;
4365#line 862
4366 __cil_tmp7 = op->flush_chars;
4367#line 862
4368 driver->flush_chars = (void (*)(struct tty_struct *tty ))__cil_tmp7;
4369#line 863
4370 __cil_tmp8 = op->write_room;
4371#line 863
4372 driver->write_room = (int (*)(struct tty_struct *tty ))__cil_tmp8;
4373#line 864
4374 __cil_tmp9 = op->chars_in_buffer;
4375#line 864
4376 driver->chars_in_buffer = (int (*)(struct tty_struct *tty ))__cil_tmp9;
4377#line 865
4378 __cil_tmp10 = op->ioctl;
4379#line 865
4380 driver->ioctl = (int (*)(struct tty_struct *tty , struct file *file , unsigned int cmd ,
4381 unsigned long arg ))__cil_tmp10;
4382#line 866
4383 __cil_tmp11 = op->set_termios;
4384#line 866
4385 driver->set_termios = (void (*)(struct tty_struct *tty , struct termios *old ))__cil_tmp11;
4386#line 867
4387 __cil_tmp12 = op->throttle;
4388#line 867
4389 driver->throttle = (void (*)(struct tty_struct *tty ))__cil_tmp12;
4390#line 868
4391 __cil_tmp13 = op->unthrottle;
4392#line 868
4393 driver->unthrottle = (void (*)(struct tty_struct *tty ))__cil_tmp13;
4394#line 869
4395 __cil_tmp14 = op->stop;
4396#line 869
4397 driver->stop = (void (*)(struct tty_struct *tty ))__cil_tmp14;
4398#line 870
4399 __cil_tmp15 = op->start;
4400#line 870
4401 driver->start = (void (*)(struct tty_struct *tty ))__cil_tmp15;
4402#line 871
4403 __cil_tmp16 = op->hangup;
4404#line 871
4405 driver->hangup = (void (*)(struct tty_struct *tty ))__cil_tmp16;
4406#line 872
4407 __cil_tmp17 = op->break_ctl;
4408#line 872
4409 driver->break_ctl = (void (*)(struct tty_struct *tty , int state ))__cil_tmp17;
4410#line 873
4411 __cil_tmp18 = op->flush_buffer;
4412#line 873
4413 driver->flush_buffer = (void (*)(struct tty_struct *tty ))__cil_tmp18;
4414#line 874
4415 __cil_tmp19 = op->set_ldisc;
4416#line 874
4417 driver->set_ldisc = (void (*)(struct tty_struct *tty ))__cil_tmp19;
4418#line 875
4419 __cil_tmp20 = op->wait_until_sent;
4420#line 875
4421 driver->wait_until_sent = (void (*)(struct tty_struct *tty , int timeout ))__cil_tmp20;
4422#line 876
4423 __cil_tmp21 = op->send_xchar;
4424#line 876
4425 driver->send_xchar = (void (*)(struct tty_struct *tty , char ch ))__cil_tmp21;
4426#line 877
4427 __cil_tmp22 = op->read_proc;
4428#line 877
4429 driver->read_proc = (int (*)(char *page , char **start , off_t off , int count ,
4430 int *eof , void *data ))__cil_tmp22;
4431#line 878
4432 __cil_tmp23 = op->write_proc;
4433#line 878
4434 driver->write_proc = (int (*)(struct file *file , char const *buffer , unsigned long count ,
4435 void *data ))__cil_tmp23;
4436#line 879
4437 __cil_tmp24 = op->tiocmget;
4438#line 879
4439 driver->tiocmget = (int (*)(struct tty_struct *tty , struct file *file ))__cil_tmp24;
4440#line 880
4441 __cil_tmp25 = op->tiocmset;
4442#line 880
4443 driver->tiocmset = (int (*)(struct tty_struct *tty , struct file *file , unsigned int set ,
4444 unsigned int clear ))__cil_tmp25;
4445#line 881
4446 return;
4447}
4448}
4449#line 890 "concatenated.c"
4450__inline int alloc_chrdev_region(dev_t *dev , unsigned int baseminor , unsigned int count ,
4451 char const *name )
4452{ int major ;
4453 int return_value ;
4454 int tmp ;
4455 int tmp___0 ;
4456 unsigned int tmp___1 ;
4457 int __cil_tmp10 ;
4458 unsigned int __cil_tmp11 ;
4459
4460 {
4461 {
4462#line 893
4463 tmp = __VERIFIER_nondet_int();
4464#line 893
4465 return_value = tmp;
4466 }
4467#line 894
4468 if (return_value == 0) {
4469#line 894
4470 tmp___0 = 1;
4471 } else {
4472#line 894
4473 if (return_value == -1) {
4474#line 894
4475 tmp___0 = 1;
4476 } else {
4477#line 894
4478 tmp___0 = 0;
4479 }
4480 }
4481 {
4482#line 894
4483 __VERIFIER_assume(tmp___0);
4484 }
4485#line 896
4486 if (return_value == 0) {
4487 {
4488#line 897
4489 tmp___1 = __VERIFIER_nondet_uint();
4490#line 897
4491 major = (int )tmp___1;
4492#line 898
4493 __cil_tmp10 = major << 20;
4494#line 898
4495 __cil_tmp11 = (unsigned int )__cil_tmp10;
4496#line 898
4497 *dev = __cil_tmp11 | baseminor;
4498 }
4499 } else {
4500
4501 }
4502#line 901
4503 return (return_value);
4504}
4505}
4506#line 904 "concatenated.c"
4507__inline int register_chrdev_region(dev_t from , unsigned int count , char const *name )
4508{ int return_value ;
4509 int tmp ;
4510 int tmp___0 ;
4511
4512 {
4513 {
4514#line 906
4515 tmp = __VERIFIER_nondet_int();
4516#line 906
4517 return_value = tmp;
4518 }
4519#line 907
4520 if (return_value == 0) {
4521#line 907
4522 tmp___0 = 1;
4523 } else {
4524#line 907
4525 if (return_value == -1) {
4526#line 907
4527 tmp___0 = 1;
4528 } else {
4529#line 907
4530 tmp___0 = 0;
4531 }
4532 }
4533 {
4534#line 907
4535 __VERIFIER_assume(tmp___0);
4536 }
4537#line 909
4538 return (return_value);
4539}
4540}
4541#line 914 "concatenated.c"
4542__inline int register_chrdev(unsigned int major , char const *name , struct file_operations *fops )
4543{ struct cdev *cdev ;
4544 int err ;
4545 int tmp ;
4546 unsigned int __cil_tmp7 ;
4547 void const *__cil_tmp8 ;
4548
4549 {
4550 {
4551#line 921
4552 tmp = register_chrdev_region(0U, 256U, name);
4553#line 921
4554 major = (unsigned int )tmp;
4555#line 923
4556 cdev = cdev_alloc();
4557#line 924
4558 cdev->owner = fops->owner;
4559#line 925
4560 cdev->ops = fops;
4561#line 927
4562 __cil_tmp7 = major << 20;
4563#line 927
4564 err = cdev_add(cdev, __cil_tmp7, 256U);
4565 }
4566#line 929
4567 if (err) {
4568 {
4569#line 930
4570 __cil_tmp8 = (void const *)cdev;
4571#line 930
4572 kfree(__cil_tmp8);
4573 }
4574#line 931
4575 return (err);
4576 } else {
4577
4578 }
4579#line 934
4580 return ((int )major);
4581}
4582}
4583#line 937 "concatenated.c"
4584__inline int unregister_chrdev(unsigned int major , char const *name )
4585{
4586
4587 {
4588#line 939
4589 return (0);
4590}
4591}
4592#line 942 "concatenated.c"
4593__inline struct cdev *cdev_alloc(void)
4594{ int tmp ;
4595
4596 {
4597#line 944
4598 if (fixed_cdev_used < 1) {
4599#line 945
4600 tmp = fixed_cdev_used;
4601#line 945
4602 fixed_cdev_used = fixed_cdev_used + 1;
4603#line 945
4604 return (& fixed_cdev[tmp]);
4605 } else {
4606
4607 }
4608#line 947
4609 return ((struct cdev *)0);
4610}
4611}
4612#line 949 "concatenated.c"
4613__inline void cdev_init(struct cdev *cdev , struct file_operations *fops )
4614{
4615
4616 {
4617#line 951
4618 cdev->ops = fops;
4619#line 952
4620 return;
4621}
4622}
4623#line 954 "concatenated.c"
4624__inline int cdev_add(struct cdev *p , dev_t dev , unsigned int count )
4625{ int return_value ;
4626 int tmp ;
4627 int tmp___0 ;
4628 int __cil_tmp7 ;
4629 int __cil_tmp8 ;
4630 int __cil_tmp9 ;
4631
4632 {
4633 {
4634#line 956
4635 p->dev = dev;
4636#line 957
4637 p->count = count;
4638#line 959
4639 tmp = __VERIFIER_nondet_int();
4640#line 959
4641 return_value = tmp;
4642 }
4643#line 960
4644 if (return_value == 0) {
4645#line 960
4646 tmp___0 = 1;
4647 } else {
4648#line 960
4649 if (return_value == -1) {
4650#line 960
4651 tmp___0 = 1;
4652 } else {
4653#line 960
4654 tmp___0 = 0;
4655 }
4656 }
4657 {
4658#line 960
4659 __VERIFIER_assume(tmp___0);
4660 }
4661#line 962
4662 if (return_value == 0) {
4663 {
4664#line 963
4665 __cil_tmp7 = (int )number_cdev_registered;
4666#line 963
4667 if (__cil_tmp7 < 1) {
4668#line 965
4669 cdev_registered[number_cdev_registered].cdevp = p;
4670#line 966
4671 cdev_registered[number_cdev_registered].inode.i_rdev = dev;
4672#line 967
4673 cdev_registered[number_cdev_registered].inode.i_cdev = p;
4674#line 968
4675 cdev_registered[number_cdev_registered].open = 0;
4676#line 970
4677 __cil_tmp8 = (int )number_cdev_registered;
4678#line 970
4679 __cil_tmp9 = __cil_tmp8 + 1;
4680#line 970
4681 number_cdev_registered = (short )__cil_tmp9;
4682 } else {
4683#line 972
4684 return (-1);
4685 }
4686 }
4687 } else {
4688
4689 }
4690#line 976
4691 return (return_value);
4692}
4693}
4694#line 979 "concatenated.c"
4695__inline void cdev_del(struct cdev *p )
4696{ int i ;
4697 int __cil_tmp3 ;
4698 unsigned long __cil_tmp4 ;
4699 unsigned long __cil_tmp5 ;
4700
4701 {
4702#line 983
4703 i = 0;
4704 {
4705#line 983
4706 while (1) {
4707 while_15_continue: ;
4708 {
4709#line 983
4710 __cil_tmp3 = (int )number_cdev_registered;
4711#line 983
4712 if (i < __cil_tmp3) {
4713
4714 } else {
4715 goto while_15_break;
4716 }
4717 }
4718 {
4719#line 984
4720 __cil_tmp4 = (unsigned long )p;
4721#line 984
4722 __cil_tmp5 = (unsigned long )cdev_registered[i].cdevp;
4723#line 984
4724 if (__cil_tmp5 == __cil_tmp4) {
4725#line 985
4726 cdev_registered[i].cdevp = (struct cdev *)0;
4727#line 987
4728 return;
4729 } else {
4730
4731 }
4732 }
4733#line 983
4734 i = i + 1;
4735 }
4736 while_15_break: ;
4737 }
4738#line 990
4739 return;
4740}
4741}
4742#line 994 "concatenated.c"
4743__inline void mutex_init(struct mutex *lock )
4744{
4745
4746 {
4747#line 1000
4748 lock->locked = 0;
4749#line 1001
4750 lock->init = 1;
4751#line 1002
4752 return;
4753}
4754}
4755#line 1004 "concatenated.c"
4756__inline void mutex_lock(struct mutex *lock )
4757{
4758
4759 {
4760 {
4761#line 1007
4762 __VERIFIER_atomic_begin();
4763#line 1008
4764 assert_context_process();
4765#line 1013
4766 lock->locked = 1;
4767#line 1014
4768 __VERIFIER_atomic_end();
4769 }
4770#line 1015
4771 return;
4772}
4773}
4774#line 1017 "concatenated.c"
4775__inline void mutex_unlock(struct mutex *lock )
4776{
4777
4778 {
4779 {
4780#line 1020
4781 assert_context_process();
4782#line 1024
4783 lock->locked = 0;
4784 }
4785#line 1025
4786 return;
4787}
4788}
4789#line 1031 "concatenated.c"
4790int ddv_ioport_request_start ;
4791#line 1032 "concatenated.c"
4792int ddv_ioport_request_len ;
4793#line 1034 "concatenated.c"
4794__inline struct resource *request_region(unsigned long start , unsigned long len ,
4795 char const *name )
4796{ struct resource *resource ;
4797 void *tmp ;
4798 unsigned int __cil_tmp7 ;
4799
4800 {
4801 {
4802#line 1037
4803 __cil_tmp7 = (unsigned int )32UL;
4804#line 1037
4805 tmp = malloc(__cil_tmp7);
4806#line 1037
4807 resource = (struct resource *)tmp;
4808#line 1042
4809 ddv_ioport_request_start = (int )start;
4810#line 1043
4811 ddv_ioport_request_len = (int )len;
4812 }
4813#line 1045
4814 return (resource);
4815}
4816}
4817#line 1048 "concatenated.c"
4818__inline void release_region(unsigned long start , unsigned long len )
4819{ unsigned int i ;
4820
4821 {
4822#line 1050
4823 i = 0U;
4824#line 1056
4825 ddv_ioport_request_start = 0;
4826#line 1057
4827 ddv_ioport_request_len = 0;
4828#line 1058
4829 return;
4830}
4831}
4832#line 1060 "concatenated.c"
4833__inline unsigned char inb(unsigned int port )
4834{ unsigned char tmp ;
4835
4836 {
4837 {
4838#line 1062
4839 tmp = __VERIFIER_nondet_uchar();
4840 }
4841#line 1062
4842 return (tmp);
4843}
4844}
4845#line 1065 "concatenated.c"
4846__inline void outb(unsigned char byte , unsigned int port )
4847{
4848
4849 {
4850#line 1067
4851 return;
4852}
4853}
4854#line 1069 "concatenated.c"
4855__inline unsigned short inw(unsigned int port )
4856{ unsigned short tmp ;
4857
4858 {
4859 {
4860#line 1071
4861 tmp = __VERIFIER_nondet_ushort();
4862 }
4863#line 1071
4864 return (tmp);
4865}
4866}
4867#line 1074 "concatenated.c"
4868__inline void outw(unsigned short word , unsigned int port )
4869{
4870
4871 {
4872#line 1076
4873 return;
4874}
4875}
4876#line 1078 "concatenated.c"
4877__inline unsigned int inl(unsigned int port )
4878{ unsigned int tmp ;
4879
4880 {
4881 {
4882#line 1080
4883 tmp = __VERIFIER_nondet_unsigned();
4884 }
4885#line 1080
4886 return (tmp);
4887}
4888}
4889#line 1083 "concatenated.c"
4890__inline void outl(unsigned int doubleword , unsigned int port )
4891{
4892
4893 {
4894#line 1085
4895 return;
4896}
4897}
4898#line 1087 "concatenated.c"
4899__inline unsigned char inb_p(unsigned int port )
4900{ unsigned char tmp ;
4901
4902 {
4903 {
4904#line 1089
4905 tmp = __VERIFIER_nondet_uchar();
4906 }
4907#line 1089
4908 return (tmp);
4909}
4910}
4911#line 1092 "concatenated.c"
4912__inline void outb_p(unsigned char byte , unsigned int port )
4913{
4914
4915 {
4916#line 1094
4917 return;
4918}
4919}
4920#line 1096 "concatenated.c"
4921__inline unsigned short inw_p(unsigned int port )
4922{ int tmp ;
4923 unsigned short tmp___0 ;
4924 unsigned int __cil_tmp4 ;
4925 int __cil_tmp5 ;
4926 unsigned int __cil_tmp6 ;
4927 char *__cil_tmp7 ;
4928
4929 {
4930 {
4931#line 1099
4932 __cil_tmp4 = (unsigned int )ddv_ioport_request_start;
4933#line 1099
4934 if (port >= __cil_tmp4) {
4935 {
4936#line 1099
4937 __cil_tmp5 = ddv_ioport_request_start + ddv_ioport_request_len;
4938#line 1099
4939 __cil_tmp6 = (unsigned int )__cil_tmp5;
4940#line 1099
4941 if (port < __cil_tmp6) {
4942#line 1099
4943 tmp = 1;
4944 } else {
4945#line 1099
4946 tmp = 0;
4947 }
4948 }
4949 } else {
4950#line 1099
4951 tmp = 0;
4952 }
4953 }
4954 {
4955#line 1099
4956 __cil_tmp7 = (char *)"I/O port is requested";
4957#line 1099
4958 __VERIFIER_assert(tmp, __cil_tmp7);
4959#line 1101
4960 tmp___0 = __VERIFIER_nondet_ushort();
4961 }
4962#line 1101
4963 return (tmp___0);
4964}
4965}
4966#line 1104 "concatenated.c"
4967__inline void outw_p(unsigned short word , unsigned int port )
4968{
4969
4970 {
4971#line 1106
4972 return;
4973}
4974}
4975#line 1108 "concatenated.c"
4976__inline unsigned int inl_p(unsigned int port )
4977{ unsigned int tmp ;
4978
4979 {
4980 {
4981#line 1110
4982 tmp = __VERIFIER_nondet_unsigned();
4983 }
4984#line 1110
4985 return (tmp);
4986}
4987}
4988#line 1113 "concatenated.c"
4989__inline void outl_p(unsigned int doubleword , unsigned int port )
4990{
4991
4992 {
4993#line 1115
4994 return;
4995}
4996}
4997#line 1123 "concatenated.c"
4998void schedule(void)
4999{
5000
5001 {
5002 {
5003#line 1125
5004 assert_context_process();
5005 }
5006#line 1126
5007 return;
5008}
5009}
5010#line 1128 "concatenated.c"
5011long schedule_timeout(long timeout )
5012{ long tmp ;
5013
5014 {
5015 {
5016#line 1130
5017 assert_context_process();
5018#line 1132
5019 tmp = __VERIFIER_nondet_long();
5020 }
5021#line 1132
5022 return (tmp);
5023}
5024}
5025#line 1139 "concatenated.c"
5026__inline void sema_init(struct semaphore *sem , int val )
5027{
5028
5029 {
5030#line 1141
5031 sem->init = 1;
5032#line 1142
5033 sem->locked = 0;
5034#line 1143
5035 return;
5036}
5037}
5038#line 1145 "concatenated.c"
5039__inline void init_MUTEX(struct semaphore *sem )
5040{
5041
5042 {
5043#line 1147
5044 sem->init = 1;
5045#line 1148
5046 sem->locked = 0;
5047#line 1149
5048 return;
5049}
5050}
5051#line 1151 "concatenated.c"
5052__inline void init_MUTEX_LOCKED(struct semaphore *sem )
5053{
5054
5055 {
5056#line 1153
5057 sem->init = 1;
5058#line 1154
5059 sem->locked = 1;
5060#line 1155
5061 return;
5062}
5063}
5064#line 1157 "concatenated.c"
5065__inline void down(struct semaphore *sem )
5066{
5067
5068 {
5069 {
5070#line 1160
5071 __VERIFIER_atomic_begin();
5072#line 1161
5073 assert_context_process();
5074#line 1166
5075 sem->locked = 1;
5076#line 1167
5077 __VERIFIER_atomic_end();
5078 }
5079#line 1168
5080 return;
5081}
5082}
5083#line 1170 "concatenated.c"
5084__inline int down_interruptible(struct semaphore *sem )
5085{ int tmp ;
5086
5087 {
5088 {
5089#line 1172
5090 tmp = __VERIFIER_nondet_int();
5091 }
5092#line 1172
5093 if (tmp) {
5094 {
5095#line 1174
5096 __VERIFIER_atomic_begin();
5097#line 1175
5098 assert_context_process();
5099#line 1180
5100 sem->locked = 1;
5101#line 1181
5102 __VERIFIER_atomic_end();
5103 }
5104#line 1183
5105 return (0);
5106 } else {
5107#line 1185
5108 return (-1);
5109 }
5110}
5111}
5112#line 1189 "concatenated.c"
5113__inline int down_trylock(struct semaphore *sem )
5114{ int __cil_tmp2 ;
5115
5116 {
5117 {
5118#line 1192
5119 __VERIFIER_atomic_begin();
5120#line 1193
5121 assert_context_process();
5122 }
5123 {
5124#line 1199
5125 __cil_tmp2 = sem->locked;
5126#line 1199
5127 if (__cil_tmp2 == 0) {
5128#line 1200
5129 sem->locked = 1;
5130#line 1201
5131 return (0);
5132 } else {
5133#line 1203
5134 return (1);
5135 }
5136 }
5137 {
5138#line 1206
5139 __VERIFIER_atomic_end();
5140 }
5141#line 1208
5142 return (0);
5143}
5144}
5145#line 1211 "concatenated.c"
5146__inline void up(struct semaphore *sem )
5147{
5148
5149 {
5150 {
5151#line 1214
5152 assert_context_process();
5153#line 1218
5154 sem->locked = 0;
5155 }
5156#line 1219
5157 return;
5158}
5159}
5160#line 1223 "concatenated.c"
5161__inline void tasklet_schedule(struct tasklet_struct *t )
5162{ int i ;
5163 int next_free ;
5164 void *__cil_tmp4 ;
5165 unsigned long __cil_tmp5 ;
5166 unsigned long __cil_tmp6 ;
5167 unsigned long __cil_tmp7 ;
5168 unsigned long __cil_tmp8 ;
5169 int __cil_tmp9 ;
5170
5171 {
5172#line 1226
5173 next_free = -1;
5174#line 1232
5175 i = 0;
5176 {
5177#line 1232
5178 while (1) {
5179 while_16_continue: ;
5180#line 1232
5181 if (i < 1) {
5182
5183 } else {
5184 goto while_16_break;
5185 }
5186 {
5187#line 1233
5188 __cil_tmp4 = (void *)0;
5189#line 1233
5190 __cil_tmp5 = (unsigned long )__cil_tmp4;
5191#line 1233
5192 __cil_tmp6 = (unsigned long )tasklet_registered[i].tasklet;
5193#line 1233
5194 if (__cil_tmp6 == __cil_tmp5) {
5195#line 1234
5196 next_free = i;
5197 } else {
5198
5199 }
5200 }
5201 {
5202#line 1236
5203 __cil_tmp7 = (unsigned long )t;
5204#line 1236
5205 __cil_tmp8 = (unsigned long )tasklet_registered[i].tasklet;
5206#line 1236
5207 if (__cil_tmp8 == __cil_tmp7) {
5208 {
5209#line 1236
5210 __cil_tmp9 = (int )tasklet_registered[i].is_running;
5211#line 1236
5212 if (__cil_tmp9 == 0) {
5213#line 1238
5214 return;
5215 } else {
5216
5217 }
5218 }
5219 } else {
5220
5221 }
5222 }
5223#line 1232
5224 i = i + 1;
5225 }
5226 while_16_break: ;
5227 }
5228#line 1242
5229 if (next_free == -1) {
5230
5231 } else {
5232
5233 }
5234#line 1246
5235 tasklet_registered[next_free].tasklet = t;
5236#line 1247
5237 tasklet_registered[next_free].is_running = (unsigned short)0;
5238#line 1248
5239 return;
5240}
5241}
5242#line 1250 "concatenated.c"
5243__inline void tasklet_init(struct tasklet_struct *t , void (*func)(unsigned long ) ,
5244 unsigned long data )
5245{
5246
5247 {
5248#line 1254
5249 t->count = 0;
5250#line 1255
5251 t->init = 0;
5252#line 1256
5253 t->func = func;
5254#line 1257
5255 t->data = data;
5256#line 1258
5257 return;
5258}
5259}
5260#line 1262 "concatenated.c"
5261__inline void spin_lock_init(spinlock_t *lock )
5262{
5263
5264 {
5265#line 1264
5266 lock->init = 1;
5267#line 1265
5268 lock->locked = 0;
5269#line 1266
5270 return;
5271}
5272}
5273#line 1268 "concatenated.c"
5274__inline void spin_lock(spinlock_t *lock )
5275{
5276
5277 {
5278 {
5279#line 1271
5280 __VERIFIER_atomic_begin();
5281#line 1276
5282 lock->locked = 1;
5283#line 1277
5284 __VERIFIER_atomic_end();
5285 }
5286#line 1278
5287 return;
5288}
5289}
5290#line 1280 "concatenated.c"
5291__inline void spin_lock_irqsave(spinlock_t *lock , unsigned long flags )
5292{
5293
5294 {
5295 {
5296#line 1283
5297 __VERIFIER_atomic_begin();
5298#line 1288
5299 lock->locked = 1;
5300#line 1289
5301 __VERIFIER_atomic_end();
5302 }
5303#line 1290
5304 return;
5305}
5306}
5307#line 1292 "concatenated.c"
5308__inline void spin_lock_irq(spinlock_t *lock )
5309{
5310
5311 {
5312 {
5313#line 1295
5314 __VERIFIER_atomic_begin();
5315#line 1300
5316 lock->locked = 1;
5317#line 1301
5318 __VERIFIER_atomic_end();
5319 }
5320#line 1302
5321 return;
5322}
5323}
5324#line 1304 "concatenated.c"
5325__inline void spin_lock_bh(spinlock_t *lock )
5326{
5327
5328 {
5329 {
5330#line 1307
5331 __VERIFIER_atomic_begin();
5332#line 1312
5333 lock->locked = 1;
5334#line 1313
5335 __VERIFIER_atomic_end();
5336 }
5337#line 1314
5338 return;
5339}
5340}
5341#line 1316 "concatenated.c"
5342__inline void spin_unlock(spinlock_t *lock )
5343{
5344
5345 {
5346#line 1322
5347 lock->locked = 0;
5348#line 1323
5349 return;
5350}
5351}
5352#line 1325 "concatenated.c"
5353__inline void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags )
5354{
5355
5356 {
5357#line 1331
5358 lock->locked = 0;
5359#line 1332
5360 return;
5361}
5362}
5363#line 1334 "concatenated.c"
5364__inline void spin_unlock_irq(spinlock_t *lock )
5365{
5366
5367 {
5368#line 1340
5369 lock->locked = 0;
5370#line 1341
5371 return;
5372}
5373}
5374#line 1343 "concatenated.c"
5375__inline void spin_unlock_bh(spinlock_t *lock )
5376{
5377
5378 {
5379#line 1349
5380 lock->locked = 0;
5381#line 1350
5382 return;
5383}
5384}
5385#line 1354 "concatenated.c"
5386__inline void init_timer(struct timer_list *timer )
5387{ int __cil_tmp2 ;
5388 int __cil_tmp3 ;
5389 int __cil_tmp4 ;
5390
5391 {
5392 {
5393#line 1356
5394 __cil_tmp2 = (int )number_timer_registered;
5395#line 1356
5396 if (__cil_tmp2 < 1) {
5397#line 1357
5398 timer->__ddv_active = (short)0;
5399#line 1358
5400 timer->__ddv_init = (short)1;
5401#line 1359
5402 timer_registered[number_timer_registered].timer = timer;
5403#line 1361
5404 __cil_tmp3 = (int )number_timer_registered;
5405#line 1361
5406 __cil_tmp4 = __cil_tmp3 + 1;
5407#line 1361
5408 number_timer_registered = (short )__cil_tmp4;
5409 } else {
5410
5411 }
5412 }
5413#line 1363
5414 return;
5415}
5416}
5417#line 1365 "concatenated.c"
5418__inline void add_timer(struct timer_list *timer )
5419{
5420
5421 {
5422#line 1371
5423 timer->__ddv_active = (short)1;
5424#line 1372
5425 return;
5426}
5427}
5428#line 1374 "concatenated.c"
5429__inline void add_timer_on(struct timer_list *timer , int cpu )
5430{
5431
5432 {
5433 {
5434#line 1377
5435 add_timer(timer);
5436 }
5437#line 1378
5438 return;
5439}
5440}
5441#line 1380 "concatenated.c"
5442__inline int del_timer(struct timer_list *timer )
5443{
5444
5445 {
5446#line 1382
5447 timer->__ddv_active = (short)0;
5448#line 1383
5449 return (0);
5450}
5451}
5452#line 1385 "concatenated.c"
5453__inline int mod_timer(struct timer_list *timer , unsigned long expires )
5454{
5455
5456 {
5457#line 1391
5458 timer->expires = expires;
5459#line 1392
5460 timer->__ddv_active = (short)1;
5461#line 1393
5462 return (0);
5463}
5464}
5465#line 1396 "concatenated.c"
5466__inline void init_waitqueue_head(wait_queue_head_t *q )
5467{
5468
5469 {
5470#line 1398
5471 q->init = 1;
5472#line 1399
5473 return;
5474}
5475}
5476#line 1401 "concatenated.c"
5477__inline void wake_up(wait_queue_head_t *q )
5478{
5479
5480 {
5481#line 1407
5482 return;
5483}
5484}
5485#line 1409 "concatenated.c"
5486__inline void wake_up_all(wait_queue_head_t *q )
5487{
5488
5489 {
5490#line 1415
5491 return;
5492}
5493}
5494#line 1417 "concatenated.c"
5495__inline void wake_up_interruptible(wait_queue_head_t *q )
5496{
5497
5498 {
5499#line 1423
5500 return;
5501}
5502}
5503#line 1425 "concatenated.c"
5504__inline void sleep_on(wait_queue_head_t *q )
5505{
5506
5507 {
5508#line 1431
5509 return;
5510}
5511}
5512#line 1433 "concatenated.c"
5513__inline void interruptible_sleep_on(wait_queue_head_t *q )
5514{
5515
5516 {
5517#line 1439
5518 return;
5519}
5520}
5521#line 1444 "concatenated.c"
5522__inline int schedule_work(struct work_struct *work )
5523{ int i ;
5524 unsigned long __cil_tmp3 ;
5525 unsigned long __cil_tmp4 ;
5526 void *__cil_tmp5 ;
5527 unsigned long __cil_tmp6 ;
5528 unsigned long __cil_tmp7 ;
5529
5530 {
5531#line 1453
5532 i = 0;
5533 {
5534#line 1453
5535 while (1) {
5536 while_17_continue: ;
5537#line 1453
5538 if (i < 10) {
5539
5540 } else {
5541 goto while_17_break;
5542 }
5543 {
5544#line 1454
5545 __cil_tmp3 = (unsigned long )work;
5546#line 1454
5547 __cil_tmp4 = (unsigned long )shared_workqueue[i];
5548#line 1454
5549 if (__cil_tmp4 == __cil_tmp3) {
5550#line 1455
5551 return (0);
5552 } else {
5553
5554 }
5555 }
5556 {
5557#line 1458
5558 __cil_tmp5 = (void *)0;
5559#line 1458
5560 __cil_tmp6 = (unsigned long )__cil_tmp5;
5561#line 1458
5562 __cil_tmp7 = (unsigned long )shared_workqueue[i];
5563#line 1458
5564 if (__cil_tmp7 == __cil_tmp6) {
5565#line 1459
5566 shared_workqueue[i] = work;
5567#line 1461
5568 return (1);
5569 } else {
5570
5571 }
5572 }
5573#line 1453
5574 i = i + 1;
5575 }
5576 while_17_break: ;
5577 }
5578#line 1466
5579 return (-1);
5580}
5581}
5582#line 1469 "concatenated.c"
5583__inline void call_shared_workqueue_functions(void)
5584{ unsigned short i ;
5585 unsigned short tmp ;
5586 int __cil_tmp3 ;
5587 int __cil_tmp4 ;
5588 void *__cil_tmp5 ;
5589 unsigned long __cil_tmp6 ;
5590 unsigned long __cil_tmp7 ;
5591 void (*__cil_tmp8)(void * ) ;
5592 void *__cil_tmp9 ;
5593 void *__cil_tmp10 ;
5594
5595 {
5596 {
5597#line 1471
5598 tmp = __VERIFIER_nondet_ushort();
5599#line 1471
5600 i = tmp;
5601#line 1472
5602 __cil_tmp3 = (int )i;
5603#line 1472
5604 __cil_tmp4 = __cil_tmp3 < 10;
5605#line 1472
5606 __VERIFIER_assume(__cil_tmp4);
5607 }
5608 {
5609#line 1474
5610 __cil_tmp5 = (void *)0;
5611#line 1474
5612 __cil_tmp6 = (unsigned long )__cil_tmp5;
5613#line 1474
5614 __cil_tmp7 = (unsigned long )shared_workqueue[i];
5615#line 1474
5616 if (__cil_tmp7 != __cil_tmp6) {
5617 {
5618#line 1475
5619 __cil_tmp8 = (shared_workqueue[i])->func;
5620#line 1475
5621 __cil_tmp9 = (shared_workqueue[i])->data;
5622#line 1475
5623 (*__cil_tmp8)(__cil_tmp9);
5624#line 1476
5625 __cil_tmp10 = (void *)0;
5626#line 1476
5627 shared_workqueue[i] = (struct work_struct *)__cil_tmp10;
5628 }
5629 } else {
5630
5631 }
5632 }
5633#line 1478
5634 return;
5635}
5636}
5637#line 1482 "concatenated.c"
5638int request_irq(unsigned int irq , irqreturn_t (*handler)(int , void * , struct pt_regs * ) ,
5639 unsigned long irqflags , char const *devname , void *dev_id )
5640{ int tmp ;
5641
5642 {
5643 {
5644#line 1485
5645 tmp = __VERIFIER_nondet_int();
5646 }
5647#line 1485
5648 if (tmp) {
5649#line 1486
5650 registered_irq[irq].handler = handler;
5651#line 1487
5652 registered_irq[irq].dev_id = dev_id;
5653#line 1489
5654 return (0);
5655 } else {
5656#line 1491
5657 return (-1);
5658 }
5659}
5660}
5661#line 1495 "concatenated.c"
5662void free_irq(unsigned int irq , void *dev_id )
5663{ void *__cil_tmp3 ;
5664
5665 {
5666#line 1497
5667 __cil_tmp3 = (void *)0;
5668#line 1497
5669 registered_irq[irq].handler = (irqreturn_t (*)(int , void * , struct pt_regs * ))__cil_tmp3;
5670#line 1498
5671 registered_irq[irq].dev_id = (void *)0;
5672#line 1499
5673 return;
5674}
5675}
5676#line 1504 "concatenated.c"
5677__inline unsigned long __get_free_pages(gfp_t gfp_mask , unsigned int order )
5678{
5679
5680 {
5681#line 1507
5682 if (gfp_mask & 16U) {
5683 {
5684#line 1508
5685 assert_context_process();
5686 }
5687 } else {
5688
5689 }
5690#line 1510
5691 return (0UL);
5692}
5693}
5694#line 1512 "concatenated.c"
5695__inline unsigned long __get_free_page(gfp_t gfp_mask )
5696{
5697
5698 {
5699#line 1515
5700 if (gfp_mask & 16U) {
5701 {
5702#line 1516
5703 assert_context_process();
5704 }
5705 } else {
5706
5707 }
5708#line 1518
5709 return (0UL);
5710}
5711}
5712#line 1520 "concatenated.c"
5713__inline unsigned long get_zeroed_page(gfp_t gfp_mask )
5714{
5715
5716 {
5717#line 1523
5718 if (gfp_mask & 16U) {
5719 {
5720#line 1524
5721 assert_context_process();
5722 }
5723 } else {
5724
5725 }
5726#line 1526
5727 return (0UL);
5728}
5729}
5730#line 1537 "concatenated.c"
5731__inline struct page *alloc_pages(gfp_t gfp_mask , unsigned int order )
5732{
5733
5734 {
5735#line 1540
5736 if (gfp_mask & 16U) {
5737 {
5738#line 1541
5739 assert_context_process();
5740 }
5741 } else {
5742
5743 }
5744#line 1543
5745 return ((struct page *)0);
5746}
5747}
5748#line 1545 "concatenated.c"
5749__inline struct page *alloc_page(gfp_t gfp_mask )
5750{
5751
5752 {
5753#line 1548
5754 if (gfp_mask & 16U) {
5755 {
5756#line 1549
5757 assert_context_process();
5758 }
5759 } else {
5760
5761 }
5762#line 1551
5763 return ((struct page *)0);
5764}
5765}
5766#line 1557 "concatenated.c"
5767void *kmalloc(size_t size , gfp_t flags )
5768{ void *tmp ;
5769
5770 {
5771#line 1559
5772 if (flags & 16U) {
5773 {
5774#line 1560
5775 assert_context_process();
5776 }
5777 } else {
5778
5779 }
5780 {
5781#line 1563
5782 tmp = malloc(size);
5783 }
5784#line 1563
5785 return (tmp);
5786}
5787}
5788#line 1566 "concatenated.c"
5789void *kzalloc(size_t size , gfp_t flags )
5790{ void *tmp ;
5791
5792 {
5793#line 1568
5794 if (flags & 16U) {
5795 {
5796#line 1569
5797 assert_context_process();
5798 }
5799 } else {
5800
5801 }
5802 {
5803#line 1572
5804 tmp = malloc(size);
5805 }
5806#line 1572
5807 return (tmp);
5808}
5809}
5810#line 6 "/ddverify-2010-04-30/models/seq1/include/linux/vmalloc.h"
5811void *vmalloc(unsigned long size ) ;
5812#line 1606 "concatenated.c"
5813void *vmalloc(unsigned long size )
5814{ void *tmp ;
5815 unsigned int __cil_tmp3 ;
5816
5817 {
5818 {
5819#line 1608
5820 __cil_tmp3 = (unsigned int )size;
5821#line 1608
5822 tmp = malloc(__cil_tmp3);
5823 }
5824#line 1608
5825 return (tmp);
5826}
5827}
5828#line 1610 "concatenated.c"
5829int printk(char const *fmt , ...)
5830{
5831
5832 {
5833#line 1612
5834 return (0);
5835}
5836}
5837#line 1615 "concatenated.c"
5838unsigned short __VERIFIER_nondet_ushort(void)
5839{ unsigned short us ;
5840
5841 {
5842#line 1615
5843 return (us);
5844}
5845}
5846#line 1616 "concatenated.c"
5847unsigned long __VERIFIER_nondet_ulong(void)
5848{ unsigned long ul ;
5849
5850 {
5851#line 1616
5852 return (ul);
5853}
5854}
5855#line 1617 "concatenated.c"
5856short __VERIFIER_nondet_short(void)
5857{ short s ;
5858
5859 {
5860#line 1617
5861 return (s);
5862}
5863}
5864#line 1618 "concatenated.c"
5865int __VERIFIER_nondet_int(void)
5866{ int i ;
5867
5868 {
5869#line 1618
5870 return (i);
5871}
5872}
5873#line 1619 "concatenated.c"
5874char __VERIFIER_nondet_char(void)
5875{ char c ;
5876
5877 {
5878#line 1619
5879 return (c);
5880}
5881}
5882#line 1620 "concatenated.c"
5883size_t __VERIFIER_nondet_size_t(void)
5884{ size_t s ;
5885
5886 {
5887#line 1620
5888 return (s);
5889}
5890}
5891#line 1621 "concatenated.c"
5892unsigned int __VERIFIER_nondet_uint(void)
5893{ unsigned int ui ;
5894
5895 {
5896#line 1621
5897 return (ui);
5898}
5899}
5900#line 1622 "concatenated.c"
5901unsigned char __VERIFIER_nondet_uchar(void)
5902{ unsigned char uc ;
5903
5904 {
5905#line 1622
5906 return (uc);
5907}
5908}
5909#line 1623 "concatenated.c"
5910unsigned int __VERIFIER_nondet_unsigned(void)
5911{ unsigned int u ;
5912
5913 {
5914#line 1623
5915 return (u);
5916}
5917}
5918#line 1624 "concatenated.c"
5919long __VERIFIER_nondet_long(void)
5920{ long l ;
5921
5922 {
5923#line 1624
5924 return (l);
5925}
5926}
5927#line 1625 "concatenated.c"
5928char *__VERIFIER_nondet_pchar(void)
5929{ char *pc ;
5930
5931 {
5932#line 1625
5933 return (pc);
5934}
5935}
5936#line 1626 "concatenated.c"
5937loff_t __VERIFIER_nondet_loff_t(void)
5938{ loff_t l ;
5939
5940 {
5941#line 1626
5942 return (l);
5943}
5944}
5945#line 1627 "concatenated.c"
5946sector_t __VERIFIER_nondet_sector_t(void)
5947{ sector_t s ;
5948
5949 {
5950#line 1627
5951 return (s);
5952}
5953}
5954#line 1628 "concatenated.c"
5955loff_t no_llseek(struct file *file , loff_t offset , int origin )
5956{ loff_t l ;
5957
5958 {
5959#line 1628
5960 return (l);
5961}
5962}
5963#line 1633 "concatenated.c"
5964void __VERIFIER_assume(int phi )
5965{
5966
5967 {
5968 {
5969#line 1633
5970 while (1) {
5971 while_18_continue: ;
5972#line 1633
5973 if (! phi) {
5974
5975 } else {
5976 goto while_18_break;
5977 }
5978 }
5979 while_18_break: ;
5980 }
5981#line 1633
5982 return;
5983}
5984}
5985#line 1634 "concatenated.c"
5986void __VERIFIER_assert(int phi , char *txt )
5987{
5988
5989 {
5990#line 1634
5991 if (! phi) {
5992 ERROR:
5993 goto ERROR;
5994 } else {
5995
5996 }
5997#line 1634
5998 return;
5999}
6000}
6001#line 1636 "concatenated.c"
6002int nonseekable_open(struct inode *inode , struct file *filp )
6003{ int i ;
6004
6005 {
6006#line 1636
6007 return (i);
6008}
6009}
6010#line 1637 "concatenated.c"
6011void __module_get(struct module *module )
6012{
6013
6014 {
6015#line 1637
6016 return;
6017}
6018}
6019#line 1638 "concatenated.c"
6020int test_and_set_bit(int nr , unsigned long *addr )
6021{ unsigned int bit ;
6022 unsigned long old ;
6023 int __cil_tmp5 ;
6024 int __cil_tmp6 ;
6025 int __cil_tmp7 ;
6026 unsigned long __cil_tmp8 ;
6027 unsigned long __cil_tmp9 ;
6028 unsigned long __cil_tmp10 ;
6029
6030 {
6031#line 1640
6032 __cil_tmp5 = nr & 31;
6033#line 1640
6034 __cil_tmp6 = 1 << __cil_tmp5;
6035#line 1640
6036 bit = (unsigned int )__cil_tmp6;
6037#line 1641
6038 __cil_tmp7 = nr >> 5;
6039#line 1641
6040 addr = addr + __cil_tmp7;
6041#line 1642
6042 old = *addr;
6043#line 1643
6044 __cil_tmp8 = (unsigned long )bit;
6045#line 1643
6046 *addr = old | __cil_tmp8;
6047 {
6048#line 1644
6049 __cil_tmp9 = (unsigned long )bit;
6050#line 1644
6051 __cil_tmp10 = old & __cil_tmp9;
6052#line 1644
6053 return (__cil_tmp10 != 0UL);
6054 }
6055}
6056}
6057#line 1647 "concatenated.c"
6058void clear_bit(int nr , unsigned long volatile *addr )
6059{ unsigned int bit ;
6060 unsigned long old ;
6061 int __cil_tmp5 ;
6062 int __cil_tmp6 ;
6063 int __cil_tmp7 ;
6064 unsigned long volatile __cil_tmp8 ;
6065 unsigned int __cil_tmp9 ;
6066 unsigned long __cil_tmp10 ;
6067 unsigned long __cil_tmp11 ;
6068
6069 {
6070#line 1649
6071 __cil_tmp5 = nr & 31;
6072#line 1649
6073 __cil_tmp6 = 1 << __cil_tmp5;
6074#line 1649
6075 bit = (unsigned int )__cil_tmp6;
6076#line 1650
6077 __cil_tmp7 = nr >> 5;
6078#line 1650
6079 addr = addr + __cil_tmp7;
6080#line 1651
6081 __cil_tmp8 = *addr;
6082#line 1651
6083 old = (unsigned long )__cil_tmp8;
6084#line 1652
6085 __cil_tmp9 = ~ bit;
6086#line 1652
6087 __cil_tmp10 = (unsigned long )__cil_tmp9;
6088#line 1652
6089 __cil_tmp11 = old & __cil_tmp10;
6090#line 1652
6091 *addr = (unsigned long volatile )__cil_tmp11;
6092#line 1653
6093 return;
6094}
6095}
6096#line 1655 "concatenated.c"
6097int register_reboot_notifier(struct notifier_block *dummy )
6098{ int i ;
6099
6100 {
6101#line 1655
6102 return (i);
6103}
6104}
6105#line 1656 "concatenated.c"
6106int misc_deregister(struct miscdevice *misc )
6107{ int i ;
6108
6109 {
6110#line 1656
6111 return (i);
6112}
6113}
6114#line 1657 "concatenated.c"
6115int unregister_reboot_notifier(struct notifier_block *dummy )
6116{ int i ;
6117
6118 {
6119#line 1657
6120 return (i);
6121}
6122}
6123#line 1658 "concatenated.c"
6124void release_mem_region(unsigned long start , unsigned long len )
6125{
6126
6127 {
6128#line 1658
6129 return;
6130}
6131}
6132#line 1659 "concatenated.c"
6133void kfree(void const *addr )
6134{
6135
6136 {
6137#line 1659
6138 return;
6139}
6140}
6141#line 1661 "concatenated.c"
6142struct resource *request_mem_region(unsigned long start , unsigned long len , char const *name )
6143{ void *tmp ;
6144 unsigned int __cil_tmp5 ;
6145
6146 {
6147 {
6148#line 1663
6149 __cil_tmp5 = (unsigned int )32UL;
6150#line 1663
6151 tmp = malloc(__cil_tmp5);
6152 }
6153#line 1663
6154 return ((struct resource *)tmp);
6155}
6156}
6157#line 1666 "concatenated.c"
6158void __VERIFIER_atomic_begin(void)
6159{
6160
6161 {
6162#line 1666
6163 return;
6164}
6165}
6166#line 1667 "concatenated.c"
6167void __VERIFIER_atomic_end(void)
6168{
6169
6170 {
6171#line 1667
6172 return;
6173}
6174}