Line 24330:	N18078 -{long int subdev_do_ioctl(struct file *file, unsigned int cmd, void *arg);}-> N18079
Line 25428:	N11746 -{struct file *var_group1;}-> N11747
Line 25430:	N11748 -{unsigned int var_subdev_ioctl_5_p1;}-> N11749
Line 25431:	N11749 -{unsigned long var_subdev_ioctl_5_p2;}-> N11750
Line 25443:	N11756 -{ldv_initialize()}-> N16573
Line 32508:	N16577 -{ldv_mutex_lock_of_video_device = 1;}-> N16578
Line 32516:	N16581 -{return;}-> N16572
Line 25509:	N11801 -{tmp___0 = nondet_int();}-> N11802
Line 25511:	N11802 -{[tmp___0 != 0]}-> N11804
Line 25513:	N11804 -{Goto: ldv_25189}-> N11759
Line 25448:	N11759 -{tmp = nondet_int();}-> N11760
Line 25488:	N11779 -{[tmp == 2]}-> N11787
Line 25490:	N11787 -{ldv_handler_precall();}-> N11789
Line 25492:	N11789 -{subdev_ioctl(var_group1, var_subdev_ioctl_5_p1, var_subdev_ioctl_5_p2)}-> N11601
Line 25172:	N11603 -{video_usercopy(file, cmd, arg, &subdev_do_ioctl)}-> N5169
Line 14903:	N5182 -{int tmp___1;}-> N5183
Line 14910:	N5186 -{mbuf = 0;}-> N5187
Line 14916:	N5189 -{array_size = 0UL;}-> N5190
Line 14918:	N5190 -{user_ptr = 0;}-> N5191
Line 14920:	N5191 -{kernel_ptr = 0;}-> N5192
Line 14922:	N5192 -{[(cmd >> 30) != 0U]}-> N5194
Line 14924:	N5194 -{[!(((cmd >> 16) & 16383U) <= 128U)]}-> N5198
Line 14929:	N5198 -{kmalloc(((size_t )(cmd >> 16)) & 16383UL, 208U)}-> N72
Line 5793:	N74 -{tmp___2 = __kmalloc(size, flags);}-> N75
Line 5795:	N75 -{return tmp___2;}-> N71
Line 14931:	N5200 -{[!(((unsigned long)mbuf) == ((unsigned long)((void *)0)))]}-> N5203
Line 14938:	N5201 -{parg = mbuf;}-> N5205
Line 14943:	N5206 -{[!((cmd & 1073741824U) != 0U)]}-> N5209
Line 14980:	N5209 -{memset(parg, 0, ((size_t )(cmd >> 16)) & 16383UL);}-> N5229
Line 14986:	N5193 -{check_array_args(cmd, parg, &array_size, &user_ptr, &kernel_ptr)}-> N5094
Line 14790:	N5099 -{ret = 0;}-> N5100
Line 14793:	N5101 -{[!(cmd == 3227014749U)]}-> N5105
Line 14794:	N5105 -{[!(cmd == 3227014665U)]}-> N5107
Line 14795:	N5107 -{[!(cmd == 3227014671U)]}-> N5109
Line 14796:	N5109 -{[!(cmd == 3227014673U)]}-> N5111
Line 14823:	N5111 -{[!(cmd == 3223868968U)]}-> N5129
Line 14824:	N5129 -{[!(cmd == 3223868969U)]}-> N5131
Line 14851:	N5131 -{[!(cmd == 3223344712U)]}-> N5147
Line 14852:	N5147 -{[!(cmd == 3223344711U)]}-> N5149
Line 14853:	N5149 -{[!(cmd == 3223344713U)]}-> N5151
Line 14883:	N5166 -{return ret;}-> N5093
Line 14988:	N5230 -{err = (long)tmp___1;}-> N5231
Line 14990:	N5231 -{[!(err < 0L)]}-> N5234
Line 14997:	N5232 -{has_array_args = err != 0L;}-> N5236
Line 14999:	N5236 -{[((int)has_array_args) == 0]}-> N5239
Line 15028:	N5237 -{(*func)(file, cmd, parg)}-> N11031
Line 24436:	N11129 -{vfh = (struct v4l2_fh *)(file->private_data);}-> N11130
Line 24478:	N11161 -{[cmd == 2156418649U]}-> N11164
Line 24480:	N11164 -{[!(((sd->flags) & 8U) == 0U)]}-> N11168
Line 24487:	N11166 -{v4l2_event_dequeue(vfh, (struct v4l2_event *)arg, ((int)(file->f_flags)) & 2048)}-> N6163
Line 16871:	N6171 -{[!(nonblocking != 0)]}-> N6174
Line 16880:	N6172 -{[((unsigned long)(fh->vdev->lock)) != ((unsigned long)((struct mutex *)0))]}-> N6178
Line 16882:	N6178 -{ldv_mutex_unlock_106(fh->vdev->lock)}-> N6550
Line 17558:	N6551 -{ldv_mutex_unlock_lock_of_video_device(ldv_func_arg1)}-> N16288
Line 31964:	N16289 -{[!(ldv_mutex_lock_of_video_device == 2)]}-> N16292
Line 31968:	N16292 -{ldv_error()}-> N15920
Line 31266:	N15921 -{Label: LDV_ERROR}-> N15922
Line 31268:	N15922 -{Goto: LDV_ERROR}-> N15922