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
26
bool
ensure_one_backedge_per_target
(
goto_programt
&goto_program);
27
36
bool
ensure_one_backedge_per_target
(
goto_model_functiont
&goto_model_function);
37
46
bool
ensure_one_backedge_per_target
(
goto_modelt
&goto_model);
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
goto-programs
ensure_one_backedge_per_target.h
Generated by
1.8.20