#include <list>
#include <string>
#include "goto_harness_generator.h"
#include "recursive_initialization.h"
#include <goto-programs/goto_model.h>
#include <util/message.h>
#include <util/optional.h>

Include dependency graph for memory_snapshot_harness_generator.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	memory_snapshot_harness_generatort
	Generates a harness which first assigns global variables with values from a given memory snapshot and then calls a specified function. More...

struct	memory_snapshot_harness_generatort::entry_goto_locationt
	User provided goto location: function name and (maybe) location number; the structure wraps this option with a parser. More...

struct	memory_snapshot_harness_generatort::entry_source_locationt
	User provided source location: file name and line number; the structure wraps this option with a parser. More...

struct	memory_snapshot_harness_generatort::entry_locationt
	Wraps the information needed to identify the entry point. More...

struct	memory_snapshot_harness_generatort::source_location_matcht
	Wraps the information for source location match candidates. More...

struct	memory_snapshot_harness_generatort::preordert< Key >
	Simple structure for linearising posets. More...

Classes