User Tools

Site Tools


sv-comp_2015_device-drivers-64

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sv-comp_2015_device-drivers-64 [2015/01/16 11:31]
ruben
sv-comp_2015_device-drivers-64 [2015/01/16 11:57] (current)
ruben
Line 11: Line 11:
  
 <​code>​ ldv-linux-3.7.3/​linux-3.10-rc1-43_1a-bitvector-drivers--atm--he.ko-ldv_main0_true-unreach-call.cil.out.c </​code>​ <​code>​ ldv-linux-3.7.3/​linux-3.10-rc1-43_1a-bitvector-drivers--atm--he.ko-ldv_main0_true-unreach-call.cil.out.c </​code>​
 +
 +Lihao analysis:
 +
 +In main:
 +var_group1 doesn'​t get initialised (line 12595 in the c file) so CBMC
 +assigns NULL to it:
 +
 +var_group1=((struct atm_vcc *)NULL)
 +(0000000000000000000000000000000000000000000000000000000000000000)
 +
 +tmp___0 (line 12641) gets an non-deterministic assignment which is 3
 +in the counterexample so we are in case 3 of the switch statement
 +(line 12688) where function he_send is called with the var_group1
 +being NULL.
 +
 +In he_send, ldv_spin_lock is called (line 11915) where ldv_spin is set
 +to 1. Then the function pointer vcc->pop is called (line 11924).
 +
 +Note that vcc is the first argument of he_send which is the NULL
 +var_group1. In the counterexample CBMC calls he_init_one which in turn
 +calls kzalloc(792UL,​ 208U) in line 7949.
 +
 +Then ldv_check_alloc_flags is called with parameter 208U and ldv_spin
 +is 1 (line 12883). So the ERROR label is reachable (line 13069).
  
 ====== Trunk version - Analysis of programs that returned unknown ====== ====== Trunk version - Analysis of programs that returned unknown ======
Line 52: Line 76:
 main15_false-unreach-call_drivers-usb-core-usbcore-ko--32_7a--linux-3.7.3.c main15_false-unreach-call_drivers-usb-core-usbcore-ko--32_7a--linux-3.7.3.c
 module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i module_get_put-drivers-block-loop.ko_false-unreach-call.cil.out.i.pp.i
 +</​code>​
 +
 +**cannot unwind the program:**
 +8 Programs are not unwound (even with unwinding 2):
 +
 +<​code>​
 +module_get_put-drivers-bluetooth-btmrvl.ko_true-unreach-call.cil.out.i.pp.i
 +m0_true-unreach-call_drivers-net-myri10ge-myri10ge-ko--138_1a--7cb2521.c
 +linux-stable-d47b389-1-32_7a-drivers--media--video--cx88--cx88-blackbird.ko-entry_point_false-unreach-call.cil.out.c
 +linux-3.12-rc1.tar.xz-144_2a-drivers--media--usb--usbvision--usbvision.ko-entry_point_false-unreach-call.cil.out.c
 +32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-fs--ceph--ceph.ko-ldv_main7_sequence_infinite_withcheck_stateful.cil.out.c
 +205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--rtlwifi--rtl8723be--rtl8723be.ko-entry_point_false-unreach-call.cil.out.c
 +205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--ath--wcn36xx--wcn36xx.ko-entry_point_false-unreach-call.cil.out.c
 +205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--can--can-dev.ko-entry_point_false-unreach-call.cil.out.c
 </​code>​ </​code>​
  
sv-comp_2015_device-drivers-64.txt ยท Last modified: 2015/01/16 11:57 by ruben