CBMC
field_sensitivity.h File Reference
#include <util/ssa_expr.h>
+ Include dependency graph for field_sensitivity.h:
+ This graph shows which files directly or indirectly include this file:

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_exprtto_field_sensitive_ssa_expr (const exprt &expr)
 
field_sensitive_ssa_exprtto_field_sensitive_ssa_expr (exprt &expr)
 

Function Documentation

◆ can_cast_expr< field_sensitive_ssa_exprt >()

template<>
bool can_cast_expr< field_sensitive_ssa_exprt > ( const exprt base)
inline

Definition at line 34 of file field_sensitivity.h.

◆ to_field_sensitive_ssa_expr() [1/2]

const field_sensitive_ssa_exprt& to_field_sensitive_ssa_expr ( const exprt expr)
inline

Definition at line 40 of file field_sensitivity.h.

◆ to_field_sensitive_ssa_expr() [2/2]

field_sensitive_ssa_exprt& to_field_sensitive_ssa_expr ( exprt expr)
inline

Definition at line 48 of file field_sensitivity.h.