goto_program_dereference.h File Reference

Value Set. More...

#include <util/namespace.h>
#include <goto-programs/goto_functions.h>
#include "value_sets.h"
#include "value_set_dereference.h"

Include dependency graph for goto_program_dereference.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	goto_program_dereferencet

Functions
void	dereference (goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
void	remove_pointers (goto_programt &goto_program, symbol_tablet &symbol_table, value_setst &value_sets)
void	remove_pointers (goto_functionst &goto_functions, symbol_tablet &symbol_table, value_setst &value_sets)
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)

Detailed Description

Value Set.

Definition in file goto_program_dereference.h.

Function Documentation

dereference()

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

Definition at line 434 of file goto_program_dereference.cpp.

References goto_program_dereferencet::dereference_expression().

pointer_checks() [1/2]

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

Definition at line 410 of file goto_program_dereference.cpp.

References goto_program_dereferencet::pointer_checks().

pointer_checks() [2/2]

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

Definition at line 422 of file goto_program_dereference.cpp.

References goto_program_dereferencet::pointer_checks().

remove_pointers() [1/2]

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

Definition at line 379 of file goto_program_dereference.cpp.

References goto_program_dereferencet::dereference_program().

Referenced by goto_instrument_parse_optionst::instrument_goto_program().

remove_pointers() [2/2]

void remove_pointers	(	goto_functionst &	goto_functions,
		symbol_tablet &	symbol_table,
		value_setst &	value_sets
	)

Definition at line 394 of file goto_program_dereference.cpp.

References goto_program_dereferencet::dereference_program(), and Forall_goto_functions.