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 34 of file field_sensitivity.h.
|
inline |
Definition at line 40 of file field_sensitivity.h.
|
inline |
Definition at line 48 of file field_sensitivity.h.