The complex approach of the C-lightVer system to the automated error localization in C-programs

The C-lightVer system for the deductive verification of C programs is being developed at the IIS SB RAS. Based on the two-level architecture of the system, the C-light input language is translated into the intermediate C-kernel language. The meta generator of the correctness conditions receives the C-kernel program and Hoare logic for the C-kernel as input. To solve the well-known problem of determining loop invariants, the definite iteration approach was chosen. The body of the definite iteration loop is executed once for each element of the finite dimensional data structure, and the inference rule for them uses the substitution operation rep, which represents the action of the cycle in symbolic form. Also, in our meta generator, the method of semantic markup of correctness conditions has been implemented and expanded. It allows to generate explanations for unproven conditions and simplifies the errors localization. Finally, if the theorem prover fails to determine the truth of the condition, we can focus on proving its falsity. Thus a method of proving the falsity of the correctness conditions in the ACL2 system was developed. The need for more detailed explanations of the correctness conditions containing the replacement operation rep has led to a change of the algorithms for generating the replacement operation, and the generation of explanations for unproven correctness conditions. Modifications of these algorithms are presented in the article. They allow marking rep definition with semantic labels, extracting semantic labels from rep definition and generating description of break execution condition.