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
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Definition: loop_utils.cpp:88
std::set< T > natural_loopt
Definition: natural_loops.h:27
const natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
instructionst::iterator targett
Definition: goto_program.h:397
std::set< exprt > modifiest
Definition: loop_utils.h:17
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
goto_programt::targett get_loop_exit(const loopt &)
Definition: loop_utils.cpp:19
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Definition: loop_utils.cpp:37
Compute natural loops in a goto_function.