cprover
ahistoricalt Class Reference

The common case of history is to only care about where you are now, not how you got there! Invariants are not checkable due to C++... More...

#include <ai_history.h>

+ Inheritance diagram for ahistoricalt:
+ Collaboration diagram for ahistoricalt:

Public Member Functions

 ahistoricalt (locationt l)
 
 ahistoricalt (const ahistoricalt &old)
 
step_returnt step (locationt to, const trace_sett &others) const override
 Step creates a new history by advancing the current one to location "to" It is given the set of all other histories that have reached this point. More...
 
bool operator< (const ai_history_baset &op) const override
 The order for history_sett. More...
 
bool operator== (const ai_history_baset &op) const override
 History objects should be comparable. More...
 
const locationtcurrent_location (void) const override
 The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable) More...
 
bool should_widen (const ai_history_baset &other) const override
 Domains with a substantial height may need to widen when merging this method allows the history to provide a hint on when to do this The suggested use of this is for domains merge operation to check this and then widen in a domain specific way. More...
 
void output (std::ostream &out) const override
 
- Public Member Functions inherited from ai_history_baset
virtual ~ai_history_baset ()
 
virtual jsont output_json (void) const
 
virtual xmlt output_xml (void) const
 

Protected Attributes

locationt current
 

Additional Inherited Members

- Public Types inherited from ai_history_baset
enum  step_statust { step_statust::NEW, step_statust::MERGED, step_statust::BLOCKED }
 
typedef goto_programt::const_targett locationt
 
typedef std::shared_ptr< const ai_history_basettrace_ptrt
 History objects are intended to be immutable so they can be shared to reduce memory overhead. More...
 
typedef std::set< trace_ptrt, compare_historyttrace_sett
 
typedef std::pair< step_statust, trace_ptrtstep_returnt
 
- Protected Member Functions inherited from ai_history_baset
 ai_history_baset (locationt)
 Create a new history starting from a given location This is used to start the analysis from scratch PRECONDITION(l.is_dereferenceable());. More...
 
 ai_history_baset (const ai_history_baset &)
 

Detailed Description

The common case of history is to only care about where you are now, not how you got there! Invariants are not checkable due to C++...

Definition at line 144 of file ai_history.h.

Constructor & Destructor Documentation

◆ ahistoricalt() [1/2]

ahistoricalt::ahistoricalt ( locationt  l)
inlineexplicit

Definition at line 151 of file ai_history.h.

◆ ahistoricalt() [2/2]

ahistoricalt::ahistoricalt ( const ahistoricalt old)
inline

Definition at line 155 of file ai_history.h.

Member Function Documentation

◆ current_location()

const locationt& ahistoricalt::current_location ( void  ) const
inlineoverridevirtual

The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)

Implements ai_history_baset.

Definition at line 203 of file ai_history.h.

◆ operator<()

bool ahistoricalt::operator< ( const ai_history_baset op) const
inlineoverridevirtual

The order for history_sett.

Implements ai_history_baset.

Definition at line 182 of file ai_history.h.

◆ operator==()

bool ahistoricalt::operator== ( const ai_history_baset op) const
inlineoverridevirtual

History objects should be comparable.

Implements ai_history_baset.

Definition at line 190 of file ai_history.h.

◆ output()

void ahistoricalt::output ( std::ostream &  out) const
inlineoverridevirtual

Reimplemented from ai_history_baset.

Definition at line 216 of file ai_history.h.

◆ should_widen()

bool ahistoricalt::should_widen ( const ai_history_baset other) const
inlineoverridevirtual

Domains with a substantial height may need to widen when merging this method allows the history to provide a hint on when to do this The suggested use of this is for domains merge operation to check this and then widen in a domain specific way.

However it could be used in other ways (such as the transformer). The key idea is that the history tracks / should know when to widen and when to continue.

Reimplemented from ai_history_baset.

Definition at line 211 of file ai_history.h.

◆ step()

step_returnt ahistoricalt::step ( locationt  to,
const trace_sett others 
) const
inlineoverridevirtual

Step creates a new history by advancing the current one to location "to" It is given the set of all other histories that have reached this point.

PRECONDITION(to.id_dereferenceable()); PRECONDITION(to in goto_program.get_successors(current_location()) || current_location()->is_function_call() || current_location()->is_end_function());

Step may do one of three things :

  1. Create a new history object and return a pointer to it This will force the analyser to continue regardless of domain changes POSTCONDITION(IMPLIES(result.first == step_statust::NEW, result.second.use_count() == 1 ));
  2. Merge with an existing history This means the analyser will only continue if the domain is updated POSTCONDITION(IMPLIES(result.first == step_statust::MERGED, result.second is an element of others));
  3. Block this flow of execution This indicates the transition is impossible (returning to a location other than the call location) or undesireable (omitting some traces) POSTCONDITION(IMPLIES(result.first == BLOCKED, result.second == nullptr()));

Implements ai_history_baset.

Definition at line 160 of file ai_history.h.

Member Data Documentation

◆ current

locationt ahistoricalt::current
protected

Definition at line 148 of file ai_history.h.


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