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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Tue, 8 Feb 2011 16:23:06 +0100
  • In-reply-to: <1297168099.2827.102.camel@coquet>
  • References: <1297168099.2827.102.camel@coquet>
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