cprover
|
#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 |
Definition at line 47 of file local_bitvector_analysis.h.
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.
|
inline |
Definition at line 49 of file local_bitvector_analysis.h.
Referenced by mk_dynamic_heap(), mk_dynamic_local(), mk_integer_address(), mk_null(), mk_static_lifetime(), mk_uninitialized(), mk_unknown(), and mk_uses_offset().
|
inlineexplicit |
Definition at line 71 of file local_bitvector_analysis.h.
|
inline |
Definition at line 53 of file local_bitvector_analysis.h.
References bits.
|
inline |
Definition at line 129 of file local_bitvector_analysis.h.
References B_dynamic_heap, and bits.
Referenced by print().
|
inline |
Definition at line 119 of file local_bitvector_analysis.h.
References B_dynamic_local, and bits.
Referenced by print().
|
inline |
Definition at line 159 of file local_bitvector_analysis.h.
References B_integer_address, and bits.
Referenced by print().
|
inline |
Definition at line 139 of file local_bitvector_analysis.h.
Referenced by goto_checkt::goto_check(), and print().
|
inline |
Definition at line 149 of file local_bitvector_analysis.h.
References B_static_lifetime, and bits.
Referenced by print().
|
inline |
Definition at line 99 of file local_bitvector_analysis.h.
References B_uninitialized, and bits.
Referenced by print().
|
inline |
Definition at line 89 of file local_bitvector_analysis.h.
References B_unknown, and bits.
Referenced by goto_checkt::goto_check(), and print().
|
inline |
Definition at line 109 of file local_bitvector_analysis.h.
References B_uses_offset, and bits.
Referenced by print().
|
inline |
Definition at line 77 of file local_bitvector_analysis.h.
References bits.
|
inlinestatic |
Definition at line 124 of file local_bitvector_analysis.h.
References B_dynamic_heap, and flagst().
Referenced by local_bitvector_analysist::get_rec().
|
inlinestatic |
Definition at line 114 of file local_bitvector_analysis.h.
References B_dynamic_local, and flagst().
Referenced by local_bitvector_analysist::get_rec().
|
inlinestatic |
Definition at line 154 of file local_bitvector_analysis.h.
References B_integer_address, and flagst().
Referenced by local_bitvector_analysist::get_rec().
|
inlinestatic |
Definition at line 134 of file local_bitvector_analysis.h.
References B_null, and flagst().
Referenced by local_bitvector_analysist::get_rec().
|
inlinestatic |
Definition at line 144 of file local_bitvector_analysis.h.
References B_static_lifetime, and flagst().
Referenced by local_bitvector_analysist::get_rec().
|
inlinestatic |
Definition at line 94 of file local_bitvector_analysis.h.
References B_uninitialized, and flagst().
Referenced by local_bitvector_analysist::get_rec().
|
inlinestatic |
Definition at line 84 of file local_bitvector_analysis.h.
References B_unknown, and flagst().
Referenced by local_bitvector_analysist::build(), and local_bitvector_analysist::get_rec().
|
inlinestatic |
Definition at line 104 of file local_bitvector_analysis.h.
References B_uses_offset, and flagst().
Referenced by local_bitvector_analysist::get_rec().
Definition at line 166 of file local_bitvector_analysis.h.
References bits.
void local_bitvector_analysist::flagst::print | ( | std::ostream & | out | ) | const |
Definition at line 24 of file local_bitvector_analysis.cpp.
References is_dynamic_heap(), is_dynamic_local(), is_integer_address(), is_null(), is_static_lifetime(), is_uninitialized(), is_unknown(), and is_uses_offset().
Referenced by operator<<().
unsigned local_bitvector_analysist::flagst::bits |
Definition at line 75 of file local_bitvector_analysis.h.
Referenced by clear(), is_dynamic_heap(), is_dynamic_local(), is_integer_address(), is_null(), is_static_lifetime(), is_uninitialized(), is_unknown(), is_uses_offset(), merge(), and operator|().