Contents

• Kleaver usage
• Parsing
  • Optimize parsing in case of independent queries
• Solver
• Query Logging

Kleaver usage

$ kleaver [options] <input query log>

In particular, <input query log> must be a file containing a query in KQuery format. To get a complete list of Kleaver’s command-line options run: kleaver --help

The remainder of this page illustrate Kleaver’s distinctive command-line options.

Parsing

Kleaver parses the input query log assuming the most general definition of the KQuery format. A KQuery source file consists of a sequence of declarations:

kquery = { array-declaration | query-command }

In particular, the set of array declarations can be used in several distinct queries.

Optimize parsing in case of independent queries

An input query log may contain independent queries, that is query declarations that immediately follow their own array declarations. For instance, KLEE logs the queries issued to the solver as a list of independent queries. In this scenario, it is possible to optimize Kleaver runtime to substantially reduce its memory footprint by running Kleaver with the option -clear-array-decls-after-query. For example:

$ kleaver --clear-array-decls-after-query=true klee-queries.kquery

Solver

Kleaver can leverage several backend SMT solvers to compute the query see Solver Chain for details.

Query Logging

To log the queries issued by Kleaver to the underlying solver see Solver Chain for details.

To select where to store the log, you can use the -query-log-dir option. The default value is the current working directory. For example:

$ kleaver --query-log-dir=kleaver-log query.kquery