Loading...

Searching...

No Matches

dfcc_root_object.h

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:57

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

CBMC: /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_root_object.h Source File