--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on February 2011 ---
Hello, On Tue, Feb 8, 2011 at 1:28 PM, Daniel Sheridan <djs at adelard.com> wrote: > I notice that Cil includes an inter-procedural points-to analysis which > I've found quite useful. I would like to make use of the results of the > analysis in a Frama-C plugin that I am writing, but the module isn't > included in the Frama-C version of Cil. Yes, there was a big clean-up of (our forked version of) CIL at some point. We removed everything we didn't use so as to make all the changes we needed and will need to do in CIL easier. We do not have anything against that analysis and would be glad to see it available as a Frama-C plug-in. It would definitely be a plus to have this option to resolve pointers when writing another plug-in. I may be mistaken, but I think the developers of the STAC plug-in at Grenoble may already have a points-to analysis. I'll let them talk about it if they think it may match your needs. > I prefer not to use the value analysis plugin in this case, as it is > significantly slower and reports large quantities of dead code (mostly > due to variables that should be declared volatile). Yes, we have also noticed that while it is, to the best of our knowledge, correct, the value analysis' aggressive research of precision means on some programs that some behaviors are left out; missing "volatile" attributes in the target code are a typical example. Less precise analyses have an easier job of capturing all the intended behaviors. In some cases, this could be solved in an ad-hoc fashion, for instance if there was a way to recognize automatically that a variable should be treated as volatile (e.g. for a program where all globals should be treated as volatile, or when the variable's name matches a provided regular expression). Pascal