CBMC
ensure_one_backedge_per_target.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Ensure one backedge per target
4 
5 Author: 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 
15 class goto_programt;
16 class goto_modelt;
17 class goto_model_functiont;
18 
27 bool ensure_one_backedge_per_target(goto_programt &goto_program);
28 
37 bool ensure_one_backedge_per_target(goto_model_functiont &goto_model_function);
38 
47 bool ensure_one_backedge_per_target(goto_modelt &goto_model);
48 
49 #endif // CPROVER_GOTO_PROGRAMS_ENSURE_ONE_BACKEDGE_PER_TARGET_H
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:73
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