#include <memory>
#include <regex>
#include <goto-programs/goto_function.h>
#include <goto-programs/goto_model.h>
#include <util/cmdline.h>
#include <util/message.h>
#include <util/std_code.h>
#include <util/std_types.h>

Include dependency graph for generate_function_bodies.h:

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

Go to the source code of 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 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 A list of currently accepted command line arguments. More...

Macro Definition Documentation

◆ HELP_REPLACE_FUNCTION_BODY

#define HELP_REPLACE_FUNCTION_BODY

Value:

" --generate-function-body <regex>\n" \
  /* NOLINTNEXTLINE(whitespace/line_length) */ \
  "                              Generate bodies for functions matching regex\n" \
  " --generate-function-body-options <option>\n" \
  "                              One of assert-false, assume-false,\n" \
  /* NOLINTNEXTLINE(whitespace/line_length) */ \
  "                              nondet-return, assert-false-assume-false and\n" \
  "                              havoc[,params:<regex>][,globals:<regex>]\n" \
  "                              (default: nondet-return)"

Definition at line 76 of file generate_function_bodies.h.

◆ OPT_REPLACE_FUNCTION_BODY

#define OPT_REPLACE_FUNCTION_BODY

Value:

"(generate-function-body):" \

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

Definition at line 72 of file generate_function_bodies.h.

Function Documentation

◆ generate_function_bodies()

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 A list of currently accepted command line arguments.

the type of bodies generated by them

assert-false: { assert(false); }

assume-false: { assume(false); }

assert-false-assume-false: { assert(false); assume(false); }

havoc[,params:regex][,globals:regex]: Assign nondet to the targets of pointer-to-non-const parameters matching regex, and non-const globals matching regex and then return nondet for non-void functions, e.g.:

int global; const int c_global; int function(int *param, const int *const_param);

havoc,params:(?!__).*,globals:(?!__).* (where (?!__) means "not preceded by __", which is recommended to avoid overwrite internal symbols), leads to

int function(int *param, consnt int *const_param) { *param = nondet_int(); global = nondet_int(); return nondet_int(); }

nondet-return: return nondet for non-void functions

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 454 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 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 335 of file generate_function_bodies.cpp.

Classes