CBMC
object_id.cpp File Reference

Object Identifiers. More...

+ Include dependency graph for object_id.cpp:

Go to the source code of this file.

Enumerations

enum class  get_modet { LHS_R , LHS_W , READ }
 

Functions

void get_objects_rec (get_modet mode, const exprt &expr, object_id_sett &dest, const std::string &suffix)
 
void get_objects (const exprt &expr, object_id_sett &dest)
 
void get_objects_r (const code_assignt &assign, object_id_sett &dest)
 
void get_objects_w (const code_assignt &assign, object_id_sett &dest)
 
void get_objects_w (const exprt &lhs, object_id_sett &dest)
 
void get_objects_r_lhs (const exprt &lhs, object_id_sett &dest)
 

Detailed Description

Object Identifiers.

Definition in file object_id.cpp.

Enumeration Type Documentation

◆ get_modet

enum get_modet
strong
Enumerator
LHS_R 
LHS_W 
READ 

Definition at line 18 of file object_id.cpp.

Function Documentation

◆ get_objects()

void get_objects ( const exprt expr,
object_id_sett dest 
)

Definition at line 78 of file object_id.cpp.

◆ get_objects_r()

void get_objects_r ( const code_assignt assign,
object_id_sett dest 
)

Definition at line 83 of file object_id.cpp.

◆ get_objects_r_lhs()

void get_objects_r_lhs ( const exprt lhs,
object_id_sett dest 
)

Definition at line 99 of file object_id.cpp.

◆ get_objects_rec()

void get_objects_rec ( get_modet  mode,
const exprt expr,
object_id_sett dest,
const std::string &  suffix 
)

Definition at line 20 of file object_id.cpp.

◆ get_objects_w() [1/2]

void get_objects_w ( const code_assignt assign,
object_id_sett dest 
)

Definition at line 89 of file object_id.cpp.

◆ get_objects_w() [2/2]

void get_objects_w ( const exprt lhs,
object_id_sett dest 
)

Definition at line 94 of file object_id.cpp.