Smallfoot: Modular Automatic Assertion Checking with Separation Logic

Abstract

Separation logic is a program logic for reasoning about programs that manipulate pointer data structures. We describe Smallfoot, a tool for checking certain lightweight separation logic specifications. The assertions describe the shapes of data structures rather than their detailed contents, and this allows reasoning to be fully automatic. The presentation in the paper is tutorial in style. We illustrate what the tool can do via examples which are oriented toward novel aspects of separation logic, namely: avoidance of frame axioms (which say what a procedure does not change); embracement of "dirty" features such as memory disposal and address arithmetic; information hiding in the presence of pointers; and modular reasoning about concurrent programs.