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;
21 
23  const local_may_aliast &local_may_alias,
24  const loopt &loop,
25  modifiest &modifies);
26 
27 void get_modifies_lhs(
28  const local_may_aliast &local_may_alias,
30  const exprt &lhs,
31  modifiest &modifies);
32 
33 void build_havoc_code(
34  const goto_programt::targett loop_head,
35  const modifiest &modifies,
36  goto_programt &dest);
37 
39 
40 #endif // CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H
exprt
Base class for all expressions.
Definition: expr.h:53
loopt
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
local_may_aliast
Definition: local_may_alias.h:26
get_modifies_lhs
void get_modifies_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, modifiest &modifies)
Definition: loop_utils.cpp:57
modifiest
std::set< exprt > modifiest
Definition: loop_utils.h:17
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
natural_loops.h
Compute natural loops in a goto_function.
get_modifies
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
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:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
get_loop_exit
goto_programt::targett get_loop_exit(const loopt &)