#include <validate_goto_model.h>

Public Types
enum class	set_optionst { all_true , all_false }

Public Member Functions
	goto_model_validation_optionst ()=default

	goto_model_validation_optionst (set_optionst flag_option)

Public Attributes
bool	entry_point_exists = false

bool	check_returns_removed = true

Private Member Functions
void	set_all_flags (bool options_value)

Detailed Description

Definition at line 15 of file validate_goto_model.h.

Member Enumeration Documentation

◆ set_optionst

enum goto_model_validation_optionst::set_optionst

strong

Enumerator
all_true
all_false

Definition at line 33 of file validate_goto_model.h.

Constructor & Destructor Documentation

◆ goto_model_validation_optionst() [1/2]

goto_model_validation_optionst::goto_model_validation_optionst ( )

default

◆ goto_model_validation_optionst() [2/2]

goto_model_validation_optionst::goto_model_validation_optionst ( set_optionst flag_option )

inlineexplicit

Definition at line 39 of file validate_goto_model.h.

Member Function Documentation

◆ set_all_flags()

void goto_model_validation_optionst::set_all_flags ( bool options_value )

inlineprivate

Definition at line 24 of file validate_goto_model.h.

Member Data Documentation

◆ check_returns_removed

bool goto_model_validation_optionst::check_returns_removed = true

Definition at line 21 of file validate_goto_model.h.

◆ entry_point_exists

bool goto_model_validation_optionst::entry_point_exists = false

Definition at line 20 of file validate_goto_model.h.

The documentation for this class was generated from the following file:

/home/runner/work/cbmc/cbmc/src/goto-programs/validate_goto_model.h

Public Types

Public Member Functions

Public Attributes

Private Member Functions