Ensure one backedge per target. More...
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Functions | |
| 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.h.
Function Documentation
◆ ensure_one_backedge_per_target() [1/3]
| 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/3]
| 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/3]
| 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.
