CBMC
Loading...
Searching...
No Matches
ensure_one_backedge_per_target.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Ensure one backedge per target
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_PROGRAMS_ENSURE_ONE_BACKEDGE_PER_TARGET_H
13#define CPROVER_GOTO_PROGRAMS_ENSURE_ONE_BACKEDGE_PER_TARGET_H
14
15class goto_programt;
16class goto_modelt;
17class goto_model_functiont;
18
27bool ensure_one_backedge_per_target(goto_programt &goto_program);
28
37bool ensure_one_backedge_per_target(goto_model_functiont &goto_model_function);
38
47bool ensure_one_backedge_per_target(goto_modelt &goto_model);
48
49#endif // CPROVER_GOTO_PROGRAMS_ENSURE_ONE_BACKEDGE_PER_TARGET_H
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:190
goto_modelt
Definition goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:72
ensure_one_backedge_per_target
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 le...
Definition ensure_one_backedge_per_target.cpp:99