--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Global kernel could not find entry point: main



Hello,

> What does the error message shown below imply?

> Global kernel could not find entry point: main

You are trying to use the value analysis with its default settings
on a collection of C file which do not contain any "main" function.

The value analysis works best either for complete applications,
or for libraries or subsets of an application for which you are
ready to write a functions that describes the values of globals
and pattern for calling the functions. You can find an example of
this process in the tutorial which is part of the value analysis
manual:

http://frama-c.cea.fr/download/value-analysis-Beryllium-20090902.pdf

A more lightweight way to use the value analysis is to let it construct
values for globals from their types. This works well for simple
functions that manipulate scalar types, and you still need to give
hints what the memory should look like if you have recursive types
or otherwise deeply linked data structures.

In this case, you would use the options -lib-entry -main f where f is the
function you are interested in, and you may need to use the option
-context-depth, -context-width and -context-valid-pointers to
describe the shape for the memory structures. Here is a discussion of
these options, in addition to what is in the manual:

http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2008-August/000588.html

Pascal