It is not clear what you mean by 'still it remains unreachable'.
Do you mean that the body of the function is not analyzed at all? That is expected behavior if a function is stubbed. I am not sure I understood the question well, so I am explaining how stubbing works and maybe you will have your answer here.
If a function is stubbed by Polyspace, it means that somehow Polyspace did not find the function definition in the files given to the analysis. If the function is a standard function, say, a standard library function, then Polyspace will correctly emulate its effect, and when you call the function, you will see a precise result as if Polyspace had the function definition. If the function is a user-defined one, then Polyspace has no way of knowing what the function actually does. Then, Polyspace has to make the best assumptions possible from the function signature.
In all these cases, if the function definition actually exists and Polyspace just did not happen to find the definition, the function will not be reachable. In other words, the function body will look black (no greens/oranges/greys), indicating that it was not verified. The situation where a function definition actually exists and Polyspace still cannot find it is rare. For instance, it might happen if you call a function through several layers of function pointers and Polyspace cannot resolve a call through a function pointer to an actual function.
However, in your case, this is what seems to be happening (or is it?). You probably have the function definitions, but Polyspace seems to not find them and uses stubs instead (if a stub is used, that itself means that the function definition was not found and it is not reachable). If this is indeed the case, we have to understand why.
You say that you are using the option Verify module or library (-main-generator) but does your code have a main function? In that case, it might simply mean that somehow Polyspace cannot find a path starting from the main to the unverified function bodies.