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