CBMC
memory_snapshot_harness_generator.h File Reference
#include <goto-programs/goto_program.h>
#include "goto_harness_generator.h"
#include "recursive_initialization.h"
#include <list>
#include <string>
+ 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...