20class validate_goto_modelt
35 void entry_point_exists();
38 void function_pointer_calls_removed();
49 void check_called_functions();
52 const function_mapt &function_map;
55validate_goto_modelt::validate_goto_modelt(
59 : vm{vm}, function_map{goto_functions.function_map}
66 function_pointer_calls_removed();
70 check_called_functions();
73void validate_goto_modelt::entry_point_exists()
78 "an entry point must exist");
81void validate_goto_modelt::function_pointer_calls_removed()
83 for(
const auto &
fun : function_map)
85 for(
const auto &
instr :
fun.second.body.instructions)
87 if(
instr.is_function_call())
92 "no calls via function pointer should be present");
98void validate_goto_modelt::check_called_functions()
101 [
this](
const exprt &expr) {
112 function_map.find(identifier) != function_map.end(),
113 "every function whose address is taken must be in the "
119 for(
const auto &
fun : function_map)
121 for(
const auto &
instr :
fun.second.body.instructions)
124 if(
instr.is_function_call())
131 function_map.find(identifier) != function_map.end(),
132 "every function call callee must be in the function map");
136 const auto &src =
static_cast<const exprt &
>(
instr.get_code());
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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.
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.
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)