cprover
local_bitvector_analysist::flagst Struct Reference

#include <local_bitvector_analysis.h>

Public Types

enum  bitst {
  B_unknown =1<<0 , B_uninitialized =1<<1 , B_uses_offset =1<<2 , B_dynamic_local =1<<3 ,
  B_dynamic_heap =1<<4 , B_null =1<<5 , B_static_lifetime =1<<6 , B_integer_address =1<<7
}
 

Public Member Functions

 flagst ()
 
void clear ()
 
 flagst (const bitst _bits)
 
bool merge (const flagst &other)
 
bool is_unknown () const
 
bool is_uninitialized () const
 
bool is_uses_offset () const
 
bool is_dynamic_local () const
 
bool is_dynamic_heap () const
 
bool is_null () const
 
bool is_static_lifetime () const
 
bool is_integer_address () const
 
void print (std::ostream &) const
 
flagst operator| (const flagst other) const
 

Static Public Member Functions

static flagst mk_unknown ()
 
static flagst mk_uninitialized ()
 
static flagst mk_uses_offset ()
 
static flagst mk_dynamic_local ()
 
static flagst mk_dynamic_heap ()
 
static flagst mk_null ()
 
static flagst mk_static_lifetime ()
 
static flagst mk_integer_address ()
 

Public Attributes

unsigned bits
 

Detailed Description

Definition at line 50 of file local_bitvector_analysis.h.

Member Enumeration Documentation

◆ bitst

Enumerator
B_unknown 
B_uninitialized 
B_uses_offset 
B_dynamic_local 
B_dynamic_heap 
B_null 
B_static_lifetime 
B_integer_address 

Definition at line 62 of file local_bitvector_analysis.h.

Constructor & Destructor Documentation

◆ flagst() [1/2]

local_bitvector_analysist::flagst::flagst ( )
inline

Definition at line 52 of file local_bitvector_analysis.h.

◆ flagst() [2/2]

local_bitvector_analysist::flagst::flagst ( const bitst  _bits)
inlineexplicit

Definition at line 74 of file local_bitvector_analysis.h.

Member Function Documentation

◆ clear()

void local_bitvector_analysist::flagst::clear ( void  )
inline

Definition at line 56 of file local_bitvector_analysis.h.

◆ is_dynamic_heap()

bool local_bitvector_analysist::flagst::is_dynamic_heap ( ) const
inline

Definition at line 132 of file local_bitvector_analysis.h.

◆ is_dynamic_local()

bool local_bitvector_analysist::flagst::is_dynamic_local ( ) const
inline

Definition at line 122 of file local_bitvector_analysis.h.

◆ is_integer_address()

bool local_bitvector_analysist::flagst::is_integer_address ( ) const
inline

Definition at line 162 of file local_bitvector_analysis.h.

◆ is_null()

bool local_bitvector_analysist::flagst::is_null ( ) const
inline

Definition at line 142 of file local_bitvector_analysis.h.

◆ is_static_lifetime()

bool local_bitvector_analysist::flagst::is_static_lifetime ( ) const
inline

Definition at line 152 of file local_bitvector_analysis.h.

◆ is_uninitialized()

bool local_bitvector_analysist::flagst::is_uninitialized ( ) const
inline

Definition at line 102 of file local_bitvector_analysis.h.

◆ is_unknown()

bool local_bitvector_analysist::flagst::is_unknown ( ) const
inline

Definition at line 92 of file local_bitvector_analysis.h.

◆ is_uses_offset()

bool local_bitvector_analysist::flagst::is_uses_offset ( ) const
inline

Definition at line 112 of file local_bitvector_analysis.h.

◆ merge()

bool local_bitvector_analysist::flagst::merge ( const flagst other)
inline

Definition at line 80 of file local_bitvector_analysis.h.

◆ mk_dynamic_heap()

static flagst local_bitvector_analysist::flagst::mk_dynamic_heap ( )
inlinestatic

Definition at line 127 of file local_bitvector_analysis.h.

◆ mk_dynamic_local()

static flagst local_bitvector_analysist::flagst::mk_dynamic_local ( )
inlinestatic

Definition at line 117 of file local_bitvector_analysis.h.

◆ mk_integer_address()

static flagst local_bitvector_analysist::flagst::mk_integer_address ( )
inlinestatic

Definition at line 157 of file local_bitvector_analysis.h.

◆ mk_null()

static flagst local_bitvector_analysist::flagst::mk_null ( )
inlinestatic

Definition at line 137 of file local_bitvector_analysis.h.

◆ mk_static_lifetime()

static flagst local_bitvector_analysist::flagst::mk_static_lifetime ( )
inlinestatic

Definition at line 147 of file local_bitvector_analysis.h.

◆ mk_uninitialized()

static flagst local_bitvector_analysist::flagst::mk_uninitialized ( )
inlinestatic

Definition at line 97 of file local_bitvector_analysis.h.

◆ mk_unknown()

static flagst local_bitvector_analysist::flagst::mk_unknown ( )
inlinestatic

Definition at line 87 of file local_bitvector_analysis.h.

◆ mk_uses_offset()

static flagst local_bitvector_analysist::flagst::mk_uses_offset ( )
inlinestatic

Definition at line 107 of file local_bitvector_analysis.h.

◆ operator|()

flagst local_bitvector_analysist::flagst::operator| ( const flagst  other) const
inline

Definition at line 169 of file local_bitvector_analysis.h.

◆ print()

void local_bitvector_analysist::flagst::print ( std::ostream &  out) const

Definition at line 20 of file local_bitvector_analysis.cpp.

Member Data Documentation

◆ bits

unsigned local_bitvector_analysist::flagst::bits

Definition at line 78 of file local_bitvector_analysis.h.


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