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] Getting a node from its id for a particular pdg

  • Subject: [Frama-c-discuss] Getting a node from its id for a particular pdg
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Wed, 18 Mar 2009 18:58:56 +0100
  • References: <1237387890.3508.114.camel@supelec>
Greetings,

Please find in this e-mail the answer to a 
different but perhaps related question, and
a remark concerning node ids.

> Let's consider this simple piece of C code:
> 1.	b += z;
> 2.	c = toto(b,a);
> 3.	c++;
> 4.	e = toto(c,a);

There was earlier on this list someone who wanted 
dependencies like this : for a variable y and
a program point, the list of variables that have served
to compute the value of y at that point.

This is almost the same thing that options -deps
and -calldeps compute, but not quite because
-deps and -calldeps  do not include in the dependency list
the variables that participate in the computation but have
certainly been overwritten with something different
from their initial value at the time they do, or the
variables that have served to compute a value for y
that was not the final one.

If this is not what you are trying to compute, disregard
this part of my reply. But if this is what you are trying to
compute, you "can" transform the "from" plug-in into a
plug-in that computes just that, with the attached patch.

An example:
void main () {
  T1= T3[3];
  T2= T4[3];
  T1= T5[1];
  T2= T6[1];
}

Function main:
  T1 FROM T3[3]; T5[1]; (and default:true)
  T2 FROM T4[3]; T6[1]; (and default:true)

Now, by 'you "can"', I mean that you can't, because
you would be changing the behavior of a plug-in
that is used by other plug-ins, with an already
defined interface. This would break Frama-C,
even for you, because you might be using 
computations that rely on the current behavior
of options -deps or -calldeps without realizing it.

But nothing prevents you from
making your own plug-in which is exactly identical
to the from plug-in except for the name, 
command-line options, and for the four lines that
make it compute the slightly different dependencies.
See the plug-in development guide for a list of
what you need to change to let your plug-in 
coexist with the existing "from" plug-in. Off the top
of my head, you may need to copy the directory src/from
to a different name, rename the From.* files
inside the directory, change the Makefile, rename the
command-line options, duplicate the "From" section
in db.ml and change the name there too.

> So, within the dependencies of a particular statement, when I find a
> node the key match 'PdgIndex.Key.SigCallKey (_,PdgIndex.Signature.Out
> PdgIndex.Signature.OutRet)', I add the dependencies of the nodes with
> the ids (id-1) and (id-2), with id the elem_id of the matched node (I'm
> not sure I'm clear... ^^).

My colleagues may not have picked up the fact that you seemed
to be relying on numbering conventions for the Pdg nodes
to get what you wanted. If they had, I am sure that they would
have advised against doing this.

And because they are more knowledgeable
than me, they would have recommended a better way to get the
nodes you are interested in than just subtracting a constant from
the id of the node you are currently on.

Pascal
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: deps_add_and_remember
Type: application/octet-stream
Taille: 680 octets
Desc: deps_add_and_remember
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090318/e6285062/attachment.obj