CBMC
uninitializedt Class Reference
+ Collaboration diagram for uninitializedt:

Public Member Functions

 uninitializedt (symbol_table_baset &_symbol_table)
 
void add_assertions (const irep_idt &function_identifer, goto_programt &goto_program)
 

Protected Member Functions

void get_tracking (goto_programt::const_targett i_it)
 which variables need tracking, i.e., are uninitialized and may be read? More...
 

Protected Attributes

symbol_table_basetsymbol_table
 
namespacet ns
 
uninitialized_analysist uninitialized_analysis
 
std::set< irep_idttracking
 

Detailed Description

Definition at line 18 of file uninitialized.cpp.

Constructor & Destructor Documentation

◆ uninitializedt()

uninitializedt::uninitializedt ( symbol_table_baset _symbol_table)
inlineexplicit

Definition at line 21 of file uninitialized.cpp.

Member Function Documentation

◆ add_assertions()

void uninitializedt::add_assertions ( const irep_idt function_identifer,
goto_programt goto_program 
)

Definition at line 63 of file uninitialized.cpp.

◆ get_tracking()

void uninitializedt::get_tracking ( goto_programt::const_targett  i_it)
protected

which variables need tracking, i.e., are uninitialized and may be read?

Definition at line 43 of file uninitialized.cpp.

Member Data Documentation

◆ ns

namespacet uninitializedt::ns
protected

Definition at line 32 of file uninitialized.cpp.

◆ symbol_table

symbol_table_baset& uninitializedt::symbol_table
protected

Definition at line 31 of file uninitialized.cpp.

◆ tracking

std::set<irep_idt> uninitializedt::tracking
protected

Definition at line 37 of file uninitialized.cpp.

◆ uninitialized_analysis

uninitialized_analysist uninitializedt::uninitialized_analysis
protected

Definition at line 33 of file uninitialized.cpp.


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