Introduction

BANSHEE is a toolkit that simplfies the task of building constraint-based program analyses. Program analyses are widely used in compilers and software engineering tools for discovering or verifying specific properties of software systems, such as type safety and opportunities for program optimization. To use BANSHEE, the analysis designer provides a short specification file describing the kinds of constraints used in the analysis. From this specification, BANSHEE builds a customized constraint resolution engine which solves those constraints very efficiently. BANSHEE also builds a customized interface for that engine which is easy to use.

BANSHEE is the successor to BANE, the Berkeley ANalysis Engine, which is no longer supported.

Example Applications

Here are a few of the program analyses we have built using BANSHEE:

Pointer Analysis: We have implemented Andersen's points-to analysis in BANSHEE, achieving orders of magnitude improvement over BANE. Our implementation of Andersen's analysis uses a C front-end derived from GCC and is therefore distributed under the GNU General Public License.
CFL Reachability: We have implemented an API for solving context-free language reachability problems with BANSHEE. This API can be used for a large class of program analyses including polymorphic flow analysis, interprocedural dataflow analysis, and field-sensitive points-to analysis.

Download

Current version: 1.02

banshee-1.02.tar.gz

BANSHEE is available for download under the BSD License. The code has been tested under various versions of RedHat Linux and Windows with Cygwin. The pointer analysis application, which includes a C parser derived from GCC, is also included and is released under the GNU General Public License.

Subversion access is managed through SourceForge. For svn access, please look here.

This page is maintained by John Kodumal (jkodumal AT cs.berkeley.edu)