range_domain_baset Class Reference

#include <goto_rw.h>

Inheritance diagram for range_domain_baset:

Public Member Functions
	range_domain_baset ()=default
	range_domain_baset (const range_domain_baset &rhs)=delete
range_domain_baset &	operator= (const range_domain_baset &rhs)=delete
	range_domain_baset (range_domain_baset &&rhs)=delete
range_domain_baset &	operator= (range_domain_baset &&rhs)=delete
virtual	~range_domain_baset ()
virtual void	output (const namespacet &ns, std::ostream &out) const =0

Detailed Description

Definition at line 41 of file goto_rw.h.

Constructor & Destructor Documentation

range_domain_baset() [1/3]

range_domain_baset::range_domain_baset ( )

default

range_domain_baset() [2/3]

range_domain_baset::range_domain_baset ( const range_domain_baset &  rhs )

delete

range_domain_baset() [3/3]

range_domain_baset::range_domain_baset ( range_domain_baset &&  rhs )

delete

~range_domain_baset()

range_domain_baset::~range_domain_baset ( )

virtual

Definition at line 30 of file goto_rw.cpp.

Member Function Documentation

operator=() [1/2]

range_domain_baset & range_domain_baset::operator= ( const range_domain_baset &  rhs )

delete

operator=() [2/2]

range_domain_baset & range_domain_baset::operator= ( range_domain_baset &&  rhs )

delete

output()

virtual void range_domain_baset::output ( const namespacet &  ns, std::ostream &  out  ) const

pure virtual

Implemented in range_domaint, and guarded_range_domaint.

---

The documentation for this class was generated from the following files:

• /home/runner/work/cbmc/cbmc/src/analyses/goto_rw.h
• /home/runner/work/cbmc/cbmc/src/analyses/goto_rw.cpp