cprover
validate_goto_model.h
Go to the documentation of this file.
1 /*******************************************************************\
2 Module: Validate Goto Programs
3 
4 Author: Diffblue
5 
6 Date: Oct 2018
7 
8 \*******************************************************************/
9 
10 #ifndef CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H
11 #define CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H
12 
13 #include <util/validate.h>
14 
16 {
17 public:
18  // this check is disabled by default (not all goto programs
19  // have an entry point)
20  bool entry_point_exists = false;
21 
23  bool check_returns_removed = true;
25 
26 private:
27  void set_all_flags(bool options_value)
28  {
29  entry_point_exists = options_value;
30  function_pointer_calls_removed = options_value;
31  check_returns_removed = options_value;
32  check_called_functions = options_value;
33  }
34 
35 public:
37 
38  enum class set_optionst
39  {
40  all_true,
41  all_false
42  };
43 
45  {
46  switch(flag_option)
47  {
49  set_all_flags(true);
50  break;
52  set_all_flags(false);
53  break;
54  }
55  }
56 };
57 
58 class goto_functionst;
59 
61  const goto_functionst &goto_functions,
62  const validation_modet vm,
63  const goto_model_validation_optionst validation_options);
64 
65 #endif // CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H
goto_model_validation_optionst::function_pointer_calls_removed
bool function_pointer_calls_removed
Definition: validate_goto_model.h:22
goto_model_validation_optionst
Definition: validate_goto_model.h:16
goto_model_validation_optionst::goto_model_validation_optionst
goto_model_validation_optionst(set_optionst flag_option)
Definition: validate_goto_model.h:44
validate_goto_model
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
Definition: validate_goto_model.cpp:190
goto_model_validation_optionst::check_returns_removed
bool check_returns_removed
Definition: validate_goto_model.h:23
validation_modet
validation_modet
Definition: validation_mode.h:13
goto_model_validation_optionst::check_called_functions
bool check_called_functions
Definition: validate_goto_model.h:24
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_model_validation_optionst::set_optionst
set_optionst
Definition: validate_goto_model.h:39
goto_model_validation_optionst::entry_point_exists
bool entry_point_exists
Definition: validate_goto_model.h:20
goto_model_validation_optionst::goto_model_validation_optionst
goto_model_validation_optionst()=default
validate.h
goto_model_validation_optionst::set_optionst::all_true
@ all_true
goto_model_validation_optionst::set_all_flags
void set_all_flags(bool options_value)
Definition: validate_goto_model.h:27
goto_model_validation_optionst::set_optionst::all_false
@ all_false