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] Global kernel could not find entry point: main

  • Subject: [Frama-c-discuss] Global kernel could not find entry point: main
  • From: Pascal.CUOQ at (CUOQ Pascal)
  • Date: Fri, 20 Nov 2009 14:57:24 +0100
  • References: <1D0F31F3F3ABA947B3B4FAD31A6565624AC5A6EDCE@antunes6.antunes.local>


> 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

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: