Rezumat articol ediţie STUDIA UNIVERSITATIS BABEŞ-BOLYAI

În partea de jos este prezentat rezumatul articolului selectat. Pentru revenire la cuprinsul ediţiei din care face parte acest articol, se accesează linkul din titlu. Pentru vizualizarea tuturor articolelor din arhivă la care este autor/coautor unul din autorii de mai jos, se accesează linkul din numele autorului.

 
       
         
    STUDIA INFORMATICA - Ediţia nr.2 din 2018  
         
  Articol:   AN INITIAL PROTOTYPE OF TIERED CONSTRAINT SOLVING IN THE CLANG STATIC ANALYZER.

Autori:  RÉKA KOVÁCS, GÁBOR HORVÁTH.
 
       
         
  Rezumat:  
DOI: 10.24193/subbi.2018.2.06

Published Online: 2017-06-19
Published Print: 2017-06-29
pp. 88-101
VIEW PDF: An Initial Prototype of Tiered Constraint Solving in the Clang Static Analyzer

Abstract. Static analysis is a widely used method for finding bugs in large code bases. One of the most popular static analysis tools used for software written in C/C++ languages is the Clang Static Analyzer [1]. During symbolic execution [2] of the source code, the analyzer models path sensitivity by keeping track of constraints on symbolic variables. The built-in constraint manager module, while granting excellent performance, only handles constraints on certain types of integer expressions, which has a detrimental effect on the quality of the analysis, as the infeasibility of certain execution paths cannot be proved. This often leads to false positive findings, i.e. error reports issued for code parts that are actually correct.
This paper records the first milestone in an effort to integrate the state-of-the-art Z3 theorem prover [3] into the Clang Static Analyzer in order to post-process bug reports. While full integration is hindered by the burden Z3 places on the duration of the analysis, the refutation of false positive reports using information collected by the default pass can improve analysis quality substantially while introducing only a moderate regression in performance. We present an initial prototype of the tiered constraint solving solution that is already capable of filtering out some bogus reports, evaluate it on real-world software projects, and explore possible improvements we plan to accomplish in our future work.
2010 Mathematics Subject Classification. 68N20.
1998 CR Categories and Descriptors. F.3.2 [Logics and meanings of programs]: Semantics of Programming Languages - Program analysis.
Key words and phrases. Static analysis, symbolic execution, Clang, SMT solver.
 
         
     
         
         
      Revenire la pagina precedentă