CBMC: /home/runner/work/cbmc/cbmc/src/goto-symex/field_sensitivity.h File Reference

CBMC

Loading...

Searching...

No Matches

Classes | Functions

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_exprt & to_field_sensitive_ssa_expr (const exprt &expr)

field_sensitive_ssa_exprt & to_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 36 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 42 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 50 of file field_sensitivity.h.