--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on February 2010 ---
Dear Patrick and Pascal, Thank you for your comments. I confirmed what you have mentioned: > Looking at the result given by the gui with the > development version of Frama-C, line 24 isn't green, > nor striked out. That means the semantics of the line 24 > doesn't impact the slicing criteria, but the line must be keept > just for compilation reason (to be able to re-analyse code > resulting from the slicing pulgin). These kinds of lines have > a spare mark. Going back to your example, the spare > mark of the line 24 is /imprecise/, but /correct. > > /Patrick. > > I printed out slicing-marks by using -slicing-debug "-debug 2" option, and found that line 24's is [---][ S ]. Is this what you meant by "/imprecise/ ,but /correct?" Certainly all marks of relevant (to be more precise) statements contained at least one character inside the first brackets (one exception was that of slicing criterion line. It was [ S ][---]). This information might be used to filter out imprecise statements I think. If this understanding is not correct, please let me know. > The only workaround that we can offer for the moment is to slice again > on the same criterion a second time: > > frama-c -lib-entry -slice-pragma main -slice-print -quiet t.c > -calldeps -ocode t2.c > frama-c -lib-entry -slice-pragma main -slice-print -quiet t2.c -calldeps > > This removes anything related to s2t_1. > > We will look at the behavior you have reported. > > Pascal > Thank you for your comments on PDGs, and a possible workaround. I tested it and confirmed it worked. Slicing twice or referring the slicing-marks might be two alternative solutions to the issue I think. Thank you. Myung-Jin