cprover
validate_goto_model.h
Go to the documentation of this file.
1/*******************************************************************\
2Module: Validate Goto Programs
3
4Author: Diffblue
5
6Date: Oct 2018
7
8\*******************************************************************/
9
10#ifndef CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H
11#define CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H
12
14
16{
17public:
18 // this check is disabled by default (not all goto programs
19 // have an entry point)
20 bool entry_point_exists = false;
21
25
26private:
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
35public:
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
58class 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