--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on January 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis manual: questions and remarks



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