CBMC
goto_rw.cpp File Reference
+ Include dependency graph for goto_rw.cpp:

Go to the source code of this file.

Functions

static void goto_rw_assign (const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &rhs, rw_range_sett &rw_set)
 
static void goto_rw_other (const irep_idt &function, goto_programt::const_targett target, const codet &code, rw_range_sett &rw_set)
 
static void goto_rw (const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
 
void goto_rw (const irep_idt &function, goto_programt::const_targett target, rw_range_sett &rw_set)
 
void goto_rw (const irep_idt &function, const goto_programt &goto_program, rw_range_sett &rw_set)
 
void goto_rw (const goto_functionst &goto_functions, const irep_idt &function, rw_range_sett &rw_set)
 

Function Documentation

◆ goto_rw() [1/4]

void goto_rw ( const goto_functionst goto_functions,
const irep_idt function,
rw_range_sett rw_set 
)

Definition at line 944 of file goto_rw.cpp.

◆ goto_rw() [2/4]

void goto_rw ( const irep_idt function,
const goto_programt goto_program,
rw_range_sett rw_set 
)

Definition at line 935 of file goto_rw.cpp.

◆ goto_rw() [3/4]

static void goto_rw ( const irep_idt function,
goto_programt::const_targett  target,
const exprt lhs,
const exprt function_expr,
const exprt::operandst arguments,
rw_range_sett rw_set 
)
static

Definition at line 845 of file goto_rw.cpp.

◆ goto_rw() [4/4]

void goto_rw ( const irep_idt function,
goto_programt::const_targett  target,
rw_range_sett rw_set 
)

Definition at line 867 of file goto_rw.cpp.

◆ goto_rw_assign()

static void goto_rw_assign ( const irep_idt function,
goto_programt::const_targett  target,
const exprt lhs,
const exprt rhs,
rw_range_sett rw_set 
)
static

Definition at line 778 of file goto_rw.cpp.

◆ goto_rw_other()

static void goto_rw_other ( const irep_idt function,
goto_programt::const_targett  target,
const codet code,
rw_range_sett rw_set 
)
static

Definition at line 790 of file goto_rw.cpp.