I agree. It depends on what subset of C and C++ is used. If macros are used the only way to actually verify the code will be to pre-process it. Worse is if templates are used. Some templates don't even finish compiling.
Most likely no one will write such a template in a mission critical system. However, from a formal verification standpoint the only way to verify the code is to check the binaries.
http://cpptruths.blogspot.com/2005/11/c-templates-are-turing...
Most likely no one will write such a template in a mission critical system. However, from a formal verification standpoint the only way to verify the code is to check the binaries.