CBMC
Public Types | Public Member Functions | Static Public Member Functions | Public Attributes | List of all members
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 48 of file local_bitvector_analysis.h.

Member Enumeration Documentation

◆ bitst

enum local_bitvector_analysist::flagst::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 60 of file local_bitvector_analysis.h.

Constructor & Destructor Documentation

◆ flagst() [1/2]

local_bitvector_analysist::flagst::flagst ( )
inline

Definition at line 50 of file local_bitvector_analysis.h.

◆ flagst() [2/2]

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

Definition at line 72 of file local_bitvector_analysis.h.

Member Function Documentation

◆ clear()

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

Definition at line 54 of file local_bitvector_analysis.h.

◆ is_dynamic_heap()

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

Definition at line 130 of file local_bitvector_analysis.h.

◆ is_dynamic_local()

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

Definition at line 120 of file local_bitvector_analysis.h.

◆ is_integer_address()

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

Definition at line 160 of file local_bitvector_analysis.h.

◆ is_null()

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

Definition at line 140 of file local_bitvector_analysis.h.

◆ is_static_lifetime()

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

Definition at line 150 of file local_bitvector_analysis.h.

◆ is_uninitialized()

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

Definition at line 100 of file local_bitvector_analysis.h.

◆ is_unknown()

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

Definition at line 90 of file local_bitvector_analysis.h.

◆ is_uses_offset()

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

Definition at line 110 of file local_bitvector_analysis.h.

◆ merge()

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

Definition at line 78 of file local_bitvector_analysis.h.

◆ mk_dynamic_heap()

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

Definition at line 125 of file local_bitvector_analysis.h.

◆ mk_dynamic_local()

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

Definition at line 115 of file local_bitvector_analysis.h.

◆ mk_integer_address()

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

Definition at line 155 of file local_bitvector_analysis.h.

◆ mk_null()

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

Definition at line 135 of file local_bitvector_analysis.h.

◆ mk_static_lifetime()

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

Definition at line 145 of file local_bitvector_analysis.h.

◆ mk_uninitialized()

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

Definition at line 95 of file local_bitvector_analysis.h.

◆ mk_unknown()

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

Definition at line 85 of file local_bitvector_analysis.h.

◆ mk_uses_offset()

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

Definition at line 105 of file local_bitvector_analysis.h.

◆ operator|()

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

Definition at line 167 of file local_bitvector_analysis.h.

◆ print()

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

Definition at line 21 of file local_bitvector_analysis.cpp.

Member Data Documentation

◆ bits

unsigned local_bitvector_analysist::flagst::bits

Definition at line 76 of file local_bitvector_analysis.h.

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