CBMC
Loading...
Searching...
No Matches
Classes | Functions
state.h File Reference
#include <util/mathematical_types.h>
#include <util/pointer_expr.h>
+ Include dependency graph for state.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class   state_typet
 
class   initial_state_exprt
 
class   evaluate_exprt
 
class   update_state_exprt
 
class   allocate_exprt
 
class   allocate_state_exprt
 
class   reallocate_exprt
 
class   reallocate_state_exprt
 
class   deallocate_state_exprt
 
class   state_live_object_exprt
 
class   state_writeable_object_exprt
 
class   state_is_cstring_exprt
 
class   state_cstrlen_exprt
 
class   state_is_dynamic_object_exprt
 
class   state_object_size_exprt
 
class   state_ok_exprt
 
class   state_type_compatible_exprt
 
class   enter_scope_state_exprt
 
class   exit_scope_state_exprt
 

Functions

static mathematical_function_typet  state_predicate_type ()
 
static symbol_exprt  state_expr ()
 
const initial_state_exprt &  to_initial_state_expr (const exprt &expr)
  Cast an exprt to a initial_state_exprt.
 
initial_state_exprt &  to_initial_state_expr (exprt &expr)
  Cast an exprt to a initial_state_exprt.
 
const evaluate_exprt &  to_evaluate_expr (const exprt &expr)
  Cast an exprt to a evaluate_exprt.
 
evaluate_exprt &  to_evaluate_expr (exprt &expr)
  Cast an exprt to a evaluate_exprt.
 
const update_state_exprt &  to_update_state_expr (const exprt &expr)
  Cast an exprt to a update_state_exprt.
 
update_state_exprt &  to_update_state_expr (exprt &expr)
  Cast an exprt to a update_state_exprt.
 
const allocate_exprt &  to_allocate_expr (const exprt &expr)
  Cast an exprt to a allocate_exprt.
 
const allocate_state_exprt &  to_allocate_state_expr (const exprt &expr)
  Cast an exprt to a allocate_state_exprt.
 
const reallocate_exprt &  to_reallocate_expr (const exprt &expr)
  Cast an exprt to a reallocate_exprt.
 
const reallocate_state_exprt &  to_reallocate_state_expr (const exprt &expr)
  Cast an exprt to a reallocate_state_exprt.
 
const deallocate_state_exprt &  to_deallocate_state_expr (const exprt &expr)
  Cast an exprt to a deallocate_state_exprt.
 
const state_live_object_exprt &  to_state_live_object_expr (const exprt &expr)
  Cast an exprt to a state_live_object_exprt.
 
state_live_object_exprt &  to_state_live_object_expr (exprt &expr)
  Cast an exprt to a state_live_object_exprt.
 
const state_writeable_object_exprt &  to_state_writeable_object_expr (const exprt &expr)
  Cast an exprt to a state_writeable_object_exprt.
 
state_writeable_object_exprt &  to_state_writeable_object_expr (exprt &expr)
  Cast an exprt to a state_writeable_object_exprt.
 
const state_is_cstring_exprt &  to_state_is_cstring_expr (const exprt &expr)
  Cast an exprt to a state_is_cstring_exprt.
 
state_is_cstring_exprt &  to_state_is_cstring_expr (exprt &expr)
  Cast an exprt to a state_is_cstring_exprt.
 
const state_cstrlen_exprt &  to_state_cstrlen_expr (const exprt &expr)
  Cast an exprt to a state_cstrlen_exprt.
 
state_cstrlen_exprt &  to_state_cstrlen_expr (exprt &expr)
  Cast an exprt to a state_cstrlen_exprt.
 
const state_is_dynamic_object_exprt &  to_state_is_dynamic_object_expr (const exprt &expr)
  Cast an exprt to a state_is_dynamic_object_exprt.
 
state_is_dynamic_object_exprt &  to_state_is_dynamic_object_expr (exprt &expr)
  Cast an exprt to a state_is_dynamic_object_exprt.
 
const state_object_size_exprt &  to_state_object_size_expr (const exprt &expr)
  Cast an exprt to a state_object_size_exprt.
 
state_object_size_exprt &  to_state_object_size_expr (exprt &expr)
  Cast an exprt to a state_object_size_exprt.
 
const state_ok_exprt &  to_state_ok_expr (const exprt &expr)
  Cast an exprt to a state_ok_exprt.
 
state_ok_exprt &  to_state_ok_expr (exprt &expr)
  Cast an exprt to a state_ok_exprt.
 
const state_type_compatible_exprt &  to_state_type_compatible_expr (const exprt &expr)
  Cast an exprt to a state_type_compatible_exprt.
 
state_type_compatible_exprt &  to_state_type_compatible_expr (exprt &expr)
  Cast an exprt to a state_type_compatible_exprt.
 
const enter_scope_state_exprt &  to_enter_scope_state_expr (const exprt &expr)
  Cast an exprt to a enter_scope_state_exprt.
 
enter_scope_state_exprt &  to_enter_scope_state_expr (exprt &expr)
  Cast an exprt to a enter_scope_state_exprt.
 
const exit_scope_state_exprt &  to_exit_scope_state_expr (const exprt &expr)
  Cast an exprt to a exit_scope_state_exprt.
 
exit_scope_state_exprt &  to_exit_scope_state_expr (exprt &expr)
  Cast an exprt to a exit_scope_state_exprt.
 

Function Documentation

◆  state_expr()

static symbol_exprt state_expr ( )
inlinestatic

Definition at line 28 of file state.h.

◆  state_predicate_type()

static mathematical_function_typet state_predicate_type ( )
inlinestatic

Definition at line 23 of file state.h.

◆  to_allocate_expr()

const allocate_exprt & to_allocate_expr ( const exprt &  expr )
inline

Cast an exprt to a allocate_exprt.

expr must be known to be allocate_exprt.

Parameters
expr Source expression
Returns
Object of type allocate_exprt

Definition at line 260 of file state.h.

◆  to_allocate_state_expr()

const allocate_state_exprt & to_allocate_state_expr ( const exprt &  expr )
inline

Cast an exprt to a allocate_state_exprt.

expr must be known to be allocate_state_exprt.

Parameters
expr Source expression
Returns
Object of type allocate_state_exprt

Definition at line 303 of file state.h.

◆  to_deallocate_state_expr()

const deallocate_state_exprt & to_deallocate_state_expr ( const exprt &  expr )
inline

Cast an exprt to a deallocate_state_exprt.

expr must be known to be deallocate_state_exprt.

Parameters
expr Source expression
Returns
Object of type deallocate_state_exprt

Definition at line 446 of file state.h.

◆  to_enter_scope_state_expr() [1/2]

const enter_scope_state_exprt & to_enter_scope_state_expr ( const exprt &  expr )
inline

Cast an exprt to a enter_scope_state_exprt.

expr must be known to be enter_scope_state_exprt.

Parameters
expr Source expression
Returns
Object of type enter_scope_state_exprt

Definition at line 1042 of file state.h.

◆  to_enter_scope_state_expr() [2/2]

enter_scope_state_exprt & to_enter_scope_state_expr ( exprt &  expr )
inline

Cast an exprt to a enter_scope_state_exprt.

expr must be known to be enter_scope_state_exprt.

Parameters
expr Source expression
Returns
Object of type enter_scope_state_exprt

Definition at line 1052 of file state.h.

◆  to_evaluate_expr() [1/2]

const evaluate_exprt & to_evaluate_expr ( const exprt &  expr )
inline

Cast an exprt to a evaluate_exprt.

expr must be known to be evaluate_exprt.

Parameters
expr Source expression
Returns
Object of type evaluate_exprt

Definition at line 130 of file state.h.

◆  to_evaluate_expr() [2/2]

evaluate_exprt & to_evaluate_expr ( exprt &  expr )
inline

Cast an exprt to a evaluate_exprt.

expr must be known to be evaluate_exprt.

Parameters
expr Source expression
Returns
Object of type evaluate_exprt

Definition at line 139 of file state.h.

◆  to_exit_scope_state_expr() [1/2]

const exit_scope_state_exprt & to_exit_scope_state_expr ( const exprt &  expr )
inline

Cast an exprt to a exit_scope_state_exprt.

expr must be known to be exit_scope_state_exprt.

Parameters
expr Source expression
Returns
Object of type exit_scope_state_exprt

Definition at line 1119 of file state.h.

◆  to_exit_scope_state_expr() [2/2]

exit_scope_state_exprt & to_exit_scope_state_expr ( exprt &  expr )
inline

Cast an exprt to a exit_scope_state_exprt.

expr must be known to be exit_scope_state_exprt.

Parameters
expr Source expression
Returns
Object of type exit_scope_state_exprt

Definition at line 1129 of file state.h.

◆  to_initial_state_expr() [1/2]

const initial_state_exprt & to_initial_state_expr ( const exprt &  expr )
inline

Cast an exprt to a initial_state_exprt.

expr must be known to be initial_state_exprt.

Parameters
expr Source expression
Returns
Object of type initial_state_exprt

Definition at line 59 of file state.h.

◆  to_initial_state_expr() [2/2]

initial_state_exprt & to_initial_state_expr ( exprt &  expr )
inline

Cast an exprt to a initial_state_exprt.

expr must be known to be initial_state_exprt.

Parameters
expr Source expression
Returns
Object of type initial_state_exprt

Definition at line 69 of file state.h.

◆  to_reallocate_expr()

const reallocate_exprt & to_reallocate_expr ( const exprt &  expr )
inline

Cast an exprt to a reallocate_exprt.

expr must be known to be reallocate_exprt.

Parameters
expr Source expression
Returns
Object of type allocate_exprt

Definition at line 353 of file state.h.

◆  to_reallocate_state_expr()

const reallocate_state_exprt & to_reallocate_state_expr ( const exprt &  expr )
inline

Cast an exprt to a reallocate_state_exprt.

expr must be known to be reallocate_state_exprt.

Parameters
expr Source expression
Returns
Object of type reallocate_state_exprt

Definition at line 402 of file state.h.

◆  to_state_cstrlen_expr() [1/2]

const state_cstrlen_exprt & to_state_cstrlen_expr ( const exprt &  expr )
inline

Cast an exprt to a state_cstrlen_exprt.

expr must be known to be state_cstrlen_exprt.

Parameters
expr Source expression
Returns
Object of type state_cstrlen_exprt

Definition at line 677 of file state.h.

◆  to_state_cstrlen_expr() [2/2]

state_cstrlen_exprt & to_state_cstrlen_expr ( exprt &  expr )
inline

Cast an exprt to a state_cstrlen_exprt.

expr must be known to be state_cstrlen_exprt.

Parameters
expr Source expression
Returns
Object of type state_cstrlen_exprt

Definition at line 687 of file state.h.

◆  to_state_is_cstring_expr() [1/2]

const state_is_cstring_exprt & to_state_is_cstring_expr ( const exprt &  expr )
inline

Cast an exprt to a state_is_cstring_exprt.

expr must be known to be state_is_cstring_exprt.

Parameters
expr Source expression
Returns
Object of type state_is_cstring_exprt

Definition at line 615 of file state.h.

◆  to_state_is_cstring_expr() [2/2]

state_is_cstring_exprt & to_state_is_cstring_expr ( exprt &  expr )
inline

Cast an exprt to a state_is_cstring_exprt.

expr must be known to be state_is_cstring_exprt.

Parameters
expr Source expression
Returns
Object of type state_is_cstring_exprt

Definition at line 625 of file state.h.

◆  to_state_is_dynamic_object_expr() [1/2]

const state_is_dynamic_object_exprt & to_state_is_dynamic_object_expr ( const exprt &  expr )
inline

Cast an exprt to a state_is_dynamic_object_exprt.

expr must be known to be state_is_dynamic_object_exprt.

Parameters
expr Source expression
Returns
Object of type state_is_dynamic_object_exprt

Definition at line 739 of file state.h.

◆  to_state_is_dynamic_object_expr() [2/2]

state_is_dynamic_object_exprt & to_state_is_dynamic_object_expr ( exprt &  expr )
inline

Cast an exprt to a state_is_dynamic_object_exprt.

expr must be known to be state_is_dynamic_object_exprt.

Parameters
expr Source expression
Returns
Object of type state_is_dynamic_object_exprt

Definition at line 750 of file state.h.

◆  to_state_live_object_expr() [1/2]

const state_live_object_exprt & to_state_live_object_expr ( const exprt &  expr )
inline

Cast an exprt to a state_live_object_exprt.

expr must be known to be state_live_object_exprt.

Parameters
expr Source expression
Returns
Object of type state_live_object_exprt

Definition at line 499 of file state.h.

◆  to_state_live_object_expr() [2/2]

state_live_object_exprt & to_state_live_object_expr ( exprt &  expr )
inline

Cast an exprt to a state_live_object_exprt.

expr must be known to be state_live_object_exprt.

Parameters
expr Source expression
Returns
Object of type state_live_object_exprt

Definition at line 509 of file state.h.

◆  to_state_object_size_expr() [1/2]

const state_object_size_exprt & to_state_object_size_expr ( const exprt &  expr )
inline

Cast an exprt to a state_object_size_exprt.

expr must be known to be state_object_size_exprt.

Parameters
expr Source expression
Returns
Object of type state_object_size_exprt

Definition at line 804 of file state.h.

◆  to_state_object_size_expr() [2/2]

state_object_size_exprt & to_state_object_size_expr ( exprt &  expr )
inline

Cast an exprt to a state_object_size_exprt.

expr must be known to be state_object_size_exprt.

Parameters
expr Source expression
Returns
Object of type state_object_size_exprt

Definition at line 814 of file state.h.

◆  to_state_ok_expr() [1/2]

const state_ok_exprt & to_state_ok_expr ( const exprt &  expr )
inline

Cast an exprt to a state_ok_exprt.

expr must be known to be state_ok_exprt.

Parameters
expr Source expression
Returns
Object of type state_ok_exprt

Definition at line 882 of file state.h.

◆  to_state_ok_expr() [2/2]

state_ok_exprt & to_state_ok_expr ( exprt &  expr )
inline

Cast an exprt to a state_ok_exprt.

expr must be known to be state_ok_exprt.

Parameters
expr Source expression
Returns
Object of type state_ok_exprt

Definition at line 893 of file state.h.

◆  to_state_type_compatible_expr() [1/2]

const state_type_compatible_exprt & to_state_type_compatible_expr ( const exprt &  expr )
inline

Cast an exprt to a state_type_compatible_exprt.

expr must be known to be state_type_compatible_exprt.

Parameters
expr Source expression
Returns
Object of type state_type_compatible_exprt

Definition at line 958 of file state.h.

◆  to_state_type_compatible_expr() [2/2]

state_type_compatible_exprt & to_state_type_compatible_expr ( exprt &  expr )
inline

Cast an exprt to a state_type_compatible_exprt.

expr must be known to be state_type_compatible_exprt.

Parameters
expr Source expression
Returns
Object of type state_type_compatible_exprt

Definition at line 968 of file state.h.

◆  to_state_writeable_object_expr() [1/2]

const state_writeable_object_exprt & to_state_writeable_object_expr ( const exprt &  expr )
inline

Cast an exprt to a state_writeable_object_exprt.

expr must be known to be state_writeable_object_exprt.

Parameters
expr Source expression
Returns
Object of type state_writeable_object_exprt

Definition at line 553 of file state.h.

◆  to_state_writeable_object_expr() [2/2]

state_writeable_object_exprt & to_state_writeable_object_expr ( exprt &  expr )
inline

Cast an exprt to a state_writeable_object_exprt.

expr must be known to be state_writeable_object_exprt.

Parameters
expr Source expression
Returns
Object of type state_writeable_object_exprt

Definition at line 563 of file state.h.

◆  to_update_state_expr() [1/2]

const update_state_exprt & to_update_state_expr ( const exprt &  expr )
inline

Cast an exprt to a update_state_exprt.

expr must be known to be update_state_exprt.

Parameters
expr Source expression
Returns
Object of type update_state_exprt

Definition at line 200 of file state.h.

◆  to_update_state_expr() [2/2]

update_state_exprt & to_update_state_expr ( exprt &  expr )
inline

Cast an exprt to a update_state_exprt.

expr must be known to be update_state_exprt.

Parameters
expr Source expression
Returns
Object of type update_state_exprt

Definition at line 209 of file state.h.

AltStyle によって変換されたページ (->オリジナル) /