CBMC
goto_harness_parse_options.cpp File Reference
#include "goto_harness_parse_options.h"
#include <util/config.h>
#include <util/exception_utils.h>
#include <util/exit_codes.h>
#include <util/help_formatter.h>
#include <util/invariant.h>
#include <util/suffix.h>
#include <util/version.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/read_goto_binary.h>
#include <goto-programs/write_goto_binary.h>
#include <goto-instrument/dump_c.h>
#include "function_call_harness_generator.h"
#include "goto_harness_generator_factory.h"
#include "memory_snapshot_harness_generator.h"
#include <algorithm>
#include <fstream>
#include <iostream>
#include <set>
#include <string>
#include <unordered_set>
#include <utility>
+ Include dependency graph for goto_harness_parse_options.cpp:

Go to the source code of this file.

Functions

std::unordered_set< irep_idtget_symbol_names_from_goto_model (const goto_modelt &goto_model)
 
static void filter_goto_model (goto_modelt &goto_model_with_harness, const std::unordered_set< irep_idt > &goto_model_without_harness_symbols)
 

Function Documentation

◆ filter_goto_model()

static void filter_goto_model ( goto_modelt goto_model_with_harness,
const std::unordered_set< irep_idt > &  goto_model_without_harness_symbols 
)
static

Definition at line 51 of file goto_harness_parse_options.cpp.

◆ get_symbol_names_from_goto_model()

std::unordered_set<irep_idt> get_symbol_names_from_goto_model ( const goto_modelt goto_model)

Definition at line 38 of file goto_harness_parse_options.cpp.