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 (Pascal Cuoq)
  • Date: Fri, 20 Mar 2009 10:49:38 +0100
  • In-reply-to: <1237402185.3508.226.camel@supelec>
  • References: <1237387890.3508.114.camel@supelec> <49C116F4.5050507@sophia.inria.fr> <1237402185.3508.226.camel@supelec>
>
>
> That's why I want to assume a 'worst case scenario' and add all the
> statements that statement 2 depends on to the dependencies of  
> statement
> 4. (because Db.Pdg.all_dpds stops at the OutRet and InCtrl nodes of
> statement 2)


Two remarks :

1/ To reiterate what Anne was saying, it doesn't make sense to
use different assumptions for the different computations that are
taking place (i.e. the value analysis and the PDG). Using a
worst case scenario for the library function at the time of
exploiting the PDG is a bad idea because the value analysis
already made some assumptions, that may have been more
optimistic, about the library function, and the PDG uses the
results of the value analysis (and therefore depends on its
assumptions) everywhere else in the analyzed program.

The right way is to have every plug-in agree on the same
specification for the library function. If the default specification
generated for a library function when none is present is not to
your liking, and if it's not practical for you to write specifications
for all the library functions in your analysis project, please tell
us how these specifications should have been generated
automatically and we will see what we can do.

2/ The real worst-case scenario is when your library function
overwrites every global in memory -- actually, any reachable cell.
Needless to say, the value analysis can not possibly
say anything interesting after the call if it has to assume this.
What exactly do you mean by "worst-case scenario"?
Considering the dependencies that you would like to get,
it seems that you mean that the
library function may access any reachable cell but not
write any. Is that it?

Regards,

Pascal