cprover
goto_program_dereference.h File Reference
+ 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
 Wrapper for functions removing dereferences in expressions contained in a goto program. More...
 

Functions

void dereference (goto_programt::const_targett target, exprt &expr, const namespacet &, value_setst &)
 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 &)
 Remove dereferences in all expressions contained in the program goto_model. More...
 
void remove_pointers (goto_functionst &, symbol_tablet &, value_setst &)
 
void pointer_checks (goto_programt &, symbol_tablet &, const optionst &, value_setst &)
 
void pointer_checks (goto_functionst &, symbol_tablet &, const optionst &, value_setst &)
 

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 ,
value_setst  
)

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_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.

◆ pointer_checks() [2/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.

◆ remove_pointers() [1/2]

void remove_pointers ( goto_functionst ,
symbol_tablet ,
value_setst  
)

◆ 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.