Value Set. More...

#include "dereference_callback.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:

Classes
class	goto_program_dereferencet
	Wrapper for functions removing dereferences in expressions contained in a goto program. More...

Macros
#define	OPT_REMOVE_POINTERS "(remove-pointers)"

#define	HELP_REMOVE_POINTERS

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

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

Detailed Description

Value Set.

Macro Definition Documentation

#define HELP_REMOVE_POINTERS

Value:

" {y--remove-pointers} \t " \

"converts pointer arithmetic to base+offset expressions\n"

#define OPT_REMOVE_POINTERS "(remove-pointers)"

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

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.