Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] context sensitive points-to analysis
  • From: myungjin at jung.tec.toyota.co.jp (jung, myung-jin)
  • Date: Thu, 04 Feb 2010 16:59:18 +0900
  • In-reply-to: <4B020D36.7060901@jung.tec.toyota.co.jp>
  • References: <4B020D36.7060901@jung.tec.toyota.co.jp>
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 ------------