cprover
Loading...
Searching...
No Matches
function_call_harness_generatort Class Reference

Function harness generator that for a specified goto-function generates a harness that sets up its arguments and calls it. More...

#include <function_call_harness_generator.h>

Inheritance diagram for function_call_harness_generatort:
Collaboration diagram for function_call_harness_generatort:

Classes

struct  implt
 This contains implementation details of function call harness generator to avoid leaking them out into the header. More...

Public Member Functions

 function_call_harness_generatort (ui_message_handlert &message_handler)
 ~function_call_harness_generatort () override
void generate (goto_modelt &goto_model, const irep_idt &harness_function_name) override
 Generate a harness according to the set options.
Public Member Functions inherited from goto_harness_generatort
virtual ~goto_harness_generatort ()=default

Protected Member Functions

void handle_option (const std::string &option, const std::list< std::string > &values) override
 Handle a command line argument.
void validate_options (const goto_modelt &goto_model) override
 Check if options are in a sane state, throw otherwise.

Private Member Functions

std::size_t require_one_size_value (const std::string &option, const std::list< std::string > &values)

Private Attributes

std::unique_ptr< impltp_impl

Detailed Description

Function harness generator that for a specified goto-function generates a harness that sets up its arguments and calls it.

Definition at line 22 of file function_call_harness_generator.h.

Constructor & Destructor Documentation

◆ function_call_harness_generatort()

function_call_harness_generatort::function_call_harness_generatort ( ui_message_handlert & message_handler)
explicit

Definition at line 96 of file function_call_harness_generator.cpp.

◆ ~function_call_harness_generatort()

function_call_harness_generatort::~function_call_harness_generatort ( )
overridedefault

Member Function Documentation

◆ generate()

void function_call_harness_generatort::generate ( goto_modelt & goto_model,
const irep_idt & harness_function_name )
overridevirtual

Generate a harness according to the set options.

Implements goto_harness_generatort.

Definition at line 219 of file function_call_harness_generator.cpp.

◆ handle_option()

void function_call_harness_generatort::handle_option ( const std::string & option,
const std::list< std::string > & values )
overrideprotectedvirtual

Handle a command line argument.

Should throw an exception if the option doesn't apply to this generator. Should only set options rather than immediately performing work

Implements goto_harness_generatort.

Definition at line 105 of file function_call_harness_generator.cpp.

◆ require_one_size_value()

std::size_t function_call_harness_generatort::require_one_size_value ( const std::string & option,
const std::list< std::string > & values )
private

◆ validate_options()

void function_call_harness_generatort::validate_options ( const goto_modelt & goto_model)
overrideprotectedvirtual

Check if options are in a sane state, throw otherwise.

Implements goto_harness_generatort.

Definition at line 307 of file function_call_harness_generator.cpp.

Member Data Documentation

◆ p_impl

std::unique_ptr<implt> function_call_harness_generatort::p_impl
private

Definition at line 43 of file function_call_harness_generator.h.


The documentation for this class was generated from the following files: