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 
18 
19 typedef std::set<exprt> modifiest;
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 
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