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] ask for slicing spec


  • Subject: [Frama-c-discuss] ask for slicing spec
  • From: anne.pacalet at sophia.inria.fr (Anne Pacalet)
  • Date: Thu, 01 Oct 2009 09:37:10 +0200
  • In-reply-to: <e4a09de30909291928h160a4460g51f8882e22480611@mail.gmail.com>
  • References: <e4a09de30909251853i52e44551t4681529738e60642@mail.gmail.com> <4AC06533.4090803@sophia.inria.fr> <e4a09de30909280926x2ff7a0c6t11ed1a3a8bc72282@mail.gmail.com> <4AC1B340.7020904@sophia.inria.fr> <e4a09de30909291928h160a4460g51f8882e22480611@mail.gmail.com>

jun shen a ?crit :
> I am interested in the details of slicing, because I might do some
> academic work above Frama-C and I have to make sure that the
> foundation is what I expected.

Interesting. Maybe you can tell us a bit more about the subject
you are working on ?

> By the way, can you send me the document now? It doesn't matter that
> it is in French.

In fact, after a short discussion with the team, it appears that
this document is not distributed with Frama-C because
it doesn't reflect the status of the implementation...
It is rather a preliminary document that was made to decide what to do.

Sorry that there is no detailed documentation about the implementation,
but I would be happy to answer to your questions if I can.

> My question is whether you have implemented Susan Horwitz's PDG
> algorithm described in her paper. And what are the differences between
> your pdg and hers?

If I remember well, the PDG is similar to Horwitz one, except
for the inter-procedural part, because to handle the function calls,
the PDG uses the result of another dependence analysis.
You can see the results of this other analysis by using
the -deps option of frama-c.

Moreover, I don't know if you have seen that you can see the PDG
of a function ? If not, you can have a look at an answer
I have ealier made on the list :
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-September/001403.html

Hope this will help,
-- 
Anne.