CBMC
Public Types | Public Member Functions | Public Attributes | Private Member Functions | List of all members
goto_model_validation_optionst Class Referencefinal

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