CBMC
goto_program_dereference.h File Reference

Value Set. More...

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

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.

Definition in file goto_program_dereference.h.

Macro Definition Documentation

◆ HELP_REMOVE_POINTERS

#define HELP_REMOVE_POINTERS
Value:
" {y--remove-pointers} \t " \
"converts pointer arithmetic to base+offset expressions\n"

Definition at line 108 of file goto_program_dereference.h.

◆ OPT_REMOVE_POINTERS

#define OPT_REMOVE_POINTERS   "(remove-pointers)"

Definition at line 106 of file goto_program_dereference.h.

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.