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
irep.h
src
goto-instrument
contracts
dynamic-frames
dfcc_root_object.h
Generated by
1.9.1