CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
location_update_visitor.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: A visitor class to update the last_written_locations of any visited
4 abstract_object with a given set of locations.
5
6 Author: Jez Higgins
7
8\*******************************************************************/
9#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LOCATION_UPDATE_VISITOR_H
10#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LOCATION_UPDATE_VISITOR_H
11
12#include "abstract_object.h"
13
16{
17public:
22
24 visit(const abstract_object_pointert &element) const override
25 {
26 return element->write_location_context(location);
27 }
28
29private:
31};
32
35{
36public:
42
44 visit(const abstract_object_pointert &element) const override
45 {
46 return element->merge_location_context(location);
47 }
48
49private:
51};
52
53#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_LOCATION_UPDATE_VISITOR_H
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
sharing_ptrt< class abstract_objectt > abstract_object_pointert
goto_programt::const_targett locationt
abstract_object_pointert visit(const abstract_object_pointert &element) const override
const abstract_objectt::locationt & location
location_update_visitort(const abstract_objectt::locationt &location)
const abstract_objectt::locationt & location
merge_location_update_visitort(const abstract_objectt::locationt &location)
abstract_object_pointert visit(const abstract_object_pointert &element) const override
Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstr...