In a number of places we need to work with sets of histories so that these (a) make use of the immutability and sharing and (b) ownership can be transfered if necessary, we use shared pointers rather than references. More...

#include <ai_history.h>

Public Member Functions
bool	operator() (const trace_ptrt &l, const trace_ptrt &r) const

Detailed Description

In a number of places we need to work with sets of histories so that these (a) make use of the immutability and sharing and (b) ownership can be transfered if necessary, we use shared pointers rather than references.

One of the uses of this structure is as the work-list of the analyzer. Here the ordering of the set is very significant as it controls the order of exploration of the program. This affects performance and in some cases it can affect the results. This custom comparison allows particular histories to control the order of exploration.

Definition at line 72 of file ai_history.h.

Member Function Documentation

◆ operator()()

bool ai_history_baset::compare_historyt::operator()	(	const trace_ptrt &	l,
		const trace_ptrt &	r
	)		const

inline

Definition at line 74 of file ai_history.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/ai_history.h

Public Member Functions

Detailed Description

Member Function Documentation

◆ operator()()