21 class validate_goto_modelt
36 void entry_point_exists();
39 void function_pointer_calls_removed();
51 void check_returns_removed();
62 void check_called_functions();
65 const function_mapt &function_map;
68 validate_goto_modelt::validate_goto_modelt(
72 : vm{vm}, function_map{goto_functions.function_map}
74 if(validation_options.entry_point_exists)
81 validation_options.function_pointer_calls_removed ||
82 validation_options.check_returns_removed)
84 function_pointer_calls_removed();
87 if(validation_options.check_returns_removed)
88 check_returns_removed();
90 if(validation_options.check_called_functions)
91 check_called_functions();
94 void validate_goto_modelt::entry_point_exists()
99 "an entry point must exist");
102 void validate_goto_modelt::function_pointer_calls_removed()
104 for(
const auto &fun : function_map)
106 for(
const auto &instr : fun.second.body.instructions)
108 if(instr.is_function_call())
114 "no calls via function pointer should be present");
120 void validate_goto_modelt::check_returns_removed()
122 for(
const auto &fun : function_map)
129 vm, !instr.is_return(),
"no return instructions should be present");
131 if(instr.is_function_call())
133 const auto &function_call = instr.get_function_call();
137 "function call lhs return should be nil");
143 void validate_goto_modelt::check_called_functions()
145 auto test_for_function_address =
146 [
this](
const exprt &expr) {
147 if(expr.id() == ID_address_of)
151 if(pointee.id() == ID_symbol && pointee.type().id() == ID_code)
157 function_map.find(identifier) != function_map.end(),
158 "every function whose address is taken must be in the "
164 for(
const auto &fun : function_map)
166 for(
const auto &instr : fun.second.body.instructions)
169 if(instr.is_function_call())
171 const auto &function_call = instr.get_function_call();
177 function_map.find(identifier) != function_map.end(),
178 "every function call callee must be in the function map");
182 const auto &src =
static_cast<const exprt &
>(instr.code);
183 src.
visit_pre(test_for_function_address);
195 validate_goto_modelt{goto_functions, vm, validation_options};