Overview of Kleaver’s main command-line options
<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:
The remainder of this page illustrate Kleaver’s distinctive command-line options.
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:
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 can leverage several backend SMT solvers to compute the query see Solver Chain for details.
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: