cprover
call_stack_historyt Class Reference

Records the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion. More...

#include <ai_history.h>

+ Inheritance diagram for call_stack_historyt:
+ Collaboration diagram for call_stack_historyt:

Classes

class  call_stack_entryt
 

Public Member Functions

 call_stack_historyt (locationt l)
 
 call_stack_historyt (locationt l, unsigned int rec_lim)
 
 call_stack_historyt (const call_stack_historyt &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 Types

typedef std::shared_ptr< const call_stack_entrytcse_ptrt
 

Protected Member Functions

bool has_recursion_limit (void) const
 
 call_stack_historyt (cse_ptrt cur_stack, unsigned int rec_lim)
 
- 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 &)
 

Protected Attributes

cse_ptrt current_stack
 
unsigned int recursion_limit
 

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
 

Detailed Description

Records the call stack Care must be taken when using this on recursive code; it will need the domain to be capable of limiting the recursion.

Definition at line 225 of file ai_history.h.

Member Typedef Documentation

◆ cse_ptrt

typedef std::shared_ptr<const call_stack_entryt> call_stack_historyt::cse_ptrt
protected

Definition at line 229 of file ai_history.h.

Constructor & Destructor Documentation

◆ call_stack_historyt() [1/4]

call_stack_historyt::call_stack_historyt ( cse_ptrt  cur_stack,
unsigned int  rec_lim 
)
inlineprotected

Definition at line 258 of file ai_history.h.

◆ call_stack_historyt() [2/4]

call_stack_historyt::call_stack_historyt ( locationt  l)
inlineexplicit

Definition at line 268 of file ai_history.h.

◆ call_stack_historyt() [3/4]

call_stack_historyt::call_stack_historyt ( locationt  l,
unsigned int  rec_lim 
)
inline

Definition at line 275 of file ai_history.h.

◆ call_stack_historyt() [4/4]

call_stack_historyt::call_stack_historyt ( const call_stack_historyt old)
inline

Definition at line 282 of file ai_history.h.

Member Function Documentation

◆ current_location()

const locationt& call_stack_historyt::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 294 of file ai_history.h.

◆ has_recursion_limit()

bool call_stack_historyt::has_recursion_limit ( void  ) const
inlineprotected

Definition at line 253 of file ai_history.h.

◆ operator<()

bool call_stack_historyt::operator< ( const ai_history_baset op) const
overridevirtual

The order for history_sett.

Implements ai_history_baset.

Definition at line 142 of file ai_history.cpp.

◆ operator==()

bool call_stack_historyt::operator== ( const ai_history_baset op) const
overridevirtual

History objects should be comparable.

Implements ai_history_baset.

Definition at line 150 of file ai_history.cpp.

◆ output()

void call_stack_historyt::output ( std::ostream &  out) const
overridevirtual

Reimplemented from ai_history_baset.

Definition at line 158 of file ai_history.cpp.

◆ should_widen()

bool call_stack_historyt::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 302 of file ai_history.h.

◆ step()

ai_history_baset::step_returnt call_stack_historyt::step ( locationt  to,
const trace_sett others 
) const
overridevirtual

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 32 of file ai_history.cpp.

Member Data Documentation

◆ current_stack

cse_ptrt call_stack_historyt::current_stack
protected

Definition at line 244 of file ai_history.h.

◆ recursion_limit

unsigned int call_stack_historyt::recursion_limit
protected

Definition at line 251 of file ai_history.h.


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