CBMC
Classes | Public Member Functions | Protected Member Functions | Private Member Functions | Private Attributes | List of all members
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. More...
 
- 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. More...
 
void validate_options (const goto_modelt &goto_model) override
 Check if options are in a sane state, throw otherwise. More...
 

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< implt > p_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: