Module Flags

module Flags: sig .. end
Parsing of command line arguments


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. *)
  (* 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

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


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

module MyModule : sig
  include FlagModule

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(s): Christoph Sticksel, Adrien Champion *

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.

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

val clear_input_files : unit -> unit
Adds a lustre file in the cone of influence of the input file.
val add_input_file : string -> unit
val lus_main : unit -> string option
Main node in Lustre file
type input_format = [ `Horn | `Lustre | `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 log_invs : unit -> bool
Minimizes and logs invariants as contracts.
val debug : unit -> string list
Debug sections to enable
val debug_log : unit -> string option
Logfile for debug output
val log_level : unit -> Lib.log_level
Verbosity level
val log_format_xml : unit -> bool
Output in XML 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 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.
val lus_strict : unit -> bool
Strict Lustre mode.
val lus_compile : unit -> bool
Activates compilation to Rust.
val color : unit -> bool
Colored output.
val weakhcons : unit -> bool
Use weak hash-consing.
module Smt: sig .. end
SMT solver flags
module BmcKind: sig .. end
BMC / k-induction flags
module IC3: sig .. end
IC3 flags
module QE: sig .. end
QE flags
module Contracts: sig .. end
Contracts flags
module Certif: sig .. end
Certificates and Proofs
module Arrays: sig .. end
Arrays flags

Testgen flags

module Testgen: sig .. end
module Invgen: sig .. end
Invgen flags
module C2I: sig .. end
C2I flags
module Interpreter: sig .. end
Interpreter flags

Convenience functions

val subdir_for : string list -> string
Path to subdirectory for a system (in the output directory).

Parsing of the command line

Parsing of the command line arguments is performed when loading this module.