Module Flags.Contracts

Contracts flags

val compositional : unit -> bool

Compositional analysis.

val translate_contracts : unit -> string option

Translate contracts.

val check_modes : unit -> bool

Check modes.

val check_environment : unit -> bool

Check realizability of node environments.

val check_implem : unit -> bool

Check modes.

val contract_gen : unit -> bool

Contract generation.

val contract_gen_depth : unit -> int

Contract generation: max depth.

val assumption_gen : unit -> bool

Assumption generation.

val two_state_assumption : unit -> bool
val assumption_gen_iter : unit -> int

Assumption generation: generalization iterations

val refinement : unit -> bool

Activate refinement.

val rec_unrollings : unit -> int

Unrollings of a recursive function a refinement tries, its recursive calls abstracted by its contract, before defining it

val rec_learn_values : unit -> bool

Whether the values of the calls that the check of a spurious counterexample evaluated are given to the refinements of the caller, in a compositional and modular analysis (see Analysis.info.learned)

val rec_instances : unit -> int

Instances of recursive functions the unrolling of the functions may create in a system, outside of compositional analyses

val rec_contract_unrollings : unit -> int

Unrollings of a recursive function in the analysis of the function itself, when its recursive calls are abstracted by its contract

val print_deadlock : unit -> bool

Print deadlocking trace and a conflict

val dump_deadlock : unit -> bool

Dump deadlocking trace to a file *

val check_contract_is_sat : unit -> bool

Check whether a unrealizable contract is satisfiable

val print_viable_states : unit -> bool