CBMC
Loading...
Searching...
No Matches
Classes | Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | List of all members
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 <call_stack_history.h>

+ Inheritance diagram for call_stack_historyt:
[フレーム]
[legend]
+ Collaboration diagram for call_stack_historyt:
[フレーム]
[legend]

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, trace_ptrt caller_hist) 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.
 
bool  operator< (const ai_history_baset &op) const override
  The order for history_sett.
 
bool  operator== (const ai_history_baset &op) const override
  History objects should be comparable.
 
const locationt &  current_location (void) const override
  The current location in the history, used to compute the transformer POSTCONDITION(return value is dereferenceable)
 
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.
 
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_entryt >  cse_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());.
 
  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 class   step_statust { NEW , MERGED , BLOCKED }
 
typedef goto_programt::const_targett  locationt
 
typedef std::shared_ptr< const ai_history_baset >  trace_ptrt
  History objects are intended to be immutable so they can be shared to reduce memory overhead.
 
typedef std::set< trace_ptrt, compare_historyt >  trace_sett
 
typedef std::pair< step_statust, trace_ptrt >  step_returnt
 
- Static Public Attributes inherited from ai_history_baset
static const trace_ptrt  no_caller_history
 

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 20 of file call_stack_history.h.

Member Typedef Documentation

◆  cse_ptrt

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

Definition at line 24 of file call_stack_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 53 of file call_stack_history.h.

◆  call_stack_historyt() [2/4]

call_stack_historyt::call_stack_historyt ( locationt  l )
inlineexplicit

Definition at line 63 of file call_stack_history.h.

◆  call_stack_historyt() [3/4]

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

Definition at line 70 of file call_stack_history.h.

◆  call_stack_historyt() [4/4]

call_stack_historyt::call_stack_historyt ( const call_stack_historyt &  old )
inline

Definition at line 77 of file call_stack_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 92 of file call_stack_history.h.

◆  has_recursion_limit()

bool call_stack_historyt::has_recursion_limit ( void  ) const
inlineprotected

Definition at line 48 of file call_stack_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 144 of file call_stack_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 152 of file call_stack_history.cpp.

◆  output()

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

Reimplemented from ai_history_baset.

Definition at line 160 of file call_stack_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 100 of file call_stack_history.h.

◆  step()

ai_history_baset::step_returnt call_stack_historyt::step ( locationt  to,
const trace_sett &  others,
trace_ptrt  caller_hist 
) 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.

In the case of function call return it is also given the full history of the caller. This allows function-local histories as they can "pick up" the state from before the call when computing the return edge.

PRECONDITION(to.id_dereferenceable()); PRECONDITION(to in goto_program.get_successors(current_location()) || current_location()->is_function_call() || current_location()->is_end_function()); PRECONDITION(caller_hist == no_caller_history || 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 14 of file call_stack_history.cpp.

Member Data Documentation

◆  current_stack

cse_ptrt call_stack_historyt::current_stack
protected

Definition at line 39 of file call_stack_history.h.

◆  recursion_limit

unsigned int call_stack_historyt::recursion_limit
protected

Definition at line 46 of file call_stack_history.h.

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

AltStyle によって変換されたページ (->オリジナル) /