require_goto_statements.cpp File Reference

#include "require_goto_statements.h"
#include <util/expr_iterator.h>
#include <util/expr_util.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <util/suffix.h>
#include <util/symbol_table_base.h>
#include <goto-programs/goto_functions.h>
#include <java_bytecode/java_types.h>
#include <testing-utils/use_catch.h>

Include dependency graph for require_goto_statements.cpp:

Go to the source code of this file.

Functions
const exprt &	get_unique_non_null_expression_assigned_to_symbol (const std::vector< codet > &entry_point_instructions, const irep_idt &symbol_identifier)
	Get the unique non-null expression assigned to a symbol. More...
const symbol_exprt *	try_get_unique_symbol_assigned_to_symbol (const std::vector< codet > &entry_point_instructions, const irep_idt &symbol_identifier)
	Get the unique symbol assigned to a symbol, if one exists. More...
static const irep_idt &	get_ultimate_source_symbol (const std::vector< codet > &entry_point_instructions, const irep_idt &input_symbol_identifier)
	Follow the chain of non-null assignments until we find a symbol that hasn't ever had another symbol assigned to it. More...

Function Documentation

get_ultimate_source_symbol()

static const irep_idt& get_ultimate_source_symbol ( const std::vector< codet > &  entry_point_instructions, const irep_idt &  input_symbol_identifier  )

static

Follow the chain of non-null assignments until we find a symbol that hasn't ever had another symbol assigned to it.

For example, if this code is

a = 5 + g(7)
b = a
c = b

then given input c we return a.

Parameters

entry_point_instructions	A vector of instructions
input_symbol_identifier	The identifier of the symbol we are currently considering

Returns

The identifier of the symbol which is (possibly indirectly) assigned to input_symbol_identifier and which does not have any symbol assigned to it

Definition at line 353 of file require_goto_statements.cpp.

get_unique_non_null_expression_assigned_to_symbol()

const exprt& get_unique_non_null_expression_assigned_to_symbol	(	const std::vector< codet > &	entry_point_instructions,
		const irep_idt &	symbol_identifier
	)

Get the unique non-null expression assigned to a symbol.

The symbol may have many null assignments, but only one non-null assignment.

Parameters

entry_point_instructions	A vector of instructions
symbol_identifier	The identifier of the symbol we are considering

Returns

The unique non-null expression assigned to the symbol

Definition at line 309 of file require_goto_statements.cpp.

try_get_unique_symbol_assigned_to_symbol()

const symbol_exprt* try_get_unique_symbol_assigned_to_symbol	(	const std::vector< codet > &	entry_point_instructions,
		const irep_idt &	symbol_identifier
	)

Get the unique symbol assigned to a symbol, if one exists.

There must be a unique non-null assignment to the symbol, and it is either another symbol, in which case we return that symbol expression, or something else, which case we return a null pointer.

Parameters

entry_point_instructions	A vector of instructions
symbol_identifier	The identifier of the symbol

Returns

The unique symbol assigned to input_symbol_identifier, or a null pointer if no symbols are assigned to it

Definition at line 328 of file require_goto_statements.cpp.