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
A collection of goto functions.
goto_model_validation_optionst(set_optionst flag_option)
void set_all_flags(bool options_value)
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)
validation_modet