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

Hello,

jung, myung-jin wrote:

> Please let me know what I should do to have correct results for either
> case. I am using frama-c-Lithium-20081201.


and in the example:

> // line52: result seems not correct for this criterion

Let me start with two warnings: first, we call correct
a slicing where no statement that was necessary for
the slicing criterion has been removed. Your problem
seems to be that too many useless statements are left,
or in other words, that the slicing is too imprecise to your
taste.

Second warning: my answer was tested in the development
version of Frama-C, which is very close to version
Beryllium 20090902, but may or may not work in Lithium.
Supporting fixed Frama-C versions is the sort of advantage
we can offer in the context of an industrial contract.

> 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

Removing the -node-infoonly option and slicing on
> s2t_main_temp = (s2)s2g_out1;

I get:

void fun_slice_1(void)
{
   s2 s2t_fun_temp1 ;
   s2t_fun_temp1 = (s2 )0;
   set_s2g_out1_slice_1(s2t_fun_temp1);
   return;
}

I think that this is what you describe and expect.

Slicing on
> s2t_main_temp = (s2)s2g_out11;

with the same option, I get:

void fun_slice_1(void)
{
   s2 s2t_fun_temp1 ;
   s2 s2t_fun_temp2 ;
   s2t_fun_temp1 = (s2 )0;
   s2t_fun_temp2 = (s2 )0;
   set_s2g_out1_slice_1(s2t_fun_temp1);
   set_s2g_out2_slice_1(s2t_fun_temp2);
   return;
}

I think again this is what you describe and find too imprecise.

If I use the same slicing statement again, adding the -calldeps
option to the commandline, I get the result :

void fun_slice_1(void)
{
   s2 s2t_fun_temp1 ;
   s2t_fun_temp1 = (s2 )0;
   set_s2g_out1_slice_1(s2t_fun_temp1);
   return;
}

Is this what you expected?

Pascal

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100204/2c24582d/attachment.htm