Loading...

Searching...

No Matches

goto_program_dereference.cpp File Reference

Dereferencing Operations on GOTO Programs. More...

#include "goto_program_dereference.h"
#include <util/expr_util.h>
#include <util/options.h>
#include <util/pointer_expr.h>
#include <util/std_code.h>
#include <util/symbol_table.h>
#include <goto-programs/goto_model.h>

+ Include dependency graph for goto_program_dereference.cpp:

[フレーム]

Go to the source code of this file.

Functions

void remove_pointers (goto_modelt &goto_model, value_setst &value_sets, message_handlert &message_handler)

Remove dereferences in all expressions contained in the program goto_model.

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

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

Detailed Description

Dereferencing Operations on GOTO Programs.

Definition in file goto_program_dereference.cpp.

Function Documentation

◆ dereference()

void dereference ( const irep_idt & function_id,

goto_programt::const_targett target,

exprt & expr,

const namespacet & ns,

value_setst & value_sets,

message_handlert & message_handler

)

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

Definition at line 278 of file goto_program_dereference.cpp.

◆ remove_pointers()

void remove_pointers ( goto_modelt & goto_model,

value_setst & value_sets,

message_handlert & message_handler

)

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 260 of file goto_program_dereference.cpp.