cprover
goto_program_dereference.cpp File Reference

Dereferencing Operations on GOTO Programs. More...

#include "goto_program_dereference.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_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)
 
void dereference (goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets)
 

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 
)

§ pointer_checks() [1/2]

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

§ pointer_checks() [2/2]

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

§ remove_pointers() [1/2]

§ remove_pointers() [2/2]

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