--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] context sensitive points-to analysis



Hello,
I am testing context sensitive points-to analysis feature of Frama-C.
I am confused with this feature because depending on slicing criteria,
results seem fine or not fine. Can any one help how to get fine results
in any case (at least for the sample code below)?

I attach my test program at the end of the text, and here is a brief
description of the symptom:
When I choose "s2t_main_temp = (s2)s2g_out1;" of line 53 as slicing
criterion, only statements of variable subscript 1 are sliced. For
example for "fun()," only lines 40 and 42 are sliced. This is a fine result.
However when I choose "s2t_main_temp = (s2)s2g_out11;" of line 52 as
slicing criterion, all lines of "fun()" are selected, which are
different from my expectation.

For slicing I simply insert "/*@slice pragma stmt;*/" at the beginning
of slicing criterion line, and use the following command:
toplevel.opt.exe -cpp-command "gcc.exe -C -E -I." -lib-entry -main main
-slice-pragma main -slice-print -quiet -ulevel 2 -node-infoonly *.i
where "*.i"are referring preprocessed version of the c files with
slicing pragma being inserted.
Please let me know what I should do to have correct results for either
case. I am using frama-c-Lithium-20081201.

Myung-Jin

------------- START test code ------------
typedef signed short s2;

s2 s2g_in1;
s2 s2g_in2;

s2 s2g_out1;
s2 s2g_out2;

s2 s2g_out11;
s2 s2g_out22;

s2 s2g_in1_get()
{
return s2g_in1;
}
s2 s2g_in2_get()
{
return s2g_in2;
}

void set(s2* s2g, s2 s2t)
{
*s2g = s2t;
}

void set_s2g_out1(s2 s2t_out_temp1)
{
set(&s2g_out11, s2t_out_temp1);
s2g_out1 = (s2)s2g_out11;
}

void set_s2g_out2(s2 s2t_out_temp2)
{
set(&s2g_out22, s2t_out_temp2);
s2g_out2 = (s2)s2g_out22;
}

void fun()
{
s2 s2t_fun_temp1 = 0;
s2 s2t_fun_temp2 = 0;

set_s2g_out1(s2t_fun_temp1);

set_s2g_out2(s2t_fun_temp2);
}

void main(void)
{
s2 s2t_main_temp;
fun();
s2t_main_temp = (s2)s2g_out11; // line52: result seems not correct for
this criterion
s2t_main_temp = (s2)s2g_out1; // line53: result seems correct for this
criterion
}
------------- END test code ------------