1
2 /*
3 ***************************************************************************
4 *
5 * radio-gemtek-pci.c - Gemtek PCI Radio driver
6 * (C) 2001 Vladimir Shebordaev <vshebordaev@mail.ru>
7 *
8 ***************************************************************************
9 *
10 * This program is free software; you can redistribute it and/or
11 * modify it under the terms of the GNU General Public License as
12 * published by the Free Software Foundation; either version 2 of
13 * the License, or (at your option) any later version.
14 *
15 * This program is distributed in the hope that it will be useful,
16 * but WITHOUT ANY WARRANTY; without even the implied warranty of
17 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
18 * GNU General Public License for more details.
19 *
20 * You should have received a copy of the GNU General Public
21 * License along with this program; if not, write to the Free
22 * Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139,
23 * USA.
24 *
25 ***************************************************************************
26 *
27 * Gemtek Corp still silently refuses to release any specifications
28 * of their multimedia devices, so the protocol still has to be
29 * reverse engineered.
30 *
31 * The v4l code was inspired by Jonas Munsin's Gemtek serial line
32 * radio device driver.
33 *
34 * Please, let me know if this piece of code was useful :)
35 *
36 * TODO: multiple device support and portability were not tested
37 *
38 * Converted to V4L2 API by Mauro Carvalho Chehab <mchehab@infradead.org>
39 *
40 ***************************************************************************
41 */
42
43 #include <linux/types.h>
44 #include <linux/list.h>
45 #include <linux/module.h>
46 #include <linux/init.h>
47 #include <linux/pci.h>
48 #include <linux/videodev2.h>
49 #include <linux/errno.h>
50 #include <linux/version.h>
/* for KERNEL_VERSION MACRO */
51 #include <linux/io.h>
52 #include <media/v4l2-device.h>
53 #include <media/v4l2-ioctl.h>
54
55 MODULE_AUTHOR(
"Vladimir Shebordaev <vshebordaev@mail.ru>");
56 MODULE_DESCRIPTION(
"The video4linux driver for the Gemtek PCI Radio Card");
57 MODULE_LICENSE(
"GPL");
58
59 static int nr_radio = -
1;
60 static int mx =
1;
61
62 module_param(mx,
bool,
0);
63 MODULE_PARM_DESC(mx,
"single digit: 1 - turn off the turner upon module exit (default), 0 - do not");
64 module_param(nr_radio,
int,
0);
65 MODULE_PARM_DESC(nr_radio,
"video4linux device number to use");
66
67 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
68
69 #ifndef PCI_VENDOR_ID_GEMTEK
70 #define PCI_VENDOR_ID_GEMTEK 0x5046
71 #endif
72
73 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
74 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
75 #endif
76
77 #ifndef GEMTEK_PCI_RANGE_LOW
78 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
79 #endif
80
81 #ifndef GEMTEK_PCI_RANGE_HIGH
82 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
83 #endif
84
85 struct gemtek_pci {
86 struct v4l2_device v4l2_dev;
87 struct video_device vdev;
88 struct mutex lock;
89 struct pci_dev *pdev;
90
91 u32 iobase;
92 u32 length;
93
94 u32 current_frequency;
95 u8 mute;
96 };
97
98 static inline struct gemtek_pci *to_gemtek_pci(
struct v4l2_device *v4l2_dev)
99 {
100 return container_of(v4l2_dev,
struct gemtek_pci, v4l2_dev);
101 }
102
103 static inline u8 gemtek_pci_out(u16 value, u32 port)
104 {
105 outw(value, port);
106
107 return (u8)value;
108 }
109
110 #define _b0(v) (*((u8 *)&v))
111
112 static void __gemtek_pci_cmd(u16 value, u32 port, u8 *last_byte,
int keep)
113 {
114 u8 byte = *last_byte;
115
116 if (!value) {
117 if (!keep)
118 value = (u16)port;
119 byte &= 0xfd;
120 }
else
121 byte |=
2;
122
123 _b0(value) = byte;
124 outw(value, port);
125 byte |=
1;
126 _b0(value) = byte;
127 outw(value, port);
128 byte &= 0xfe;
129 _b0(value) = byte;
130 outw(value, port);
131
132 *last_byte = byte;
133 }
134
135 static inline void gemtek_pci_nil(u32 port, u8 *last_byte)
136 {
137 __gemtek_pci_cmd(0x00, port, last_byte, false);
138 }
139
140 static inline void gemtek_pci_cmd(u16 cmd, u32 port, u8 *last_byte)
141 {
142 __gemtek_pci_cmd(cmd, port, last_byte, true);
143 }
144
145 static void gemtek_pci_setfrequency(
struct gemtek_pci *card,
unsigned long frequency)
146 {
147 int i;
148 u32 value = frequency /
200 +
856;
149 u16 mask = 0x8000;
150 u8 last_byte;
151 u32 port = card->iobase;
152
153 mutex_lock(&card->lock);
154 card->current_frequency = frequency;
155 last_byte = gemtek_pci_out(0x06, port);
156
157 i =
0;
158 do {
159 gemtek_pci_nil(port, &last_byte);
160 i++;
161 }
while (i <
9);
162
163 i =
0;
164 do {
165 gemtek_pci_cmd(value & mask, port, &last_byte);
166 mask >>=
1;
167 i++;
168 }
while (i <
16);
169
170 outw(0x10, port);
171 mutex_unlock(&card->lock);
172 }
173
174
175 static void gemtek_pci_mute(
struct gemtek_pci *card)
176 {
177 mutex_lock(&card->lock);
178 outb(0x1f, card->iobase);
179 card->mute = true;
180 mutex_unlock(&card->lock);
181 }
182
183 static void gemtek_pci_unmute(
struct gemtek_pci *card)
184 {
185 mutex_lock(&card->lock);
186 if (card->mute) {
187 gemtek_pci_setfrequency(card, card->current_frequency);
188 card->mute = false;
189 }
190 mutex_unlock(&card->lock);
191 }
192
193 static int gemtek_pci_getsignal(
struct gemtek_pci *card)
194 {
195 int sig;
196
197 mutex_lock(&card->lock);
198 sig = (inb(card->iobase) & 0x08) ?
0 :
1;
199 mutex_unlock(&card->lock);
200 return sig;
201 }
202
203 static int vidioc_querycap(
struct file *file,
void *priv,
204 struct v4l2_capability *v)
205 {
206 struct gemtek_pci *card = video_drvdata(file);
207
208 strlcpy(v->driver,
"radio-gemtek-pci",
sizeof(v->driver));
209 strlcpy(v->card,
"GemTek PCI Radio",
sizeof(v->card));
210 snprintf(v->bus_info,
sizeof(v->bus_info),
"PCI:%s", pci_name(card->pdev));
211 v->version = RADIO_VERSION;
212 v->capabilities = V4L2_CAP_TUNER | V4L2_CAP_RADIO;
213 return 0;
214 }
215
216 static int vidioc_g_tuner(
struct file *file,
void *priv,
217 struct v4l2_tuner *v)
218 {
219 struct gemtek_pci *card = video_drvdata(file);
220
221 if (v->index >
0)
222 return -EINVAL;
223
224 strlcpy(v->name,
"FM",
sizeof(v->name));
225 v->type = V4L2_TUNER_RADIO;
226 v->rangelow = GEMTEK_PCI_RANGE_LOW;
227 v->rangehigh = GEMTEK_PCI_RANGE_HIGH;
228 v->rxsubchans = V4L2_TUNER_SUB_MONO;
229 v->capability = V4L2_TUNER_CAP_LOW;
230 v->audmode = V4L2_TUNER_MODE_MONO;
231 v->signal = 0xffff * gemtek_pci_getsignal(card);
232 return 0;
233 }
234
235 static int vidioc_s_tuner(
struct file *file,
void *priv,
236 struct v4l2_tuner *v)
237 {
238 return v->index ? -EINVAL :
0;
239 }
240
241 static int vidioc_s_frequency(
struct file *file,
void *priv,
242 struct v4l2_frequency *f)
243 {
244 struct gemtek_pci *card = video_drvdata(file);
245
246 if (f->frequency < GEMTEK_PCI_RANGE_LOW ||
247 f->frequency > GEMTEK_PCI_RANGE_HIGH)
248 return -EINVAL;
249 gemtek_pci_setfrequency(card, f->frequency);
250 card->mute = false;
251 return 0;
252 }
253
254 static int vidioc_g_frequency(
struct file *file,
void *priv,
255 struct v4l2_frequency *f)
256 {
257 struct gemtek_pci *card = video_drvdata(file);
258
259 f->type = V4L2_TUNER_RADIO;
260 f->frequency = card->current_frequency;
261 return 0;
262 }
263
264 static int vidioc_queryctrl(
struct file *file,
void *priv,
265 struct v4l2_queryctrl *qc)
266 {
267 switch (qc->id) {
268 case V4L2_CID_AUDIO_MUTE:
269 return v4l2_ctrl_query_fill(qc,
0,
1,
1,
1);
270 case V4L2_CID_AUDIO_VOLUME:
271 return v4l2_ctrl_query_fill(qc,
0,
65535,
65535,
65535);
272 }
273 return -EINVAL;
274 }
275
276 static int vidioc_g_ctrl(
struct file *file,
void *priv,
277 struct v4l2_control *ctrl)
278 {
279 struct gemtek_pci *card = video_drvdata(file);
280
281 switch (ctrl->id) {
282 case V4L2_CID_AUDIO_MUTE:
283 ctrl->value = card->mute;
284 return 0;
285 case V4L2_CID_AUDIO_VOLUME:
286 if (card->mute)
287 ctrl->value =
0;
288 else
289 ctrl->value =
65535;
290 return 0;
291 }
292 return -EINVAL;
293 }
294
295 static int vidioc_s_ctrl(
struct file *file,
void *priv,
296 struct v4l2_control *ctrl)
297 {
298 struct gemtek_pci *card = video_drvdata(file);
299
300 switch (ctrl->id) {
301 case V4L2_CID_AUDIO_MUTE:
302 if (ctrl->value)
303 gemtek_pci_mute(card);
304 else
305 gemtek_pci_unmute(card);
306 return 0;
307 case V4L2_CID_AUDIO_VOLUME:
308 if (ctrl->value)
309 gemtek_pci_unmute(card);
310 else
311 gemtek_pci_mute(card);
312 return 0;
313 }
314 return -EINVAL;
315 }
316
317 static int vidioc_g_input(
struct file *filp,
void *priv,
unsigned int *i)
318 {
319 *i =
0;
320 return 0;
321 }
322
323 static int vidioc_s_input(
struct file *filp,
void *priv,
unsigned int i)
324 {
325 return i ? -EINVAL :
0;
326 }
327
328 static int vidioc_g_audio(
struct file *file,
void *priv,
329 struct v4l2_audio *a)
330 {
331 a->index =
0;
332 strlcpy(a->name,
"Radio",
sizeof(a->name));
333 a->capability = V4L2_AUDCAP_STEREO;
334 return 0;
335 }
336
337 static int vidioc_s_audio(
struct file *file,
void *priv,
338 struct v4l2_audio *a)
339 {
340 return a->index ? -EINVAL :
0;
341 }
342
343 enum {
344 GEMTEK_PR103
345 };
346
347 static char *card_names[] __devinitdata = {
348 "GEMTEK_PR103"
349 };
350
351 static struct pci_device_id gemtek_pci_id[] =
352 {
353 { PCI_VENDOR_ID_GEMTEK, PCI_DEVICE_ID_GEMTEK_PR103,
354 PCI_ANY_ID, PCI_ANY_ID,
0,
0, GEMTEK_PR103 },
355 {
0 }
356 };
357
358 MODULE_DEVICE_TABLE(pci, gemtek_pci_id);
359
360 static const struct v4l2_file_operations gemtek_pci_fops = {
361 .owner = THIS_MODULE,
362 .ioctl = video_ioctl2,
363 };
364
365 static const struct v4l2_ioctl_ops gemtek_pci_ioctl_ops = {
366 .vidioc_querycap = vidioc_querycap,
367 .vidioc_g_tuner = vidioc_g_tuner,
368 .vidioc_s_tuner = vidioc_s_tuner,
369 .vidioc_g_audio = vidioc_g_audio,
370 .vidioc_s_audio = vidioc_s_audio,
371 .vidioc_g_input = vidioc_g_input,
372 .vidioc_s_input = vidioc_s_input,
373 .vidioc_g_frequency = vidioc_g_frequency,
374 .vidioc_s_frequency = vidioc_s_frequency,
375 .vidioc_queryctrl = vidioc_queryctrl,
376 .vidioc_g_ctrl = vidioc_g_ctrl,
377 .vidioc_s_ctrl = vidioc_s_ctrl,
378 };
379
380 static int __devinit gemtek_pci_probe(
struct pci_dev *pdev,
const struct pci_device_id *pci_id)
381 {
382 struct gemtek_pci *card;
383 struct v4l2_device *v4l2_dev;
384 int res;
385
386 card = kzalloc(
sizeof(
struct gemtek_pci), GFP_KERNEL);
387 if (card == NULL) {
388 dev_err(&pdev->dev,
"out of memory\n");
389 return -ENOMEM;
390 }
391
392 v4l2_dev = &card->v4l2_dev;
393 mutex_init(&card->lock);
394 card->pdev = pdev;
395
396 strlcpy(v4l2_dev->name,
"gemtek_pci",
sizeof(v4l2_dev->name));
397
398 res = v4l2_device_register(&pdev->dev, v4l2_dev);
399 if (res <
0) {
400 v4l2_err(v4l2_dev,
"Could not register v4l2_device\n");
401 kfree(card);
402 return res;
403 }
404
405 if (pci_enable_device(pdev))
406 goto err_pci;
407
408 card->iobase = pci_resource_start(pdev,
0);
409 card->length = pci_resource_len(pdev,
0);
410
411 if (request_region(card->iobase, card->length, card_names[pci_id->driver_data]) == NULL) {
412 v4l2_err(v4l2_dev,
"i/o port already in use\n");
413 goto err_pci;
414 }
415
416 strlcpy(card->vdev.name, v4l2_dev->name,
sizeof(card->vdev.name));
417 card->vdev.v4l2_dev = v4l2_dev;
418 card->vdev.fops = &gemtek_pci_fops;
419 card->vdev.ioctl_ops = &gemtek_pci_ioctl_ops;
420 card->vdev.release = video_device_release_empty;
421 video_set_drvdata(&card->vdev, card);
422
423 if (video_register_device(&card->vdev, VFL_TYPE_RADIO, nr_radio) <
0)
424 goto err_video;
425
426 gemtek_pci_mute(card);
427
428 v4l2_info(v4l2_dev,
"Gemtek PCI Radio (rev. %d) found at 0x%04x-0x%04x.\n",
429 pdev->revision, card->iobase, card->iobase + card->length -
1);
430
431 return 0;
432
433 err_video:
434 release_region(card->iobase, card->length);
435
436 err_pci:
437 v4l2_device_unregister(v4l2_dev);
438 kfree(card);
439 return -ENODEV;
440 }
441
442 static void __devexit gemtek_pci_remove(
struct pci_dev *pdev)
443 {
444 struct v4l2_device *v4l2_dev = dev_get_drvdata(&pdev->dev);
445 struct gemtek_pci *card = to_gemtek_pci(v4l2_dev);
446
447 video_unregister_device(&card->vdev);
448 v4l2_device_unregister(v4l2_dev);
449
450 release_region(card->iobase, card->length);
451
452 if (mx)
453 gemtek_pci_mute(card);
454
455 kfree(card);
456 }
457
458 static struct pci_driver gemtek_pci_driver = {
459 .name =
"gemtek_pci",
460 .id_table = gemtek_pci_id,
461 .probe = gemtek_pci_probe,
462 .remove = __devexit_p(gemtek_pci_remove),
463 };
464
465 static int __init gemtek_pci_init(
void)
466 {
467 return pci_register_driver(&gemtek_pci_driver);
468 }
469
470 static void __exit gemtek_pci_exit(
void)
471 {
472 pci_unregister_driver(&gemtek_pci_driver);
473 }
474
475 module_init(gemtek_pci_init);
476 module_exit(gemtek_pci_exit);
477
478
479
480
481
482 /* LDV_COMMENT_BEGIN_MAIN */
483 #ifdef LDV_MAIN0_sequence_infinite_withcheck_stateful
484
485 /*###########################################################################*/
486
487 /*############## Driver Environment Generator 0.2 output ####################*/
488
489 /*###########################################################################*/
490
491
492
493 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test if all kernel resources are correctly released by driver before driver will be unloaded. */
494 void ldv_check_final_state(
void);
495
496 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Test correct return result. */
497 void ldv_check_return_value(
int res);
498
499 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Initializes the model. */
500 void ldv_initialize(
void);
501
502 /* LDV_COMMENT_FUNCTION_DECLARE_LDV Special function for LDV verifier. Returns arbitrary interger value. */
503 int nondet_int(
void);
504
505 /* LDV_COMMENT_VAR_DECLARE_LDV Special variable for LDV verifier. */
506 int LDV_IN_INTERRUPT;
507
508 /* LDV_COMMENT_FUNCTION_MAIN Main function for LDV verifier. */
509 void ldv_main0_sequence_infinite_withcheck_stateful(
void) {
510
511
512
513 /* LDV_COMMENT_BEGIN_VARIABLE_DECLARATION_PART */
514 /*============================= VARIABLE DECLARATION PART =============================*/
515 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
516 /* content: static int vidioc_querycap(struct file *file, void *priv, struct v4l2_capability *v)*/
517 /* LDV_COMMENT_BEGIN_PREP */
518 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
519 #ifndef PCI_VENDOR_ID_GEMTEK
520 #define PCI_VENDOR_ID_GEMTEK 0x5046
521 #endif
522 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
523 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
524 #endif
525 #ifndef GEMTEK_PCI_RANGE_LOW
526 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
527 #endif
528 #ifndef GEMTEK_PCI_RANGE_HIGH
529 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
530 #endif
531 #define _b0(v) (*((u8 *)&v))
532 /* LDV_COMMENT_END_PREP */
533 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_querycap" */
534 struct file * var_group1;
535 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_querycap" */
536 void * var_vidioc_querycap_9_p1;
537 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_querycap" */
538 struct v4l2_capability * var_vidioc_querycap_9_p2;
539 /* content: static int vidioc_g_tuner(struct file *file, void *priv, struct v4l2_tuner *v)*/
540 /* LDV_COMMENT_BEGIN_PREP */
541 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
542 #ifndef PCI_VENDOR_ID_GEMTEK
543 #define PCI_VENDOR_ID_GEMTEK 0x5046
544 #endif
545 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
546 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
547 #endif
548 #ifndef GEMTEK_PCI_RANGE_LOW
549 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
550 #endif
551 #ifndef GEMTEK_PCI_RANGE_HIGH
552 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
553 #endif
554 #define _b0(v) (*((u8 *)&v))
555 /* LDV_COMMENT_END_PREP */
556 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_tuner" */
557 void * var_vidioc_g_tuner_10_p1;
558 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_tuner" */
559 struct v4l2_tuner * var_vidioc_g_tuner_10_p2;
560 /* content: static int vidioc_s_tuner(struct file *file, void *priv, struct v4l2_tuner *v)*/
561 /* LDV_COMMENT_BEGIN_PREP */
562 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
563 #ifndef PCI_VENDOR_ID_GEMTEK
564 #define PCI_VENDOR_ID_GEMTEK 0x5046
565 #endif
566 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
567 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
568 #endif
569 #ifndef GEMTEK_PCI_RANGE_LOW
570 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
571 #endif
572 #ifndef GEMTEK_PCI_RANGE_HIGH
573 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
574 #endif
575 #define _b0(v) (*((u8 *)&v))
576 /* LDV_COMMENT_END_PREP */
577 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_tuner" */
578 void * var_vidioc_s_tuner_11_p1;
579 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_tuner" */
580 struct v4l2_tuner * var_vidioc_s_tuner_11_p2;
581 /* content: static int vidioc_g_audio(struct file *file, void *priv, struct v4l2_audio *a)*/
582 /* LDV_COMMENT_BEGIN_PREP */
583 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
584 #ifndef PCI_VENDOR_ID_GEMTEK
585 #define PCI_VENDOR_ID_GEMTEK 0x5046
586 #endif
587 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
588 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
589 #endif
590 #ifndef GEMTEK_PCI_RANGE_LOW
591 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
592 #endif
593 #ifndef GEMTEK_PCI_RANGE_HIGH
594 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
595 #endif
596 #define _b0(v) (*((u8 *)&v))
597 /* LDV_COMMENT_END_PREP */
598 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_audio" */
599 void * var_vidioc_g_audio_19_p1;
600 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_audio" */
601 struct v4l2_audio * var_vidioc_g_audio_19_p2;
602 /* content: static int vidioc_s_audio(struct file *file, void *priv, struct v4l2_audio *a)*/
603 /* LDV_COMMENT_BEGIN_PREP */
604 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
605 #ifndef PCI_VENDOR_ID_GEMTEK
606 #define PCI_VENDOR_ID_GEMTEK 0x5046
607 #endif
608 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
609 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
610 #endif
611 #ifndef GEMTEK_PCI_RANGE_LOW
612 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
613 #endif
614 #ifndef GEMTEK_PCI_RANGE_HIGH
615 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
616 #endif
617 #define _b0(v) (*((u8 *)&v))
618 /* LDV_COMMENT_END_PREP */
619 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_audio" */
620 void * var_vidioc_s_audio_20_p1;
621 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_audio" */
622 struct v4l2_audio * var_vidioc_s_audio_20_p2;
623 /* content: static int vidioc_g_input(struct file *filp, void *priv, unsigned int *i)*/
624 /* LDV_COMMENT_BEGIN_PREP */
625 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
626 #ifndef PCI_VENDOR_ID_GEMTEK
627 #define PCI_VENDOR_ID_GEMTEK 0x5046
628 #endif
629 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
630 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
631 #endif
632 #ifndef GEMTEK_PCI_RANGE_LOW
633 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
634 #endif
635 #ifndef GEMTEK_PCI_RANGE_HIGH
636 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
637 #endif
638 #define _b0(v) (*((u8 *)&v))
639 /* LDV_COMMENT_END_PREP */
640 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_input" */
641 void * var_vidioc_g_input_17_p1;
642 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_input" */
643 unsigned int * var_vidioc_g_input_17_p2;
644 /* content: static int vidioc_s_input(struct file *filp, void *priv, unsigned int i)*/
645 /* LDV_COMMENT_BEGIN_PREP */
646 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
647 #ifndef PCI_VENDOR_ID_GEMTEK
648 #define PCI_VENDOR_ID_GEMTEK 0x5046
649 #endif
650 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
651 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
652 #endif
653 #ifndef GEMTEK_PCI_RANGE_LOW
654 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
655 #endif
656 #ifndef GEMTEK_PCI_RANGE_HIGH
657 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
658 #endif
659 #define _b0(v) (*((u8 *)&v))
660 /* LDV_COMMENT_END_PREP */
661 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_input" */
662 void * var_vidioc_s_input_18_p1;
663 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_input" */
664 unsigned int var_vidioc_s_input_18_p2;
665 /* content: static int vidioc_g_frequency(struct file *file, void *priv, struct v4l2_frequency *f)*/
666 /* LDV_COMMENT_BEGIN_PREP */
667 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
668 #ifndef PCI_VENDOR_ID_GEMTEK
669 #define PCI_VENDOR_ID_GEMTEK 0x5046
670 #endif
671 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
672 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
673 #endif
674 #ifndef GEMTEK_PCI_RANGE_LOW
675 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
676 #endif
677 #ifndef GEMTEK_PCI_RANGE_HIGH
678 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
679 #endif
680 #define _b0(v) (*((u8 *)&v))
681 /* LDV_COMMENT_END_PREP */
682 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_frequency" */
683 void * var_vidioc_g_frequency_13_p1;
684 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_frequency" */
685 struct v4l2_frequency * var_vidioc_g_frequency_13_p2;
686 /* content: static int vidioc_s_frequency(struct file *file, void *priv, struct v4l2_frequency *f)*/
687 /* LDV_COMMENT_BEGIN_PREP */
688 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
689 #ifndef PCI_VENDOR_ID_GEMTEK
690 #define PCI_VENDOR_ID_GEMTEK 0x5046
691 #endif
692 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
693 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
694 #endif
695 #ifndef GEMTEK_PCI_RANGE_LOW
696 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
697 #endif
698 #ifndef GEMTEK_PCI_RANGE_HIGH
699 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
700 #endif
701 #define _b0(v) (*((u8 *)&v))
702 /* LDV_COMMENT_END_PREP */
703 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_frequency" */
704 void * var_vidioc_s_frequency_12_p1;
705 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_frequency" */
706 struct v4l2_frequency * var_vidioc_s_frequency_12_p2;
707 /* content: static int vidioc_queryctrl(struct file *file, void *priv, struct v4l2_queryctrl *qc)*/
708 /* LDV_COMMENT_BEGIN_PREP */
709 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
710 #ifndef PCI_VENDOR_ID_GEMTEK
711 #define PCI_VENDOR_ID_GEMTEK 0x5046
712 #endif
713 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
714 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
715 #endif
716 #ifndef GEMTEK_PCI_RANGE_LOW
717 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
718 #endif
719 #ifndef GEMTEK_PCI_RANGE_HIGH
720 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
721 #endif
722 #define _b0(v) (*((u8 *)&v))
723 /* LDV_COMMENT_END_PREP */
724 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_queryctrl" */
725 void * var_vidioc_queryctrl_14_p1;
726 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_queryctrl" */
727 struct v4l2_queryctrl * var_vidioc_queryctrl_14_p2;
728 /* content: static int vidioc_g_ctrl(struct file *file, void *priv, struct v4l2_control *ctrl)*/
729 /* LDV_COMMENT_BEGIN_PREP */
730 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
731 #ifndef PCI_VENDOR_ID_GEMTEK
732 #define PCI_VENDOR_ID_GEMTEK 0x5046
733 #endif
734 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
735 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
736 #endif
737 #ifndef GEMTEK_PCI_RANGE_LOW
738 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
739 #endif
740 #ifndef GEMTEK_PCI_RANGE_HIGH
741 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
742 #endif
743 #define _b0(v) (*((u8 *)&v))
744 /* LDV_COMMENT_END_PREP */
745 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_ctrl" */
746 void * var_vidioc_g_ctrl_15_p1;
747 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_g_ctrl" */
748 struct v4l2_control * var_vidioc_g_ctrl_15_p2;
749 /* content: static int vidioc_s_ctrl(struct file *file, void *priv, struct v4l2_control *ctrl)*/
750 /* LDV_COMMENT_BEGIN_PREP */
751 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
752 #ifndef PCI_VENDOR_ID_GEMTEK
753 #define PCI_VENDOR_ID_GEMTEK 0x5046
754 #endif
755 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
756 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
757 #endif
758 #ifndef GEMTEK_PCI_RANGE_LOW
759 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
760 #endif
761 #ifndef GEMTEK_PCI_RANGE_HIGH
762 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
763 #endif
764 #define _b0(v) (*((u8 *)&v))
765 /* LDV_COMMENT_END_PREP */
766 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_ctrl" */
767 void * var_vidioc_s_ctrl_16_p1;
768 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "vidioc_s_ctrl" */
769 struct v4l2_control * var_vidioc_s_ctrl_16_p2;
770
771 /** STRUCT: struct type: pci_driver, struct name: gemtek_pci_driver **/
772 /* content: static int __devinit gemtek_pci_probe(struct pci_dev *pdev, const struct pci_device_id *pci_id)*/
773 /* LDV_COMMENT_BEGIN_PREP */
774 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
775 #ifndef PCI_VENDOR_ID_GEMTEK
776 #define PCI_VENDOR_ID_GEMTEK 0x5046
777 #endif
778 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
779 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
780 #endif
781 #ifndef GEMTEK_PCI_RANGE_LOW
782 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
783 #endif
784 #ifndef GEMTEK_PCI_RANGE_HIGH
785 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
786 #endif
787 #define _b0(v) (*((u8 *)&v))
788 /* LDV_COMMENT_END_PREP */
789 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "gemtek_pci_probe" */
790 struct pci_dev * var_group2;
791 /* LDV_COMMENT_VAR_DECLARE Variable declaration for function "gemtek_pci_probe" */
792 const struct pci_device_id * var_gemtek_pci_probe_21_p1;
793 /* LDV_COMMENT_VAR_DECLARE Variable declaration for test return result from function call "gemtek_pci_probe" */
794 static int res_gemtek_pci_probe_21;
795
796
797
798
799 /* LDV_COMMENT_END_VARIABLE_DECLARATION_PART */
800 /* LDV_COMMENT_BEGIN_VARIABLE_INITIALIZING_PART */
801 /*============================= VARIABLE INITIALIZING PART =============================*/
802 LDV_IN_INTERRUPT=
1;
803
804
805
806
807 /* LDV_COMMENT_END_VARIABLE_INITIALIZING_PART */
808 /* LDV_COMMENT_BEGIN_FUNCTION_CALL_SECTION */
809 /*============================= FUNCTION CALL SECTION =============================*/
810 /* LDV_COMMENT_FUNCTION_CALL Initialize LDV model. */
811 ldv_initialize();
812
813 /** INIT: init_type: ST_MODULE_INIT **/
814 /* content: static int __init gemtek_pci_init(void)*/
815 /* LDV_COMMENT_BEGIN_PREP */
816 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
817 #ifndef PCI_VENDOR_ID_GEMTEK
818 #define PCI_VENDOR_ID_GEMTEK 0x5046
819 #endif
820 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
821 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
822 #endif
823 #ifndef GEMTEK_PCI_RANGE_LOW
824 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
825 #endif
826 #ifndef GEMTEK_PCI_RANGE_HIGH
827 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
828 #endif
829 #define _b0(v) (*((u8 *)&v))
830 /* LDV_COMMENT_END_PREP */
831 /* LDV_COMMENT_FUNCTION_CALL Kernel calls driver init function after driver loading to kernel. This function declared as "MODULE_INIT(function name)". */
832 if(gemtek_pci_init())
833 goto ldv_final;
834
835
836 int ldv_s_gemtek_pci_driver_pci_driver =
0;
837
838
839 while( nondet_int()
840 || !(ldv_s_gemtek_pci_driver_pci_driver ==
0)
841 ) {
842
843 switch(nondet_int()) {
844
845 case 0: {
846
847 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
848
849
850 /* content: static int vidioc_querycap(struct file *file, void *priv, struct v4l2_capability *v)*/
851 /* LDV_COMMENT_BEGIN_PREP */
852 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
853 #ifndef PCI_VENDOR_ID_GEMTEK
854 #define PCI_VENDOR_ID_GEMTEK 0x5046
855 #endif
856 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
857 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
858 #endif
859 #ifndef GEMTEK_PCI_RANGE_LOW
860 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
861 #endif
862 #ifndef GEMTEK_PCI_RANGE_HIGH
863 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
864 #endif
865 #define _b0(v) (*((u8 *)&v))
866 /* LDV_COMMENT_END_PREP */
867 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_querycap" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
868 vidioc_querycap( var_group1, var_vidioc_querycap_9_p1, var_vidioc_querycap_9_p2);
869
870
871
872
873 }
874
875 break;
876 case 1: {
877
878 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
879
880
881 /* content: static int vidioc_g_tuner(struct file *file, void *priv, struct v4l2_tuner *v)*/
882 /* LDV_COMMENT_BEGIN_PREP */
883 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
884 #ifndef PCI_VENDOR_ID_GEMTEK
885 #define PCI_VENDOR_ID_GEMTEK 0x5046
886 #endif
887 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
888 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
889 #endif
890 #ifndef GEMTEK_PCI_RANGE_LOW
891 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
892 #endif
893 #ifndef GEMTEK_PCI_RANGE_HIGH
894 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
895 #endif
896 #define _b0(v) (*((u8 *)&v))
897 /* LDV_COMMENT_END_PREP */
898 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_g_tuner" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
899 vidioc_g_tuner( var_group1, var_vidioc_g_tuner_10_p1, var_vidioc_g_tuner_10_p2);
900
901
902
903
904 }
905
906 break;
907 case 2: {
908
909 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
910
911
912 /* content: static int vidioc_s_tuner(struct file *file, void *priv, struct v4l2_tuner *v)*/
913 /* LDV_COMMENT_BEGIN_PREP */
914 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
915 #ifndef PCI_VENDOR_ID_GEMTEK
916 #define PCI_VENDOR_ID_GEMTEK 0x5046
917 #endif
918 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
919 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
920 #endif
921 #ifndef GEMTEK_PCI_RANGE_LOW
922 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
923 #endif
924 #ifndef GEMTEK_PCI_RANGE_HIGH
925 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
926 #endif
927 #define _b0(v) (*((u8 *)&v))
928 /* LDV_COMMENT_END_PREP */
929 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_s_tuner" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
930 vidioc_s_tuner( var_group1, var_vidioc_s_tuner_11_p1, var_vidioc_s_tuner_11_p2);
931
932
933
934
935 }
936
937 break;
938 case 3: {
939
940 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
941
942
943 /* content: static int vidioc_g_audio(struct file *file, void *priv, struct v4l2_audio *a)*/
944 /* LDV_COMMENT_BEGIN_PREP */
945 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
946 #ifndef PCI_VENDOR_ID_GEMTEK
947 #define PCI_VENDOR_ID_GEMTEK 0x5046
948 #endif
949 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
950 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
951 #endif
952 #ifndef GEMTEK_PCI_RANGE_LOW
953 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
954 #endif
955 #ifndef GEMTEK_PCI_RANGE_HIGH
956 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
957 #endif
958 #define _b0(v) (*((u8 *)&v))
959 /* LDV_COMMENT_END_PREP */
960 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_g_audio" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
961 vidioc_g_audio( var_group1, var_vidioc_g_audio_19_p1, var_vidioc_g_audio_19_p2);
962
963
964
965
966 }
967
968 break;
969 case 4: {
970
971 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
972
973
974 /* content: static int vidioc_s_audio(struct file *file, void *priv, struct v4l2_audio *a)*/
975 /* LDV_COMMENT_BEGIN_PREP */
976 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
977 #ifndef PCI_VENDOR_ID_GEMTEK
978 #define PCI_VENDOR_ID_GEMTEK 0x5046
979 #endif
980 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
981 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
982 #endif
983 #ifndef GEMTEK_PCI_RANGE_LOW
984 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
985 #endif
986 #ifndef GEMTEK_PCI_RANGE_HIGH
987 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
988 #endif
989 #define _b0(v) (*((u8 *)&v))
990 /* LDV_COMMENT_END_PREP */
991 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_s_audio" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
992 vidioc_s_audio( var_group1, var_vidioc_s_audio_20_p1, var_vidioc_s_audio_20_p2);
993
994
995
996
997 }
998
999 break;
1000 case 5: {
1001
1002 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
1003
1004
1005 /* content: static int vidioc_g_input(struct file *filp, void *priv, unsigned int *i)*/
1006 /* LDV_COMMENT_BEGIN_PREP */
1007 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1008 #ifndef PCI_VENDOR_ID_GEMTEK
1009 #define PCI_VENDOR_ID_GEMTEK 0x5046
1010 #endif
1011 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1012 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1013 #endif
1014 #ifndef GEMTEK_PCI_RANGE_LOW
1015 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1016 #endif
1017 #ifndef GEMTEK_PCI_RANGE_HIGH
1018 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1019 #endif
1020 #define _b0(v) (*((u8 *)&v))
1021 /* LDV_COMMENT_END_PREP */
1022 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_g_input" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
1023 vidioc_g_input( var_group1, var_vidioc_g_input_17_p1, var_vidioc_g_input_17_p2);
1024
1025
1026
1027
1028 }
1029
1030 break;
1031 case 6: {
1032
1033 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
1034
1035
1036 /* content: static int vidioc_s_input(struct file *filp, void *priv, unsigned int i)*/
1037 /* LDV_COMMENT_BEGIN_PREP */
1038 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1039 #ifndef PCI_VENDOR_ID_GEMTEK
1040 #define PCI_VENDOR_ID_GEMTEK 0x5046
1041 #endif
1042 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1043 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1044 #endif
1045 #ifndef GEMTEK_PCI_RANGE_LOW
1046 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1047 #endif
1048 #ifndef GEMTEK_PCI_RANGE_HIGH
1049 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1050 #endif
1051 #define _b0(v) (*((u8 *)&v))
1052 /* LDV_COMMENT_END_PREP */
1053 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_s_input" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
1054 vidioc_s_input( var_group1, var_vidioc_s_input_18_p1, var_vidioc_s_input_18_p2);
1055
1056
1057
1058
1059 }
1060
1061 break;
1062 case 7: {
1063
1064 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
1065
1066
1067 /* content: static int vidioc_g_frequency(struct file *file, void *priv, struct v4l2_frequency *f)*/
1068 /* LDV_COMMENT_BEGIN_PREP */
1069 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1070 #ifndef PCI_VENDOR_ID_GEMTEK
1071 #define PCI_VENDOR_ID_GEMTEK 0x5046
1072 #endif
1073 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1074 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1075 #endif
1076 #ifndef GEMTEK_PCI_RANGE_LOW
1077 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1078 #endif
1079 #ifndef GEMTEK_PCI_RANGE_HIGH
1080 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1081 #endif
1082 #define _b0(v) (*((u8 *)&v))
1083 /* LDV_COMMENT_END_PREP */
1084 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_g_frequency" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
1085 vidioc_g_frequency( var_group1, var_vidioc_g_frequency_13_p1, var_vidioc_g_frequency_13_p2);
1086
1087
1088
1089
1090 }
1091
1092 break;
1093 case 8: {
1094
1095 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
1096
1097
1098 /* content: static int vidioc_s_frequency(struct file *file, void *priv, struct v4l2_frequency *f)*/
1099 /* LDV_COMMENT_BEGIN_PREP */
1100 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1101 #ifndef PCI_VENDOR_ID_GEMTEK
1102 #define PCI_VENDOR_ID_GEMTEK 0x5046
1103 #endif
1104 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1105 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1106 #endif
1107 #ifndef GEMTEK_PCI_RANGE_LOW
1108 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1109 #endif
1110 #ifndef GEMTEK_PCI_RANGE_HIGH
1111 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1112 #endif
1113 #define _b0(v) (*((u8 *)&v))
1114 /* LDV_COMMENT_END_PREP */
1115 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_s_frequency" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
1116 vidioc_s_frequency( var_group1, var_vidioc_s_frequency_12_p1, var_vidioc_s_frequency_12_p2);
1117
1118
1119
1120
1121 }
1122
1123 break;
1124 case 9: {
1125
1126 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
1127
1128
1129 /* content: static int vidioc_queryctrl(struct file *file, void *priv, struct v4l2_queryctrl *qc)*/
1130 /* LDV_COMMENT_BEGIN_PREP */
1131 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1132 #ifndef PCI_VENDOR_ID_GEMTEK
1133 #define PCI_VENDOR_ID_GEMTEK 0x5046
1134 #endif
1135 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1136 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1137 #endif
1138 #ifndef GEMTEK_PCI_RANGE_LOW
1139 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1140 #endif
1141 #ifndef GEMTEK_PCI_RANGE_HIGH
1142 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1143 #endif
1144 #define _b0(v) (*((u8 *)&v))
1145 /* LDV_COMMENT_END_PREP */
1146 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_queryctrl" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
1147 vidioc_queryctrl( var_group1, var_vidioc_queryctrl_14_p1, var_vidioc_queryctrl_14_p2);
1148
1149
1150
1151
1152 }
1153
1154 break;
1155 case 10: {
1156
1157 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
1158
1159
1160 /* content: static int vidioc_g_ctrl(struct file *file, void *priv, struct v4l2_control *ctrl)*/
1161 /* LDV_COMMENT_BEGIN_PREP */
1162 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1163 #ifndef PCI_VENDOR_ID_GEMTEK
1164 #define PCI_VENDOR_ID_GEMTEK 0x5046
1165 #endif
1166 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1167 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1168 #endif
1169 #ifndef GEMTEK_PCI_RANGE_LOW
1170 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1171 #endif
1172 #ifndef GEMTEK_PCI_RANGE_HIGH
1173 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1174 #endif
1175 #define _b0(v) (*((u8 *)&v))
1176 /* LDV_COMMENT_END_PREP */
1177 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_g_ctrl" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
1178 vidioc_g_ctrl( var_group1, var_vidioc_g_ctrl_15_p1, var_vidioc_g_ctrl_15_p2);
1179
1180
1181
1182
1183 }
1184
1185 break;
1186 case 11: {
1187
1188 /** STRUCT: struct type: v4l2_ioctl_ops, struct name: gemtek_pci_ioctl_ops **/
1189
1190
1191 /* content: static int vidioc_s_ctrl(struct file *file, void *priv, struct v4l2_control *ctrl)*/
1192 /* LDV_COMMENT_BEGIN_PREP */
1193 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1194 #ifndef PCI_VENDOR_ID_GEMTEK
1195 #define PCI_VENDOR_ID_GEMTEK 0x5046
1196 #endif
1197 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1198 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1199 #endif
1200 #ifndef GEMTEK_PCI_RANGE_LOW
1201 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1202 #endif
1203 #ifndef GEMTEK_PCI_RANGE_HIGH
1204 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1205 #endif
1206 #define _b0(v) (*((u8 *)&v))
1207 /* LDV_COMMENT_END_PREP */
1208 /* LDV_COMMENT_FUNCTION_CALL Function from field "vidioc_s_ctrl" from driver structure with callbacks "gemtek_pci_ioctl_ops" */
1209 vidioc_s_ctrl( var_group1, var_vidioc_s_ctrl_16_p1, var_vidioc_s_ctrl_16_p2);
1210
1211
1212
1213
1214 }
1215
1216 break;
1217 case 12: {
1218
1219 /** STRUCT: struct type: pci_driver, struct name: gemtek_pci_driver **/
1220 if(ldv_s_gemtek_pci_driver_pci_driver==
0) {
1221
1222 /* content: static int __devinit gemtek_pci_probe(struct pci_dev *pdev, const struct pci_device_id *pci_id)*/
1223 /* LDV_COMMENT_BEGIN_PREP */
1224 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1225 #ifndef PCI_VENDOR_ID_GEMTEK
1226 #define PCI_VENDOR_ID_GEMTEK 0x5046
1227 #endif
1228 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1229 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1230 #endif
1231 #ifndef GEMTEK_PCI_RANGE_LOW
1232 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1233 #endif
1234 #ifndef GEMTEK_PCI_RANGE_HIGH
1235 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1236 #endif
1237 #define _b0(v) (*((u8 *)&v))
1238 /* LDV_COMMENT_END_PREP */
1239 /* LDV_COMMENT_FUNCTION_CALL Function from field "probe" from driver structure with callbacks "gemtek_pci_driver". Standart function test for correct return result. */
1240 res_gemtek_pci_probe_21 = gemtek_pci_probe( var_group2, var_gemtek_pci_probe_21_p1);
1241 ldv_check_return_value(res_gemtek_pci_probe_21);
1242 if(res_gemtek_pci_probe_21)
1243 goto ldv_module_exit;
1244 ldv_s_gemtek_pci_driver_pci_driver=
0;
1245
1246 }
1247
1248 }
1249
1250 break;
1251 default:
break;
1252
1253 }
1254
1255 }
1256
1257 ldv_module_exit:
1258
1259 /** INIT: init_type: ST_MODULE_EXIT **/
1260 /* content: static void __exit gemtek_pci_exit(void)*/
1261 /* LDV_COMMENT_BEGIN_PREP */
1262 #define RADIO_VERSION KERNEL_VERSION(
0,
0,
2)
1263 #ifndef PCI_VENDOR_ID_GEMTEK
1264 #define PCI_VENDOR_ID_GEMTEK 0x5046
1265 #endif
1266 #ifndef PCI_DEVICE_ID_GEMTEK_PR103
1267 #define PCI_DEVICE_ID_GEMTEK_PR103 0x1001
1268 #endif
1269 #ifndef GEMTEK_PCI_RANGE_LOW
1270 #define GEMTEK_PCI_RANGE_LOW (
87*
16000)
1271 #endif
1272 #ifndef GEMTEK_PCI_RANGE_HIGH
1273 #define GEMTEK_PCI_RANGE_HIGH (
108*
16000)
1274 #endif
1275 #define _b0(v) (*((u8 *)&v))
1276 /* LDV_COMMENT_END_PREP */
1277 /* LDV_COMMENT_FUNCTION_CALL Kernel calls driver release function before driver will be uploaded from kernel. This function declared as "MODULE_EXIT(function name)". */
1278 gemtek_pci_exit();
1279
1280 /* LDV_COMMENT_FUNCTION_CALL Checks that all resources and locks are correctly released before the driver will be unloaded. */
1281 ldv_final: ldv_check_final_state();
1282
1283 /* LDV_COMMENT_END_FUNCTION_CALL_SECTION */
1284 return;
1285
1286 }
1287 #endif
1288
1289 /* LDV_COMMENT_END_MAIN */
1290 /* LDV_COMMENT_BEGIN_MODEL */
1291
1292 /*
1293 * CONFIG_DEBUG_LOCK_ALLOC must be turned off to apply the given model.
1294 * To be independ on the value of this flag there is the corresponding
1295 * aspect model.
1296 */
1297
1298 /* the function works only without aspectator */
1299 long __builtin_expect(
long val,
long res) {
1300 return val;
1301 }
1302
1303 #include "engine-blast.h"
1304
1305 #include <linux/kernel.h>
1306 #include <linux/mutex.h>
1307
1308 /* Need this because rerouter is buggy!.. */
1309 extern int ldv_mutex_TEMPLATE;
1310 /* Now the actual variable goes... */
1311 int ldv_mutex_TEMPLATE =
1;
1312
1313 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='mutex_lock_interruptible') Check that the mutex was unlocked and nondeterministically lock it. Return the corresponding error code on fails*/
1314 int mutex_lock_interruptible_TEMPLATE(
struct mutex *lock)
1315 {
1316 int nondetermined;
1317
1318 /* LDV_COMMENT_ASSERT Mutex must be unlocked*/
1319 ldv_assert(ldv_mutex_TEMPLATE ==
1);
1320
1321 /* LDV_COMMENT_OTHER Construct the nondetermined result*/
1322 nondetermined = ldv_undef_int();
1323
1324 /* LDV_COMMENT_ASSERT Nondeterministically lock the mutex*/
1325 if (nondetermined)
1326 {
1327 /* LDV_COMMENT_CHANGE_STATE Lock the mutex*/
1328 ldv_mutex_TEMPLATE =
2;
1329 /* LDV_COMMENT_RETURN Finish with success*/
1330 return 0;
1331 }
1332 else
1333 {
1334 /* LDV_COMMENT_RETURN Finish with the fail. The mutex is keeped unlocked*/
1335 return -EINTR;
1336 }
1337 }
1338
1339 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='atomic_dec_and_mutex_lock') Lock if atomic decrement result is zero */
1340 int atomic_dec_and_mutex_lock_TEMPLATE(atomic_t *cnt,
struct mutex *lock)
1341 {
1342 int atomic_value_after_dec;
1343
1344 /* LDV_COMMENT_ASSERT Mutex must be unlocked (since we may lock it in this function) */
1345 ldv_assert(ldv_mutex_TEMPLATE ==
1);
1346
1347 /* LDV_COMMENT_OTHER Assign the result of atomic decrement */
1348 atomic_value_after_dec = ldv_undef_int();
1349
1350 /* LDV_COMMENT_ASSERT Check if atomic decrement returns zero */
1351 if (atomic_value_after_dec ==
0)
1352 {
1353 /* LDV_COMMENT_CHANGE_STATE Lock the mutex, as atomic has decremented to zero*/
1354 ldv_mutex_TEMPLATE =
2;
1355 /* LDV_COMMENT_RETURN Return 1 with a locked mutex */
1356 return 1;
1357 }
1358
1359 /* LDV_COMMENT_RETURN Atomic decrement is still not zero, return 0 without locking the mutex */
1360 return 0;
1361 }
1362
1363 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='mutex_lock_killable') Check that the mutex wasn unlocked and nondeterministically lock it. Return the corresponding error code on fails*/
1364 int __must_check mutex_lock_killable_TEMPLATE(
struct mutex *lock)
1365 {
1366 int nondetermined;
1367
1368 /* LDV_COMMENT_ASSERT Mutex must be unlocked*/
1369 ldv_assert(ldv_mutex_TEMPLATE ==
1);
1370
1371 /* LDV_COMMENT_OTHER Construct the nondetermined result*/
1372 nondetermined = ldv_undef_int();
1373
1374 /* LDV_COMMENT_ASSERT Nondeterministically lock the mutex*/
1375 if (nondetermined)
1376 {
1377 /* LDV_COMMENT_CHANGE_STATE Lock the mutex*/
1378 ldv_mutex_TEMPLATE =
2;
1379 /* LDV_COMMENT_RETURN Finish with success*/
1380 return 0;
1381 }
1382 else
1383 {
1384 /* LDV_COMMENT_RETURN Finish with the fail. The mutex is keeped unlocked*/
1385 return -EINTR;
1386 }
1387 }
1388
1389 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='mutex_is_locked') Checks whether the mutex is locked*/
1390 int mutex_is_locked_TEMPLATE(
struct mutex *lock)
1391 {
1392 int nondetermined;
1393
1394 if(ldv_mutex_TEMPLATE ==
1) {
1395 /* LDV_COMMENT_OTHER Construct the nondetermined result*/
1396 nondetermined = ldv_undef_int();
1397 if(nondetermined) {
1398 /* LDV_COMMENT_RETURN the mutex is unlocked*/
1399 return 0;
1400 }
else {
1401 /* LDV_COMMENT_RETURN the mutex is locked*/
1402 return 1;
1403 }
1404 }
else {
1405 /* LDV_COMMENT_RETURN the mutex is locked*/
1406 return 1;
1407 }
1408 }
1409
1410 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='mutex_lock(?!_interruptible|_killable)') Check that the mutex was not locked and lock it*/
1411 void mutex_lock_TEMPLATE(
struct mutex *lock)
1412 {
1413 /* LDV_COMMENT_ASSERT Mutex must be unlocked*/
1414 ldv_assert(ldv_mutex_TEMPLATE ==
1);
1415 /* LDV_COMMENT_CHANGE_STATE Lock the mutex*/
1416 ldv_mutex_TEMPLATE =
2;
1417 }
1418
1419 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='mutex_trylock') Check that the mutex was not locked and nondeterministically lock it. Return 0 on fails*/
1420 int mutex_trylock_TEMPLATE(
struct mutex *lock)
1421 {
1422 int is_mutex_held_by_another_thread;
1423
1424 /* LDV_COMMENT_ASSERT Mutex must be unlocked*/
1425 ldv_assert(ldv_mutex_TEMPLATE ==
1);
1426
1427 /* LDV_COMMENT_OTHER Construct the nondetermined result*/
1428 is_mutex_held_by_another_thread = ldv_undef_int();
1429
1430 /* LDV_COMMENT_ASSERT Nondeterministically lock the mutex*/
1431 if (is_mutex_held_by_another_thread)
1432 {
1433 /* LDV_COMMENT_RETURN Finish with fail*/
1434 return 0;
1435 }
1436 else
1437 {
1438 /* LDV_COMMENT_CHANGE_STATE Lock the mutex*/
1439 ldv_mutex_TEMPLATE =
2;
1440 /* LDV_COMMENT_RETURN Finish with success*/
1441 return 1;
1442 }
1443 }
1444
1445 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='mutex_unlock') Check that the mutex was locked and unlock it*/
1446 void mutex_unlock_TEMPLATE(
struct mutex *lock)
1447 {
1448 /* LDV_COMMENT_ASSERT Mutex must be locked*/
1449 ldv_assert(ldv_mutex_TEMPLATE ==
2);
1450 /* LDV_COMMENT_CHANGE_STATE Unlock the mutex*/
1451 ldv_mutex_TEMPLATE =
1;
1452 }
1453
1454 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='check_final_state') Check that the mutex is unlocked at the end*/
1455 void ldv_check_final_state_TEMPLATE(
void)
1456 {
1457 /* LDV_COMMENT_ASSERT The mutex must be unlocked at the end*/
1458 ldv_assert(ldv_mutex_TEMPLATE ==
1);
1459 }
1460
1461 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_initialize') Initialize mutex variables*/
1462 void ldv_initialize_TEMPLATE(
void)
1463 {
1464 /* LDV_COMMENT_ASSERT Initialize mutex with initial model value*/
1465 ldv_mutex_TEMPLATE =
1;
1466 }
1467
1468 /* LDV_COMMENT_END_MODEL */
Online Linux Driver Verification Service (alpha)