Module Flags

Parsing of command line arguments

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

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 *

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

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

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 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

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 log_invs : unit -> bool

Minimizes and logs invariants as contracts.

val print_invs : unit -> bool

Prints invariants *

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 log_format_json : 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 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.

val slice_nodes : unit -> bool

Node slicing

val check_subproperties : unit -> bool

Check properties of subnodes

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
module BmcKind : sig ... end
module IC3 : 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

Testgen flags

module Testgen : sig ... end
module Invgen : sig ... end
module C2I : sig ... end
module Interpreter : 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

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