CBMC
Public Member Functions | Protected Member Functions | Friends | List of all members
goto_harness_generatort Class Referenceabstract

#include <goto_harness_generator.h>

+ Inheritance diagram for goto_harness_generatort:

Public Member Functions

virtual void generate (goto_modelt &goto_model, const irep_idt &harness_function_name)=0
 Generate a harness according to the set options. More...
 
virtual ~goto_harness_generatort ()=default
 

Protected Member Functions

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

Friends

class goto_harness_generator_factoryt
 

Detailed Description

Definition at line 41 of file goto_harness_generator.h.

Constructor & Destructor Documentation

◆ ~goto_harness_generatort()

virtual goto_harness_generatort::~goto_harness_generatort ( )
virtualdefault

Member Function Documentation

◆ generate()

virtual void goto_harness_generatort::generate ( goto_modelt &  goto_model,
const irep_idt &  harness_function_name 
)
pure virtual

Generate a harness according to the set options.

Implemented in memory_snapshot_harness_generatort, and function_call_harness_generatort.

◆ handle_option()

virtual void goto_harness_generatort::handle_option ( const std::string &  option,
const std::list< std::string > &  values 
)
protectedpure virtual

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

Implemented in memory_snapshot_harness_generatort, and function_call_harness_generatort.

◆ validate_options()

virtual void goto_harness_generatort::validate_options ( const goto_modelt &  goto_model)
protectedpure virtual

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

Implemented in memory_snapshot_harness_generatort, and function_call_harness_generatort.

Friends And Related Function Documentation

◆ goto_harness_generator_factoryt

friend class goto_harness_generator_factoryt
friend

Definition at line 49 of file goto_harness_generator.h.

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