We are using C to build a system on ARM core (i.e. an embedded system). The question is: how can we avoid reentry problem in a formal way so that we are confident all reentry bugs are removed. This may not be a practical wish but surely important for any system, I guess.
Just for the discussion, I guess drawing UML diagram or have a complete state machine would be a good start (but how to generate it AFTER the whole system is developed?). Any suggestions on how to use state machine / UML diagram to do the analysis?
I'm not exactly sure about the problem you want to solve, but let me make an educated guess.
The first point is to identify the functions that could be problematic. A reentry happens either by recursive calls, which may go over several nested calls and even be hidden by callbacks/dependency injection, or by functions that are used within multiple threads.
You could draw a directed call graph. Say function A calls B and C, function B calls D, E and F, function C calls nothing, and so on. Draw this for each thread when multithreading. If there are cycles in the graph, then all functions making this cycle need to be reentry-safe. You can ignore subbranches in this case. Functions that are used in multiple threads need to be safe, too, but now including all subbranches, because you do not exactly know where each thread currently is. Things will get complex and complicated when locks are used, so let us ignore this for now.
This step can surely be automated by code analysis tools.
Now that the functions are identified,