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