CBMC
dfcc_root_object.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 
7 Date: 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 
22 class exprt;
23 
28 std::unordered_set<exprt, irep_hash> dfcc_root_objects(const exprt &expr);
29 #endif
exprt
Base class for all expressions.
Definition: expr.h:56
dfcc_root_objects
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.
Definition: dfcc_root_object.cpp:133