Kratos2 Configuration Options

Here is the list of options supported by Kratos2. They can be set from the command-line when running the kratos binary, or programmatically via the C or Python APIs (using kratos_config in C, or by populating dictionaries in Python).

Options exclusive to the kratos binary

• h, help: print help message.
• output_file=STR: output file.
• stage=ENUM: if set, stop at the given stage of the translation pipeline. Possible values:
  • cex: cex trace reconstruction.
  • cfg: CFG building.
  • check_inv: check given inductive invariant.
  • flatten: flattening of expressions.
  • inline: function inlining.
  • mc: model checking.
  • parse: input file parsing.
  • sim: interactive simulation.
  • smt: use Kratos as an SMT solver (by executing the embedded MathSAT solver).
  • symexec: perform symbolic execution.
  • trans: transition system encoding.
• version: show version info.
• dump_intermediate_stages=BOOL: dump results of intermediate stages.
• dump_program_stats=ENUM: Dump program statistics at different transformation stages. Possible values:
  • after_flattening: After flattening.
  • after_inlining: After inlining.
  • after_parsing: After input file parsing.
  • always: At each stage.
• intermediate_output_dir=STR: output directory for intermediate stage dumping.

General

• random_seed=INT: Seed for the internal random number generators.
• verbosity=INT: verbosity level.

Preprocessing

• apply_slicing=BOOL: Apply slicing to the CFG before converting into transition system.
• functions_to_inline=STR: space-separated list of function names to inline (if not given, all functions will be inlined). Meaningful only with -stage=inline.
• functions_to_inline_file=STR: name of file with the list of functions to inline (one per line).
• inline_calls_threshold=INT: if > 0, inline all functions that with <= NUM calls.
• inline_detect_output_params=BOOL: if true, detect output parameters when doing function inlining to avoid generating intermediate memory stores.
• inline_max_depth=INT: maximum recursion depth for function inlining.
• inline_max_depth_add_check=BOOL: if true, add a run-time check that the max inlining depth is not reached.
• propagate_constants=ENUM: Apply constant propagation to the CFG. Possible values:
  • false: No constant propagation.
  • maps: Constant propagation only on map indices.
  • true: Full constant propagation.
• remove_const_maps=BOOL: Replace maps always accessed by constant indices with regular variables in the CFG.
• remove_globals=BOOL: Remove global variables.
• remove_loops=BOOL: If true, do not add loopback edges after loop unrolling.
• unroll_loops=INT: Unroll loops N times in the CFG.
• unroll_loops_maxdepth=INT: If nonzero, do not unroll loops with more than N nested loops.

Verification

• error_id=STR: id of the error to check.
• inv_check_file=STR: Inductive invariant to check.
• inv_output_file=STR: Inductive invariant output file.
• live_id=STR: id of the live label to check.
• mc_use_exit_codes=BOOL: If false, exit with zero instead of result codes when model checking is successful.
• model_checking_bmc_bound=INT: If >0, maximum bound for BMC.
• model_checking_engine=ENUM: Model checking engine to use. Possible values:
  • bitprophic3: BitProphIC3.
  • bitprophic3abs: BitProphIC3 with abstraction.
  • bitprophic3bmc: BitProphIC3 BMC.
  • bitprophic3kind: BitProphIC3 K-induction.
  • bmc: BMC.
  • kind: K-induction.
  • msatic3: IC3 with Implicit Abstraction.
  • msatic3smt: IC3 for SMT(LRA) and SMT(LIA).
  • simplic3: SimplIC3.
  • simplic3abs: SimplIC3 with abstraction.
  • simplic3avy: SimplIC3 with Avy.
  • simplic3bmc: SimplIC3 BMC.
  • simplic3kind: SimplIC3 k-induction.
• model_checking_invert_ts=BOOL: If true, invert the transition system for model checking.
• show_inv=BOOL: Show the inductive invariant (for the underlying transition system) proving the property.
• single_error=BOOL: check unreachability of all error labels as a single property.
• trans_cfg=BOOL: if true, use an explicit representation of the CFG when encoding into transition system (currently supported only by the vmt output).
• trans_defines_prefix=STR: prefix to use for defines when dumping the transition system in VMT or nuXmv format.
• trans_encoding=ENUM: transition system encoding type. Possible values:
  • basic: basic blocks.
  • large: large blocks.
• trans_enum_mode=ENUM: encoding mode for enum types. Possible values:
  • bv: Bit-vector values.
  • int: Integer values.
  • symbolic: Symbolic values.
• trans_int_as_real=BOOL: if true, encode integer variables as reals.
• trans_loc_int=BOOL: if true, encode locations as integers instead of bits.
• trans_output_format=ENUM: transition system output format. Possible values:
  • aiger: Aiger.
  • btor: Btor2.
  • chc: Constrained Horn Clauses (CHCs).
  • nuxmv: nuXmv output.
  • nuxmv-no-defines: nuXmv output without DEFINEs.
  • vmt: VMT output.
• trans_procedural=BOOL: if true, enable procedural encoding (only supported by CHC backend).
• trans_unsupported_op_uf=BOOL: if true, use uninterpreted functions to encode unsupported operations over integers/reals.
• trans_use_ite=BOOL: if true, allow term-ITEs when encoding into transition system.

Simulation

• sim_assume_error=BOOL: If false, terminate the simulation instead of raising an error when reaching a violated assumption.
• sim_interactive=BOOL: If true, perform interactive instead of random simulation.
• sim_max_count=INT: If nonzero, stop the simulation after having reached the target(s) N times.
• sim_target=STR: Target for simulation.
• symexec_concretize=BOOL: If true, use concretization in symbolic execution.
• symexec_concretize_target=STR: Target for concretization in symbolic execution.
• symexec_depth_inc=INT: Increment value for the iterative deepening in symbolic execution.
• symexec_depth_target=STR: Target for measuring the depth of symbolic execution (if not given, the depth will be based on the number of backtrack points in the solver).
• symexec_initial_depth=INT: Initial bound for the iterative deepening in symbolic execution.
• symexec_iterative=BOOL: If true, use an iterative-deepening strategy for symbolic execution.
• symexec_max_depth=INT: Max depth for symbolic execution.
• symexec_random=BOOL: If true, randomise the search during symbolic execution.
• symexec_solver_reset_frequency=INT: If nonzero, the reset interval (in number of checks) for the SMT solver in symbolic execution.

Counterexamples

• cex_important_functions=STR: space-separated list of important functions,used when -cex_type=cfg
• cex_output_file=STR: Counterexample output file.
• cex_type=ENUM: Type of counterexamples to generate (when -stage=mc). Possible values:
  • cfg: Only control flow graph information.
  • none: No counterexample.
  • path: Full execution path.
  • patheval: Execution path with evaluated rvalues.
  • pathevalmap: Execution path with evaluated map indices.
• trans_cex_trace_file=STR: File with counterexample trace to reconstruct.
• trans_cex_trace_format=ENUM: Counterexample trace input format. Possible values:
  • nuxmv: nuXmv XML format.
  • vmt: VMT format.