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 
22 void get_modifies(
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
Base class for all expressions.
Definition: expr.h:54
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
instructionst::iterator targett
Definition: goto_program.h:550
instructionst::const_iterator const_targett
Definition: goto_program.h:551
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:88
std::set< exprt > modifiest
Definition: loop_utils.h:17
goto_programt::targett get_loop_exit(const loopt &)
Definition: loop_utils.cpp:20
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:38
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:58
Compute natural loops in a goto_function.