--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on February 2010 ---
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 ------------