README.md
1<!--
2 Copyright 2017, Data61
3 Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 ABN 41 687 119 230.
5
6 This software may be distributed and modified according to the terms of
7 the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 See "LICENSE_BSD2.txt" for details.
9
10 @TAG(DATA61_BSD)
11-->
12# Prune
13
14This is a tool for removing excess functions from C code. It is possible to
15dramatically reduce the runtime of the C parser and friends (and your
16resulting find_theorems search space) by removing functions you are not
17calling before parsing.
18
19## Usage
20
21You will need the libclang and glib headers available to build this. I have not
22located a packaged version of libclang and LLVM that work together, so I
23recommend you build these from source as described on the
24[Clang getting started page](http://clang.llvm.org/get_started.html). I have
25successfully built this tool using r207601 of all the LLVM pieces.
26
27Run `prune --help` for options. For anything more, read the source code.
28
29## Caveats
30
31No attempt is made to automatically prune anything other than functions. Other
32entities don't cost us much in parsing. If you do want to explicitly prune
33other things you can use the `--blacklist` option.
34
35Some tricky C is clever enough to even baffle Clang (e.g. seL4_IPCBuffer
36alignment). Report anything serious, but minor issues like this will have to be
37worked around yourself.
38
39## Issues
40
41Email Matthew Fernandez with questions or problems.
42