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] Value analysis manual: questions and remarks

  • Subject: [Frama-c-discuss] Value analysis manual: questions and remarks
  • From: Julien.Signoles at cea.fr (Julien Signoles)
  • Date: Mon, 10 Jan 2011 16:45:11 +0100
  • In-reply-to: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com>
  • References: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com>
Hello David,

Le 10/01/2011 15:18, David MENTRE a ?crit :
>   * [more a feature wish] The Call-graph displayed on a non trivial
> example (ex. skein example of the manual) by a call to Analyses->Show
> callgraph is unreadable (spaghetti of boxes and arrows). I think it
> would be better to display it in text form with references, for
> example as done by GNU cflow;

IMHO displaying a big graph which remains fully readable is quite an 
impossible task. As Pascal said, we try to improve this feature from 
version to version, but it is still not perfect.

Nevertheless I would not say that the skein's callgraph is unreadable: I 
never read the Skein source code, but just by reading the syntactic 
callgraph and so-called services quickly (one or two minutes, I discover 
the following things about Skein:
- there is a main named "main"
- there are two major sets of functions (called "services" in Frama-C): 
one set in which the root is the function "hash" and another in which 
the root is the function "initial_updates"
- all the other functions which are not in these services and which are 
not the main should not be so important (e.g. they could be library 
functions): I could just skip it for a first reading
- for the first major service, the name "hash" seems to indicate that 
the function "hash" is the most important function for skein (I don't 
know the code, but I know what Skein is expected to do)
- that is quite strange that the hash function is never called: I guess 
that there is a function pointer somewhere that the syntactic callgraph 
does not handle: if I have to analyse Skein in details, I would check 
this point first (I could use the semantic callgraph for this purpose 
but I didn't).
- for the second major service, the name "initial_updates" seems to 
indicate that this function initializes something: clicking on the name 
shows all the other functions of this service: the name of its internal 
functions are mostly of the form "Frama_C_*": I can now confirm that 
"initial_updates" initializes the context of the value analysis plug-in.

@Pascal or someone else who know the skein's code: am I wrong somewhere?

To conclude, I agree that it is certainly possible to display a more 
readable callgraph, but I don't agree that it is not readable at all. I 
also agree that there is no manual for the syntactic callgraph at this 
day and that there is no way to display the callgraph in text form. If 
you think that one of both features is useful, please feel free to add a 
feature wish on the BTS (bts.frama-c.com).

Hope this helps and thanks for your feedback,
Julien