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: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Mon, 10 Jan 2011 17:00:55 +0100
  • In-reply-to: <4D2B2987.1030401@cea.fr>
  • References: <AANLkTi=AOF2nkFeK8SUWNBFCdDzi8WMoOBE34GSmyo8Q@mail.gmail.com> <4D2B2987.1030401@cea.fr>
> - 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"

I was trying to maintain an aura of never having looked at the code of
Skein although I verified some basic properties about it. Nevertheless,
since Julien forces me:

There are two APIs for the same library. One is used directly by the main()
function from the tutorial, and this is why the functions in this API appear
as sub-services of service main().

The other API has a single function that does all the work. From file
SHA3api_ref.c:

/* all-in-one hash function */
HashReturn Hash(int hashbitlen, const BitSequence *data, /* all-in-one call */
                DataLength databitlen,BitSequence *hashval)

This means that:

- the functions Init, Update and Final in the second API appear
as sub-services of Hash, since they are called by Hash().

- Hash appears as one of the main services of the library, using
others but not used by others. This classification is only heuristic.
Other functions of the library may be intended to be called directly.
But indeed, Julien has correctly inferred, based on the shape of
the call graph, that Hash is one of the high-level functions in the
library.

> - 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

This is only because the library has two alternative APIs and my
main() function only uses one.

Pascal