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 47 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 59 of file local_bitvector_analysis.h.

Constructor & Destructor Documentation

§ flagst() [1/2]

local_bitvector_analysist::flagst::flagst ( )
inline

§ flagst() [2/2]

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

Definition at line 71 of file local_bitvector_analysis.h.

Member Function Documentation

§ clear()

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

Definition at line 53 of file local_bitvector_analysis.h.

References bits.

§ is_dynamic_heap()

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

Definition at line 129 of file local_bitvector_analysis.h.

References B_dynamic_heap.

Referenced by goto_checkt::pointer_validity_check(), and print().

§ is_dynamic_local()

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

Definition at line 119 of file local_bitvector_analysis.h.

References B_dynamic_local.

Referenced by goto_checkt::pointer_validity_check(), and print().

§ is_integer_address()

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

Definition at line 159 of file local_bitvector_analysis.h.

References B_integer_address, and print().

Referenced by print().

§ is_null()

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

§ is_static_lifetime()

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

Definition at line 149 of file local_bitvector_analysis.h.

References B_static_lifetime.

Referenced by goto_checkt::pointer_validity_check(), and print().

§ is_uninitialized()

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

Definition at line 99 of file local_bitvector_analysis.h.

References B_uninitialized.

Referenced by goto_checkt::pointer_validity_check(), and print().

§ is_unknown()

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

§ is_uses_offset()

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

Definition at line 109 of file local_bitvector_analysis.h.

References B_uses_offset.

Referenced by print().

§ merge()

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

§ mk_dynamic_heap()

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

Definition at line 124 of file local_bitvector_analysis.h.

References B_dynamic_heap, and flagst().

Referenced by local_bitvector_analysist::get_rec().

§ mk_dynamic_local()

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

Definition at line 114 of file local_bitvector_analysis.h.

References B_dynamic_local, and flagst().

Referenced by local_bitvector_analysist::get_rec().

§ mk_integer_address()

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

Definition at line 154 of file local_bitvector_analysis.h.

References B_integer_address, and flagst().

Referenced by local_bitvector_analysist::get_rec().

§ mk_null()

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

Definition at line 134 of file local_bitvector_analysis.h.

References B_null, and flagst().

Referenced by local_bitvector_analysist::get_rec().

§ mk_static_lifetime()

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

Definition at line 144 of file local_bitvector_analysis.h.

References B_static_lifetime, and flagst().

Referenced by local_bitvector_analysist::get_rec().

§ mk_uninitialized()

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

Definition at line 94 of file local_bitvector_analysis.h.

References B_uninitialized, and flagst().

Referenced by local_bitvector_analysist::get_rec().

§ mk_unknown()

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

§ mk_uses_offset()

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

Definition at line 104 of file local_bitvector_analysis.h.

References B_uses_offset, and flagst().

Referenced by local_bitvector_analysist::get_rec().

§ operator|()

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

Definition at line 166 of file local_bitvector_analysis.h.

References bits, and local_bitvector_analysist::build().

§ print()

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

Member Data Documentation

§ bits

unsigned local_bitvector_analysist::flagst::bits

Definition at line 75 of file local_bitvector_analysis.h.

Referenced by clear(), merge(), and operator|().


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