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] Points-to analysis

  • Subject: [Frama-c-discuss] Points-to analysis
  • From: djs at adelard.com (Daniel Sheridan)
  • Date: Tue, 08 Feb 2011 12:28:19 +0000
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