Automatic Contract Insertion with CCBot

作者：Carr Scott A^*; Logozzo Francesco; Payer Mathias

来源：IEEE Transactions on Software Engineering, 2017, 43(8): 701-714.

DOI：10.1109/TSE.2016.2625248

• Contract-based verification
• automated patching
• assertions
• class invariants

Existing static analysis tools require significant programmer effort. On large code bases, static analysis tools produce thousands of warnings. It is unrealistic to expect users to review such a massive list and to manually make changes for each warning. To address this issue we propose CCBot (short for CodeContractsBot), a new tool that applies the results of static analysis to existing code through automatic code transformation. Specifically, CCBot instruments the code with method preconditions, postconditions, and object invariants which detect faults at runtime or statically using a static contract checker. The only configuration the programmer needs to perform is to give CCBot the file paths to code she wants instrumented. This allows the programmer to adopt contract-based static analysis with little effort. CCBot's instrumented version of the code is guaranteed to compile if the original code did. This guarantee means the programmer can deploy or test the instrumented code immediately without additional manual effort. The inserted contracts can detect common errors such as null pointer dereferences and out-of-bounds array accesses. CCBot is a robust large-scale tool with an open-source C# implementation. We have tested it on real world projects with tens of thousands of lines of code. We discuss several projects as case studies, highlighting undiscovered bugs found by CCBot, including 22 new contracts that were accepted by the project authors.

• 出版日期2017-8-1