Maximal employment of formal and sound methods is one of the distinctive features of C-light project. This concerns not only the fundamental verification bases, like Plotkin's operational semantics or Hoare's logics, but also implementation aspects. The localization of possible errors is one of them. In the majority of known verification systems such localization is simply coded by developers as a part of system functionality without any formal basis for it. The recent reinforcement of the C-light project by the semantical labeling technique and the choice of LLVM/Clang for the system input block allowed us to obtain some new results, which are surveyed in this paper.