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{ struct request rq ;
2581
2582 {
2583 {
2584#line 281
2585 rq.cmd_type = (enum rq_cmd_type_bits )1;
2586#line 282
2587 rq.rq_disk = genhd_registered[genhd_no].gd;
2588#line 283
2589 rq.sector = __VERIFIER_nondet_sector_t();
2590#line 284
2591 rq.current_nr_sectors = __VERIFIER_nondet_uint();
2592#line 285
2593 rq.buffer = __VERIFIER_nondet_pchar();
2594#line 287
2595 genhd_registered[genhd_no].current_request = rq;
2596#line 288
2597 genhd_registered[genhd_no].requests_open = 1;
2598 }
2599#line 289
2600 return (0);
2601}
2602}
2603#line 291 "concatenated.c"
2604void call_rq_function(int genhd_no )
2605{ void *__cil_tmp2 ;
2606 unsigned long __cil_tmp3 ;
2607 struct request_queue *__cil_tmp4 ;
2608 request_fn_proc *__cil_tmp5 ;
2609 unsigned long __cil_tmp6 ;
2610 struct request_queue *__cil_tmp7 ;
2611 struct request_queue *__cil_tmp8 ;
2612 spinlock_t *__cil_tmp9 ;
2613 struct request_queue *__cil_tmp10 ;
2614 struct request_queue *__cil_tmp11 ;
2615 request_fn_proc *__cil_tmp12 ;
2616 struct request_queue *__cil_tmp13 ;
2617 struct request_queue *__cil_tmp14 ;
2618 spinlock_t *__cil_tmp15 ;
2619 struct request_queue *__cil_tmp16 ;
2620
2621 {
2622 {
2623#line 293
2624 __cil_tmp2 = (void *)0;
2625#line 293
2626 __cil_tmp3 = (unsigned long )__cil_tmp2;
2627#line 293
2628 __cil_tmp4 = (genhd_registered[genhd_no].gd)->queue;
2629#line 293
2630 __cil_tmp5 = __cil_tmp4->request_fn;
2631#line 293
2632 __cil_tmp6 = (unsigned long )__cil_tmp5;
2633#line 293
2634 if (__cil_tmp6 != __cil_tmp3) {
2635 {
2636#line 293
2637 __cil_tmp7 = (genhd_registered[genhd_no].gd)->queue;
2638#line 293
2639 if (__cil_tmp7->__ddv_queue_alive) {
2640 {
2641#line 296
2642 __cil_tmp8 = (genhd_registered[genhd_no].gd)->queue;
2643#line 296
2644 __cil_tmp9 = __cil_tmp8->queue_lock;
2645#line 296
2646 spin_lock(__cil_tmp9);
2647#line 298
2648 create_request(genhd_no);
2649#line 299
2650 __cil_tmp10 = (genhd_registered[genhd_no].gd)->queue;
2651#line 299
2652 __cil_tmp10->__ddv_genhd_no = genhd_no;
2653#line 301
2654 __cil_tmp11 = (genhd_registered[genhd_no].gd)->queue;
2655#line 301
2656 __cil_tmp12 = __cil_tmp11->request_fn;
2657#line 301
2658 __cil_tmp13 = (genhd_registered[genhd_no].gd)->queue;
2659#line 301
2660 (*__cil_tmp12)(__cil_tmp13);
2661#line 304
2662 __cil_tmp14 = (genhd_registered[genhd_no].gd)->queue;
2663#line 304
2664 __cil_tmp15 = __cil_tmp14->queue_lock;
2665#line 304
2666 spin_unlock(__cil_tmp15);
2667 }
2668#line 306
2669 return;
2670 } else {
2671
2672 }
2673 }
2674 } else {
2675
2676 }
2677 }
2678 {
2679#line 309
2680 __cil_tmp16 = (genhd_registered[genhd_no].gd)->queue;
2681#line 309
2682 if (__cil_tmp16->make_request_fn) {
2683#line 310
2684 return;
2685 } else {
2686
2687 }
2688 }
2689#line 312
2690 return;
2691}
2692}
2693#line 314 "concatenated.c"
2694void call_genhd_functions(void)
2695{ unsigned short genhd_no ;
2696 unsigned short function_no ;
2697 unsigned int uint_value ;
2698 unsigned long ulong_value ;
2699 void *tmp ;
2700 struct hd_geometry hdg ;
2701 struct block_device blk_dev ;
2702 int __cil_tmp9 ;
2703 int __cil_tmp10 ;
2704 int __cil_tmp11 ;
2705 int __cil_tmp12 ;
2706 int __cil_tmp13 ;
2707 struct block_device_operations *__cil_tmp14 ;
2708 unsigned int __cil_tmp15 ;
2709 struct block_device_operations *__cil_tmp16 ;
2710 int (*__cil_tmp17)(struct inode * , struct file * ) ;
2711 struct inode *__cil_tmp18 ;
2712 struct file *__cil_tmp19 ;
2713 struct block_device_operations *__cil_tmp20 ;
2714 struct block_device_operations *__cil_tmp21 ;
2715 int (*__cil_tmp22)(struct inode * , struct file * ) ;
2716 struct inode *__cil_tmp23 ;
2717 struct file *__cil_tmp24 ;
2718 struct block_device_operations *__cil_tmp25 ;
2719 struct block_device_operations *__cil_tmp26 ;
2720 int (*__cil_tmp27)(struct inode * , struct file * , unsigned int , unsigned long ) ;
2721 struct inode *__cil_tmp28 ;
2722 struct file *__cil_tmp29 ;
2723 struct block_device_operations *__cil_tmp30 ;
2724 struct block_device_operations *__cil_tmp31 ;
2725 int (*__cil_tmp32)(struct gendisk * ) ;
2726 struct block_device_operations *__cil_tmp33 ;
2727 struct block_device_operations *__cil_tmp34 ;
2728 int (*__cil_tmp35)(struct gendisk * ) ;
2729 struct block_device_operations *__cil_tmp36 ;
2730 struct block_device_operations *__cil_tmp37 ;
2731 int (*__cil_tmp38)(struct block_device * , struct hd_geometry * ) ;
2732
2733 {
2734 {
2735#line 321
2736 __cil_tmp9 = (int )number_genhd_registered;
2737#line 321
2738 if (__cil_tmp9 == 0) {
2739#line 322
2740 return;
2741 } else {
2742
2743 }
2744 }
2745 {
2746#line 325
2747 genhd_no = __VERIFIER_nondet_ushort();
2748#line 326
2749 __cil_tmp10 = (int )number_genhd_registered;
2750#line 326
2751 __cil_tmp11 = (int )genhd_no;
2752#line 326
2753 __cil_tmp12 = __cil_tmp11 < __cil_tmp10;
2754#line 326
2755 __VERIFIER_assume(__cil_tmp12);
2756#line 329
2757 function_no = __VERIFIER_nondet_ushort();
2758 }
2759#line 332
2760 if ((int )function_no == 0) {
2761 goto switch_8_0;
2762 } else {
2763#line 336
2764 if ((int )function_no == 1) {
2765 goto switch_8_1;
2766 } else {
2767#line 346
2768 if ((int )function_no == 2) {
2769 goto switch_8_2;
2770 } else {
2771#line 353
2772 if ((int )function_no == 3) {
2773 goto switch_8_3;
2774 } else {
2775#line 364
2776 if ((int )function_no == 4) {
2777 goto switch_8_4;
2778 } else {
2779#line 370
2780 if ((int )function_no == 5) {
2781 goto switch_8_5;
2782 } else {
2783#line 376
2784 if ((int )function_no == 6) {
2785 goto switch_8_6;
2786 } else {
2787 {
2788 goto switch_8_default;
2789#line 331
2790 if (0) {
2791 switch_8_0:
2792 {
2793#line 333
2794 __cil_tmp13 = (int )genhd_no;
2795#line 333
2796 call_rq_function(__cil_tmp13);
2797 }
2798 goto switch_8_break;
2799 switch_8_1:
2800 {
2801#line 337
2802 __cil_tmp14 = (genhd_registered[genhd_no].gd)->fops;
2803#line 337
2804 if (__cil_tmp14->open) {
2805 {
2806#line 338
2807 __cil_tmp15 = (unsigned int )32UL;
2808#line 338
2809 tmp = malloc(__cil_tmp15);
2810#line 338
2811 genhd_registered[genhd_no].inode.i_bdev = (struct block_device *)tmp;
2812#line 339
2813 (genhd_registered[genhd_no].inode.i_bdev)->bd_disk = genhd_registered[genhd_no].gd;
2814#line 341
2815 __cil_tmp16 = (genhd_registered[genhd_no].gd)->fops;
2816#line 341
2817 __cil_tmp17 = __cil_tmp16->open;
2818#line 341
2819 __cil_tmp18 = & genhd_registered[genhd_no].inode;
2820#line 341
2821 __cil_tmp19 = & genhd_registered[genhd_no].file;
2822#line 341
2823 (*__cil_tmp17)(__cil_tmp18, __cil_tmp19);
2824 }
2825 } else {
2826
2827 }
2828 }
2829 goto switch_8_break;
2830 switch_8_2:
2831 {
2832#line 347
2833 __cil_tmp20 = (genhd_registered[genhd_no].gd)->fops;
2834#line 347
2835 if (__cil_tmp20->release) {
2836 {
2837#line 348
2838 __cil_tmp21 = (genhd_registered[genhd_no].gd)->fops;
2839#line 348
2840 __cil_tmp22 = __cil_tmp21->release;
2841#line 348
2842 __cil_tmp23 = & genhd_registered[genhd_no].inode;
2843#line 348
2844 __cil_tmp24 = & genhd_registered[genhd_no].file;
2845#line 348
2846 (*__cil_tmp22)(__cil_tmp23, __cil_tmp24);
2847 }
2848 } else {
2849
2850 }
2851 }
2852 goto switch_8_break;
2853 switch_8_3:
2854 {
2855#line 354
2856 __cil_tmp25 = (genhd_registered[genhd_no].gd)->fops;
2857#line 354
2858 if (__cil_tmp25->ioctl) {
2859 {
2860#line 355
2861 uint_value = __VERIFIER_nondet_uint();
2862#line 356
2863 ulong_value = __VERIFIER_nondet_ulong();
2864#line 357
2865 __cil_tmp26 = (genhd_registered[genhd_no].gd)->fops;
2866#line 357
2867 __cil_tmp27 = __cil_tmp26->ioctl;
2868#line 357
2869 __cil_tmp28 = & genhd_registered[genhd_no].inode;
2870#line 357
2871 __cil_tmp29 = & genhd_registered[genhd_no].file;
2872#line 357
2873 (*__cil_tmp27)(__cil_tmp28, __cil_tmp29, uint_value, ulong_value);
2874 }
2875 } else {
2876
2877 }
2878 }
2879 goto switch_8_break;
2880 switch_8_4:
2881 {
2882#line 365
2883 __cil_tmp30 = (genhd_registered[genhd_no].gd)->fops;
2884#line 365
2885 if (__cil_tmp30->media_changed) {
2886 {
2887#line 366
2888 __cil_tmp31 = (genhd_registered[genhd_no].gd)->fops;
2889#line 366
2890 __cil_tmp32 = __cil_tmp31->media_changed;
2891#line 366
2892 (*__cil_tmp32)(genhd_registered[genhd_no].gd);
2893 }
2894 } else {
2895
2896 }
2897 }
2898 goto switch_8_break;
2899 switch_8_5:
2900 {
2901#line 371
2902 __cil_tmp33 = (genhd_registered[genhd_no].gd)->fops;
2903#line 371
2904 if (__cil_tmp33->revalidate_disk) {
2905 {
2906#line 372
2907 __cil_tmp34 = (genhd_registered[genhd_no].gd)->fops;
2908#line 372
2909 __cil_tmp35 = __cil_tmp34->revalidate_disk;
2910#line 372
2911 (*__cil_tmp35)(genhd_registered[genhd_no].gd);
2912 }
2913 } else {
2914
2915 }
2916 }
2917 goto switch_8_break;
2918 switch_8_6:
2919 {
2920#line 377
2921 __cil_tmp36 = (genhd_registered[genhd_no].gd)->fops;
2922#line 377
2923 if (__cil_tmp36->getgeo) {
2924 {
2925#line 381
2926 blk_dev.bd_disk = genhd_registered[genhd_no].gd;
2927#line 383
2928 __cil_tmp37 = (genhd_registered[genhd_no].gd)->fops;
2929#line 383
2930 __cil_tmp38 = __cil_tmp37->getgeo;
2931#line 383
2932 (*__cil_tmp38)(& blk_dev, & hdg);
2933 }
2934 } else {
2935
2936 }
2937 }
2938 goto switch_8_break;
2939 switch_8_default: ;
2940 goto switch_8_break;
2941 } else {
2942 switch_8_break: ;
2943 }
2944 }
2945 }
2946 }
2947 }
2948 }
2949 }
2950 }
2951 }
2952#line 390
2953 return;
2954}
2955}
2956#line 400 "concatenated.c"
2957void call_interrupt_handler(void)
2958{ unsigned short i ;
2959 struct pt_regs regs ;
2960 int tmp ;
2961 int __cil_tmp4 ;
2962 int __cil_tmp5 ;
2963 int __cil_tmp6 ;
2964
2965 {
2966 {
2967#line 405
2968 tmp = __VERIFIER_nondet_int();
2969#line 405
2970 i = (unsigned short )tmp;
2971#line 406
2972 __cil_tmp4 = (int )i;
2973#line 406
2974 __cil_tmp5 = __cil_tmp4 < 16;
2975#line 406
2976 __VERIFIER_assume(__cil_tmp5);
2977 }
2978#line 408
2979 if (registered_irq[i].handler) {
2980 {
2981#line 409
2982 __cil_tmp6 = (int )i;
2983#line 409
2984 (*(registered_irq[i].handler))(__cil_tmp6, registered_irq[i].dev_id, & regs);
2985 }
2986 } else {
2987
2988 }
2989#line 412
2990 return;
2991}
2992}
2993#line 438 "concatenated.c"
2994void create_pci_dev(void)
2995{
2996
2997 {
2998#line 440
2999 return;
3000}
3001}
3002#line 442 "concatenated.c"
3003int pci_probe_device(void)
3004{ int err ;
3005 unsigned int dev_id ;
3006 int __cil_tmp3 ;
3007 int (*__cil_tmp4)(struct pci_dev *dev , struct pci_device_id const *id ) ;
3008 struct pci_dev *__cil_tmp5 ;
3009 struct pci_device_id const *__cil_tmp6 ;
3010 struct pci_device_id const *__cil_tmp7 ;
3011
3012 {
3013 {
3014#line 447
3015 registered_pci_driver.no_pci_device_id = 1U;
3016#line 449
3017 dev_id = __VERIFIER_nondet_uint();
3018#line 450
3019 __cil_tmp3 = dev_id < registered_pci_driver.no_pci_device_id;
3020#line 450
3021 __VERIFIER_assume(__cil_tmp3);
3022#line 452
3023 __cil_tmp4 = (registered_pci_driver.pci_driver)->probe;
3024#line 452
3025 __cil_tmp5 = & registered_pci_driver.pci_dev;
3026#line 452
3027 __cil_tmp6 = (registered_pci_driver.pci_driver)->id_table;
3028#line 452
3029 __cil_tmp7 = __cil_tmp6 + dev_id;
3030#line 452
3031 err = (*__cil_tmp4)(__cil_tmp5, __cil_tmp7);
3032 }
3033#line 455
3034 if (! err) {
3035#line 456
3036 registered_pci_driver.dev_initialized = 1;
3037 } else {
3038
3039 }
3040#line 459
3041 return (err);
3042}
3043}
3044#line 462 "concatenated.c"
3045void pci_remove_device(void)
3046{ void (*__cil_tmp1)(struct pci_dev *dev ) ;
3047 struct pci_dev *__cil_tmp2 ;
3048
3049 {
3050 {
3051#line 464
3052 __cil_tmp1 = (registered_pci_driver.pci_driver)->remove;
3053#line 464
3054 __cil_tmp2 = & registered_pci_driver.pci_dev;
3055#line 464
3056 (*__cil_tmp1)(__cil_tmp2);
3057#line 466
3058 registered_pci_driver.dev_initialized = 0;
3059 }
3060#line 467
3061 return;
3062}
3063}
3064#line 469 "concatenated.c"
3065void call_pci_functions(void)
3066{ unsigned int tmp ;
3067
3068 {
3069 {
3070#line 471
3071 tmp = __VERIFIER_nondet_uint();
3072 }
3073#line 472
3074 if ((int )tmp == 0) {
3075 goto switch_9_0;
3076 } else {
3077#line 478
3078 if ((int )tmp == 1) {
3079 goto switch_9_1;
3080 } else {
3081 {
3082 goto switch_9_default;
3083#line 471
3084 if (0) {
3085 switch_9_0:
3086#line 473
3087 if (! registered_pci_driver.dev_initialized) {
3088 {
3089#line 474
3090 pci_probe_device();
3091 }
3092 } else {
3093
3094 }
3095 goto switch_9_break;
3096 switch_9_1:
3097#line 479
3098 if (registered_pci_driver.dev_initialized) {
3099 {
3100#line 480
3101 pci_remove_device();
3102 }
3103 } else {
3104
3105 }
3106 goto switch_9_break;
3107 switch_9_default: ;
3108 goto switch_9_break;
3109 } else {
3110 switch_9_break: ;
3111 }
3112 }
3113 }
3114 }
3115#line 487
3116 return;
3117}
3118}
3119#line 490 "concatenated.c"
3120void call_tasklet_functions(void)
3121{ unsigned int i ;
3122 int __cil_tmp2 ;
3123 void *__cil_tmp3 ;
3124 unsigned long __cil_tmp4 ;
3125 unsigned long __cil_tmp5 ;
3126 atomic_t __cil_tmp6 ;
3127 void (*__cil_tmp7)(unsigned long ) ;
3128 unsigned long __cil_tmp8 ;
3129 void *__cil_tmp9 ;
3130
3131 {
3132 {
3133#line 493
3134 __cil_tmp2 = i < 1U;
3135#line 493
3136 __VERIFIER_assume(__cil_tmp2);
3137 }
3138 {
3139#line 495
3140 __cil_tmp3 = (void *)0;
3141#line 495
3142 __cil_tmp4 = (unsigned long )__cil_tmp3;
3143#line 495
3144 __cil_tmp5 = (unsigned long )tasklet_registered[i].tasklet;
3145#line 495
3146 if (__cil_tmp5 != __cil_tmp4) {
3147 {
3148#line 495
3149 __cil_tmp6 = (tasklet_registered[i].tasklet)->count;
3150#line 495
3151 if (__cil_tmp6 == 0) {
3152 {
3153#line 497
3154 tasklet_registered[i].is_running = (unsigned short)1;
3155#line 498
3156 __cil_tmp7 = (tasklet_registered[i].tasklet)->func;
3157#line 498
3158 __cil_tmp8 = (tasklet_registered[i].tasklet)->data;
3159#line 498
3160 (*__cil_tmp7)(__cil_tmp8);
3161#line 499
3162 tasklet_registered[i].is_running = (unsigned short)0;
3163#line 500
3164 __cil_tmp9 = (void *)0;
3165#line 500
3166 tasklet_registered[i].tasklet = (struct tasklet_struct *)__cil_tmp9;
3167 }
3168 } else {
3169
3170 }
3171 }
3172 } else {
3173
3174 }
3175 }
3176#line 502
3177 return;
3178}
3179}
3180#line 506 "concatenated.c"
3181void call_timer_functions(void)
3182{ unsigned short i ;
3183 unsigned short tmp ;
3184 int __cil_tmp3 ;
3185 int __cil_tmp4 ;
3186 int __cil_tmp5 ;
3187 void (*__cil_tmp6)(unsigned long ) ;
3188 unsigned long __cil_tmp7 ;
3189
3190 {
3191 {
3192#line 508
3193 tmp = __VERIFIER_nondet_ushort();
3194#line 508
3195 i = tmp;
3196#line 510
3197 __cil_tmp3 = (int )number_timer_registered;
3198#line 510
3199 __cil_tmp4 = (int )i;
3200#line 510
3201 __cil_tmp5 = __cil_tmp4 < __cil_tmp3;
3202#line 510
3203 __VERIFIER_assume(__cil_tmp5);
3204 }
3205#line 512
3206 if ((timer_registered[i].timer)->__ddv_active) {
3207 {
3208#line 513
3209 __cil_tmp6 = (timer_registered[i].timer)->function;
3210#line 513
3211 __cil_tmp7 = (timer_registered[i].timer)->data;
3212#line 513
3213 (*__cil_tmp6)(__cil_tmp7);
3214 }
3215 } else {
3216
3217 }
3218#line 515
3219 return;
3220}
3221}
3222#line 523 "concatenated.c"
3223__inline int pci_enable_device(struct pci_dev *dev )
3224{ int i ;
3225 unsigned int tmp ;
3226 unsigned short tmp___0 ;
3227 unsigned long __cil_tmp5 ;
3228 unsigned long __cil_tmp6 ;
3229
3230 {
3231#line 527
3232 i = 0;
3233 {
3234#line 527
3235 while (1) {
3236 while_10_continue: ;
3237#line 527
3238 if (i < 12) {
3239
3240 } else {
3241 goto while_10_break;
3242 }
3243 {
3244#line 528
3245 dev->resource[i].flags = 256UL;
3246#line 529
3247 tmp = __VERIFIER_nondet_uint();
3248#line 529
3249 dev->resource[i].start = (unsigned long )tmp;
3250#line 530
3251 tmp___0 = __VERIFIER_nondet_ushort();
3252#line 530
3253 __cil_tmp5 = (unsigned long )tmp___0;
3254#line 530
3255 __cil_tmp6 = dev->resource[i].start;
3256#line 530
3257 dev->resource[i].end = __cil_tmp6 + __cil_tmp5;
3258#line 527
3259 i = i + 1;
3260 }
3261 }
3262 while_10_break: ;
3263 }
3264#line 532
3265 return (0);
3266}
3267}
3268#line 534 "concatenated.c"
3269__inline struct pci_dev *pci_get_class(unsigned int class , struct pci_dev *from )
3270{ void *tmp ;
3271 int tmp___0 ;
3272 void *__cil_tmp5 ;
3273 unsigned long __cil_tmp6 ;
3274 unsigned long __cil_tmp7 ;
3275 unsigned int __cil_tmp8 ;
3276 unsigned int __cil_tmp9 ;
3277 int __cil_tmp10 ;
3278 void *__cil_tmp11 ;
3279
3280 {
3281 {
3282#line 536
3283 __cil_tmp5 = (void *)0;
3284#line 536
3285 __cil_tmp6 = (unsigned long )__cil_tmp5;
3286#line 536
3287 __cil_tmp7 = (unsigned long )from;
3288#line 536
3289 if (__cil_tmp7 == __cil_tmp6) {
3290 {
3291#line 537
3292 __cil_tmp8 = (unsigned int )432UL;
3293#line 537
3294 tmp = malloc(__cil_tmp8);
3295#line 537
3296 from = (struct pci_dev *)tmp;
3297 }
3298 } else {
3299
3300 }
3301 }
3302 {
3303#line 540
3304 tmp___0 = __VERIFIER_nondet_int();
3305 }
3306#line 540
3307 if (tmp___0) {
3308 {
3309#line 541
3310 from->vendor = __VERIFIER_nondet_ushort();
3311#line 542
3312 from->device = __VERIFIER_nondet_ushort();
3313#line 543
3314 from->irq = __VERIFIER_nondet_uint();
3315#line 544
3316 __cil_tmp9 = from->irq;
3317#line 544
3318 __cil_tmp10 = __cil_tmp9 < 16U;
3319#line 544
3320 __VERIFIER_assume(__cil_tmp10);
3321 }
3322#line 546
3323 return (from);
3324 } else {
3325 {
3326#line 548
3327 __cil_tmp11 = (void *)0;
3328#line 548
3329 return ((struct pci_dev *)__cil_tmp11);
3330 }
3331 }
3332}
3333}
3334#line 552 "concatenated.c"
3335__inline int pci_register_driver(struct pci_driver *driver )
3336{ int tmp ;
3337 unsigned long __cil_tmp3 ;
3338
3339 {
3340 {
3341#line 554
3342 tmp = __VERIFIER_nondet_int();
3343 }
3344#line 554
3345 if (tmp) {
3346#line 555
3347 registered_pci_driver.pci_driver = driver;
3348#line 556
3349 __cil_tmp3 = 8UL / 32UL;
3350#line 556
3351 registered_pci_driver.no_pci_device_id = (unsigned int )__cil_tmp3;
3352#line 557
3353 registered_pci_driver.dev_initialized = 0;
3354#line 559
3355 return (0);
3356 } else {
3357#line 561
3358 return (-1);
3359 }
3360}
3361}
3362#line 565 "concatenated.c"
3363__inline void pci_unregister_driver(struct pci_driver *driver )
3364{ void *__cil_tmp2 ;
3365
3366 {
3367#line 567
3368 __cil_tmp2 = (void *)0;
3369#line 567
3370 registered_pci_driver.pci_driver = (struct pci_driver *)__cil_tmp2;
3371#line 568
3372 registered_pci_driver.no_pci_device_id = 0U;
3373#line 569
3374 return;
3375}
3376}
3377#line 571 "concatenated.c"
3378__inline void pci_release_region(struct pci_dev *pdev , int bar )
3379{ unsigned long tmp ;
3380 unsigned long tmp___0 ;
3381 unsigned long tmp___1 ;
3382 unsigned long __cil_tmp6 ;
3383 unsigned long __cil_tmp7 ;
3384 unsigned long __cil_tmp8 ;
3385 unsigned long __cil_tmp9 ;
3386 unsigned long __cil_tmp10 ;
3387 unsigned long __cil_tmp11 ;
3388 unsigned long __cil_tmp12 ;
3389 unsigned long __cil_tmp13 ;
3390 unsigned long __cil_tmp14 ;
3391 unsigned long __cil_tmp15 ;
3392 unsigned long __cil_tmp16 ;
3393 unsigned long __cil_tmp17 ;
3394 unsigned long __cil_tmp18 ;
3395 unsigned long __cil_tmp19 ;
3396 unsigned long __cil_tmp20 ;
3397 unsigned long __cil_tmp21 ;
3398 unsigned long __cil_tmp22 ;
3399 unsigned long __cil_tmp23 ;
3400 unsigned long __cil_tmp24 ;
3401 unsigned long __cil_tmp25 ;
3402 unsigned long __cil_tmp26 ;
3403 unsigned long __cil_tmp27 ;
3404 unsigned long __cil_tmp28 ;
3405 unsigned long __cil_tmp29 ;
3406 unsigned long __cil_tmp30 ;
3407 unsigned long __cil_tmp31 ;
3408 unsigned long __cil_tmp32 ;
3409 unsigned long __cil_tmp33 ;
3410 unsigned long __cil_tmp34 ;
3411 unsigned long __cil_tmp35 ;
3412 unsigned long __cil_tmp36 ;
3413
3414 {
3415 {
3416#line 573
3417 __cil_tmp6 = pdev->resource[bar].start;
3418#line 573
3419 if (__cil_tmp6 == 0UL) {
3420 {
3421#line 573
3422 __cil_tmp7 = pdev->resource[bar].start;
3423#line 573
3424 __cil_tmp8 = pdev->resource[bar].end;
3425#line 573
3426 if (__cil_tmp8 == __cil_tmp7) {
3427#line 573
3428 tmp = 0UL;
3429 } else {
3430#line 573
3431 __cil_tmp9 = pdev->resource[bar].start;
3432#line 573
3433 __cil_tmp10 = pdev->resource[bar].end;
3434#line 573
3435 __cil_tmp11 = __cil_tmp10 - __cil_tmp9;
3436#line 573
3437 tmp = __cil_tmp11 + 1UL;
3438 }
3439 }
3440 } else {
3441#line 573
3442 __cil_tmp12 = pdev->resource[bar].start;
3443#line 573
3444 __cil_tmp13 = pdev->resource[bar].end;
3445#line 573
3446 __cil_tmp14 = __cil_tmp13 - __cil_tmp12;
3447#line 573
3448 tmp = __cil_tmp14 + 1UL;
3449 }
3450 }
3451#line 573
3452 if (tmp == 0UL) {
3453#line 574
3454 return;
3455 } else {
3456
3457 }
3458 {
3459#line 575
3460 __cil_tmp15 = pdev->resource[bar].flags;
3461#line 575
3462 if (__cil_tmp15 & 256UL) {
3463 {
3464#line 576
3465 __cil_tmp16 = pdev->resource[bar].start;
3466#line 576
3467 if (__cil_tmp16 == 0UL) {
3468 {
3469#line 576
3470 __cil_tmp17 = pdev->resource[bar].start;
3471#line 576
3472 __cil_tmp18 = pdev->resource[bar].end;
3473#line 576
3474 if (__cil_tmp18 == __cil_tmp17) {
3475#line 576
3476 tmp___0 = 0UL;
3477 } else {
3478#line 576
3479 __cil_tmp19 = pdev->resource[bar].start;
3480#line 576
3481 __cil_tmp20 = pdev->resource[bar].end;
3482#line 576
3483 __cil_tmp21 = __cil_tmp20 - __cil_tmp19;
3484#line 576
3485 tmp___0 = __cil_tmp21 + 1UL;
3486 }
3487 }
3488 } else {
3489#line 576
3490 __cil_tmp22 = pdev->resource[bar].start;
3491#line 576
3492 __cil_tmp23 = pdev->resource[bar].end;
3493#line 576
3494 __cil_tmp24 = __cil_tmp23 - __cil_tmp22;
3495#line 576
3496 tmp___0 = __cil_tmp24 + 1UL;
3497 }
3498 }
3499 {
3500#line 576
3501 __cil_tmp25 = pdev->resource[bar].start;
3502#line 576
3503 release_region(__cil_tmp25, tmp___0);
3504 }
3505 } else {
3506 {
3507#line 578
3508 __cil_tmp26 = pdev->resource[bar].flags;
3509#line 578
3510 if (__cil_tmp26 & 512UL) {
3511 {
3512#line 579
3513 __cil_tmp27 = pdev->resource[bar].start;
3514#line 579
3515 if (__cil_tmp27 == 0UL) {
3516 {
3517#line 579
3518 __cil_tmp28 = pdev->resource[bar].start;
3519#line 579
3520 __cil_tmp29 = pdev->resource[bar].end;
3521#line 579
3522 if (__cil_tmp29 == __cil_tmp28) {
3523#line 579
3524 tmp___1 = 0UL;
3525 } else {
3526#line 579
3527 __cil_tmp30 = pdev->resource[bar].start;
3528#line 579
3529 __cil_tmp31 = pdev->resource[bar].end;
3530#line 579
3531 __cil_tmp32 = __cil_tmp31 - __cil_tmp30;
3532#line 579
3533 tmp___1 = __cil_tmp32 + 1UL;
3534 }
3535 }
3536 } else {
3537#line 579
3538 __cil_tmp33 = pdev->resource[bar].start;
3539#line 579
3540 __cil_tmp34 = pdev->resource[bar].end;
3541#line 579
3542 __cil_tmp35 = __cil_tmp34 - __cil_tmp33;
3543#line 579
3544 tmp___1 = __cil_tmp35 + 1UL;
3545 }
3546 }
3547 {
3548#line 579
3549 __cil_tmp36 = pdev->resource[bar].start;
3550#line 579
3551 release_mem_region(__cil_tmp36, tmp___1);
3552 }
3553 } else {
3554
3555 }
3556 }
3557 }
3558 }
3559#line 581
3560 return;
3561}
3562}
3563#line 583 "concatenated.c"
3564__inline int pci_request_region(struct pci_dev *pdev , int bar , char const *res_name )
3565{ unsigned long tmp ;
3566 unsigned long tmp___0 ;
3567 struct resource *tmp___1 ;
3568 unsigned long tmp___2 ;
3569 struct resource *tmp___3 ;
3570 unsigned long __cil_tmp9 ;
3571 unsigned long __cil_tmp10 ;
3572 unsigned long __cil_tmp11 ;
3573 unsigned long __cil_tmp12 ;
3574 unsigned long __cil_tmp13 ;
3575 unsigned long __cil_tmp14 ;
3576 unsigned long __cil_tmp15 ;
3577 unsigned long __cil_tmp16 ;
3578 unsigned long __cil_tmp17 ;
3579 unsigned long __cil_tmp18 ;
3580 unsigned long __cil_tmp19 ;
3581 unsigned long __cil_tmp20 ;
3582 unsigned long __cil_tmp21 ;
3583 unsigned long __cil_tmp22 ;
3584 unsigned long __cil_tmp23 ;
3585 unsigned long __cil_tmp24 ;
3586 unsigned long __cil_tmp25 ;
3587 unsigned long __cil_tmp26 ;
3588 unsigned long __cil_tmp27 ;
3589 unsigned long __cil_tmp28 ;
3590 unsigned long __cil_tmp29 ;
3591 unsigned long __cil_tmp30 ;
3592 unsigned long __cil_tmp31 ;
3593 unsigned long __cil_tmp32 ;
3594 unsigned long __cil_tmp33 ;
3595 unsigned long __cil_tmp34 ;
3596 unsigned long __cil_tmp35 ;
3597 unsigned long __cil_tmp36 ;
3598 unsigned long __cil_tmp37 ;
3599 unsigned long __cil_tmp38 ;
3600 unsigned long __cil_tmp39 ;
3601
3602 {
3603 {
3604#line 585
3605 __cil_tmp9 = pdev->resource[bar].start;
3606#line 585
3607 if (__cil_tmp9 == 0UL) {
3608 {
3609#line 585
3610 __cil_tmp10 = pdev->resource[bar].start;
3611#line 585
3612 __cil_tmp11 = pdev->resource[bar].end;
3613#line 585
3614 if (__cil_tmp11 == __cil_tmp10) {
3615#line 585
3616 tmp = 0UL;
3617 } else {
3618#line 585
3619 __cil_tmp12 = pdev->resource[bar].start;
3620#line 585
3621 __cil_tmp13 = pdev->resource[bar].end;
3622#line 585
3623 __cil_tmp14 = __cil_tmp13 - __cil_tmp12;
3624#line 585
3625 tmp = __cil_tmp14 + 1UL;
3626 }
3627 }
3628 } else {
3629#line 585
3630 __cil_tmp15 = pdev->resource[bar].start;
3631#line 585
3632 __cil_tmp16 = pdev->resource[bar].end;
3633#line 585
3634 __cil_tmp17 = __cil_tmp16 - __cil_tmp15;
3635#line 585
3636 tmp = __cil_tmp17 + 1UL;
3637 }
3638 }
3639#line 585
3640 if (tmp == 0UL) {
3641#line 586
3642 return (0);
3643 } else {
3644
3645 }
3646 {
3647#line 588
3648 __cil_tmp18 = pdev->resource[bar].flags;
3649#line 588
3650 if (__cil_tmp18 & 256UL) {
3651 {
3652#line 589
3653 __cil_tmp19 = pdev->resource[bar].start;
3654#line 589
3655 if (__cil_tmp19 == 0UL) {
3656 {
3657#line 589
3658 __cil_tmp20 = pdev->resource[bar].start;
3659#line 589
3660 __cil_tmp21 = pdev->resource[bar].end;
3661#line 589
3662 if (__cil_tmp21 == __cil_tmp20) {
3663#line 589
3664 tmp___0 = 0UL;
3665 } else {
3666#line 589
3667 __cil_tmp22 = pdev->resource[bar].start;
3668#line 589
3669 __cil_tmp23 = pdev->resource[bar].end;
3670#line 589
3671 __cil_tmp24 = __cil_tmp23 - __cil_tmp22;
3672#line 589
3673 tmp___0 = __cil_tmp24 + 1UL;
3674 }
3675 }
3676 } else {
3677#line 589
3678 __cil_tmp25 = pdev->resource[bar].start;
3679#line 589
3680 __cil_tmp26 = pdev->resource[bar].end;
3681#line 589
3682 __cil_tmp27 = __cil_tmp26 - __cil_tmp25;
3683#line 589
3684 tmp___0 = __cil_tmp27 + 1UL;
3685 }
3686 }
3687 {
3688#line 589
3689 __cil_tmp28 = pdev->resource[bar].start;
3690#line 589
3691 tmp___1 = request_region(__cil_tmp28, tmp___0, res_name);
3692 }
3693#line 589
3694 if (tmp___1) {
3695
3696 } else {
3697#line 591
3698 return (-16);
3699 }
3700 } else {
3701 {
3702#line 593
3703 __cil_tmp29 = pdev->resource[bar].flags;
3704#line 593
3705 if (__cil_tmp29 & 512UL) {
3706 {
3707#line 594
3708 __cil_tmp30 = pdev->resource[bar].start;
3709#line 594
3710 if (__cil_tmp30 == 0UL) {
3711 {
3712#line 594
3713 __cil_tmp31 = pdev->resource[bar].start;
3714#line 594
3715 __cil_tmp32 = pdev->resource[bar].end;
3716#line 594
3717 if (__cil_tmp32 == __cil_tmp31) {
3718#line 594
3719 tmp___2 = 0UL;
3720 } else {
3721#line 594
3722 __cil_tmp33 = pdev->resource[bar].start;
3723#line 594
3724 __cil_tmp34 = pdev->resource[bar].end;
3725#line 594
3726 __cil_tmp35 = __cil_tmp34 - __cil_tmp33;
3727#line 594
3728 tmp___2 = __cil_tmp35 + 1UL;
3729 }
3730 }
3731 } else {
3732#line 594
3733 __cil_tmp36 = pdev->resource[bar].start;
3734#line 594
3735 __cil_tmp37 = pdev->resource[bar].end;
3736#line 594
3737 __cil_tmp38 = __cil_tmp37 - __cil_tmp36;
3738#line 594
3739 tmp___2 = __cil_tmp38 + 1UL;
3740 }
3741 }
3742 {
3743#line 594
3744 __cil_tmp39 = pdev->resource[bar].start;
3745#line 594
3746 tmp___3 = request_mem_region(__cil_tmp39, tmp___2, res_name);
3747 }
3748#line 594
3749 if (tmp___3) {
3750
3751 } else {
3752#line 596
3753 return (-16);
3754 }
3755 } else {
3756
3757 }
3758 }
3759 }
3760 }
3761#line 599
3762 return (0);
3763}
3764}
3765#line 602 "concatenated.c"
3766__inline void pci_release_regions(struct pci_dev *pdev )
3767{ int i ;
3768
3769 {
3770#line 606
3771 i = 0;
3772 {
3773#line 606
3774 while (1) {
3775 while_11_continue: ;
3776#line 606
3777 if (i < 6) {
3778
3779 } else {
3780 goto while_11_break;
3781 }
3782 {
3783#line 607
3784 pci_release_region(pdev, i);
3785#line 606
3786 i = i + 1;
3787 }
3788 }
3789 while_11_break: ;
3790 }
3791#line 608
3792 return;
3793}
3794}
3795#line 610 "concatenated.c"
3796__inline int pci_request_regions(struct pci_dev *pdev , char const *res_name )
3797{ int i ;
3798 int tmp ;
3799
3800 {
3801#line 614
3802 i = 0;
3803 {
3804#line 614
3805 while (1) {
3806 while_12_continue: ;
3807#line 614
3808 if (i < 6) {
3809
3810 } else {
3811 goto while_12_break;
3812 }
3813 {
3814#line 615
3815 tmp = pci_request_region(pdev, i, res_name);
3816 }
3817#line 615
3818 if (tmp) {
3819 goto err_out;
3820 } else {
3821
3822 }
3823#line 614
3824 i = i + 1;
3825 }
3826 while_12_break: ;
3827 }
3828#line 617
3829 return (0);
3830 err_out:
3831 {
3832#line 620
3833 while (1) {
3834 while_13_continue: ;
3835#line 620
3836 i = i - 1;
3837#line 620
3838 if (i >= 0) {
3839
3840 } else {
3841 goto while_13_break;
3842 }
3843 {
3844#line 621
3845 pci_release_region(pdev, i);
3846 }
3847 }
3848 while_13_break: ;
3849 }
3850#line 623
3851 return (-16);
3852}
3853}
3854#line 629 "concatenated.c"
3855__inline int __get_user(int size , void *ptr )
3856{ int tmp ;
3857
3858 {
3859 {
3860#line 632
3861 assert_context_process();
3862#line 634
3863 tmp = __VERIFIER_nondet_int();
3864 }
3865#line 634
3866 return (tmp);
3867}
3868}
3869#line 637 "concatenated.c"
3870__inline int get_user(int size , void *ptr )
3871{ int tmp ;
3872
3873 {
3874 {
3875#line 640
3876 assert_context_process();
3877#line 642
3878 tmp = __VERIFIER_nondet_int();
3879 }
3880#line 642
3881 return (tmp);
3882}
3883}
3884#line 645 "concatenated.c"
3885__inline int __put_user(int size , void *ptr )
3886{ int tmp ;
3887
3888 {
3889 {
3890#line 648
3891 assert_context_process();
3892#line 650
3893 tmp = __VERIFIER_nondet_int();
3894 }
3895#line 650
3896 return (tmp);
3897}
3898}
3899#line 653 "concatenated.c"
3900__inline int put_user(int size , void *ptr )
3901{ int tmp ;
3902
3903 {
3904 {
3905#line 656
3906 assert_context_process();
3907#line 658
3908 tmp = __VERIFIER_nondet_int();
3909 }
3910#line 658
3911 return (tmp);
3912}
3913}
3914#line 661 "concatenated.c"
3915__inline unsigned long copy_to_user(void *to , void const *from , unsigned long n )
3916{ unsigned long tmp ;
3917
3918 {
3919 {
3920#line 664
3921 assert_context_process();
3922#line 666
3923 tmp = __VERIFIER_nondet_ulong();
3924 }
3925#line 666
3926 return (tmp);
3927}
3928}
3929#line 669 "concatenated.c"
3930__inline unsigned long copy_from_user(void *to , void *from , unsigned long n )
3931{ unsigned long tmp ;
3932
3933 {
3934 {
3935#line 672
3936 assert_context_process();
3937#line 674
3938 tmp = __VERIFIER_nondet_ulong();
3939 }
3940#line 674
3941 return (tmp);
3942}
3943}
3944#line 681 "concatenated.c"
3945int register_blkdev(unsigned int major , char const *name )
3946{ int result ;
3947 int tmp ;
3948
3949 {
3950 {
3951#line 683
3952 tmp = __VERIFIER_nondet_int();
3953#line 683
3954 result = tmp;
3955 }
3956#line 689
3957 return (result);
3958}
3959}
3960#line 692 "concatenated.c"
3961int unregister_blkdev(unsigned int major , char const *name )
3962{
3963
3964 {
3965#line 694
3966 return (0);
3967}
3968}
3969#line 697 "concatenated.c"
3970struct gendisk *alloc_disk(int minors )
3971{ struct gendisk *gd ;
3972 int __cil_tmp3 ;
3973 int __cil_tmp4 ;
3974 int __cil_tmp5 ;
3975 void *__cil_tmp6 ;
3976
3977 {
3978 {
3979#line 701
3980 __cil_tmp3 = (int )number_fixed_genhd_used;
3981#line 701
3982 if (__cil_tmp3 < 10) {
3983#line 702
3984 gd = & fixed_gendisk[number_fixed_genhd_used];
3985#line 703
3986 gd->minors = minors;
3987#line 705
3988 __cil_tmp4 = (int )number_fixed_genhd_used;
3989#line 705
3990 __cil_tmp5 = __cil_tmp4 + 1;
3991#line 705
3992 number_fixed_genhd_used = (short )__cil_tmp5;
3993#line 707
3994 return (gd);
3995 } else {
3996 {
3997#line 709
3998 __cil_tmp6 = (void *)0;
3999#line 709
4000 return ((struct gendisk *)__cil_tmp6);
4001 }
4002 }
4003 }
4004}
4005}
4006#line 713 "concatenated.c"
4007void add_disk(struct gendisk *disk )
4008{ void *tmp ;
4009 int __cil_tmp3 ;
4010 unsigned int __cil_tmp4 ;
4011 int __cil_tmp5 ;
4012 int __cil_tmp6 ;
4013
4014 {
4015 {
4016#line 715
4017 __cil_tmp3 = (int )number_genhd_registered;
4018#line 715
4019 if (__cil_tmp3 < 10) {
4020 {
4021#line 716
4022 genhd_registered[number_genhd_registered].gd = disk;
4023#line 717
4024 __cil_tmp4 = (unsigned int )32UL;
4025#line 717
4026 tmp = malloc(__cil_tmp4);
4027#line 717
4028 genhd_registered[number_genhd_registered].inode.i_bdev = (struct block_device *)tmp;
4029#line 718
4030 (genhd_registered[number_genhd_registered].inode.i_bdev)->bd_disk = disk;
4031#line 720
4032 __cil_tmp5 = (int )number_genhd_registered;
4033#line 720
4034 __cil_tmp6 = __cil_tmp5 + 1;
4035#line 720
4036 number_genhd_registered = (short )__cil_tmp6;
4037 }
4038 } else {
4039
4040 }
4041 }
4042#line 722
4043 return;
4044}
4045}
4046#line 724 "concatenated.c"
4047void del_gendisk(struct gendisk *gp )
4048{ int i ;
4049 int __cil_tmp3 ;
4050 unsigned long __cil_tmp4 ;
4051 unsigned long __cil_tmp5 ;
4052 void *__cil_tmp6 ;
4053
4054 {
4055#line 728
4056 i = 0;
4057 {
4058#line 728
4059 while (1) {
4060 while_14_continue: ;
4061 {
4062#line 728
4063 __cil_tmp3 = (int )number_genhd_registered;
4064#line 728
4065 if (i < __cil_tmp3) {
4066
4067 } else {
4068 goto while_14_break;
4069 }
4070 }
4071 {
4072#line 729
4073 __cil_tmp4 = (unsigned long )gp;
4074#line 729
4075 __cil_tmp5 = (unsigned long )genhd_registered[i].gd;
4076#line 729
4077 if (__cil_tmp5 == __cil_tmp4) {
4078#line 730
4079 __cil_tmp6 = (void *)0;
4080#line 730
4081 genhd_registered[i].gd = (struct gendisk *)__cil_tmp6;
4082 } else {
4083
4084 }
4085 }
4086#line 728
4087 i = i + 1;
4088 }
4089 while_14_break: ;
4090 }
4091#line 733
4092 return;
4093}
4094}
4095#line 6 "/ddverify-2010-04-30/models/seq1/include/ddverify/blkdev.h"
4096request_queue_t fixed_request_queue[10] ;
4097#line 8 "/ddverify-2010-04-30/models/seq1/include/ddverify/blkdev.h"
4098int number_request_queue_used = 0;
4099#line 740 "concatenated.c"
4100request_queue_t *get_fixed_request_queue(void)
4101{ int tmp ;
4102 void *__cil_tmp2 ;
4103
4104 {
4105#line 742
4106 if (number_request_queue_used < 10) {
4107#line 743
4108 tmp = number_request_queue_used;
4109#line 743
4110 number_request_queue_used = number_request_queue_used + 1;
4111#line 743
4112 return (& fixed_request_queue[tmp]);
4113 } else {
4114 {
4115#line 745
4116 __cil_tmp2 = (void *)0;
4117#line 745
4118 return ((request_queue_t *)__cil_tmp2);
4119 }
4120 }
4121}
4122}
4123#line 749 "concatenated.c"
4124request_queue_t *blk_init_queue(request_fn_proc *rfn , spinlock_t *lock )
4125{ request_queue_t *queue ;
4126 int tmp ;
4127 void *__cil_tmp5 ;
4128 void *__cil_tmp6 ;
4129
4130 {
4131 {
4132#line 753
4133 tmp = __VERIFIER_nondet_int();
4134 }
4135#line 753
4136 if (tmp) {
4137 {
4138#line 754
4139 queue = get_fixed_request_queue();
4140#line 756
4141 queue->queue_lock = lock;
4142#line 757
4143 queue->request_fn = rfn;
4144#line 758
4145 __cil_tmp5 = (void *)0;
4146#line 758
4147 queue->make_request_fn = (make_request_fn *)__cil_tmp5;
4148#line 759
4149 queue->__ddv_queue_alive = 1;
4150 }
4151#line 761
4152 return (queue);
4153 } else {
4154 {
4155#line 763
4156 __cil_tmp6 = (void *)0;
4157#line 763
4158 return ((request_queue_t *)__cil_tmp6);
4159 }
4160 }
4161}
4162}
4163#line 767 "concatenated.c"
4164request_queue_t *blk_alloc_queue(gfp_t gfp_mask )
4165{ request_queue_t *queue ;
4166 int tmp ;
4167 void *__cil_tmp4 ;
4168 void *__cil_tmp5 ;
4169 void *__cil_tmp6 ;
4170
4171 {
4172 {
4173#line 771
4174 tmp = __VERIFIER_nondet_int();
4175 }
4176#line 771
4177 if (tmp) {
4178 {
4179#line 772
4180 queue = get_fixed_request_queue();
4181#line 774
4182 __cil_tmp4 = (void *)0;
4183#line 774
4184 queue->request_fn = (request_fn_proc *)__cil_tmp4;
4185#line 775
4186 __cil_tmp5 = (void *)0;
4187#line 775
4188 queue->make_request_fn = (make_request_fn *)__cil_tmp5;
4189#line 776
4190 queue->__ddv_queue_alive = 1;
4191 }
4192#line 778
4193 return (queue);
4194 } else {
4195 {
4196#line 780
4197 __cil_tmp6 = (void *)0;
4198#line 780
4199 return ((request_queue_t *)__cil_tmp6);
4200 }
4201 }
4202}
4203}
4204#line 784 "concatenated.c"
4205void blk_queue_make_request(request_queue_t *q , make_request_fn *mfn )
4206{
4207
4208 {
4209#line 786
4210 q->make_request_fn = mfn;
4211#line 787
4212 return;
4213}
4214}
4215#line 789 "concatenated.c"
4216void end_request(struct request *req , int uptodate )
4217{ int genhd_no ;
4218 struct gendisk *__cil_tmp4 ;
4219 struct request_queue *__cil_tmp5 ;
4220
4221 {
4222#line 791
4223 __cil_tmp4 = req->rq_disk;
4224#line 791
4225 __cil_tmp5 = __cil_tmp4->queue;
4226#line 791
4227 genhd_no = __cil_tmp5->__ddv_genhd_no;
4228#line 793
4229 genhd_registered[genhd_no].requests_open = 0;
4230#line 794
4231 return;
4232}
4233}
4234#line 797 "concatenated.c"
4235void blk_queue_hardsect_size(request_queue_t *q , unsigned short size )
4236{
4237
4238 {
4239#line 799
4240 q->hardsect_size = size;
4241#line 800
4242 return;
4243}
4244}
4245#line 802 "concatenated.c"
4246void blk_cleanup_queue(request_queue_t *q )
4247{
4248
4249 {
4250#line 804
4251 q->__ddv_queue_alive = 0;
4252#line 805
4253 return;
4254}
4255}
4256#line 11 "/ddverify-2010-04-30/models/seq1/include/linux/proc_fs.h"
4257struct proc_dir_entry *proc_root_driver ;
4258#line 823 "concatenated.c"
4259int misc_register(struct miscdevice *misc )
4260{ int i ;
4261 dev_t dev ;
4262 int tmp ;
4263 int __cil_tmp5 ;
4264 int __cil_tmp6 ;
4265 int __cil_tmp7 ;
4266 struct cdev *__cil_tmp8 ;
4267
4268 {
4269#line 828
4270 if (fixed_cdev_used < 1) {
4271 {
4272#line 829
4273 i = fixed_cdev_used;
4274#line 830
4275 fixed_cdev_used = fixed_cdev_used + 1;
4276#line 832
4277 fixed_cdev[i].owner = (struct module *)0;
4278#line 833
4279 fixed_cdev[i].ops = misc->fops;
4280#line 835
4281 __cil_tmp5 = misc->minor;
4282#line 835
4283 __cil_tmp6 = 10 << 20;
4284#line 835
4285 __cil_tmp7 = __cil_tmp6 | __cil_tmp5;
4286#line 835
4287 dev = (unsigned int )__cil_tmp7;
4288#line 837
4289 __cil_tmp8 = & fixed_cdev[i];
4290#line 837
4291 tmp = cdev_add(__cil_tmp8, dev, 0U);
4292 }
4293#line 837
4294 return (tmp);
4295 } else {
4296#line 839
4297 return (-1);
4298 }
4299}
4300}
4301#line 97 "/ddverify-2010-04-30/models/seq1/include/linux/tty_driver.h"
4302struct tty_driver *alloc_tty_driver(int lines ) ;
4303#line 101
4304void tty_set_operations(struct tty_driver *driver , struct tty_operations const *op ) ;
4305#line 13 "/ddverify-2010-04-30/models/seq1/include/ddverify/tty.h"
4306struct ddv_tty_driver global_tty_driver ;
4307#line 845 "concatenated.c"
4308struct tty_driver *alloc_tty_driver(int lines )
4309{ void *__cil_tmp2 ;
4310
4311 {
4312#line 847
4313 if (! global_tty_driver.allocated) {
4314#line 848
4315 global_tty_driver.driver.magic = 21506;
4316#line 849
4317 global_tty_driver.driver.num = lines;
4318 } else {
4319 {
4320#line 851
4321 __cil_tmp2 = (void *)0;
4322#line 851
4323 return ((struct tty_driver *)__cil_tmp2);
4324 }
4325 }
4326#line 853
4327 return ((struct tty_driver *)0);
4328}
4329}
4330#line 855 "concatenated.c"
4331void tty_set_operations(struct tty_driver *driver , struct tty_operations const *op )
4332{ int (*__cil_tmp3)(struct tty_struct *tty , struct file *filp ) ;
4333 void (*__cil_tmp4)(struct tty_struct *tty , struct file *filp ) ;
4334 int (*__cil_tmp5)(struct tty_struct *tty , unsigned char const *buf , int count ) ;
4335 void (*__cil_tmp6)(struct tty_struct *tty , unsigned char ch ) ;
4336 void (*__cil_tmp7)(struct tty_struct *tty ) ;
4337 int (*__cil_tmp8)(struct tty_struct *tty ) ;
4338 int (*__cil_tmp9)(struct tty_struct *tty ) ;
4339 int (*__cil_tmp10)(struct tty_struct *tty , struct file *file , unsigned int cmd ,
4340 unsigned long arg ) ;
4341 void (*__cil_tmp11)(struct tty_struct *tty , struct termios *old ) ;
4342 void (*__cil_tmp12)(struct tty_struct *tty ) ;
4343 void (*__cil_tmp13)(struct tty_struct *tty ) ;
4344 void (*__cil_tmp14)(struct tty_struct *tty ) ;
4345 void (*__cil_tmp15)(struct tty_struct *tty ) ;
4346 void (*__cil_tmp16)(struct tty_struct *tty ) ;
4347 void (*__cil_tmp17)(struct tty_struct *tty , int state ) ;
4348 void (*__cil_tmp18)(struct tty_struct *tty ) ;
4349 void (*__cil_tmp19)(struct tty_struct *tty ) ;
4350 void (*__cil_tmp20)(struct tty_struct *tty , int timeout ) ;
4351 void (*__cil_tmp21)(struct tty_struct *tty , char ch ) ;
4352 int (*__cil_tmp22)(char *page , char **start , off_t off , int count , int *eof ,
4353 void *data ) ;
4354 int (*__cil_tmp23)(struct file *file , char const *buffer , unsigned long count ,
4355 void *data ) ;
4356 int (*__cil_tmp24)(struct tty_struct *tty , struct file *file ) ;
4357 int (*__cil_tmp25)(struct tty_struct *tty , struct file *file , unsigned int set ,
4358 unsigned int clear ) ;
4359
4360 {
4361#line 858
4362 __cil_tmp3 = op->open;
4363#line 858
4364 driver->open = (int (*)(struct tty_struct *tty , struct file *filp ))__cil_tmp3;
4365#line 859
4366 __cil_tmp4 = op->close;
4367#line 859
4368 driver->close = (void (*)(struct tty_struct *tty , struct file *filp ))__cil_tmp4;
4369#line 860
4370 __cil_tmp5 = op->write;
4371#line 860
4372 driver->write = (int (*)(struct tty_struct *tty , unsigned char const *buf , int count ))__cil_tmp5;
4373#line 861
4374 __cil_tmp6 = op->put_char;
4375#line 861
4376 driver->put_char = (void (*)(struct tty_struct *tty , unsigned char ch ))__cil_tmp6;
4377#line 862
4378 __cil_tmp7 = op->flush_chars;
4379#line 862
4380 driver->flush_chars = (void (*)(struct tty_struct *tty ))__cil_tmp7;
4381#line 863
4382 __cil_tmp8 = op->write_room;
4383#line 863
4384 driver->write_room = (int (*)(struct tty_struct *tty ))__cil_tmp8;
4385#line 864
4386 __cil_tmp9 = op->chars_in_buffer;
4387#line 864
4388 driver->chars_in_buffer = (int (*)(struct tty_struct *tty ))__cil_tmp9;
4389#line 865
4390 __cil_tmp10 = op->ioctl;
4391#line 865
4392 driver->ioctl = (int (*)(struct tty_struct *tty , struct file *file , unsigned int cmd ,
4393 unsigned long arg ))__cil_tmp10;
4394#line 866
4395 __cil_tmp11 = op->set_termios;
4396#line 866
4397 driver->set_termios = (void (*)(struct tty_struct *tty , struct termios *old ))__cil_tmp11;
4398#line 867
4399 __cil_tmp12 = op->throttle;
4400#line 867
4401 driver->throttle = (void (*)(struct tty_struct *tty ))__cil_tmp12;
4402#line 868
4403 __cil_tmp13 = op->unthrottle;
4404#line 868
4405 driver->unthrottle = (void (*)(struct tty_struct *tty ))__cil_tmp13;
4406#line 869
4407 __cil_tmp14 = op->stop;
4408#line 869
4409 driver->stop = (void (*)(struct tty_struct *tty ))__cil_tmp14;
4410#line 870
4411 __cil_tmp15 = op->start;
4412#line 870
4413 driver->start = (void (*)(struct tty_struct *tty ))__cil_tmp15;
4414#line 871
4415 __cil_tmp16 = op->hangup;
4416#line 871
4417 driver->hangup = (void (*)(struct tty_struct *tty ))__cil_tmp16;
4418#line 872
4419 __cil_tmp17 = op->break_ctl;
4420#line 872
4421 driver->break_ctl = (void (*)(struct tty_struct *tty , int state ))__cil_tmp17;
4422#line 873
4423 __cil_tmp18 = op->flush_buffer;
4424#line 873
4425 driver->flush_buffer = (void (*)(struct tty_struct *tty ))__cil_tmp18;
4426#line 874
4427 __cil_tmp19 = op->set_ldisc;
4428#line 874
4429 driver->set_ldisc = (void (*)(struct tty_struct *tty ))__cil_tmp19;
4430#line 875
4431 __cil_tmp20 = op->wait_until_sent;
4432#line 875
4433 driver->wait_until_sent = (void (*)(struct tty_struct *tty , int timeout ))__cil_tmp20;
4434#line 876
4435 __cil_tmp21 = op->send_xchar;
4436#line 876
4437 driver->send_xchar = (void (*)(struct tty_struct *tty , char ch ))__cil_tmp21;
4438#line 877
4439 __cil_tmp22 = op->read_proc;
4440#line 877
4441 driver->read_proc = (int (*)(char *page , char **start , off_t off , int count ,
4442 int *eof , void *data ))__cil_tmp22;
4443#line 878
4444 __cil_tmp23 = op->write_proc;
4445#line 878
4446 driver->write_proc = (int (*)(struct file *file , char const *buffer , unsigned long count ,
4447 void *data ))__cil_tmp23;
4448#line 879
4449 __cil_tmp24 = op->tiocmget;
4450#line 879
4451 driver->tiocmget = (int (*)(struct tty_struct *tty , struct file *file ))__cil_tmp24;
4452#line 880
4453 __cil_tmp25 = op->tiocmset;
4454#line 880
4455 driver->tiocmset = (int (*)(struct tty_struct *tty , struct file *file , unsigned int set ,
4456 unsigned int clear ))__cil_tmp25;
4457#line 881
4458 return;
4459}
4460}
4461#line 890 "concatenated.c"
4462__inline int alloc_chrdev_region(dev_t *dev , unsigned int baseminor , unsigned int count ,
4463 char const *name )
4464{ int major ;
4465 int return_value ;
4466 int tmp ;
4467 int tmp___0 ;
4468 unsigned int tmp___1 ;
4469 int __cil_tmp10 ;
4470 unsigned int __cil_tmp11 ;
4471
4472 {
4473 {
4474#line 893
4475 tmp = __VERIFIER_nondet_int();
4476#line 893
4477 return_value = tmp;
4478 }
4479#line 894
4480 if (return_value == 0) {
4481#line 894
4482 tmp___0 = 1;
4483 } else {
4484#line 894
4485 if (return_value == -1) {
4486#line 894
4487 tmp___0 = 1;
4488 } else {
4489#line 894
4490 tmp___0 = 0;
4491 }
4492 }
4493 {
4494#line 894
4495 __VERIFIER_assume(tmp___0);
4496 }
4497#line 896
4498 if (return_value == 0) {
4499 {
4500#line 897
4501 tmp___1 = __VERIFIER_nondet_uint();
4502#line 897
4503 major = (int )tmp___1;
4504#line 898
4505 __cil_tmp10 = major << 20;
4506#line 898
4507 __cil_tmp11 = (unsigned int )__cil_tmp10;
4508#line 898
4509 *dev = __cil_tmp11 | baseminor;
4510 }
4511 } else {
4512
4513 }
4514#line 901
4515 return (return_value);
4516}
4517}
4518#line 904 "concatenated.c"
4519__inline int register_chrdev_region(dev_t from , unsigned int count , char const *name )
4520{ int return_value ;
4521 int tmp ;
4522 int tmp___0 ;
4523
4524 {
4525 {
4526#line 906
4527 tmp = __VERIFIER_nondet_int();
4528#line 906
4529 return_value = tmp;
4530 }
4531#line 907
4532 if (return_value == 0) {
4533#line 907
4534 tmp___0 = 1;
4535 } else {
4536#line 907
4537 if (return_value == -1) {
4538#line 907
4539 tmp___0 = 1;
4540 } else {
4541#line 907
4542 tmp___0 = 0;
4543 }
4544 }
4545 {
4546#line 907
4547 __VERIFIER_assume(tmp___0);
4548 }
4549#line 909
4550 return (return_value);
4551}
4552}
4553#line 914 "concatenated.c"
4554__inline int register_chrdev(unsigned int major , char const *name , struct file_operations *fops )
4555{ struct cdev *cdev ;
4556 int err ;
4557 int tmp ;
4558 unsigned int __cil_tmp7 ;
4559 void const *__cil_tmp8 ;
4560
4561 {
4562 {
4563#line 921
4564 tmp = register_chrdev_region(0U, 256U, name);
4565#line 921
4566 major = (unsigned int )tmp;
4567#line 923
4568 cdev = cdev_alloc();
4569#line 924
4570 cdev->owner = fops->owner;
4571#line 925
4572 cdev->ops = fops;
4573#line 927
4574 __cil_tmp7 = major << 20;
4575#line 927
4576 err = cdev_add(cdev, __cil_tmp7, 256U);
4577 }
4578#line 929
4579 if (err) {
4580 {
4581#line 930
4582 __cil_tmp8 = (void const *)cdev;
4583#line 930
4584 kfree(__cil_tmp8);
4585 }
4586#line 931
4587 return (err);
4588 } else {
4589
4590 }
4591#line 934
4592 return ((int )major);
4593}
4594}
4595#line 937 "concatenated.c"
4596__inline int unregister_chrdev(unsigned int major , char const *name )
4597{
4598
4599 {
4600#line 939
4601 return (0);
4602}
4603}
4604#line 942 "concatenated.c"
4605__inline struct cdev *cdev_alloc(void)
4606{ int tmp ;
4607
4608 {
4609#line 944
4610 if (fixed_cdev_used < 1) {
4611#line 945
4612 tmp = fixed_cdev_used;
4613#line 945
4614 fixed_cdev_used = fixed_cdev_used + 1;
4615#line 945
4616 return (& fixed_cdev[tmp]);
4617 } else {
4618
4619 }
4620#line 947
4621 return ((struct cdev *)0);
4622}
4623}
4624#line 949 "concatenated.c"
4625__inline void cdev_init(struct cdev *cdev , struct file_operations *fops )
4626{
4627
4628 {
4629#line 951
4630 cdev->ops = fops;
4631#line 952
4632 return;
4633}
4634}
4635#line 954 "concatenated.c"
4636__inline int cdev_add(struct cdev *p , dev_t dev , unsigned int count )
4637{ int return_value ;
4638 int tmp ;
4639 int tmp___0 ;
4640 int __cil_tmp7 ;
4641 int __cil_tmp8 ;
4642 int __cil_tmp9 ;
4643
4644 {
4645 {
4646#line 956
4647 p->dev = dev;
4648#line 957
4649 p->count = count;
4650#line 959
4651 tmp = __VERIFIER_nondet_int();
4652#line 959
4653 return_value = tmp;
4654 }
4655#line 960
4656 if (return_value == 0) {
4657#line 960
4658 tmp___0 = 1;
4659 } else {
4660#line 960
4661 if (return_value == -1) {
4662#line 960
4663 tmp___0 = 1;
4664 } else {
4665#line 960
4666 tmp___0 = 0;
4667 }
4668 }
4669 {
4670#line 960
4671 __VERIFIER_assume(tmp___0);
4672 }
4673#line 962
4674 if (return_value == 0) {
4675 {
4676#line 963
4677 __cil_tmp7 = (int )number_cdev_registered;
4678#line 963
4679 if (__cil_tmp7 < 1) {
4680#line 965
4681 cdev_registered[number_cdev_registered].cdevp = p;
4682#line 966
4683 cdev_registered[number_cdev_registered].inode.i_rdev = dev;
4684#line 967
4685 cdev_registered[number_cdev_registered].inode.i_cdev = p;
4686#line 968
4687 cdev_registered[number_cdev_registered].open = 0;
4688#line 970
4689 __cil_tmp8 = (int )number_cdev_registered;
4690#line 970
4691 __cil_tmp9 = __cil_tmp8 + 1;
4692#line 970
4693 number_cdev_registered = (short )__cil_tmp9;
4694 } else {
4695#line 972
4696 return (-1);
4697 }
4698 }
4699 } else {
4700
4701 }
4702#line 976
4703 return (return_value);
4704}
4705}
4706#line 979 "concatenated.c"
4707__inline void cdev_del(struct cdev *p )
4708{ int i ;
4709 int __cil_tmp3 ;
4710 unsigned long __cil_tmp4 ;
4711 unsigned long __cil_tmp5 ;
4712
4713 {
4714#line 983
4715 i = 0;
4716 {
4717#line 983
4718 while (1) {
4719 while_15_continue: ;
4720 {
4721#line 983
4722 __cil_tmp3 = (int )number_cdev_registered;
4723#line 983
4724 if (i < __cil_tmp3) {
4725
4726 } else {
4727 goto while_15_break;
4728 }
4729 }
4730 {
4731#line 984
4732 __cil_tmp4 = (unsigned long )p;
4733#line 984
4734 __cil_tmp5 = (unsigned long )cdev_registered[i].cdevp;
4735#line 984
4736 if (__cil_tmp5 == __cil_tmp4) {
4737#line 985
4738 cdev_registered[i].cdevp = (struct cdev *)0;
4739#line 987
4740 return;
4741 } else {
4742
4743 }
4744 }
4745#line 983
4746 i = i + 1;
4747 }
4748 while_15_break: ;
4749 }
4750#line 990
4751 return;
4752}
4753}
4754#line 994 "concatenated.c"
4755__inline void mutex_init(struct mutex *lock )
4756{
4757
4758 {
4759#line 1000
4760 lock->locked = 0;
4761#line 1001
4762 lock->init = 1;
4763#line 1002
4764 return;
4765}
4766}
4767#line 1004 "concatenated.c"
4768__inline void mutex_lock(struct mutex *lock )
4769{
4770
4771 {
4772 {
4773#line 1007
4774 __VERIFIER_atomic_begin();
4775#line 1008
4776 assert_context_process();
4777#line 1013
4778 lock->locked = 1;
4779#line 1014
4780 __VERIFIER_atomic_end();
4781 }
4782#line 1015
4783 return;
4784}
4785}
4786#line 1017 "concatenated.c"
4787__inline void mutex_unlock(struct mutex *lock )
4788{
4789
4790 {
4791 {
4792#line 1020
4793 assert_context_process();
4794#line 1024
4795 lock->locked = 0;
4796 }
4797#line 1025
4798 return;
4799}
4800}
4801#line 1031 "concatenated.c"
4802int ddv_ioport_request_start ;
4803#line 1032 "concatenated.c"
4804int ddv_ioport_request_len ;
4805#line 1034 "concatenated.c"
4806__inline struct resource *request_region(unsigned long start , unsigned long len ,
4807 char const *name )
4808{ struct resource *resource ;
4809 void *tmp ;
4810 unsigned int __cil_tmp7 ;
4811
4812 {
4813 {
4814#line 1037
4815 __cil_tmp7 = (unsigned int )32UL;
4816#line 1037
4817 tmp = malloc(__cil_tmp7);
4818#line 1037
4819 resource = (struct resource *)tmp;
4820#line 1042
4821 ddv_ioport_request_start = (int )start;
4822#line 1043
4823 ddv_ioport_request_len = (int )len;
4824 }
4825#line 1045
4826 return (resource);
4827}
4828}
4829#line 1048 "concatenated.c"
4830__inline void release_region(unsigned long start , unsigned long len )
4831{ unsigned int i ;
4832
4833 {
4834#line 1050
4835 i = 0U;
4836#line 1056
4837 ddv_ioport_request_start = 0;
4838#line 1057
4839 ddv_ioport_request_len = 0;
4840#line 1058
4841 return;
4842}
4843}
4844#line 1060 "concatenated.c"
4845__inline unsigned char inb(unsigned int port )
4846{ unsigned char tmp ;
4847
4848 {
4849 {
4850#line 1062
4851 tmp = __VERIFIER_nondet_uchar();
4852 }
4853#line 1062
4854 return (tmp);
4855}
4856}
4857#line 1065 "concatenated.c"
4858__inline void outb(unsigned char byte , unsigned int port )
4859{
4860
4861 {
4862#line 1067
4863 return;
4864}
4865}
4866#line 1069 "concatenated.c"
4867__inline unsigned short inw(unsigned int port )
4868{ unsigned short tmp ;
4869
4870 {
4871 {
4872#line 1071
4873 tmp = __VERIFIER_nondet_ushort();
4874 }
4875#line 1071
4876 return (tmp);
4877}
4878}
4879#line 1074 "concatenated.c"
4880__inline void outw(unsigned short word , unsigned int port )
4881{
4882
4883 {
4884#line 1076
4885 return;
4886}
4887}
4888#line 1078 "concatenated.c"
4889__inline unsigned int inl(unsigned int port )
4890{ unsigned int tmp ;
4891
4892 {
4893 {
4894#line 1080
4895 tmp = __VERIFIER_nondet_unsigned();
4896 }
4897#line 1080
4898 return (tmp);
4899}
4900}
4901#line 1083 "concatenated.c"
4902__inline void outl(unsigned int doubleword , unsigned int port )
4903{
4904
4905 {
4906#line 1085
4907 return;
4908}
4909}
4910#line 1087 "concatenated.c"
4911__inline unsigned char inb_p(unsigned int port )
4912{ unsigned char tmp ;
4913
4914 {
4915 {
4916#line 1089
4917 tmp = __VERIFIER_nondet_uchar();
4918 }
4919#line 1089
4920 return (tmp);
4921}
4922}
4923#line 1092 "concatenated.c"
4924__inline void outb_p(unsigned char byte , unsigned int port )
4925{
4926
4927 {
4928#line 1094
4929 return;
4930}
4931}
4932#line 1096 "concatenated.c"
4933__inline unsigned short inw_p(unsigned int port )
4934{ unsigned short tmp ;
4935
4936 {
4937 {
4938#line 1098
4939 tmp = __VERIFIER_nondet_ushort();
4940 }
4941#line 1098
4942 return (tmp);
4943}
4944}
4945#line 1101 "concatenated.c"
4946__inline void outw_p(unsigned short word , unsigned int port )
4947{
4948
4949 {
4950#line 1103
4951 return;
4952}
4953}
4954#line 1105 "concatenated.c"
4955__inline unsigned int inl_p(unsigned int port )
4956{ unsigned int tmp ;
4957
4958 {
4959 {
4960#line 1107
4961 tmp = __VERIFIER_nondet_unsigned();
4962 }
4963#line 1107
4964 return (tmp);
4965}
4966}
4967#line 1110 "concatenated.c"
4968__inline void outl_p(unsigned int doubleword , unsigned int port )
4969{
4970
4971 {
4972#line 1112
4973 return;
4974}
4975}
4976#line 1120 "concatenated.c"
4977void schedule(void)
4978{
4979
4980 {
4981 {
4982#line 1122
4983 assert_context_process();
4984 }
4985#line 1123
4986 return;
4987}
4988}
4989#line 1125 "concatenated.c"
4990long schedule_timeout(long timeout )
4991{ long tmp ;
4992
4993 {
4994 {
4995#line 1127
4996 assert_context_process();
4997#line 1129
4998 tmp = __VERIFIER_nondet_long();
4999 }
5000#line 1129
5001 return (tmp);
5002}
5003}
5004#line 1136 "concatenated.c"
5005__inline void sema_init(struct semaphore *sem , int val )
5006{
5007
5008 {
5009#line 1138
5010 sem->init = 1;
5011#line 1139
5012 sem->locked = 0;
5013#line 1140
5014 return;
5015}
5016}
5017#line 1142 "concatenated.c"
5018__inline void init_MUTEX(struct semaphore *sem )
5019{
5020
5021 {
5022#line 1144
5023 sem->init = 1;
5024#line 1145
5025 sem->locked = 0;
5026#line 1146
5027 return;
5028}
5029}
5030#line 1148 "concatenated.c"
5031__inline void init_MUTEX_LOCKED(struct semaphore *sem )
5032{
5033
5034 {
5035#line 1150
5036 sem->init = 1;
5037#line 1151
5038 sem->locked = 1;
5039#line 1152
5040 return;
5041}
5042}
5043#line 1154 "concatenated.c"
5044__inline void down(struct semaphore *sem )
5045{
5046
5047 {
5048 {
5049#line 1157
5050 __VERIFIER_atomic_begin();
5051#line 1158
5052 assert_context_process();
5053#line 1163
5054 sem->locked = 1;
5055#line 1164
5056 __VERIFIER_atomic_end();
5057 }
5058#line 1165
5059 return;
5060}
5061}
5062#line 1167 "concatenated.c"
5063__inline int down_interruptible(struct semaphore *sem )
5064{ int tmp ;
5065
5066 {
5067 {
5068#line 1169
5069 tmp = __VERIFIER_nondet_int();
5070 }
5071#line 1169
5072 if (tmp) {
5073 {
5074#line 1171
5075 __VERIFIER_atomic_begin();
5076#line 1172
5077 assert_context_process();
5078#line 1177
5079 sem->locked = 1;
5080#line 1178
5081 __VERIFIER_atomic_end();
5082 }
5083#line 1180
5084 return (0);
5085 } else {
5086#line 1182
5087 return (-1);
5088 }
5089}
5090}
5091#line 1186 "concatenated.c"
5092__inline int down_trylock(struct semaphore *sem )
5093{ int __cil_tmp2 ;
5094
5095 {
5096 {
5097#line 1189
5098 __VERIFIER_atomic_begin();
5099#line 1190
5100 assert_context_process();
5101 }
5102 {
5103#line 1196
5104 __cil_tmp2 = sem->locked;
5105#line 1196
5106 if (__cil_tmp2 == 0) {
5107#line 1197
5108 sem->locked = 1;
5109#line 1198
5110 return (0);
5111 } else {
5112#line 1200
5113 return (1);
5114 }
5115 }
5116 {
5117#line 1203
5118 __VERIFIER_atomic_end();
5119 }
5120#line 1205
5121 return (0);
5122}
5123}
5124#line 1208 "concatenated.c"
5125__inline void up(struct semaphore *sem )
5126{
5127
5128 {
5129 {
5130#line 1211
5131 assert_context_process();
5132#line 1215
5133 sem->locked = 0;
5134 }
5135#line 1216
5136 return;
5137}
5138}
5139#line 1220 "concatenated.c"
5140__inline void tasklet_schedule(struct tasklet_struct *t )
5141{ int i ;
5142 int next_free ;
5143 void *__cil_tmp4 ;
5144 unsigned long __cil_tmp5 ;
5145 unsigned long __cil_tmp6 ;
5146 unsigned long __cil_tmp7 ;
5147 unsigned long __cil_tmp8 ;
5148 int __cil_tmp9 ;
5149
5150 {
5151#line 1223
5152 next_free = -1;
5153#line 1229
5154 i = 0;
5155 {
5156#line 1229
5157 while (1) {
5158 while_16_continue: ;
5159#line 1229
5160 if (i < 1) {
5161
5162 } else {
5163 goto while_16_break;
5164 }
5165 {
5166#line 1230
5167 __cil_tmp4 = (void *)0;
5168#line 1230
5169 __cil_tmp5 = (unsigned long )__cil_tmp4;
5170#line 1230
5171 __cil_tmp6 = (unsigned long )tasklet_registered[i].tasklet;
5172#line 1230
5173 if (__cil_tmp6 == __cil_tmp5) {
5174#line 1231
5175 next_free = i;
5176 } else {
5177
5178 }
5179 }
5180 {
5181#line 1233
5182 __cil_tmp7 = (unsigned long )t;
5183#line 1233
5184 __cil_tmp8 = (unsigned long )tasklet_registered[i].tasklet;
5185#line 1233
5186 if (__cil_tmp8 == __cil_tmp7) {
5187 {
5188#line 1233
5189 __cil_tmp9 = (int )tasklet_registered[i].is_running;
5190#line 1233
5191 if (__cil_tmp9 == 0) {
5192#line 1235
5193 return;
5194 } else {
5195
5196 }
5197 }
5198 } else {
5199
5200 }
5201 }
5202#line 1229
5203 i = i + 1;
5204 }
5205 while_16_break: ;
5206 }
5207#line 1239
5208 if (next_free == -1) {
5209
5210 } else {
5211
5212 }
5213#line 1243
5214 tasklet_registered[next_free].tasklet = t;
5215#line 1244
5216 tasklet_registered[next_free].is_running = (unsigned short)0;
5217#line 1245
5218 return;
5219}
5220}
5221#line 1247 "concatenated.c"
5222__inline void tasklet_init(struct tasklet_struct *t , void (*func)(unsigned long ) ,
5223 unsigned long data )
5224{
5225
5226 {
5227#line 1251
5228 t->count = 0;
5229#line 1252
5230 t->init = 0;
5231#line 1253
5232 t->func = func;
5233#line 1254
5234 t->data = data;
5235#line 1255
5236 return;
5237}
5238}
5239#line 1259 "concatenated.c"
5240__inline void spin_lock_init(spinlock_t *lock )
5241{
5242
5243 {
5244#line 1261
5245 lock->init = 1;
5246#line 1262
5247 lock->locked = 0;
5248#line 1263
5249 return;
5250}
5251}
5252#line 1265 "concatenated.c"
5253__inline void spin_lock(spinlock_t *lock )
5254{
5255
5256 {
5257 {
5258#line 1268
5259 __VERIFIER_atomic_begin();
5260#line 1273
5261 lock->locked = 1;
5262#line 1274
5263 __VERIFIER_atomic_end();
5264 }
5265#line 1275
5266 return;
5267}
5268}
5269#line 1277 "concatenated.c"
5270__inline void spin_lock_irqsave(spinlock_t *lock , unsigned long flags )
5271{
5272
5273 {
5274 {
5275#line 1280
5276 __VERIFIER_atomic_begin();
5277#line 1285
5278 lock->locked = 1;
5279#line 1286
5280 __VERIFIER_atomic_end();
5281 }
5282#line 1287
5283 return;
5284}
5285}
5286#line 1289 "concatenated.c"
5287__inline void spin_lock_irq(spinlock_t *lock )
5288{
5289
5290 {
5291 {
5292#line 1292
5293 __VERIFIER_atomic_begin();
5294#line 1297
5295 lock->locked = 1;
5296#line 1298
5297 __VERIFIER_atomic_end();
5298 }
5299#line 1299
5300 return;
5301}
5302}
5303#line 1301 "concatenated.c"
5304__inline void spin_lock_bh(spinlock_t *lock )
5305{
5306
5307 {
5308 {
5309#line 1304
5310 __VERIFIER_atomic_begin();
5311#line 1309
5312 lock->locked = 1;
5313#line 1310
5314 __VERIFIER_atomic_end();
5315 }
5316#line 1311
5317 return;
5318}
5319}
5320#line 1313 "concatenated.c"
5321__inline void spin_unlock(spinlock_t *lock )
5322{
5323
5324 {
5325#line 1319
5326 lock->locked = 0;
5327#line 1320
5328 return;
5329}
5330}
5331#line 1322 "concatenated.c"
5332__inline void spin_unlock_irqrestore(spinlock_t *lock , unsigned long flags )
5333{
5334
5335 {
5336#line 1328
5337 lock->locked = 0;
5338#line 1329
5339 return;
5340}
5341}
5342#line 1331 "concatenated.c"
5343__inline void spin_unlock_irq(spinlock_t *lock )
5344{
5345
5346 {
5347#line 1337
5348 lock->locked = 0;
5349#line 1338
5350 return;
5351}
5352}
5353#line 1340 "concatenated.c"
5354__inline void spin_unlock_bh(spinlock_t *lock )
5355{
5356
5357 {
5358#line 1346
5359 lock->locked = 0;
5360#line 1347
5361 return;
5362}
5363}
5364#line 1351 "concatenated.c"
5365__inline void init_timer(struct timer_list *timer )
5366{ int __cil_tmp2 ;
5367 int __cil_tmp3 ;
5368 int __cil_tmp4 ;
5369
5370 {
5371 {
5372#line 1353
5373 __cil_tmp2 = (int )number_timer_registered;
5374#line 1353
5375 if (__cil_tmp2 < 1) {
5376#line 1354
5377 timer->__ddv_active = (short)0;
5378#line 1355
5379 timer->__ddv_init = (short)1;
5380#line 1356
5381 timer_registered[number_timer_registered].timer = timer;
5382#line 1358
5383 __cil_tmp3 = (int )number_timer_registered;
5384#line 1358
5385 __cil_tmp4 = __cil_tmp3 + 1;
5386#line 1358
5387 number_timer_registered = (short )__cil_tmp4;
5388 } else {
5389
5390 }
5391 }
5392#line 1360
5393 return;
5394}
5395}
5396#line 1362 "concatenated.c"
5397__inline void add_timer(struct timer_list *timer )
5398{
5399
5400 {
5401#line 1368
5402 timer->__ddv_active = (short)1;
5403#line 1369
5404 return;
5405}
5406}
5407#line 1371 "concatenated.c"
5408__inline void add_timer_on(struct timer_list *timer , int cpu )
5409{
5410
5411 {
5412 {
5413#line 1374
5414 add_timer(timer);
5415 }
5416#line 1375
5417 return;
5418}
5419}
5420#line 1377 "concatenated.c"
5421__inline int del_timer(struct timer_list *timer )
5422{
5423
5424 {
5425#line 1379
5426 timer->__ddv_active = (short)0;
5427#line 1380
5428 return (0);
5429}
5430}
5431#line 1382 "concatenated.c"
5432__inline int mod_timer(struct timer_list *timer , unsigned long expires )
5433{
5434
5435 {
5436#line 1388
5437 timer->expires = expires;
5438#line 1389
5439 timer->__ddv_active = (short)1;
5440#line 1390
5441 return (0);
5442}
5443}
5444#line 1393 "concatenated.c"
5445__inline void init_waitqueue_head(wait_queue_head_t *q )
5446{
5447
5448 {
5449#line 1395
5450 q->init = 1;
5451#line 1396
5452 return;
5453}
5454}
5455#line 1398 "concatenated.c"
5456__inline void wake_up(wait_queue_head_t *q )
5457{
5458
5459 {
5460#line 1404
5461 return;
5462}
5463}
5464#line 1406 "concatenated.c"
5465__inline void wake_up_all(wait_queue_head_t *q )
5466{
5467
5468 {
5469#line 1412
5470 return;
5471}
5472}
5473#line 1414 "concatenated.c"
5474__inline void wake_up_interruptible(wait_queue_head_t *q )
5475{
5476
5477 {
5478#line 1420
5479 return;
5480}
5481}
5482#line 1422 "concatenated.c"
5483__inline void sleep_on(wait_queue_head_t *q )
5484{
5485
5486 {
5487#line 1428
5488 return;
5489}
5490}
5491#line 1430 "concatenated.c"
5492__inline void interruptible_sleep_on(wait_queue_head_t *q )
5493{
5494
5495 {
5496#line 1436
5497 return;
5498}
5499}
5500#line 1441 "concatenated.c"
5501__inline int schedule_work(struct work_struct *work )
5502{ int i ;
5503 unsigned long __cil_tmp3 ;
5504 unsigned long __cil_tmp4 ;
5505 void *__cil_tmp5 ;
5506 unsigned long __cil_tmp6 ;
5507 unsigned long __cil_tmp7 ;
5508
5509 {
5510#line 1450
5511 i = 0;
5512 {
5513#line 1450
5514 while (1) {
5515 while_17_continue: ;
5516#line 1450
5517 if (i < 10) {
5518
5519 } else {
5520 goto while_17_break;
5521 }
5522 {
5523#line 1451
5524 __cil_tmp3 = (unsigned long )work;
5525#line 1451
5526 __cil_tmp4 = (unsigned long )shared_workqueue[i];
5527#line 1451
5528 if (__cil_tmp4 == __cil_tmp3) {
5529#line 1452
5530 return (0);
5531 } else {
5532
5533 }
5534 }
5535 {
5536#line 1455
5537 __cil_tmp5 = (void *)0;
5538#line 1455
5539 __cil_tmp6 = (unsigned long )__cil_tmp5;
5540#line 1455
5541 __cil_tmp7 = (unsigned long )shared_workqueue[i];
5542#line 1455
5543 if (__cil_tmp7 == __cil_tmp6) {
5544#line 1456
5545 shared_workqueue[i] = work;
5546#line 1458
5547 return (1);
5548 } else {
5549
5550 }
5551 }
5552#line 1450
5553 i = i + 1;
5554 }
5555 while_17_break: ;
5556 }
5557#line 1463
5558 return (-1);
5559}
5560}
5561#line 1466 "concatenated.c"
5562__inline void call_shared_workqueue_functions(void)
5563{ unsigned short i ;
5564 unsigned short tmp ;
5565 int __cil_tmp3 ;
5566 int __cil_tmp4 ;
5567 void *__cil_tmp5 ;
5568 unsigned long __cil_tmp6 ;
5569 unsigned long __cil_tmp7 ;
5570 void (*__cil_tmp8)(void * ) ;
5571 void *__cil_tmp9 ;
5572 void *__cil_tmp10 ;
5573
5574 {
5575 {
5576#line 1468
5577 tmp = __VERIFIER_nondet_ushort();
5578#line 1468
5579 i = tmp;
5580#line 1469
5581 __cil_tmp3 = (int )i;
5582#line 1469
5583 __cil_tmp4 = __cil_tmp3 < 10;
5584#line 1469
5585 __VERIFIER_assume(__cil_tmp4);
5586 }
5587 {
5588#line 1471
5589 __cil_tmp5 = (void *)0;
5590#line 1471
5591 __cil_tmp6 = (unsigned long )__cil_tmp5;
5592#line 1471
5593 __cil_tmp7 = (unsigned long )shared_workqueue[i];
5594#line 1471
5595 if (__cil_tmp7 != __cil_tmp6) {
5596 {
5597#line 1472
5598 __cil_tmp8 = (shared_workqueue[i])->func;
5599#line 1472
5600 __cil_tmp9 = (shared_workqueue[i])->data;
5601#line 1472
5602 (*__cil_tmp8)(__cil_tmp9);
5603#line 1473
5604 __cil_tmp10 = (void *)0;
5605#line 1473
5606 shared_workqueue[i] = (struct work_struct *)__cil_tmp10;
5607 }
5608 } else {
5609
5610 }
5611 }
5612#line 1475
5613 return;
5614}
5615}
5616#line 1479 "concatenated.c"
5617int request_irq(unsigned int irq , irqreturn_t (*handler)(int , void * , struct pt_regs * ) ,
5618 unsigned long irqflags , char const *devname , void *dev_id )
5619{ int tmp ;
5620
5621 {
5622 {
5623#line 1482
5624 tmp = __VERIFIER_nondet_int();
5625 }
5626#line 1482
5627 if (tmp) {
5628#line 1483
5629 registered_irq[irq].handler = handler;
5630#line 1484
5631 registered_irq[irq].dev_id = dev_id;
5632#line 1486
5633 return (0);
5634 } else {
5635#line 1488
5636 return (-1);
5637 }
5638}
5639}
5640#line 1492 "concatenated.c"
5641void free_irq(unsigned int irq , void *dev_id )
5642{ void *__cil_tmp3 ;
5643
5644 {
5645#line 1494
5646 __cil_tmp3 = (void *)0;
5647#line 1494
5648 registered_irq[irq].handler = (irqreturn_t (*)(int , void * , struct pt_regs * ))__cil_tmp3;
5649#line 1495
5650 registered_irq[irq].dev_id = (void *)0;
5651#line 1496
5652 return;
5653}
5654}
5655#line 1501 "concatenated.c"
5656__inline unsigned long __get_free_pages(gfp_t gfp_mask , unsigned int order )
5657{
5658
5659 {
5660#line 1504
5661 if (gfp_mask & 16U) {
5662 {
5663#line 1505
5664 assert_context_process();
5665 }
5666 } else {
5667
5668 }
5669#line 1507
5670 return (0UL);
5671}
5672}
5673#line 1509 "concatenated.c"
5674__inline unsigned long __get_free_page(gfp_t gfp_mask )
5675{
5676
5677 {
5678#line 1512
5679 if (gfp_mask & 16U) {
5680 {
5681#line 1513
5682 assert_context_process();
5683 }
5684 } else {
5685
5686 }
5687#line 1515
5688 return (0UL);
5689}
5690}
5691#line 1517 "concatenated.c"
5692__inline unsigned long get_zeroed_page(gfp_t gfp_mask )
5693{
5694
5695 {
5696#line 1520
5697 if (gfp_mask & 16U) {
5698 {
5699#line 1521
5700 assert_context_process();
5701 }
5702 } else {
5703
5704 }
5705#line 1523
5706 return (0UL);
5707}
5708}
5709#line 1534 "concatenated.c"
5710__inline struct page *alloc_pages(gfp_t gfp_mask , unsigned int order )
5711{
5712
5713 {
5714#line 1537
5715 if (gfp_mask & 16U) {
5716 {
5717#line 1538
5718 assert_context_process();
5719 }
5720 } else {
5721
5722 }
5723#line 1540
5724 return ((struct page *)0);
5725}
5726}
5727#line 1542 "concatenated.c"
5728__inline struct page *alloc_page(gfp_t gfp_mask )
5729{
5730
5731 {
5732#line 1545
5733 if (gfp_mask & 16U) {
5734 {
5735#line 1546
5736 assert_context_process();
5737 }
5738 } else {
5739
5740 }
5741#line 1548
5742 return ((struct page *)0);
5743}
5744}
5745#line 1554 "concatenated.c"
5746void *kmalloc(size_t size , gfp_t flags )
5747{ void *tmp ;
5748
5749 {
5750#line 1556
5751 if (flags & 16U) {
5752 {
5753#line 1557
5754 assert_context_process();
5755 }
5756 } else {
5757
5758 }
5759 {
5760#line 1560
5761 tmp = malloc(size);
5762 }
5763#line 1560
5764 return (tmp);
5765}
5766}
5767#line 1563 "concatenated.c"
5768void *kzalloc(size_t size , gfp_t flags )
5769{ void *tmp ;
5770
5771 {
5772#line 1565
5773 if (flags & 16U) {
5774 {
5775#line 1566
5776 assert_context_process();
5777 }
5778 } else {
5779
5780 }
5781 {
5782#line 1569
5783 tmp = malloc(size);
5784 }
5785#line 1569
5786 return (tmp);
5787}
5788}
5789#line 6 "/ddverify-2010-04-30/models/seq1/include/linux/vmalloc.h"
5790void *vmalloc(unsigned long size ) ;
5791#line 1606 "concatenated.c"
5792void *vmalloc(unsigned long size )
5793{ void *tmp ;
5794 unsigned int __cil_tmp3 ;
5795
5796 {
5797 {
5798#line 1608
5799 __cil_tmp3 = (unsigned int )size;
5800#line 1608
5801 tmp = malloc(__cil_tmp3);
5802 }
5803#line 1608
5804 return (tmp);
5805}
5806}
5807#line 1610 "concatenated.c"
5808int printk(char const *fmt , ...)
5809{
5810
5811 {
5812#line 1612
5813 return (0);
5814}
5815}
5816#line 1615 "concatenated.c"
5817unsigned short __VERIFIER_nondet_ushort(void)
5818{ unsigned short us ;
5819
5820 {
5821#line 1615
5822 return (us);
5823}
5824}
5825#line 1616 "concatenated.c"
5826unsigned long __VERIFIER_nondet_ulong(void)
5827{ unsigned long ul ;
5828
5829 {
5830#line 1616
5831 return (ul);
5832}
5833}
5834#line 1617 "concatenated.c"
5835short __VERIFIER_nondet_short(void)
5836{ short s ;
5837
5838 {
5839#line 1617
5840 return (s);
5841}
5842}
5843#line 1618 "concatenated.c"
5844int __VERIFIER_nondet_int(void)
5845{ int i ;
5846
5847 {
5848#line 1618
5849 return (i);
5850}
5851}
5852#line 1619 "concatenated.c"
5853char __VERIFIER_nondet_char(void)
5854{ char c ;
5855
5856 {
5857#line 1619
5858 return (c);
5859}
5860}
5861#line 1620 "concatenated.c"
5862size_t __VERIFIER_nondet_size_t(void)
5863{ size_t s ;
5864
5865 {
5866#line 1620
5867 return (s);
5868}
5869}
5870#line 1621 "concatenated.c"
5871unsigned int __VERIFIER_nondet_uint(void)
5872{ unsigned int ui ;
5873
5874 {
5875#line 1621
5876 return (ui);
5877}
5878}
5879#line 1622 "concatenated.c"
5880unsigned char __VERIFIER_nondet_uchar(void)
5881{ unsigned char uc ;
5882
5883 {
5884#line 1622
5885 return (uc);
5886}
5887}
5888#line 1623 "concatenated.c"
5889unsigned int __VERIFIER_nondet_unsigned(void)
5890{ unsigned int u ;
5891
5892 {
5893#line 1623
5894 return (u);
5895}
5896}
5897#line 1624 "concatenated.c"
5898long __VERIFIER_nondet_long(void)
5899{ long l ;
5900
5901 {
5902#line 1624
5903 return (l);
5904}
5905}
5906#line 1625 "concatenated.c"
5907char *__VERIFIER_nondet_pchar(void)
5908{ char *pc ;
5909
5910 {
5911#line 1625
5912 return (pc);
5913}
5914}
5915#line 1626 "concatenated.c"
5916loff_t __VERIFIER_nondet_loff_t(void)
5917{ loff_t l ;
5918
5919 {
5920#line 1626
5921 return (l);
5922}
5923}
5924#line 1627 "concatenated.c"
5925sector_t __VERIFIER_nondet_sector_t(void)
5926{ sector_t s ;
5927
5928 {
5929#line 1627
5930 return (s);
5931}
5932}
5933#line 1628 "concatenated.c"
5934loff_t no_llseek(struct file *file , loff_t offset , int origin )
5935{ loff_t l ;
5936
5937 {
5938#line 1628
5939 return (l);
5940}
5941}
5942#line 1633 "concatenated.c"
5943void __VERIFIER_assume(int phi )
5944{
5945
5946 {
5947 {
5948#line 1633
5949 while (1) {
5950 while_18_continue: ;
5951#line 1633
5952 if (! phi) {
5953
5954 } else {
5955 goto while_18_break;
5956 }
5957 }
5958 while_18_break: ;
5959 }
5960#line 1633
5961 return;
5962}
5963}
5964#line 1634 "concatenated.c"
5965void __VERIFIER_assert(int phi , char *txt )
5966{
5967
5968 {
5969#line 1634
5970 if (! phi) {
5971 ERROR:
5972 goto ERROR;
5973 } else {
5974
5975 }
5976#line 1634
5977 return;
5978}
5979}
5980#line 1636 "concatenated.c"
5981int nonseekable_open(struct inode *inode , struct file *filp )
5982{ int i ;
5983
5984 {
5985#line 1636
5986 return (i);
5987}
5988}
5989#line 1637 "concatenated.c"
5990void __module_get(struct module *module )
5991{
5992
5993 {
5994#line 1637
5995 return;
5996}
5997}
5998#line 1638 "concatenated.c"
5999int test_and_set_bit(int nr , unsigned long *addr )
6000{ unsigned int bit ;
6001 unsigned long old ;
6002 int __cil_tmp5 ;
6003 int __cil_tmp6 ;
6004 int __cil_tmp7 ;
6005 unsigned long __cil_tmp8 ;
6006 unsigned long __cil_tmp9 ;
6007 unsigned long __cil_tmp10 ;
6008
6009 {
6010#line 1640
6011 __cil_tmp5 = nr & 31;
6012#line 1640
6013 __cil_tmp6 = 1 << __cil_tmp5;
6014#line 1640
6015 bit = (unsigned int )__cil_tmp6;
6016#line 1641
6017 __cil_tmp7 = nr >> 5;
6018#line 1641
6019 addr = addr + __cil_tmp7;
6020#line 1642
6021 old = *addr;
6022#line 1643
6023 __cil_tmp8 = (unsigned long )bit;
6024#line 1643
6025 *addr = old | __cil_tmp8;
6026 {
6027#line 1644
6028 __cil_tmp9 = (unsigned long )bit;
6029#line 1644
6030 __cil_tmp10 = old & __cil_tmp9;
6031#line 1644
6032 return (__cil_tmp10 != 0UL);
6033 }
6034}
6035}
6036#line 1647 "concatenated.c"
6037void clear_bit(int nr , unsigned long volatile *addr )
6038{ unsigned int bit ;
6039 unsigned long old ;
6040 int __cil_tmp5 ;
6041 int __cil_tmp6 ;
6042 int __cil_tmp7 ;
6043 unsigned long volatile __cil_tmp8 ;
6044 unsigned int __cil_tmp9 ;
6045 unsigned long __cil_tmp10 ;
6046 unsigned long __cil_tmp11 ;
6047
6048 {
6049#line 1649
6050 __cil_tmp5 = nr & 31;
6051#line 1649
6052 __cil_tmp6 = 1 << __cil_tmp5;
6053#line 1649
6054 bit = (unsigned int )__cil_tmp6;
6055#line 1650
6056 __cil_tmp7 = nr >> 5;
6057#line 1650
6058 addr = addr + __cil_tmp7;
6059#line 1651
6060 __cil_tmp8 = *addr;
6061#line 1651
6062 old = (unsigned long )__cil_tmp8;
6063#line 1652
6064 __cil_tmp9 = ~ bit;
6065#line 1652
6066 __cil_tmp10 = (unsigned long )__cil_tmp9;
6067#line 1652
6068 __cil_tmp11 = old & __cil_tmp10;
6069#line 1652
6070 *addr = (unsigned long volatile )__cil_tmp11;
6071#line 1653
6072 return;
6073}
6074}
6075#line 1655 "concatenated.c"
6076int register_reboot_notifier(struct notifier_block *dummy )
6077{ int i ;
6078
6079 {
6080#line 1655
6081 return (i);
6082}
6083}
6084#line 1656 "concatenated.c"
6085int misc_deregister(struct miscdevice *misc )
6086{ int i ;
6087
6088 {
6089#line 1656
6090 return (i);
6091}
6092}
6093#line 1657 "concatenated.c"
6094int unregister_reboot_notifier(struct notifier_block *dummy )
6095{ int i ;
6096
6097 {
6098#line 1657
6099 return (i);
6100}
6101}
6102#line 1658 "concatenated.c"
6103void release_mem_region(unsigned long start , unsigned long len )
6104{
6105
6106 {
6107#line 1658
6108 return;
6109}
6110}
6111#line 1659 "concatenated.c"
6112void kfree(void const *addr )
6113{
6114
6115 {
6116#line 1659
6117 return;
6118}
6119}
6120#line 1661 "concatenated.c"
6121struct resource *request_mem_region(unsigned long start , unsigned long len , char const *name )
6122{ void *tmp ;
6123 unsigned int __cil_tmp5 ;
6124
6125 {
6126 {
6127#line 1663
6128 __cil_tmp5 = (unsigned int )32UL;
6129#line 1663
6130 tmp = malloc(__cil_tmp5);
6131 }
6132#line 1663
6133 return ((struct resource *)tmp);
6134}
6135}
6136#line 1666 "concatenated.c"
6137void __VERIFIER_atomic_begin(void)
6138{
6139
6140 {
6141#line 1666
6142 return;
6143}
6144}
6145#line 1667 "concatenated.c"
6146void __VERIFIER_atomic_end(void)
6147{
6148
6149 {
6150#line 1667
6151 return;
6152}
6153}