Flags (kind2dev@731decdf5fb1.Flags)

Workflow

Flags are separated based on the technique(s) they impact. Global flags are the ones that don't impact any technique, or impact all of them. Log flags, help flags, timeout flags... are global flags.

NB: when adding a boolean flag, make sure to parse its value with the bool_of_string function.

Adding a new (non-global) flag to an existing module

Adding a new flag impacts three pieces of code. The first is the body of the module you're adding the flag to. Generally speaking, adding a flag looks like

(* Default value of the flag. *)
let my_flag_default = ...
(* Reference storing the value of the flag. *)
let my_flag = ref my_flag_default
(* Add flag specification to module specs. *)
let _ = add_spec (
  (* The actual flag. *)
  "--my_flag",
  (* What to do with the value given to the flag, see other flags. *)
  ...,
  (* Flag description. *)
  fun fmt ->
    Format.fprintf fmt
      "@[<v>Description of my flag.@ Default: %a@]"
      pp_print_default_value_of_my_flag my_flag_default
)
(* Flag value accessor. *)
let my_flag () = !my_flag

At this point your flag is integrated in the Kind 2 flags.

To make it available to the rest of Kind 2, you need to modify the signature of the module you added the flag to

in this file, where the module is declared, and
in flags.mli.

The update to the signature is typically

  val my_flag : unit -> type_of_my_flag

Adding a new flag module

The template to add a new module is

module MyModule : sig
  include FlagModule
end = struct

  (* Identifier of the module. No space or special characters. *)
  let id = "..."
  (* Short description of the module. *)
  let desc = "..."
  (* Explanation of the module. *)
  let fmt_explain fmt =
    Format.fprintf fmt "@[<v>\
      ...\
    @]"

  (* All the flag specification of this module. *)
  let all_specs = ref []
  let add_specs specs = all_specs := !all_specs @ specs
  let add_spec spec = add_specs [spec]

  (* Returns all the flag specification of this module. *)
  let all_specs () = !all_specs

end

Don't forget to update `flags.mli`:

module MyModule : sig
  include FlagModule
end

You then need to add your module to the module_map, the association map between module identifiers and modules. Make sure the identifier for your module is not used yet.

You can now add modules following the instructions in the previous section.

author Christoph Sticksel, Adrien Champion

exception Error

exception SolverNotFound

exception UnsupportedSolver

Accessors for flags

Meta flags

Generic flags

val input_file : unit -> string

Input file

val all_input_files : unit -> string list

All lustre files in the cone of influence of the input file.

val clear_input_files : unit -> unit

Clears the lustre files in the cone of influence of the input file.

val add_input_file : string -> bool

Adds a lustre file in the cone of influence of the input file.

Returns false if the cone of influence already contains the file

val lus_main : unit -> string option

Main node in Lustre file

val lus_main_const : unit -> string option

Main constant identifier in Lustre file

val lus_main_type : unit -> string option

Main type alias in Lustre file

type input_format = [

| `Lustre
| `Horn
| `Native

]

Format of input file

val input_format : unit -> input_format

val output_dir : unit -> string

Output directory for the files Kind 2 generates.

val include_dirs : unit -> string list

type real_precision = [

| `Rational
| `Float

]

val real_precision : unit -> real_precision

val arr_elements_printed : unit -> int

val log_invs : unit -> bool

Minimizes and logs invariants as contracts.

val print_invs : unit -> bool

Prints invariants *

val print_cex : unit -> bool

Print counterexamples *

val print_witness : unit -> bool

Print witnesses *

val dump_cex : unit -> bool

Dump counterexample to disproven invariant property to a file *

val set_dump_cex : bool -> unit

Set whether dumping counterexamples

val dump_witness : unit -> bool

Dump witness of proven reachability property to a file *

val debug : unit -> string list

Debug sections to enable

val debug_log : unit -> string option

Logfile for debug output

type exit_code_convention = [

| `RESULTS_AND_ERRORS
| `ONLY_ERRORS

]

val exit_code_mode : unit -> exit_code_convention

val log_level : unit -> Lib.log_level

Verbosity level

val log_format_xml : unit -> bool

Output in XML format

val log_format_json : unit -> bool

Output in JSON format

val log_format_ijson : unit -> bool

Output in incremental JSON format

val timeout_wall : unit -> float

Wallclock timeout.

val timeout_analysis : unit -> float

Per-run wallclock timeout.

type enable = Lib.kind_module list

The Kind modules enabled is a list of kind_modules.

val only_parse : unit -> bool

Only parse the Lustre program. No analysis is performed.

val enabled : unit -> enable

The modules enabled.

val invgen_enabled : unit -> enable

Returns the invariant generation techniques currently enabled.

val disable : Lib.kind_module -> unit

Manually disables a module.

val modular : unit -> bool

Modular analysis.

type slice_nodes = [

| `On
| `Off
| `Experimental

]

Node slicing

val slice_nodes : unit -> slice_nodes

val check_reach : unit -> bool

Check reachability properties

val check_nonvacuity : unit -> bool

Check non-vacuity of contract modes and conditional properties

val check_subproperties : unit -> bool

Check properties of subnodes

val lus_strict : unit -> bool

Strict Lustre mode.

val lus_push_pre : unit -> bool

Activates transformation that pushes pre expressions

val color : unit -> bool

Colored output.

val support_new_bv_cast_operators : unit -> bool

True iff the current solver support sbv_to_int and ubv_to_int operators

module Smt : sig ... end

module BmcKind : sig ... end

module IC3QE : sig ... end

module IC3IA : sig ... end

module QE : sig ... end

module Contracts : sig ... end

module Certif : sig ... end

module IVC : sig ... end

module MCS : sig ... end

module Arrays : sig ... end

Quantifier instantiation flags

module Quant : sig ... end

Testgen flags

module Testgen : sig ... end

module Invgen : sig ... end

module C2I : sig ... end

module Interpreter : sig ... end

module ContractMonitor : sig ... end

module Lsp : sig ... end

Convenience functions

val subdir_for : string list -> string

Path to subdirectory for a system (in the output directory).

Parsing of the command line

val parse_argv : unit -> unit

Parse the command line