How to prove a static (file scope) function using the starter kit?

[rod-chapman]

I have a translation unit in f.h and f.c, all set up for proof using contracts and the starter kit.

f.c contains a static (file scope) function that I want to prove. How do I get that to work with the starter kit, which seems to insist on putting my test harness function in a separate translation unit, so the function I want to prove is not visible from the point of view of the harness?

@feliperodri mentioned that static functions get name-mangled by CBMC... is there some trick here that I'm not aware of? Where is this documented?

[remi-delmas-3000]

By default static symbols are exported with a prefix __CPROVER_file_local + filename + symbol_name:

For instance:

// in file bar.c
static int foo(int)
{
   ...
}

can be referred to as __CPROVER_file_local_bar_c_foo in the proof harness.

Another way is to activate the crangler rewriting pass in the proof Makefile as explained here in Makefile.common

[rod-chapman]

Where is that name-mangling documented? I couldn't find it in the user manual...

[remi-delmas-3000]

it's in the goto-cc manpage https://github.com/diffblue/cbmc/blob/95f5db1f0730ab5abc970b7d798f60a65f8167df/doc/man/goto-cc.1#L74

[rod-chapman]

That info (and an example of how to do it) really needs to be in here somwhere: https://diffblue.github.io/cbmc/user_guide.html