cprover
rd_range_domaint Class Reference

#include <reaching_definitions.h>

Inheritance diagram for rd_range_domaint:
[legend]
Collaboration diagram for rd_range_domaint:
[legend]

Public Types

typedef std::multimap< range_spect, range_spectrangest
 
typedef std::map< locationt, rangestranges_at_loct
 
- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Public Member Functions

 rd_range_domaint ()
 
void set_bitvector_container (sparse_bitvector_analysist< reaching_definitiont > &_bv_container)
 
void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns) final override
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
 
void make_top () final override
 
void make_bottom () final override
 
void make_entry () final override
 
bool is_top () const override final
 
bool is_bottom () const override final
 
bool merge (const rd_range_domaint &other, locationt from, locationt to)
 
bool merge_shared (const rd_range_domaint &other, locationt from, locationt to, const namespacet &ns)
 
const ranges_at_loctget (const irep_idt &identifier) const
 
void clear_cache (const irep_idt &identifier) const
 
- Public Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 
virtual ~ai_domain_baset ()
 
virtual jsont output_json (const ai_baset &ai, const namespacet &ns) const
 
virtual xmlt output_xml (const ai_baset &ai, const namespacet &ns) const
 
virtual bool ai_simplify (exprt &condition, const namespacet &ns) const
 
virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const
 Use the information in the domain to simplify the expression on the LHS of an assignment. More...
 

Private Types

typedef std::set< std::size_t > values_innert
 
typedef std::unordered_map< irep_idt, values_innertvaluest
 
typedef std::unordered_map< irep_idt, ranges_at_loctexport_cachet
 

Private Member Functions

void populate_cache (const irep_idt &identifier) const
 
void transform_dead (const namespacet &ns, locationt from)
 
void transform_start_thread (const namespacet &ns, reaching_definitions_analysist &rd)
 
void transform_function_call (const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
 
void transform_end_function (const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
 
void transform_assign (const namespacet &ns, locationt from, locationt to, reaching_definitions_analysist &rd)
 
void kill (const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
 
void kill_inf (const irep_idt &identifier, const range_spect &range_start)
 
bool gen (locationt from, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
 
void output (std::ostream &out) const
 
bool merge_inner (values_innert &dest, const values_innert &other)
 

Private Attributes

tvt has_values
 
sparse_bitvector_analysist< reaching_definitiont > * bv_container
 
valuest values
 
export_cachet export_cache
 

Detailed Description

Definition at line 100 of file reaching_definitions.h.

Member Typedef Documentation

◆ export_cachet

typedef std::unordered_map<irep_idt, ranges_at_loct> rd_range_domaint::export_cachet
private

Definition at line 201 of file reaching_definitions.h.

◆ ranges_at_loct

Definition at line 177 of file reaching_definitions.h.

◆ rangest

Definition at line 176 of file reaching_definitions.h.

◆ values_innert

typedef std::set<std::size_t> rd_range_domaint::values_innert
private

Definition at line 190 of file reaching_definitions.h.

◆ valuest

typedef std::unordered_map<irep_idt, values_innert> rd_range_domaint::valuest
private

Definition at line 194 of file reaching_definitions.h.

Constructor & Destructor Documentation

◆ rd_range_domaint()

rd_range_domaint::rd_range_domaint ( )
inline

Definition at line 103 of file reaching_definitions.h.

Member Function Documentation

◆ clear_cache()

void rd_range_domaint::clear_cache ( const irep_idt identifier) const
inline

Definition at line 180 of file reaching_definitions.h.

References export_cache.

Referenced by output().

◆ gen()

◆ get()

const rd_range_domaint::ranges_at_loct & rd_range_domaint::get ( const irep_idt identifier) const

Definition at line 714 of file reaching_definitions.cpp.

References export_cache, and populate_cache().

◆ is_bottom()

bool rd_range_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 156 of file reaching_definitions.h.

References DATA_INVARIANT, has_values, tvt::is_false(), and values.

◆ is_top()

bool rd_range_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 149 of file reaching_definitions.h.

References DATA_INVARIANT, has_values, tvt::is_true(), and values.

◆ kill()

void rd_range_domaint::kill ( const irep_idt identifier,
const range_spect range_start,
const range_spect range_end 
)
private

◆ kill_inf()

void rd_range_domaint::kill_inf ( const irep_idt identifier,
const range_spect range_start 
)
private

Definition at line 432 of file reaching_definitions.cpp.

References values.

Referenced by kill().

◆ make_bottom()

void rd_range_domaint::make_bottom ( )
inlinefinaloverridevirtual

◆ make_entry()

void rd_range_domaint::make_entry ( )
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 144 of file reaching_definitions.h.

References make_top().

◆ make_top()

void rd_range_domaint::make_top ( )
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 128 of file reaching_definitions.h.

References bv_container, sparse_bitvector_analysist< V >::clear(), has_values, and values.

Referenced by make_entry().

◆ merge()

bool rd_range_domaint::merge ( const rd_range_domaint other,
locationt  from,
locationt  to 
)
Returns
returns true iff there is something new

Definition at line 629 of file reaching_definitions.cpp.

References export_cache, has_values, tvt::is_false(), merge_inner(), tvt::unknown(), and values.

◆ merge_inner()

bool rd_range_domaint::merge_inner ( values_innert dest,
const values_innert other 
)
private
Returns
returns true iff there is something new

Definition at line 578 of file reaching_definitions.cpp.

References gen().

Referenced by merge(), and merge_shared().

◆ merge_shared()

bool rd_range_domaint::merge_shared ( const rd_range_domaint other,
locationt  from,
locationt  to,
const namespacet ns 
)
Returns
returns true iff there is something new

Definition at line 665 of file reaching_definitions.cpp.

References export_cache, has_values, tvt::is_false(), namespacet::lookup(), merge_inner(), tvt::unknown(), and values.

◆ output() [1/2]

void rd_range_domaint::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
inlinefinaloverridevirtual

Reimplemented from ai_domain_baset.

Definition at line 120 of file reaching_definitions.h.

◆ output() [2/2]

void rd_range_domaint::output ( std::ostream &  out) const
private

◆ populate_cache()

void rd_range_domaint::populate_cache ( const irep_idt identifier) const
private

◆ set_bitvector_container()

void rd_range_domaint::set_bitvector_container ( sparse_bitvector_analysist< reaching_definitiont > &  _bv_container)
inline

Definition at line 110 of file reaching_definitions.h.

References bv_container.

Referenced by reaching_definitions_analysist::get_state().

◆ transform()

◆ transform_assign()

◆ transform_dead()

void rd_range_domaint::transform_dead ( const namespacet ns,
locationt  from 
)
private

Definition at line 127 of file reaching_definitions.cpp.

References export_cache, code_deadt::symbol(), to_code_dead(), to_symbol_expr(), and values.

Referenced by transform().

◆ transform_end_function()

◆ transform_function_call()

◆ transform_start_thread()

void rd_range_domaint::transform_start_thread ( const namespacet ns,
reaching_definitions_analysist rd 
)
private

Member Data Documentation

◆ bv_container

◆ export_cache

◆ has_values

tvt rd_range_domaint::has_values
private

◆ values


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