22 class validate_goto_modelt
37 void entry_point_exists();
40 void function_pointer_calls_removed();
52 void check_returns_removed();
63 void check_called_functions();
66 const function_mapt &function_map;
69 validate_goto_modelt::validate_goto_modelt(
73 : vm{vm}, function_map{goto_functions.function_map}
85 function_pointer_calls_removed();
89 check_returns_removed();
92 check_called_functions();
95 void validate_goto_modelt::entry_point_exists()
100 "an entry point must exist");
103 void validate_goto_modelt::function_pointer_calls_removed()
105 for(
const auto &fun : function_map)
107 for(
const auto &instr : fun.second.body.instructions)
109 if(instr.is_function_call())
115 "no calls via function pointer should be present");
121 void validate_goto_modelt::check_returns_removed()
123 for(
const auto &fun : function_map)
130 vm, !instr.is_return(),
"no return instructions should be present");
132 if(instr.is_function_call())
134 const auto &function_call = instr.get_function_call();
138 "function call lhs return should be nil");
144 void validate_goto_modelt::check_called_functions()
146 auto test_for_function_address =
147 [
this](
const exprt &expr) {
148 if(expr.id() == ID_address_of)
152 if(pointee.id() == ID_symbol && pointee.type().id() == ID_code)
158 function_map.find(identifier) != function_map.end(),
159 "every function whose address is taken must be in the "
165 for(
const auto &fun : function_map)
167 for(
const auto &instr : fun.second.body.instructions)
170 if(instr.is_function_call())
172 const auto &function_call = instr.get_function_call();
178 function_map.find(identifier) != function_map.end(),
179 "every function call callee must be in the function map");
183 const auto &src =
static_cast<const exprt &
>(instr.code);
184 src.
visit_pre(test_for_function_address);
196 validate_goto_modelt{goto_functions, vm, validation_options};
codet representation of a function call statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void visit_pre(std::function< void(exprt &)>)
A collection of goto functions.
std::map< irep_idt, goto_functiont > function_mapt
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
bool check_called_functions
bool function_pointer_calls_removed
bool check_returns_removed
instructionst instructions
The list of instructions in the goto program.
const irep_idt & id() const
const irep_idt & get_identifier() const
Goto Programs with Functions.
API to expression classes for Pointers.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
bool does_function_call_return(const code_function_callt &function_call)
Check if the function_call returns anything.
Replace function returns by assignments to global variables.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
void validate_goto_model(const goto_functionst &goto_functions, const validation_modet vm, const goto_model_validation_optionst validation_options)