/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/avtg/drivers/media/tuners/it913x.ko/generic:memory/weaver/.tmp_it913x.c.aux
path
false
false
false
false
false
violation_witness
C
CPAchecker 1.6.1-svn
CHECK( init(main()), LTL(G valid-deref) )
CHECK( init(main()), LTL(G valid-memtrack) )
CHECK( init(main()), LTL(G valid-free) )
/work/temp/cil.i
aa6c96a2c5f90269a92242eebb53b98d984b2b51
64bit
2017-02-17T13:13:09+03:00
true
extern struct module __this_module ;
33
223215
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/include/linux/export.h
extern unsigned long volatile jiffies ;
78
225206
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/include/linux/jiffies.h
jiffies == (0UL);
static struct dvb_tuner_ops const it913x_tuner_ops =
# 376 "/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/drivers/media/tuners/it913x.c"
{{{'I', 'T', 'E', ' ', 'I', 'T', '9', '1', '3', 'X', '\000'}, 174000000U, 862000000U,
0U, 0U, 0U, 0U}, 0, & it913x_init, & it913x_sleep, 0, 0, & it913x_set_params,
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0};
376
300691
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/drivers/media/tuners/it913x.c
((it913x_tuner_ops.info.name)[0]) == (73);
static struct i2c_device_id const it913x_id_table[2U] = { {{'i', 't', '9', '1', '3', 'x', '\000'}, 0UL}};
458
322508
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/drivers/media/tuners/it913x.c
(((it913x_id_table[0]).name)[0]) == (105); (((it913x_id_table[1]).name)[0]) == (51);
struct i2c_device_id const __mod_i2c__it913x_id_table_device_table[2U] ;
462
322778
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/drivers/media/tuners/it913x.c
(((__mod_i2c__it913x_id_table_device_table[0]).name)[0]) == (0);
static struct i2c_driver it913x_driver =
# 464 "/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/drivers/media/tuners/it913x.c"
{0U, 0, & it913x_probe, & it913x_remove, 0, 0, 0, {"it913x", 0, & __this_module,
0, (_Bool)0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0}, (struct i2c_device_id const *)(& it913x_id_table),
0, 0, {0, 0}};
464
323015
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/drivers/media/tuners/it913x.c
(it913x_driver.class) == (0U);
Object creation
struct ldv_thread ldv_thread_1 ;
88
330415
(ldv_thread_1.identifier) == (0);
struct ldv_thread ldv_thread_2 ;
89
330651
(ldv_thread_2.identifier) == (0);
struct ldv_thread ldv_thread_3 ;
90
330887
(ldv_thread_3.identifier) == (0);
struct ldv_thread ldv_thread_5 ;
91
331123
(ldv_thread_5.identifier) == (0);
ldv_main_5((void *)0);
538
372095
ldv_main_5
ldv_initialize();
269
346599
ldv_dispatch_insmod_register_5_3();
273
346823
ldv_dispatch_insmod_register_5_3
struct ldv_struct_insmod_3 *cf_arg_3 ;
128
334123
void *tmp ;
129
334164
tmp = ldv_xmalloc(4UL);
128
334391
ldv_xmalloc
void *res ;
68
396473
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
size == (4UL);
ldv_xmalloc
void *tmp ;
69
396487
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
long tmp___0 ;
70
396501
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
tmp = malloc(size);
68
396681
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
res = tmp;
68
396857
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume((unsigned long )res != (unsigned long )((void *)0));
69
397024
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume
[!(expression == 0)]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-false
expression == (1);
ldv_assume
return;
31
388407
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
ldv_assume
69
397024
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
tmp___0 = ldv_is_err((void const *)res);
70
397244
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_is_err
return ((unsigned long )ptr > 4294967295UL);
22
381432
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/linux/err.c
ldv_is_err
70
397244
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume(tmp___0 == 0L);
70
397441
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume
true
true
[expression == 0]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-true
[!(expression == 0)]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-false
return;
31
388407
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
ldv_assume
70
397441
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
return (res);
71
397628
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_xmalloc
128
334391
cf_arg_3 = (struct ldv_struct_insmod_3 *)tmp;
128
334621
ldv_insmod_3((void *)cf_arg_3);
129
334873
ldv_insmod_3
void (*ldv_3_it913x_driver_exit_default)(void) ;
181
339510
int (*ldv_3_it913x_driver_init_default)(void) ;
182
339561
int ldv_3_ret_default ;
183
339611
void *tmp ;
184
339637
void *tmp___0 ;
185
339651
int tmp___1 ;
186
339669
int tmp___2 ;
187
339685
tmp = external_allocated_data();
187
339914
ldv_3_it913x_driver_exit_default = (void (*)(void))tmp;
187
340153
tmp___0 = external_allocated_data();
188
340415
ldv_3_it913x_driver_init_default = (int (*)(void))tmp___0;
188
340658
ldv_free(arg0);
190
340923
ldv_free
free(s);
63
396102
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
return;
64
396271
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_free
190
340923
ldv_3_ret_default = ldv_insmod_it913x_driver_init_3_10(ldv_3_it913x_driver_init_default);
195
341145
ldv_insmod_it913x_driver_init_3_10
int tmp ;
261
345667
tmp = it913x_driver_init();
260
345892
it913x_driver_init
int tmp ;
476
323735
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/drivers/media/tuners/it913x.c
tmp = ldv_i2c_register_driver_20(& __this_module, & it913x_driver);
474
323920
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/lkbce/drivers/media/tuners/it913x.c
ldv_i2c_register_driver_20
int tmp ;
699
376364
(ldv_func_arg2->class) == (0U);
ldv_i2c_register_driver_20
tmp = ldv_emg_i2c_register_driver(ldv_func_arg1, ldv_func_arg2);
701
376589
ldv_emg_i2c_register_driver
struct i2c_driver *ldv_4_i2c_driver_i2c_driver ;
145
336974
(arg1->class) == (0U);
ldv_emg_i2c_register_driver
void *tmp ;
146
337025
int tmp___0 ;
147
337039
int tmp___1 ;
148
337055
tmp = external_allocated_data();
149
337284
ldv_4_i2c_driver_i2c_driver = (struct i2c_driver *)tmp;
149
337523
tmp___1 = ldv_undef_int();
152
337785
ldv_undef_int
int tmp ;
42
406474
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/nondet.c
tmp = __VERIFIER_nondet_int();
41
406649
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/nondet.c
return (tmp);
41
406840
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/nondet.c
ldv_undef_int
152
337785
[tmp___1 != 0]
152
338026
condition-true
[!(tmp___1 != 0)]
152
338026
condition-false
ldv_4_i2c_driver_i2c_driver = arg1;
154
338256
(ldv_4_i2c_driver_i2c_driver->class) == (0U);
ldv_emg_i2c_register_driver
ldv_dispatch_register_4_3(ldv_4_i2c_driver_i2c_driver);
158
338500
ldv_dispatch_register_4_3
struct ldv_struct_partially_ordered_scenario_1 *cf_arg_1 ;
136
335392
(arg0->class) == (0U);
ldv_dispatch_register_4_3
void *tmp ;
137
335453
tmp = ldv_xmalloc(16UL);
136
335680
ldv_xmalloc
void *res ;
68
396473
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
size == (16UL);
ldv_xmalloc
void *tmp ;
69
396487
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
long tmp___0 ;
70
396501
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
tmp = malloc(size);
68
396681
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
res = tmp;
68
396857
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume((unsigned long )res != (unsigned long )((void *)0));
69
397024
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume
[!(expression == 0)]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-false
expression == (1);
ldv_assume
return;
31
388407
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
ldv_assume
69
397024
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
tmp___0 = ldv_is_err((void const *)res);
70
397244
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_is_err
return ((unsigned long )ptr > 4294967295UL);
22
381432
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/linux/err.c
ldv_is_err
70
397244
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume(tmp___0 == 0L);
70
397441
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume
true
[expression == 0]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-true
[!(expression == 0)]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-false
return;
31
388407
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
ldv_assume
70
397441
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
return (res);
71
397628
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_xmalloc
136
335680
cf_arg_1 = (struct ldv_struct_partially_ordered_scenario_1 *)tmp;
136
335911
cf_arg_1->arg0 = arg0;
137
336183
(cf_arg_1->arg0->class) == (0U);
ldv_dispatch_register_4_3
ldv_partially_ordered_scenario_1((void *)cf_arg_1);
138
336412
ldv_partially_ordered_scenario_1
struct i2c_driver *ldv_1_container_i2c_driver ;
295
348247
struct i2c_client *ldv_1_resource_client ;
296
348297
struct i2c_device_id *ldv_1_resource_struct_i2c_device_id ;
297
348342
int ldv_1_ret_default ;
298
348404
struct ldv_struct_partially_ordered_scenario_1 *data ;
299
348430
void *tmp ;
300
348487
void *tmp___0 ;
301
348501
void *tmp___1 ;
302
348519
void *tmp___2 ;
303
348537
void *tmp___3 ;
304
348555
int tmp___4 ;
305
348573
int tmp___5 ;
306
348589
int tmp___6 ;
307
348605
data = (struct ldv_struct_partially_ordered_scenario_1 *)arg0;
301
348834
(data->arg0->class) == (0U);
ldv_partially_ordered_scenario_1
tmp = external_allocated_data();
305
349103
ldv_1_container_i2c_driver = (struct i2c_driver *)tmp;
305
349342
tmp___0 = external_allocated_data();
306
349603
ldv_1_resource_client = (struct i2c_client *)tmp___0;
306
349846
tmp___1 = external_allocated_data();
307
350106
ldv_1_resource_struct_i2c_device_id = (struct i2c_device_id *)tmp___1;
307
350349
ldv_1_ret_default = 1;
308
350626
ldv_1_ret_default == (1);
ldv_partially_ordered_scenario_1
[((unsigned long)data) != ((unsigned long)((struct ldv_struct_partially_ordered_scenario_1 *)0))]
311
350863
condition-true
ldv_1_container_i2c_driver = data->arg0;
312
351174
(ldv_1_container_i2c_driver->class) == (0U);
ldv_partially_ordered_scenario_1
ldv_free((void *)data);
313
351423
ldv_free
free(s);
63
396102
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
return;
64
396271
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_free
313
351423
tmp___2 = ldv_xmalloc(1480UL);
318
351679
ldv_xmalloc
void *res ;
68
396473
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
size == (1480UL);
ldv_xmalloc
void *tmp ;
69
396487
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
long tmp___0 ;
70
396501
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
tmp = malloc(size);
68
396681
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
res = tmp;
68
396857
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume((unsigned long )res != (unsigned long )((void *)0));
69
397024
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume
[!(expression == 0)]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-false
expression == (1);
ldv_assume
return;
31
388407
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
ldv_assume
69
397024
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
tmp___0 = ldv_is_err((void const *)res);
70
397244
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_is_err
return ((unsigned long )ptr > 4294967295UL);
22
381432
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/linux/err.c
ldv_is_err
70
397244
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume(tmp___0 == 0L);
70
397441
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume
true
[expression == 0]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-true
[!(expression == 0)]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-false
return;
31
388407
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
ldv_assume
70
397441
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
return (res);
71
397628
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_xmalloc
318
351679
ldv_1_resource_client = (struct i2c_client *)tmp___2;
318
351916
tmp___3 = ldv_xmalloc_unknown_size(0UL);
319
352176
ldv_xmalloc_unknown_size
void *res ;
116
403931
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
size == (0UL);
ldv_xmalloc_unknown_size
void *tmp ;
117
403945
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
long tmp___0 ;
118
403959
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
tmp = external_allocated_data();
116
404140
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
res = tmp;
116
404330
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume((unsigned long )res != (unsigned long )((void *)0));
117
404498
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume
[!(expression == 0)]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-false
expression == (1);
ldv_assume
return;
31
388407
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
ldv_assume
117
404498
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
tmp___0 = ldv_is_err((void const *)res);
118
404719
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_is_err
return ((unsigned long )ptr > 4294967295UL);
22
381432
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/linux/err.c
ldv_is_err
118
404719
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume(tmp___0 == 0L);
118
404917
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_assume
true
[expression == 0]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-true
[!(expression == 0)]
25
388011
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
condition-false
return;
31
388407
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/common.c
ldv_assume
118
404917
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
return (res);
119
405105
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_xmalloc_unknown_size
319
352176
true
ldv_1_resource_struct_i2c_device_id = (struct i2c_device_id *)tmp___3;
319
352423
tmp___5 = ldv_undef_int();
334
353159
ldv_undef_int
int tmp ;
42
406474
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/nondet.c
tmp = __VERIFIER_nondet_int();
41
406649
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/nondet.c
return (tmp);
41
406840
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/nondet.c
ldv_undef_int
334
353159
[tmp___5 != 0]
334
353400
condition-true
[!(tmp___5 != 0)]
334
353400
condition-false
ldv_free((void *)ldv_1_resource_client);
367
356010
ldv_free
free(s);
63
396102
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
return;
64
396271
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_free
367
356010
ldv_free((void *)ldv_1_resource_struct_i2c_device_id);
368
356259
ldv_free
free(s);
63
396102
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
return;
64
396271
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
ldv_free
368
356259
ldv_free((void *)ldv_1_container_i2c_driver);
372
356522
ldv_free
true
valid-free: invalid pointer free in /home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c, line 63
free(s);
63
396102
/home/debian/klever-work/native-scheduler-work-dir/scheduler/jobs/487df4e429c506b3d4b6e2dbfc45461b/klever-core-work-dir/job/root/verifier/memory.c
Invalid free of unallocated object is found