Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/context/cdo.h	Lines:	33	33	100.0 %
Date:	2021-05-22	Branches:	82	174	47.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Clark Barrett, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A context-dependent object.
 */

#include "cvc5_private.h"

#ifndef CVC5__CONTEXT__CDO_H
#define CVC5__CONTEXT__CDO_H

#include "context/context.h"

namespace cvc5 {
namespace context {

/**
 * Most basic template for context-dependent objects.  Simply makes a copy
 * (using the copy constructor) of class T when saving, and copies it back
 * (using operator=) during restore.
 */
template <class T>
class CDO : public ContextObj {

  /**
   * The data of type T being stored in this context-dependent object.
   */
  T d_data;

protected:

  /**
   * Copy constructor - it's private to ensure it is only used by save().
   * Basic CDO objects, cannot be copied-they have to be unique.
   */
  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}

  /**
   * operator= for CDO is private to ensure CDO object is not copied.
   */
  CDO<T>& operator=(const CDO<T>& cdo) = delete;

  /**
   * Implementation of mandatory ContextObj method save: simply copies the
   * current data to a copy using the copy constructor.  Memory is allocated
   * using the ContextMemoryManager.
   */
  ContextObj* save(ContextMemoryManager* pCMM) override
  {
    Debug("context") << "save cdo " << this;
    ContextObj* p = new(pCMM) CDO<T>(*this);
    Debug("context") << " to " << p << std::endl;
    return p;
  }

  /**
   * Implementation of mandatory ContextObj method restore: simply copies the
   * saved data back from the saved copy using operator= for T.
   */
  void restore(ContextObj* pContextObj) override
  {
    //Debug("context") << "restore cdo " << this;
    CDO<T>* p = static_cast<CDO<T>*>(pContextObj);
    d_data = p->d_data;
    //Debug("context") << " to " << get() << std::endl;
    // Explicitly call destructor as it will not otherwise get called.
    p->d_data.~T();
  }

public:

  /**
   * Main constructor - uses default constructor for T to create the initial
   * value of d_data.
   */
  CDO(Context* context) :
    ContextObj(context),
    d_data(T()) {
  }

  /**
   * Main constructor - uses default constructor for T to create the
   * initial value of d_data.
   *
   * This version takes an argument that specifies whether this CDO<>
   * was itself allocated in context memory.  If it was, it is linked
   * with the current scope rather than scope 0.
   *
   * WARNING: Read the notes in src/context/context.h on "Gotchas when
   * allocating contextual objects with non-standard allocators."
   */
  CDO(bool allocatedInCMM, Context* context) :
    ContextObj(allocatedInCMM, context),
    d_data(T()) {
  }

  /**
   * Constructor from object of type T.  Creates a ContextObj and sets the data
   * to the given data value.  Note that this value is only valid in the
   * current Scope.  If the Scope is popped, the value will revert to whatever
   * is assigned by the default constructor for T
   */
  CDO(Context* context, const T& data) :
    ContextObj(context),
    d_data(T()) {
    makeCurrent();
    d_data = data;
  }

  /**
   * Constructor from object of type T.  Creates a ContextObj and sets the data
   * to the given data value.  Note that this value is only valid in the
   * current Scope.  If the Scope is popped, the value will revert to whatever
   * is assigned by the default constructor for T.
   *
   * This version takes an argument that specifies whether this CDO<>
   * was itself allocated in context memory.  If it was, it is linked
   * with the current scope rather than scope 0.
   *
   * WARNING: Read the notes in src/context/context.h on "Gotchas when
   * allocating contextual objects with non-standard allocators."
   */
  CDO(bool allocatedInCMM, Context* context, const T& data) :
    ContextObj(allocatedInCMM, context),
    d_data(T()) {
    makeCurrent();
    d_data = data;
  }

  /**
   * Destructor - call destroy() method
   */
  ~CDO() { destroy(); }

  /**
   * Set the data in the CDO.  First call makeCurrent.
   */
  void set(const T& data) {
    makeCurrent();
    d_data = data;
  }

  /**
   * Get the current data from the CDO.  Read-only.
   */
  const T& get() const { return d_data; }

  /**
   * For convenience, define operator T() to be the same as get().
   */
  operator T() { return get(); }

  /**
   * For convenience, define operator const T() to be the same as get().
   */
  operator const T() const { return get(); }

  /**
   * For convenience, define operator= that takes an object of type T.
   */
  CDO<T>& operator=(const T& data) {
    set(data);
    return *this;
  }

};/* class CDO */

}  // namespace context
}  // namespace cvc5

#endif /* CVC5__CONTEXT__CDO_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Clark Barrett, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* A context-dependent object.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__CONTEXT__CDO_H
19		#define CVC5__CONTEXT__CDO_H
20
21		#include "context/context.h"
22
23		namespace cvc5 {
24		namespace context {
25
26		/**
27		* Most basic template for context-dependent objects. Simply makes a copy
28		* (using the copy constructor) of class T when saving, and copies it back
29		* (using operator=) during restore.
30		*/
31		template <class T>
32		class CDO : public ContextObj {
33
34		/**
35		* The data of type T being stored in this context-dependent object.
36		*/
37		T d_data;
38
39		protected:
40
41		/**
42		* Copy constructor - it's private to ensure it is only used by save().
43		* Basic CDO objects, cannot be copied-they have to be unique.
44		*/
45	20984812	CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
46
47		/**
48		* operator= for CDO is private to ensure CDO object is not copied.
49		*/
50		CDO<T>& operator=(const CDO<T>& cdo) = delete;
51
52		/**
53		* Implementation of mandatory ContextObj method save: simply copies the
54		* current data to a copy using the copy constructor. Memory is allocated
55		* using the ContextMemoryManager.
56		*/
57	20984812	ContextObj* save(ContextMemoryManager* pCMM) override
58		{
59	20984812	Debug("context") << "save cdo " << this;
60	20984812	ContextObj* p = new(pCMM) CDO<T>(*this);
61	20984812	Debug("context") << " to " << p << std::endl;
62	20984812	return p;
63		}
64
65		/**
66		* Implementation of mandatory ContextObj method restore: simply copies the
67		* saved data back from the saved copy using operator= for T.
68		*/
69	20984812	void restore(ContextObj* pContextObj) override
70		{
71		//Debug("context") << "restore cdo " << this;
72	20984812	CDO<T>* p = static_cast<CDO<T>*>(pContextObj);
73	20984812	d_data = p->d_data;
74		//Debug("context") << " to " << get() << std::endl;
75		// Explicitly call destructor as it will not otherwise get called.
76	371882	p->d_data.~T();
77	20984812	}
78
79		public:
80
81		/**
82		* Main constructor - uses default constructor for T to create the initial
83		* value of d_data.
84		*/
85	186335	CDO(Context* context) :
86		ContextObj(context),
87	186335	d_data(T()) {
88	186335	}
89
90		/**
91		* Main constructor - uses default constructor for T to create the
92		* initial value of d_data.
93		*
94		* This version takes an argument that specifies whether this CDO<>
95		* was itself allocated in context memory. If it was, it is linked
96		* with the current scope rather than scope 0.
97		*
98		* WARNING: Read the notes in src/context/context.h on "Gotchas when
99		* allocating contextual objects with non-standard allocators."
100		*/
101	10140	CDO(bool allocatedInCMM, Context* context) :
102		ContextObj(allocatedInCMM, context),
103	10140	d_data(T()) {
104	10140	}
105
106		/**
107		* Constructor from object of type T. Creates a ContextObj and sets the data
108		* to the given data value. Note that this value is only valid in the
109		* current Scope. If the Scope is popped, the value will revert to whatever
110		* is assigned by the default constructor for T
111		*/
112	2491094	CDO(Context* context, const T& data) :
113		ContextObj(context),
114	2491094	d_data(T()) {
115	2491094	makeCurrent();
116	2491094	d_data = data;
117	2491094	}
118
119		/**
120		* Constructor from object of type T. Creates a ContextObj and sets the data
121		* to the given data value. Note that this value is only valid in the
122		* current Scope. If the Scope is popped, the value will revert to whatever
123		* is assigned by the default constructor for T.
124		*
125		* This version takes an argument that specifies whether this CDO<>
126		* was itself allocated in context memory. If it was, it is linked
127		* with the current scope rather than scope 0.
128		*
129		* WARNING: Read the notes in src/context/context.h on "Gotchas when
130		* allocating contextual objects with non-standard allocators."
131		*/
132		CDO(bool allocatedInCMM, Context* context, const T& data) :
133		ContextObj(allocatedInCMM, context),
134		d_data(T()) {
135		makeCurrent();
136		d_data = data;
137		}
138
139		/**
140		* Destructor - call destroy() method
141		*/
142	2684337	~CDO() { destroy(); }
143
144		/**
145		* Set the data in the CDO. First call makeCurrent.
146		*/
147	130766526	void set(const T& data) {
148	130766526	makeCurrent();
149	130766526	d_data = data;
150	130766526	}
151
152		/**
153		* Get the current data from the CDO. Read-only.
154		*/
155	989871525	const T& get() const { return d_data; }
156
157		/**
158		* For convenience, define operator T() to be the same as get().
159		*/
160	820475137	operator T() { return get(); }
161
162		/**
163		* For convenience, define operator const T() to be the same as get().
164		*/
165	141503317	operator const T() const { return get(); }
166
167		/**
168		* For convenience, define operator= that takes an object of type T.
169		*/
170	130179309	CDO<T>& operator=(const T& data) {
171	130179309	set(data);
172	130179309	return *this;
173		}
174
175		};/* class CDO */
176
177		} // namespace context
178		} // namespace cvc5
179
180		#endif /* CVC5__CONTEXT__CDO_H */