Skip to content

Commit bea730d

Browse files
author
thk123
committed
Adding utility for verifying a set of statements contains a function call
1 parent ee2179c commit bea730d

File tree

2 files changed

+59
-0
lines changed

2 files changed

+59
-0
lines changed

unit/testing-utils/require_goto_statements.cpp

+36
Original file line numberDiff line numberDiff line change
@@ -409,3 +409,39 @@ require_goto_statements::require_entry_point_argument_assignment(
409409
.get_identifier();
410410
return argument_tmp_name;
411411
}
412+
413+
/// Verify that a collection of statements contains a function call to a
414+
/// function whose symbol identifier matches the provided identifier
415+
/// \param statements: The collection of statements to inspect
416+
/// \param function_call_identifier: The symbol identifier of the function
417+
/// that should have been called
418+
/// \return The first code_function_callt to the relevant function or throws a
419+
/// no_matching_function_callt if no call is found
420+
code_function_callt require_goto_statements::require_function_call(
421+
const std::vector<codet> &statements,
422+
const irep_idt &function_call_identifier)
423+
{
424+
// TODO: Would appreciate some review comments on whether it makes the most sense:
425+
// - return a vector of matching code_function_calls
426+
// - return an optionalt with the first matching call
427+
// - return a code_function_callt throwing an exception if none found
428+
for(const codet &statement : statements)
429+
{
430+
if(statement.get_statement() == ID_function_call)
431+
{
432+
const code_function_callt &function_call =
433+
to_code_function_call(statement);
434+
435+
if(function_call.function().id() == ID_symbol)
436+
{
437+
if(
438+
to_symbol_expr(function_call.function()).get_identifier() ==
439+
function_call_identifier)
440+
{
441+
return function_call;
442+
}
443+
}
444+
}
445+
}
446+
throw no_matching_function_callt(function_call_identifier);
447+
}

unit/testing-utils/require_goto_statements.h

+23
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,25 @@ class no_decl_found_exceptiont : public std::exception
4747
std::string _varname;
4848
};
4949

50+
class no_matching_function_callt : public std::exception
51+
{
52+
public:
53+
explicit no_matching_function_callt(const irep_idt &function_identifier)
54+
: function_identifier(function_identifier)
55+
{
56+
}
57+
58+
virtual const char *what() const throw()
59+
{
60+
std::ostringstream stringStream;
61+
stringStream << "Failed to find function call for: " << function_identifier;
62+
return stringStream.str().c_str();
63+
}
64+
65+
private:
66+
irep_idt function_identifier;
67+
};
68+
5069
pointer_assignment_locationt find_struct_component_assignments(
5170
const std::vector<codet> &statements,
5271
const irep_idt &structure_name,
@@ -85,6 +104,10 @@ const irep_idt &require_struct_array_component_assignment(
85104
const irep_idt &require_entry_point_argument_assignment(
86105
const irep_idt &argument_name,
87106
const std::vector<codet> &entry_point_statements);
107+
108+
code_function_callt require_function_call(
109+
const std::vector<codet> &statements,
110+
const irep_idt &function_call_identifier);
88111
}
89112

90113
#endif // CPROVER_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H

0 commit comments

Comments
 (0)