CBMC
|
#include <util/ssa_expr.h>
Go to the source code of this file.
Classes | |
class | field_sensitive_ssa_exprt |
class | field_sensitivityt |
Control granularity of object accesses. More... | |
Functions | |
template<> | |
bool | can_cast_expr< field_sensitive_ssa_exprt > (const exprt &base) |
const field_sensitive_ssa_exprt & | to_field_sensitive_ssa_expr (const exprt &expr) |
field_sensitive_ssa_exprt & | to_field_sensitive_ssa_expr (exprt &expr) |
|
inline |
Definition at line 35 of file field_sensitivity.h.
|
inline |
Definition at line 41 of file field_sensitivity.h.
|
inline |
Definition at line 49 of file field_sensitivity.h.