Skip to content

Commit 1bfec7e

Browse files
committed
Add stateless variant of goto_programt::get_successors
1 parent 3c7087e commit 1bfec7e

File tree

1 file changed

+51
-20
lines changed

1 file changed

+51
-20
lines changed

src/goto-programs/goto_program.h

+51-20
Original file line numberDiff line numberDiff line change
@@ -600,6 +600,10 @@ class goto_programt
600600
template <typename Target>
601601
std::list<Target> get_successors(Target target) const;
602602

603+
template <typename Target>
604+
static std::list<Target>
605+
get_well_formed_instruction_successors(Target target);
606+
603607
void compute_incoming_edges();
604608

605609
/// Insertion that preserves jumps to "target".
@@ -1068,34 +1072,24 @@ class goto_programt
10681072
}
10691073
};
10701074

1071-
/// Get control-flow successors of a given instruction. The instruction is
1072-
/// represented by a pointer `target` of type `Target`. An instruction has
1073-
/// either 0, 1, or 2 successors (more than two successors is deprecated). For
1074-
/// example, an `ASSUME` instruction with the `guard` being a `false_exprt` has
1075-
/// 0 successors, and `ASSIGN` instruction has 1 successor, and a `GOTO`
1076-
/// instruction with the `guard` not being a `true_exprt` has 2 successors.
1077-
///
1078-
/// \tparam Target: type used to represent a pointer to an instruction in a goto
1079-
/// program
1080-
/// \param target: pointer to the instruction of which to get the successors of
1081-
/// \return List of control-flow successors of the pointed-to goto program
1082-
/// instruction
10831075
template <typename Target>
1084-
std::list<Target> goto_programt::get_successors(
1085-
Target target) const
1076+
std::list<Target> get_successors(
1077+
Target target,
1078+
std::function<bool(const Target &)> is_instruction_out_of_range)
10861079
{
1087-
if(target==instructions.end())
1080+
if(is_instruction_out_of_range(target))
10881081
return std::list<Target>();
10891082

10901083
const auto next=std::next(target);
1084+
const auto next_out_of_range = is_instruction_out_of_range(next);
10911085

1092-
const instructiont &i=*target;
1086+
const goto_programt::instructiont &i = *target;
10931087

10941088
if(i.is_goto())
10951089
{
10961090
std::list<Target> successors(i.targets.begin(), i.targets.end());
10971091

1098-
if(!i.get_condition().is_true() && next != instructions.end())
1092+
if(!i.get_condition().is_true() && !next_out_of_range)
10991093
successors.push_back(next);
11001094

11011095
return successors;
@@ -1105,7 +1099,7 @@ std::list<Target> goto_programt::get_successors(
11051099
{
11061100
std::list<Target> successors(i.targets.begin(), i.targets.end());
11071101

1108-
if(next!=instructions.end())
1102+
if(!next_out_of_range)
11091103
successors.push_back(next);
11101104

11111105
return successors;
@@ -1125,19 +1119,56 @@ std::list<Target> goto_programt::get_successors(
11251119

11261120
if(i.is_assume())
11271121
{
1128-
return !i.get_condition().is_false() && next != instructions.end()
1122+
return !i.get_condition().is_false() && !next_out_of_range
11291123
? std::list<Target>{next}
11301124
: std::list<Target>();
11311125
}
11321126

1133-
if(next!=instructions.end())
1127+
if(i.is_end_function())
1128+
return std::list<Target>();
1129+
1130+
if(!next_out_of_range)
11341131
{
11351132
return std::list<Target>{next};
11361133
}
11371134

11381135
return std::list<Target>();
11391136
}
11401137

1138+
/// Get control-flow successors of a given instruction. The instruction is
1139+
/// represented by a pointer `target` of type `Target`. An instruction has
1140+
/// either 0, 1, or 2 successors (more than two successors is deprecated). For
1141+
/// example, an `ASSUME` instruction with the `guard` being a `false_exprt` has
1142+
/// 0 successors, and `ASSIGN` instruction has 1 successor, and a `GOTO`
1143+
/// instruction with the `guard` not being a `true_exprt` has 2 successors.
1144+
///
1145+
/// \tparam Target: type used to represent a pointer to an instruction in a goto
1146+
/// program
1147+
/// \param target: pointer to the instruction of which to get the successors of
1148+
/// \return List of control-flow successors of the pointed-to goto program
1149+
/// instruction
1150+
template <typename Target>
1151+
std::list<Target> goto_programt::get_successors(Target target) const
1152+
{
1153+
const std::function<bool(const Target &)> instruction_out_of_range =
1154+
[this](const Target &target) { return target == instructions.end(); };
1155+
return ::get_successors(target, instruction_out_of_range);
1156+
}
1157+
1158+
/// Like \ref get_successors, except we assume that neither \p target nor its
1159+
/// successor is out of range (i.e., equal to instructions.end()). This holds
1160+
/// so long as \p target is a valid iterator and its containing function is
1161+
/// complete (it has an END_OF_FUNCTION terminator, and all its instruction
1162+
/// targets are valid iterators).
1163+
template <typename Target>
1164+
std::list<Target>
1165+
goto_programt::get_well_formed_instruction_successors(Target target)
1166+
{
1167+
const std::function<bool(const Target &)> instructions_never_out_of_range =
1168+
[](const Target &) { return false; };
1169+
return ::get_successors(target, instructions_never_out_of_range);
1170+
}
1171+
11411172
inline bool order_const_target(
11421173
const goto_programt::const_targett i1,
11431174
const goto_programt::const_targett i2)

0 commit comments

Comments
 (0)