#include <memory>
#include <regex>
#include <util/irep.h>

Include dependency graph for generate_function_bodies.h:

This graph shows which files directly or indirectly include this file:

Classes
class	generate_function_bodiest
	Base class for replace_function_body implementations. More...

Macros
#define	OPT_REPLACE_FUNCTION_BODY

#define	HELP_REPLACE_FUNCTION_BODY

Functions
std::unique_ptr< generate_function_bodiest >	generate_function_bodies_factory (const std::string &options, const c_object_factory_parameterst &object_factory_parameters, const symbol_tablet &symbol_table, message_handlert &message_handler)
	Create the type that actually generates the functions. More...

void	generate_function_bodies (const std::regex &functions_regex, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
	Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-false, havoc, nondet-return. More...

void	generate_function_bodies (const std::string &function_name, const std::string &call_site_id, const generate_function_bodiest &generate_function_body, goto_modelt &model, message_handlert &message_handler)
	Generate a clone of `function_name` (labelled with `call_site_id`) and instantiate its body with selective havocing of its parameters. More...

Macro Definition Documentation

◆ HELP_REPLACE_FUNCTION_BODY

#define HELP_REPLACE_FUNCTION_BODY

Value:

  " {y--generate-function-body} {uregex} \t "                                  \
  "generate bodies for functions matching {uregex}\n"                          \
  " {y--generate-havocing-body} <option> "                                     \
  "{ufun_name},{yparams}:{up1};{up2};.. \t "                                   \
  "generate havocing body\n"                                                   \
  " {y--generate-havocing-body} <option> "                                     \
  "{ufun_name}[,{ucall-site-id},{yparams}:{up1};{up2};..]+ \t "                \
  "generate havocing body\n"                                                   \
  " {y--generate-function-body-options} {uoption} \t "                         \
  "One of {yassert-false}, {yassume-false}, {ynondet-return}, "                \
  "{yassert-false-assume-false} and "                                          \
  "{yhavoc}[,{yparams}:{uregex}][,{yglobals}:{uregex}]"                        \
  "[,{yparams}:{up1};{up2};..] (default: {ynondet-return})\n"

Definition at line 92 of file generate_function_bodies.h.

◆ OPT_REPLACE_FUNCTION_BODY

#define OPT_REPLACE_FUNCTION_BODY

Value:

  "(generate-function-body):" \
  "(generate-havocing-body):" \
  "(generate-function-body-options):"

Definition at line 87 of file generate_function_bodies.h.

Function Documentation

◆ generate_function_bodies() [1/2]

void generate_function_bodies	(	const std::regex &	functions_regex,
		const generate_function_bodiest &	generate_function_body,
		goto_modelt &	model,
		message_handlert &	message_handler
	)

Generate function bodies with some default behavior: assert-false, assume-false, assert-false-assume-false, havoc, nondet-return.

Parameters

functions_regex	Specifies the functions whose body should be generated
generate_function_body	Specifies what kind of body to generate
model	The goto-model in which to generate the function bodies
message_handler	Destination for status/warning messages

Definition at line 501 of file generate_function_bodies.cpp.

◆ generate_function_bodies() [2/2]

void generate_function_bodies	(	const std::string &	function_name,
		const std::string &	call_site_id,
		const generate_function_bodiest &	generate_function_body,
		goto_modelt &	model,
		message_handlert &	message_handler
	)

Generate a clone of function_name (labelled with call_site_id) and instantiate its body with selective havocing of its parameters.

Parameters

function_name	The function whose body should be generated
call_site_id	the number of the call site
generate_function_body	the previously constructed body generator
model	the goto-model to be modified
message_handler	the message-handler

Definition at line 537 of file generate_function_bodies.cpp.

◆ generate_function_bodies_factory()

std::unique_ptr<generate_function_bodiest> generate_function_bodies_factory	(	const std::string &	options,
		const c_object_factory_parameterst &	object_factory_parameters,
		const symbol_tablet &	symbol_table,
		message_handlert &	message_handler
	)

Create the type that actually generates the functions.

See also: generate_function_bodies for the syntax of the options parameter

Definition at line 375 of file generate_function_bodies.cpp.

Classes

Macros