CBMC
|
Object Identifiers. More...
#include "object_id.h"
#include <goto-programs/goto_instruction_code.h>
#include <util/pointer_expr.h>
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) |
Object Identifiers.
Definition in file object_id.cpp.
|
strong |
Enumerator | |
---|---|
LHS_R | |
LHS_W | |
READ |
Definition at line 18 of file object_id.cpp.
void get_objects | ( | const exprt & | expr, |
object_id_sett & | dest | ||
) |
Definition at line 78 of file object_id.cpp.
void get_objects_r | ( | const code_assignt & | assign, |
object_id_sett & | dest | ||
) |
Definition at line 83 of file object_id.cpp.
void get_objects_r_lhs | ( | const exprt & | lhs, |
object_id_sett & | dest | ||
) |
Definition at line 99 of file object_id.cpp.
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.
void get_objects_w | ( | const code_assignt & | assign, |
object_id_sett & | dest | ||
) |
Definition at line 89 of file object_id.cpp.
void get_objects_w | ( | const exprt & | lhs, |
object_id_sett & | dest | ||
) |
Definition at line 94 of file object_id.cpp.