Loading...

Searching...

No Matches

Public Member Functions | Protected Member Functions | Private Member Functions | Private Attributes | List of all members

havoc_generate_function_bodiest Class Reference

+ Inheritance diagram for havoc_generate_function_bodiest:

[フレーム]

[legend]

+ Collaboration diagram for havoc_generate_function_bodiest:

[フレーム]

[legend]

Public Member Functions

havoc_generate_function_bodiest (std::vector< irep_idt > globals_to_havoc, std::regex parameters_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)

havoc_generate_function_bodiest (std::vector< irep_idt > globals_to_havoc, std::vector< std::size_t > param_numbers_to_havoc, const c_object_factory_parameterst &object_factory_parameters, message_handlert &message_handler)

- Public Member Functions inherited from generate_function_bodiest

virtual ~generate_function_bodiest ()=default

void generate_function_body (goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const

Replace the function body with one based on the replace_function_body class being used.

Protected Member Functions

void generate_function_body_impl (goto_functiont &function, symbol_tablet &symbol_table, const irep_idt &function_name) const override

Produce a body for the passed function At this point the body of function is always empty, and all function parameters have identifiers.

Private Member Functions

void havoc_expr_rec (const exprt &lhs, const std::size_t initial_depth, const source_locationt &source_location, const irep_idt &function_id, symbol_tablet &symbol_table, goto_programt &dest) const

bool should_havoc_param (const std::string &param_name, std::size_t param_number) const

Private Attributes

const std::vector< irep_idt > globals_to_havoc

std::optional< std::regex > parameters_to_havoc

std::optional< std::vector< std::size_t > > param_numbers_to_havoc

const c_object_factory_parameterst & object_factory_parameters

messaget message

Detailed Description

Definition at line 133 of file generate_function_bodies.cpp.

Constructor & Destructor Documentation

◆ havoc_generate_function_bodiest() [1/2]

havoc_generate_function_bodiest::havoc_generate_function_bodiest ( std::vector< irep_idt > globals_to_havoc,

std::regex parameters_to_havoc,

const c_object_factory_parameterst & object_factory_parameters,

message_handlert & message_handler

)

inline

Definition at line 136 of file generate_function_bodies.cpp.

◆ havoc_generate_function_bodiest() [2/2]

havoc_generate_function_bodiest::havoc_generate_function_bodiest ( std::vector< irep_idt > globals_to_havoc,

std::vector< std::size_t > param_numbers_to_havoc,

const c_object_factory_parameterst & object_factory_parameters,

message_handlert & message_handler

)

inline

Definition at line 149 of file generate_function_bodies.cpp.

Member Function Documentation

◆ generate_function_body_impl()

void havoc_generate_function_bodiest::generate_function_body_impl ( goto_functiont & function,

symbol_tablet & symbol_table,

const irep_idt & function_name

) const

inlineoverrideprotectedvirtual

Produce a body for the passed function At this point the body of function is always empty, and all function parameters have identifiers.

Parameters: function whose body to generate

symbol_table of the current goto program

function_name Identifier of function

Implements generate_function_bodiest.

Definition at line 218 of file generate_function_bodies.cpp.

◆ havoc_expr_rec()

void havoc_generate_function_bodiest::havoc_expr_rec ( const exprt & lhs,

const std::size_t initial_depth,

const source_locationt & source_location,

const irep_idt & function_id,

symbol_tablet & symbol_table,

goto_programt & dest

) const

inlineprivate

Definition at line 163 of file generate_function_bodies.cpp.

◆ should_havoc_param()

bool havoc_generate_function_bodiest::should_havoc_param ( const std::string & param_name,

std::size_t param_number

) const

inlineprivate

Definition at line 199 of file generate_function_bodies.cpp.

Member Data Documentation

◆ globals_to_havoc

const std::vector<irep_idt> havoc_generate_function_bodiest::globals_to_havoc

private

Definition at line 357 of file generate_function_bodies.cpp.

◆ message

messaget havoc_generate_function_bodiest::message

mutableprivate

Definition at line 361 of file generate_function_bodies.cpp.

◆ object_factory_parameters

const c_object_factory_parameterst& havoc_generate_function_bodiest::object_factory_parameters

private

Definition at line 360 of file generate_function_bodies.cpp.

◆ param_numbers_to_havoc

std::optional<std::vector<std::size_t> > havoc_generate_function_bodiest::param_numbers_to_havoc

private

Definition at line 359 of file generate_function_bodies.cpp.

◆ parameters_to_havoc

std::optional<std::regex> havoc_generate_function_bodiest::parameters_to_havoc

private

Definition at line 358 of file generate_function_bodies.cpp.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/generate_function_bodies.cpp