model-checking
How to prove a static (file scope) function using the starter kit?
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?
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
Where is that name-mangling documented? I couldn't find it in the user manual...
it's in the goto-cc manpage https://github.com/diffblue/cbmc/blob/95f5db1f0730ab5abc970b7d798f60a65f8167df/doc/man/goto-cc.1#L74
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