Ensure one backedge per target. More...
#include "ensure_one_backedge_per_target.h"#include <analyses/natural_loops.h>#include "goto_model.h"#include <algorithm>
Include dependency graph for ensure_one_backedge_per_target.cpp:Go to the source code of this file.
Classes | |
| struct | location_number_less_thant |
Functions | |
| static bool | location_number_less_than (const goto_programt::targett &a, const goto_programt::targett &b) |
| bool | ensure_one_backedge_per_target (goto_programt::targett &it, goto_programt &goto_program) |
| bool | ensure_one_backedge_per_target (goto_programt &goto_program) |
Try to force the given goto_program into a form such that each backedge (branch going backwards in lexical program order) has a unique target. More... | |
| bool | ensure_one_backedge_per_target (goto_model_functiont &goto_model_function) |
Try to force the given goto_program into a form such that each backedge (branch going backwards in lexical program order) has a unique target. More... | |
| bool | ensure_one_backedge_per_target (goto_modelt &goto_model) |
Try to force the given goto_program into a form such that each backedge (branch going backwards in lexical program order) has a unique target. More... | |
Detailed Description
Ensure one backedge per target.
Definition in file ensure_one_backedge_per_target.cpp.
Function Documentation
◆ ensure_one_backedge_per_target() [1/4]
| bool ensure_one_backedge_per_target | ( | goto_model_functiont & | goto_model_function | ) |
Try to force the given goto_program into a form such that each backedge (branch going backwards in lexical program order) has a unique target.
This is achieved by redirecting backedges or possibly introducing a new one. Note this may not always succeed; client code must check whether the condition holds of any backedge target it is interested in. Note this overload updates goto_model_function's location numbers and incoming-edges sets.
- Returns
- true if any change is made.
Definition at line 178 of file ensure_one_backedge_per_target.cpp.
◆ ensure_one_backedge_per_target() [2/4]
| bool ensure_one_backedge_per_target | ( | goto_modelt & | goto_model | ) |
Try to force the given goto_program into a form such that each backedge (branch going backwards in lexical program order) has a unique target.
This is achieved by redirecting backedges or possibly introducing a new one. Note this may not always succeed; client code must check whether the condition holds of any backedge target it is interested in. Note this overload updates goto_model's location numbers and incoming-edges sets.
- Returns
- true if any change is made.
Definition at line 192 of file ensure_one_backedge_per_target.cpp.
◆ ensure_one_backedge_per_target() [3/4]
| bool ensure_one_backedge_per_target | ( | goto_programt & | goto_program | ) |
Try to force the given goto_program into a form such that each backedge (branch going backwards in lexical program order) has a unique target.
This is achieved by redirecting backedges or possibly introducing a new one. Note this may not always succeed; client code must check whether the condition holds of any backedge target it is interested in. Note this overload leaves goto_program's location numbers and incoming- edges sets inconsistent; the client should call goto_programt::update.
- Returns
- true if any change is made.
Definition at line 99 of file ensure_one_backedge_per_target.cpp.
◆ ensure_one_backedge_per_target() [4/4]
| bool ensure_one_backedge_per_target | ( | goto_programt::targett & | it, |
| goto_programt & | goto_program | ||
| ) |
Definition at line 27 of file ensure_one_backedge_per_target.cpp.
◆ location_number_less_than()
|
static |
Definition at line 20 of file ensure_one_backedge_per_target.cpp.
