Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Automated Technology for Verification and Analysis

ATVA 2015: Automated Technology for Verification and Analysis pp 97–113Cite as

Severity Levels of Inconsistent Code

  • Conference paper
  • First Online:

  • 900 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9364))

Abstract

Inconsistent code detection is a variant of static analysis that detects statements that never occur on feasible executions. This includes code whose execution ultimately must lead to an error, faulty error handling code, and unreachable code. Inconsistent code can be detected locally, fully automatically, and with a very low false positive rate. However, not all instances of inconsistent code are worth reporting. For example, debug code might be rendered unreachable on purpose and reporting it will be perceived as false positive.

To distinguish relevant from potentially irrelevant inconsistencies, we present an algorithm to categorize inconsistent code into (a) code that must lead to an error and may be reachable, (b) code that is unreachable because it must be preceded by an error, and (c) code that is unreachable for other reasons. We apply our algorithm to several open-source project to demonstrate that inconsistencies of the first category are highly relevant and often lead to bug fixes, while inconsistencies in the last category can largely be ignored.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    E.g., the violation of an assertion or a (user-provided) safety property. The concrete definition of error depends on the tool.

References

  1. Arlt, S., Rümmer, P., Schäf, M.: Joogie: From java through jimple to boogie. In: SOAP (2013)

    Google Scholar 

  2. Arlt, S., Schäf, M.: Joogie: infeasible code detection for java. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 767–773. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Ayewah, N., Pugh, W., Morgenthaler, J.D., Penix, J., Zhou, Y.: Evaluating static analysis defect warnings on production software. In: PASTE (2007)

    Google Scholar 

  4. Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., M. Leino, K.R.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. In: TOPLAS (1991)

    Google Scholar 

  6. Dillig, I., Dillig, T., Aiken, A.: Static error detection using semantic inconsistency inference. In: PLDI (2007)

    Google Scholar 

  7. Engler, D., Chen, D.Y., Hallem, S., Chou, A., Chelf, B.: Bugs as deviant behavior: A general approach to inferring errors in systems code. In: SOSP (2001)

    Google Scholar 

  8. Fry, Z.P., Weimer, W.: Clustering static analysis defect reports to reduce maintenance costs. In: WCRE (2013)

    Google Scholar 

  9. Heckman, S., Williams, L.: On establishing a benchmark for evaluating static analysis alert prioritization and classification techniques. In: ESEM (2008)

    Google Scholar 

  10. Hoenicke, J., Leino, K.R., Podelski, A., Schäf, M., Wies, T.: Doomed program points. In: FMSD (2010)

    Google Scholar 

  11. Hovemeyer, D., Pugh, W.: Finding more null pointer bugs, but not too many. In: PASTE (2007)

    Google Scholar 

  12. Janota, M., Grigore, R., Moskal, M.: Reachability analysis for annotated code. In: SAVCBS (2007)

    Google Scholar 

  13. Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6) (2005)

    Google Scholar 

  14. Leino, K.R.M., Millstein, T., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Sci. Comput. Program. 55(1–3), 209–226 (2005)

    Google Scholar 

  15. Livshits, B., Sridharan, M., Smaragdakis, Y., Lhoták, O., Amaral, J.N., Chang, B.-Y.E., Guyer, S.Z., Khedker, U.P., Møller, A., Vardoulakis, D.: In defense of soundiness: A manifesto. In: CACM, vol. 56(1), February 2015

    Google Scholar 

  16. McCarthy, T., Rümmer, P., Schäf, M.: Bixie: Finding and understanding inconsistent code (2015). http://www.csl.sri.com/bixie-ws/

  17. Rümmer, P.: A constraint sequent calculus for first-order logic with linear integer arithmetic. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 274–289. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  18. Tomb, A., Flanagan, C.: Detecting inconsistencies via universal reachability analysis. In: ISSTA (2012)

    Google Scholar 

  19. Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co., P.: Soot - a Java Optimization Framework. In: CASCON (1999)

    Google Scholar 

  20. Wang, X., Zeldovich, N., Kaashoek, M.F., Solar-Lezama, A.: Towards optimization-safe systems: analyzing the impact of undefined behavior. In: SOSP (2013)

    Google Scholar 

Download references

Acknowledgement

This work was supported in part by the National Science Foundation under grant contracts CCF 1423296 and CNS 1423298, and DARPA under agreement number FA8750-12-C-0225.

Author information

Authors and Affiliations

  1. SRI International, Menlo Park, CA, 94025, USA

    Martin Schäf & Ashish Tiwari

Authors
  1. Martin Schäf
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ashish Tiwari
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Martin Schäf or Ashish Tiwari .

Editor information

Editors and Affiliations

  1. Universität des Saarlandes, Saarbrücken, Germany

    Bernd Finkbeiner

  2. East China Normal University, Shanghai, China

    Geguang Pu

  3. Chinese Academy of Sciences, Beijing, China

    Lijun Zhang

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Schäf, M., Tiwari, A. (2015). Severity Levels of Inconsistent Code. In: Finkbeiner, B., Pu, G., Zhang, L. (eds) Automated Technology for Verification and Analysis. ATVA 2015. Lecture Notes in Computer Science(), vol 9364. Springer, Cham. https://doi.org/10.1007/978-3-319-24953-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-24953-7_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-24952-0

  • Online ISBN: 978-3-319-24953-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation