CBMC
Loading...
Searching...
No Matches
loop_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Helper functions for k-induction and loop invariants
4
5Author: 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
16
18
19typedef std::set<exprt> assignst;
21
22void get_assigns(
23 const local_may_aliast &local_may_alias,
24 const loopt &loop,
25 assignst &assigns);
26
28void 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
35 const local_may_aliast &local_may_alias,
37 const exprt &lhs,
38 assignst &assigns);
39
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
instructionst::const_iterator const_targett
std::set< exprt > assignst
Definition havoc_utils.h:24
natural_loops_mutablet::natural_loopt loopt
Definition loop_utils.h:20
std::set< exprt > assignst
Definition loop_utils.h:19
void get_assigns_lhs(const local_may_aliast &local_may_alias, goto_programt::const_targett t, const exprt &lhs, assignst &assigns)
goto_programt::targett get_loop_exit(const loopt &)
void get_assigns(const local_may_aliast &local_may_alias, const loopt &loop, assignst &assigns)
Compute natural loops in a goto_function.