cprover
Loading...
Searching...
No Matches
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:
34
35public:
37
38 enum class set_optionst
39 {
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,
64
65#endif // CPROVER_GOTO_PROGRAMS_VALIDATE_GOTO_MODEL_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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