Call graph verification plugin in Frama-C?

I'm working in a project where we are interested in verifying simple control flow properties of C code.

As a first problem, we want to check that a C program conforms to a "white list" of functions that the program is allowed to call. In the following minimalistic example, say that the white list is {bar}, then the program is OK.

Note that we want to separate between the "internal" call to main and the "external" one to bar.

extern void bar();

void main() {
  foo();
}

void foo() { 
  bar();
}

Is there an off-the-shelf solution in Frama-C for this? I noticed that Aorai deals with call sequence verification. But maybe there is another plugin for the simple kind of call graph analysis that we are interested in?

MetAcsl and more specifically its \calling context allows you to define properties (called HILAREs in MetAcsl's context) that will be checked at any call site. However, if I understand your question correctly, you can't use MetAcsl as such, since the corresponding HILARE is not simply \called == bar, but something like \called \in { DEFINED_FUNCTIONS } \union { bar } (ignoring typing issues for now), and there's nothing to represent the set of all defined functions there. Writing a tiny plug-in to generate this set should be fairly easy, but I'm afraid that nothing exists on the shelves.

Another possibility is to use the Callgraph plug-in, but it only outputs graphs in the dot format, you'll have to do some post-processing on the resulting graph.