Struct haybale_pitchfork::PitchforkConfig

#[non_exhaustive]
pub struct PitchforkConfig {
    pub keep_going: bool,
    pub dump_errors: bool,
    pub progress_updates: bool,
    pub debug_logging: bool,
}

pitchfork-specific configuration options, in addition to the configuration options in haybale::Config.

Like haybale::Config, PitchforkConfig uses the (new-to-Rust-1.40) #[non_exhaustive] attribute to indicate that fields may be added even in a point release (that is, without incrementing the major or minor version). Users should start with PitchforkConfig::default() and then change the settings they want to change.

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

keep_going: bool

If true, then even if we encounter an error or violation, we will continue exploring as many paths as we can in the function before returning, possibly reporting many different errors and/or violations. (Although we can't keep going on the errored path itself, we can still try to explore other paths that don't contain the error.) If false, then as soon as we encounter an error or violation, we will quit and return the results we have. It is recommended to only use keep_going == true in conjunction with solver query timeouts; see the solver_query_timeout setting in Config.

Default is false.

dump_errors: bool

Even if keep_going is set to true, the Display impl for ConstantTimeResultForFunction only displays a summary of the kinds of errors encountered, and full details about a single error. With dump_errors == true, pitchfork will dump detailed descriptions of all errors encountered to a file.

This setting only applies if keep_going == true; it is completely ignored if keep_going == false.

Default is true, meaning that if keep_going is enabled, then detailed error descriptions will be dumped to a file.

progress_updates: bool

If true, pitchfork will provide detailed progress updates in a continuously-updated terminal display. This includes counts of paths verified / errors encountered / warnings generated; the current code location being executed (in terms of both LLVM and source if available), the most recent log message generated, etc.

Also, if true, log messages other than the most recent will not be shown in the terminal; instead, all log messages will be routed to a file.

progress_updates == true requires pitchfork to take control of the global logger; users should not initialize their own logging backends such as env_logger. On the other hand, if progress_updates == false, pitchfork will not touch the global logger, and it is up to users to initialize a logging backend such as env_logger if they want to see log messages.

This setting requires the progress-updates crate feature, which is enabled by default. If the progress-updates feature is disabled, this setting will be treated as false regardless of its actual value.

If you encounter a Rust panic (as opposed to merely a haybale::Error), you may want to temporarily disable progress_updates for debugging, in order to get a clear panic message; otherwise, the progress-display-updater thread may interfere with the printing of the panic message.

Default is true.

debug_logging: bool

If progress_updates == true, pitchfork takes control of the global logger, as noted in docs there. This setting controls which log messages will be recorded in the designated log file: messages with DEBUG and higher priority (true), or only messages with INFO and higher priority (false).

If progress_updates == false, this setting has no effect; you should configure debug logging via your own chosen logging backend such as env_logger.

Default is false.

Trait Implementations

impl Clone for PitchforkConfig

fn clone(&self) -> PitchforkConfig

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for PitchforkConfig

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Default for PitchforkConfig

fn default() -> Self

Returns the "default value" for a type.