cprover
uninitializedt Class Reference
Collaboration diagram for uninitializedt:
[legend]

Public Member Functions

 uninitializedt (symbol_tablet &_symbol_table)
 
void add_assertions (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_tabletsymbol_table
 
namespacet ns
 
uninitialized_analysist uninitialized_analysis
 
std::set< irep_idttracking
 

Detailed Description

Definition at line 22 of file uninitialized.cpp.

Constructor & Destructor Documentation

◆ uninitializedt()

uninitializedt::uninitializedt ( symbol_tablet _symbol_table)
inlineexplicit

Definition at line 25 of file uninitialized.cpp.

Member Function Documentation

◆ add_assertions()

◆ 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 46 of file uninitialized.cpp.

References forall_expr_list, symbol_exprt::get_identifier(), objects_read(), to_symbol_expr(), tracking, and uninitialized_analysis.

Referenced by add_assertions().

Member Data Documentation

◆ ns

namespacet uninitializedt::ns
protected

Definition at line 35 of file uninitialized.cpp.

Referenced by add_assertions().

◆ symbol_table

symbol_tablet& uninitializedt::symbol_table
protected

Definition at line 34 of file uninitialized.cpp.

Referenced by add_assertions().

◆ tracking

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

Definition at line 40 of file uninitialized.cpp.

Referenced by add_assertions(), and get_tracking().

◆ uninitialized_analysis

uninitialized_analysist uninitializedt::uninitialized_analysis
protected

Definition at line 36 of file uninitialized.cpp.

Referenced by add_assertions(), and get_tracking().


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