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
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
 
void make_top () final
 
void make_bottom () final
 
void make_entry () 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 void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
 
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_innert, irep_id_hashvaluest
 
typedef std::unordered_map< irep_idt, ranges_at_loct, irep_id_hashexport_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

Definition at line 190 of file reaching_definitions.h.

§ ranges_at_loct

Definition at line 165 of file reaching_definitions.h.

§ rangest

Definition at line 164 of file reaching_definitions.h.

§ values_innert

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

Definition at line 178 of file reaching_definitions.h.

§ valuest

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

Definition at line 182 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 168 of file reaching_definitions.h.

Referenced by output().

§ gen()

§ get()

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

Definition at line 705 of file reaching_definitions.cpp.

References export_cache, and populate_cache().

§ 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 423 of file reaching_definitions.cpp.

References values.

Referenced by kill().

§ make_bottom()

void rd_range_domaint::make_bottom ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 138 of file reaching_definitions.h.

References sparse_bitvector_analysist< V >::values.

§ make_entry()

void rd_range_domaint::make_entry ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 146 of file reaching_definitions.h.

§ make_top()

void rd_range_domaint::make_top ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 130 of file reaching_definitions.h.

References sparse_bitvector_analysist< V >::values.

§ 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 620 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 569 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 656 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
inlinefinalvirtual

Reimplemented from ai_domain_baset.

Definition at line 122 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.

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 115 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

sparse_bitvector_analysist<reaching_definitiont>* rd_range_domaint::bv_container
private

Definition at line 176 of file reaching_definitions.h.

Referenced by gen(), kill(), populate_cache(), transform(), and transform_end_function().

§ export_cache

§ has_values

tvt rd_range_domaint::has_values
private

Definition at line 174 of file reaching_definitions.h.

Referenced by merge(), merge_shared(), and output().

§ values


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