cprover
loop_utils.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Helper functions for k-induction and loop invariants
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#ifndef CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H
13
#define CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H
14
15
#include <
analyses/natural_loops.h
>
16
17
class
local_may_aliast
;
18
19
typedef
std::set<exprt>
modifiest
;
20
typedef
const
natural_loops_mutablet::natural_loopt
loopt
;
21
22
void
get_modifies
(
23
const
local_may_aliast
&local_may_alias,
24
const
loopt
&loop,
25
modifiest
&modifies);
26
27
void
build_havoc_code
(
28
const
goto_programt::targett
loop_head,
29
const
modifiest
&modifies,
30
goto_programt
&dest);
31
32
goto_programt::targett
get_loop_exit
(
const
loopt
&);
33
34
#endif // CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H
local_may_aliast
Definition:
local_may_alias.h:25
modifiest
std::set< exprt > modifiest
Definition:
loop_utils.h:17
natural_loops.h
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition:
loop_utils.cpp:89
build_havoc_code
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition:
loop_utils.cpp:37
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition:
goto_program.h:72
loopt
const typedef natural_loops_mutablet::natural_loopt loopt
Definition:
loop_utils.h:20
goto_programt::targett
instructionst::iterator targett
Definition:
goto_program.h:414
natural_loops_templatet< goto_programt, goto_programt::targett >::natural_loopt
std::set< goto_programt::targett > natural_loopt
Definition:
natural_loops.h:49
get_loop_exit
goto_programt::targett get_loop_exit(const loopt &)
Definition:
loop_utils.cpp:19
goto-instrument
loop_utils.h
Generated by
1.8.17