cprover
Loading...
Searching...
No Matches
dfcc_infer_loop_assigns.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INFER_LOOP_ASSIGNS_H
13#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_INFER_LOOP_ASSIGNS_H
14
18class messaget;
19class namespacet;
20
21// \brief Infer assigns clause targets for a loop from its instructions and a
22// may alias analysis at the function level.
24 const local_may_aliast &local_may_alias,
25 const loopt &loop_instructions,
26 const source_locationt &loop_head_location,
27 const namespacet &ns);
28
29#endif
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:94
assignst dfcc_infer_loop_assigns(const local_may_aliast &local_may_alias, const loopt &loop_instructions, const source_locationt &loop_head_location, const namespacet &ns)
std::set< exprt > assignst
Definition havoc_utils.h:24
Field-insensitive, location-sensitive may-alias analysis.
Helper functions for k-induction and loop invariants.
natural_loops_mutablet::natural_loopt loopt
Definition loop_utils.h:20