--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Points-to analysis



Hi,

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. 

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).

Has the points-to analysis been excluded for a particular reason, and
could it be re-incorporated? Or is there something already in Frama-C
that does the same job? Or would it be better to port it to a proper
Frama-C plugin? I may do this myself if there is general interest in it.

	Dan.

-- 
Dan Sheridan (djs at adelard.com), Adelard LLP
College Building, 10 Northampton Square, London EC1V 0HB
Tel: +44 20 7490 9455 Fax: +44 20 7490 9451
Web: www.adelard.com