CBMC
function_call_harness_generator.h
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: harness generator for functions
4 
5 Author: Diffblue Ltd.
6 
7 \******************************************************************/
8 
9 #ifndef CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H
10 #define CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H
11 
12 #include <list>
13 #include <memory>
14 #include <string>
15 
16 #include "goto_harness_generator.h"
17 
19 
23 {
24 public:
26  ui_message_handlert &message_handler);
28  void generate(goto_modelt &goto_model, const irep_idt &harness_function_name)
29  override;
30 
31 protected:
32  void handle_option(
33  const std::string &option,
34  const std::list<std::string> &values) override;
35 
36  void validate_options(const goto_modelt &goto_model) override;
37 
38 private:
40  const std::string &option,
41  const std::list<std::string> &values);
42  struct implt;
43  std::unique_ptr<implt> p_impl;
44 };
45 
46 #endif // CPROVER_GOTO_HARNESS_FUNCTION_CALL_HARNESS_GENERATOR_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Function harness generator that for a specified goto-function generates a harness that sets up its ar...
void validate_options(const goto_modelt &goto_model) override
Check if options are in a sane state, throw otherwise.
std::size_t require_one_size_value(const std::string &option, const std::list< std::string > &values)
function_call_harness_generatort(ui_message_handlert &message_handler)
void handle_option(const std::string &option, const std::list< std::string > &values) override
Handle a command line argument.
void generate(goto_modelt &goto_model, const irep_idt &harness_function_name) override
Generate a harness according to the set options.
This contains implementation details of function call harness generator to avoid leaking them out int...