Linux Driver Verification » Crude_slicer

Currently I am working on verification of SVCOMP tasks. I am using crudeslicer plugin(Build fcd3b927) to slice the tasks using the below mentioned command:

./frama-c.native -no-autoload-plugins -no-findlib -load-module Crude_slicer.cmxs -machdep gcc_x86_64 -crude_slicer -timeout 400 -no-recognize_wrecked_container_of -widening_threshold 2000 -no-summaries -no-assert_stratification -print -ocode slice.c task.c

I am using Ubuntu 16.04 OS.

Some of the svcomp tasks have functions without declarations. But the function definitions are positioned in such a way that gcc compiler can encounter its definition before it is actually being called. So the original tasks get compiled successfully. But when we slice using crude_slicer the position of these function definition is changed and they happen to be present after call point of these functions. And their declaration is also not included by the slicer. So the slice generated is not gcc compilable.

In task.c the function __ip_vs_tcp_init is defined at line number 29810 and call points are after this line only(Ref line number 29843, 29883). This function does not have any declaration.
In slice.c the function __ip_vs_tcp_init is defined at line number 9605 and call points are 9483,9482,9685.

The GCC command I have used is gcc -c slice.c

The error trace is

.

/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c: In function ‘register_ip_vs_proto_netns’:
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:60: error: ‘__ip_vs_sctp_init’ undeclared (first use in this function)
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:60: note: each undeclared identifier is reported only once for each function it appears in
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:17: warning: implicit declaration of function ‘__ip_vs_sctp_init’ [-Wimplicit-function-declaration]
tmp___1 = ()(net, pd);
^
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:62: error: ‘__ip_vs_tcp_init’ undeclared (first use in this function)
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:19: warning: implicit declaration of function ‘__ip_vs_tcp_init’ [-Wimplicit-function-declaration]
tmp___1 = ((pp->init_netns))(net, pd);
^
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:64: error: ‘__udp_init’ undeclared (first use in this function)
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:21: warning: implicit declaration of function ‘__udp_init’ [-Wimplicit-function-declaration]
tmp___1 = ()(net, pd);
^
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c: At top level:
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:29810:12: error: static declaration of ‘__ip_vs_tcp_init’ follows non-static declaration
static int ip_vs_tcp_init(struct net *net , struct ip_vs_proto_data *pd )
^
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:19: note: previous implicit declaration of ‘__ip_vs_tcp_init’ was here
tmp1 = ((pp->init_netns))(net, pd);
^
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:30742:12: error: static declaration of ‘_udp_init’ follows non-static declaration
static int udp_init(struct net net , struct ip_vs_proto_data *pd )
^
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:21: note: previous implicit declaration of ‘__udp_init’ was here
tmp1 = ((pp->init_netns))(net, pd);
^
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:32319:12: error: static declaration of ‘_ip_vs_sctp_init’ follows non-static declaration
static int ip_vs_sctp_init(struct net net , struct ip_vs_proto_data *pd )
^
/home/u1364447/sv-benchmarks/c/ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-net--netfilter--ipvs--ip_vs.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c:27997:17: note: previous implicit declaration of ‘__ip_vs_sctp_init’ was here
tmp_1 = ((pp->init_netns))(net, pd);
^

The task.c and the respective slice.c are being attached along with frama_c_journal.ml file