Loading...

Searching...

No Matches

remove_returns.cpp File Reference

Replace function returns by assignments to global variables. More...

#include "remove_returns.h"
#include <util/std_code.h>
#include <util/std_expr.h>
#include <util/suffix.h>
#include <goto-symex/shadow_memory.h>
#include "goto_model.h"
#include "remove_skip.h"

+ Include dependency graph for remove_returns.cpp:

[フレーム]

Go to the source code of this file.

Classes

class remove_returnst

Macros

#define RETURN_VALUE_SUFFIX "#return_value"

Functions

void remove_returns (symbol_table_baset &symbol_table, goto_functionst &goto_functions)

removes returns

void remove_returns (goto_model_functiont &goto_model_function, function_is_stubt function_is_stub)

Removes returns from a single function.

void remove_returns (goto_modelt &goto_model)

removes returns

void restore_returns (goto_modelt &goto_model)

restores return statements

irep_idt return_value_identifier (const irep_idt &identifier)

produces the identifier that is used to store the return value of the function with the given identifier

symbol_exprt return_value_symbol (const irep_idt &identifier, const namespacet &ns)

produces the symbol that is used to store the return value of the function with the given identifier

bool is_return_value_identifier (const irep_idt &id)

Returns true if id is a special return-value symbol produced by return_value_identifier.

bool is_return_value_symbol (const symbol_exprt &symbol_expr)

Returns true if symbol_expr is a special return-value symbol produced by return_value_symbol.

bool does_function_call_return (const goto_programt::instructiont &function_call)

Check if the function_call returns anything.

Detailed Description

Replace function returns by assignments to global variables.

Definition in file remove_returns.cpp.

Macro Definition Documentation

◆ RETURN_VALUE_SUFFIX

#define RETURN_VALUE_SUFFIX "#return_value"

Definition at line 25 of file remove_returns.cpp.

Function Documentation

◆ does_function_call_return()

bool does_function_call_return ( const goto_programt::instructiont & function_call )

Check if the function_call returns anything.

Parameters: function_call the function call to be investigated

Returns: true if non-void return type and non-nil lhs

Definition at line 430 of file remove_returns.cpp.

◆ is_return_value_identifier()

bool is_return_value_identifier ( const irep_idt & id )

Returns true if id is a special return-value symbol produced by return_value_identifier.

Definition at line 420 of file remove_returns.cpp.

◆ is_return_value_symbol()

bool is_return_value_symbol ( const symbol_exprt & symbol_expr )

Returns true if symbol_expr is a special return-value symbol produced by return_value_symbol.

Definition at line 425 of file remove_returns.cpp.

◆ remove_returns() [1/3]

void remove_returns ( goto_model_functiont & goto_model_function,

function_is_stubt function_is_stub

)

Removes returns from a single function.

Only usable with Java programs at the moment; to use it with other languages, they must annotate their stub functions with ID_C_incomplete as currently done in java_bytecode_convert_method.cpp.

This will generate #return_value variables, if not already present, for both the function being altered and any callees.

Parameters: goto_model_function function to transform

function_is_stub function that will be used to test whether a given callee has been or will be given a body. It should return true if so, or false if the function will remain a bodyless stub.

Definition at line 278 of file remove_returns.cpp.

◆ remove_returns() [2/3]

void remove_returns ( goto_modelt & goto_model )

removes returns

Definition at line 287 of file remove_returns.cpp.

◆ remove_returns() [3/3]

void remove_returns ( symbol_table_baset & symbol_table,

goto_functionst & goto_functions

)

removes returns

Definition at line 259 of file remove_returns.cpp.

◆ restore_returns()

void restore_returns ( goto_modelt & goto_model )

restores return statements

Definition at line 401 of file remove_returns.cpp.

◆ return_value_identifier()

irep_idt return_value_identifier ( const irep_idt & identifier )

produces the identifier that is used to store the return value of the function with the given identifier

Definition at line 407 of file remove_returns.cpp.

◆ return_value_symbol()

symbol_exprt return_value_symbol ( const irep_idt & identifier,

const namespacet & ns

)

produces the symbol that is used to store the return value of the function with the given identifier

Definition at line 413 of file remove_returns.cpp.