Separation logic is a program logic for reasoning about programs that manipulate pointer data structures. We describe a tool, Smallfoot, for checking certain separation logic specifications. The assertions describe the shapes of data structures rather than their detailed contents, and this allows reasoning to be fully automatic. We illustrate what the tool can do via a sequence of examples which are oriented around 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.