Dereferencing Operations on GOTO Programs. More...

#include "goto_program_dereference.h"
#include <util/expr_util.h>
#include <util/simplify_expr.h>
#include <util/base_type.h>
#include <util/std_code.h>
#include <util/symbol_table.h>
#include <util/guard.h>
#include <util/options.h>

Include dependency graph for goto_program_dereference.cpp:

Go to the source code of this file.

Functions
void	remove_pointers (goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)

void	remove_pointers (goto_modelt &goto_model, value_setst &value_sets)
	Remove dereferences in all expressions contained in the program `goto_model`. More...

void	pointer_checks (goto_programt &goto_program, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets)

void	pointer_checks (goto_functionst &goto_functions, symbol_tablet &symbol_table, const optionst &options, value_setst &value_sets)

void	dereference (goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
	Remove dereferences in `expr` using `value_sets` to determine to what objects the pointers may be pointing to. More...

Detailed Description

Dereferencing Operations on GOTO Programs.

Definition in file goto_program_dereference.cpp.

Function Documentation

◆ dereference()

void dereference	(	goto_programt::const_targett	target,
		exprt &	expr,
		const namespacet &	ns,
		value_setst &	value_sets
	)

Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointing to.

Definition at line 462 of file goto_program_dereference.cpp.

◆ pointer_checks() [1/2]

void pointer_checks	(	goto_programt &	goto_program,
		symbol_tablet &	symbol_table,
		const optionst &	options,
		value_setst &	value_sets
	)

Deprecated:

Definition at line 435 of file goto_program_dereference.cpp.

◆ pointer_checks() [2/2]

void pointer_checks	(	goto_functionst &	goto_functions,
		symbol_tablet &	symbol_table,
		const optionst &	options,
		value_setst &	value_sets
	)

Deprecated:

Definition at line 448 of file goto_program_dereference.cpp.

◆ remove_pointers() [1/2]

void remove_pointers	(	goto_programt &	goto_program,
		symbol_tablet &	symbol_table,
		value_setst &	value_sets
	)

Deprecated:

Definition at line 400 of file goto_program_dereference.cpp.

◆ remove_pointers() [2/2]

void remove_pointers	(	goto_modelt &	goto_model,
		value_setst &	value_sets
	)

Remove dereferences in all expressions contained in the program goto_model.

value_sets is used to determine to what objects the pointers may be pointing to.

Definition at line 418 of file goto_program_dereference.cpp.