1111#include < algorithm>
1212#include < util/expr_iterator.h>
1313
14- std::vector<codet> get_all_statements (const exprt::operandst &instructions)
14+ // / Expand value of a function to include all child codets
15+ // / \param instructions: The value of the function (e.g. got by looking up
16+ // / the function in the symbol table and getting the value)
17+ // / \return: All ID_code statements in the tree rooted at \p function_value
18+ std::vector<codet>
19+ require_goto_statements::get_all_statements (const exprt &function_value)
1520{
1621 std::vector<codet> statements;
17- for (const exprt &instruction : instructions)
18- {
19- // Add the statement
20- statements.push_back (to_code (instruction));
21-
22- // Add any child statements (e.g. if this is a code_block
23- // TODO(tkiley): It should be possible to have a custom version of
24- // TODO(tkiley): back_inserter that also transforms to codet, but I don't
25- // TODO(tkiley): know how to do this
26- std::vector<exprt> sub_expr;
27- std::copy_if (
28- instruction.depth_begin (),
29- instruction.depth_end (),
30- std::back_inserter (sub_expr),
31- [](const exprt &sub_statement) {
32- // Get all codet
33- return sub_statement.id () == ID_code;
34- });
35-
36- std::transform (
37- sub_expr.begin (),
38- sub_expr.end (),
39- std::back_inserter (statements),
40- [](const exprt &sub_expr) { return to_code (sub_expr); });
41- }
22+
23+ // Add any child statements (e.g. if this is a code_block
24+ // TODO(tkiley): It should be possible to have a custom version of
25+ // TODO(tkiley): back_inserter that also transforms to codet, but I don't
26+ // TODO(tkiley): know how to do this
27+ std::vector<exprt> sub_expr;
28+ std::copy_if (
29+ function_value.depth_begin (),
30+ function_value.depth_end (),
31+ std::back_inserter (sub_expr),
32+ [](const exprt &sub_statement) {
33+ // Get all codet
34+ return sub_statement.id () == ID_code;
35+ });
36+
37+ std::transform (
38+ sub_expr.begin (),
39+ sub_expr.end (),
40+ std::back_inserter (statements),
41+ [](const exprt &sub_expr) { return to_code (sub_expr); });
42+
4243 return statements;
4344}
4445
45- std::vector<code_assignt> find_struct_component_assignments (
46+ // / Find assignment statements of the form \p structure_name.\component_name =
47+ // / \param statements: The statements to look through
48+ // / \param structure_name: The name of variable of type struct
49+ // / \param component_name: The name of the component that should be assigned
50+ // / \return: All the assignments to that component.
51+ std::vector<code_assignt>
52+ require_goto_statements::find_struct_component_assignments (
4653 const std::vector<codet> &statements,
4754 const irep_idt &structure_name,
4855 const irep_idt &component_name)
@@ -77,7 +84,8 @@ std::vector<code_assignt> find_struct_component_assignments(
7784// / \param instructions: The instructions to look through
7885// / \return: A structure that contains the null assignment if found, and a
7986// / vector of all other assignments
80- pointer_assignment_locationt find_pointer_assignments (
87+ require_goto_statements::pointer_assignment_locationt
88+ require_goto_statements::find_pointer_assignments (
8189 const irep_idt &pointer_name,
8290 const std::vector<codet> &instructions)
8391{
@@ -108,7 +116,11 @@ pointer_assignment_locationt find_pointer_assignments(
108116 return locations;
109117}
110118
111- const exprt &find_declaration_by_name (
119+ // / Find the declaration of the specific variable.
120+ // / \param variable_name: The name of the variable.
121+ // / \param entry_point_instructions: The statements to look through
122+ // / \return The declaration statement corresponding to that variable
123+ const code_declt &require_goto_statements::find_declaration_by_name (
112124 const irep_idt &variable_name,
113125 const std::vector<codet> &entry_point_instructions)
114126{
@@ -120,7 +132,7 @@ const exprt &find_declaration_by_name(
120132
121133 if (decl_statement.get_identifier () == variable_name)
122134 {
123- return statement ;
135+ return decl_statement ;
124136 }
125137 }
126138 }
0 commit comments