CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
dfcc_root_object.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Dynamic frame condition checking
4
5Author: Remi Delmas, delmasrd@amazon.com
6
7Date: March 2023
8
9\*******************************************************************/
10
14
15#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_ROOT_OBJECT_H
16#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_ROOT_OBJECT_H
17
18#include <util/irep.h>
19
20#include <unordered_set>
21
22class exprt;
23
28std::unordered_set<exprt, irep_hash> dfcc_root_objects(const exprt &expr);
29#endif
Base class for all expressions.
Definition expr.h:56
std::unordered_set< exprt, irep_hash > dfcc_root_objects(const exprt &expr)
Computes a set of root object expressions from an lvalue or assigns clause target expression.