Kontrol Prove Flags
Flag | Description |
---|---|
| Show this help message and exit |
| Verbose output. |
| Debug output. |
| Number of processes to run in parallel. |
| Directories to lookup K definitions in. |
| Name of the main module. |
| Name of the syntax module. |
| Code selector expression to use when reading markdown. |
| Maximum depth to execute to. |
| Path to definition to use. |
| Comma-separate list of equations to debug. |
| Check subsumption even on non-terminal nodes (default, experimental). |
| Do not check subsumption on non-terminal nodes (experimental). |
| Use fast-check on k-cell to determine subsumption (experimental). |
| Timeout in ms to use for SMT queries. |
| Number of times to retry SMT queries with scaling timeouts. |
| Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt) |
| Log traces of all simplification and rewrite rule applications. |
| Custom command to start RPC server. |
| Use the booster RPC server instead of kore-rpc (default). |
| Do not use the booster RPC server instead of kore-rpc. |
| Use existing RPC server on named port. |
| Use existing Maude RPC server on named port. |
| Generate bug report with given name |
| Store a node for every EVM opcode step (expensive). |
| Store a node for every EVM jump opcode. |
| Store a node for every EVM call made. |
| Do not store a node for every EVM call made (default). |
| Store a node for every EVM SSTORE/SLOAD made. |
| Store a node for every EVM basic block (implies --break-on-calls). |
| Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier. |
| Number of times to expand the next pending node in the CFG. |
| Show failure summary for all failing tests (default). |
| Do not show failure summary for failing tests. |
| Automatically extract gas cell when infinite gas is enabled. |
| Show models for failing nodes (default). |
| Stop execution on other branches if a failing node is detected (default). |
| Continue execution on other branches if a failing node is detected. |
| Path to Foundry project root directory. |
| Specify contract function(s) to test using a regular expression. This will match functions based on their full signature, e.g., 'ERC20Test.testTransfer(address,uint256)'. This option can be used multiple times to add more functions to test. |
| Reinitialize CFGs even if they already exist. |
| Enables bounded model checking. Specifies the maximum depth to unroll all loops to. |
| Include the contract constructor in the test execution. |
| Enables gas computation in KEVM. |
| Break on all Foundry rules. |
| Path to JSON file containing the deployment state of the deployment process used for the project. |
| Specify a summary to include as a lemma. |
| Flag used by Simbolik to initialise the state of a non test function as if it was a test function. |
| Generate a JUnit XML report |
| Use Compositional Symbolic Execution |
| Use hevm success predicate instead of foundry to determine if a test is passing. |
Last updated