Loading...

Searching...

No Matches

generate_function_bodies.cpp File Reference

#include "generate_function_bodies.h"
#include <util/fresh_symbol.h>
#include <util/pointer_expr.h>
#include <util/prefix.h>
#include <util/string2int.h>
#include <util/string_utils.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/remove_skip.h>
#include <ansi-c/c_nondet_symbol_factory.h>
#include <ansi-c/goto-conversion/goto_convert.h>
#include <ansi-c/goto-conversion/goto_convert_functions.h>

+ Include dependency graph for generate_function_bodies.cpp:

[フレーム]

Go to the source code of this file.

Classes

class assume_false_generate_function_bodiest

class assert_false_generate_function_bodiest

class assert_false_then_assume_false_generate_function_bodiest

class havoc_generate_function_bodiest

class generate_function_bodies_errort

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.

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

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

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.

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,

bool ignore_no_match

)

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

ignore_no_match Do not warn in case no function matched functions_regex

Definition at line 503 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 556 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.