CBMC
range_domain_baset Class Referenceabstract

#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_basetoperator= (const range_domain_baset &rhs)=delete
 
 range_domain_baset (range_domain_baset &&rhs)=delete
 
range_domain_basetoperator= (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 guarded_range_domaint, and range_domaint.


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