memory_snapshot_harness_generatort::preordert< Key > Struct Template Reference

Simple structure for linearising posets. More...

#include <memory_snapshot_harness_generator.h>

Collaboration diagram for memory_snapshot_harness_generatort::preordert< Key >:

Public Types
using	relationt = std::multimap< Key, Key >
using	keyst = std::set< Key >

Public Member Functions
	preordert (const relationt &preorder_relation)
template<typename T >
void	sort (const std::vector< std::pair< Key, T >> &input, std::vector< std::pair< Key, T >> &output)

Private Member Functions
template<typename Value , typename Map , typename Handler >
void	dfs (Value &&node, Map &&key_to_t, Handler &&handle)
template<typename Value , typename Map , typename Handler >
void	dfs_inner (Value &&node, Map &&key_to_t, Handler &&handle)

Private Attributes
const relationt &	preorder_relation
keyst	seen
keyst	inserted

Detailed Description

template<typename Key>
struct memory_snapshot_harness_generatort::preordert< Key >

Simple structure for linearising posets.

Should be constructed with a map assigning a key to a set of keys that precede it.

Definition at line 292 of file memory_snapshot_harness_generator.h.

Member Typedef Documentation

keyst

template<typename Key >

using memory_snapshot_harness_generatort::preordert< Key >::keyst = std::set<Key>

Definition at line 296 of file memory_snapshot_harness_generator.h.

relationt

template<typename Key >

using memory_snapshot_harness_generatort::preordert< Key >::relationt = std::multimap<Key, Key>

Definition at line 295 of file memory_snapshot_harness_generator.h.

Constructor & Destructor Documentation

preordert()

template<typename Key >

memory_snapshot_harness_generatort::preordert< Key >::preordert ( const relationt &  preorder_relation )

inlineexplicit

Definition at line 298 of file memory_snapshot_harness_generator.h.

Member Function Documentation

dfs()

template<typename Key >

template<typename Value , typename Map , typename Handler >

void memory_snapshot_harness_generatort::preordert< Key >::dfs ( Value &&  node, Map &&  key_to_t, Handler &&  handle  )

inlineprivate

Definition at line 338 of file memory_snapshot_harness_generator.h.

dfs_inner()

template<typename Key >

template<typename Value , typename Map , typename Handler >

void memory_snapshot_harness_generatort::preordert< Key >::dfs_inner ( Value &&  node, Map &&  key_to_t, Handler &&  handle  )

inlineprivate

Definition at line 347 of file memory_snapshot_harness_generator.h.

sort()

template<typename Key >

template<typename T >

void memory_snapshot_harness_generatort::preordert< Key >::sort ( const std::vector< std::pair< Key, T >> &  input, std::vector< std::pair< Key, T >> &  output  )

inline

Definition at line 304 of file memory_snapshot_harness_generator.h.

Member Data Documentation

inserted

template<typename Key >

keyst memory_snapshot_harness_generatort::preordert< Key >::inserted

private

Definition at line 335 of file memory_snapshot_harness_generator.h.

preorder_relation

template<typename Key >

const relationt& memory_snapshot_harness_generatort::preordert< Key >::preorder_relation

private

Definition at line 332 of file memory_snapshot_harness_generator.h.

seen

template<typename Key >

keyst memory_snapshot_harness_generatort::preordert< Key >::seen

private

Definition at line 334 of file memory_snapshot_harness_generator.h.

---

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

• /home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-harness/memory_snapshot_harness_generator.h