Static Contract Checking with Abstract Interpretation

摘要: We present an overview of Clousot, our current tool to statically check CodeContracts. CodeContracts enable a compiler and language-independent specification Contracts (precondition, postconditions object invariants). Clousot checks every method in isolation using assume/guarantee reasoning: For each under analysis Clousot assumes its precondition asserts the postcondition. invoked method, also absence common runtime errors, such as null-pointer buffer or array overruns, divisions by zero, well less ones checked integer overflows floating point precision mismatches comparisons. At core there is abstract interpretation engine which infers program facts. Facts are used discharge assertions. The use (vs usual weakest precondition-based checkers) has two main advantages: (i) checker automatically loop invariants letting user focus only on boundary specifications; (ii) deterministic behavior (which abstractly mimics flowof program) it can be tuned for cost. embodies other techniques, iterative domain refinement, goal-directed backward propagation, postcondition inference, message prioritization.