cprover
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 #include "goto_model.h"
16 #include "goto_program.h"
17 
27 
36 bool ensure_one_backedge_per_target(goto_model_functiont &goto_model_function);
37 
47 
48 #endif // CPROVER_GOTO_PROGRAMS_ENSURE_ONE_BACKEDGE_PER_TARGET_H
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
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:83
goto_program.h
Concrete Goto Program.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183