CBMC
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> assignst;
21 
22 void get_assigns(
23  const local_may_aliast &local_may_alias,
24  const loopt &loop,
25  assignst &assigns);
26 
28 void get_assigns(
29  const local_may_aliast &local_may_alias,
30  const loopt &loop,
31  assignst &assigns,
32  std::function<bool(const exprt &)> predicate);
33 
34 void get_assigns_lhs(
35  const local_may_aliast &local_may_alias,
37  const exprt &lhs,
38  assignst &assigns);
39 
41 void get_assigns_lhs(
42  const local_may_aliast &local_may_alias,
44  const exprt &lhs,
45  assignst &assigns,
46  std::function<bool(const exprt &)> predicate);
47 
49 
50 #endif // CPROVER_GOTO_INSTRUMENT_LOOP_UTILS_H
Base class for all expressions.
Definition: expr.h:56
instructionst::iterator targett
Definition: goto_program.h:614
instructionst::const_iterator const_targett
Definition: goto_program.h:615
std::set< exprt > assignst
Definition: havoc_utils.h:22
natural_loops_mutablet::natural_loopt loopt
Definition: loop_utils.h:20
std::set< exprt > assignst
Definition: loop_utils.h:17
void get_assigns_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns)
Definition: loop_utils.cpp:39
goto_programt::targett get_loop_exit(const loopt &)
Definition: loop_utils.cpp:21
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Definition: loop_utils.cpp:90
Compute natural loops in a goto_function.