API to expression classes. More...

#include "invariant.h"
#include "std_types.h"

Include dependency graph for std_expr.h:

Classes
class	transt
	A transition system, consisting of state invariant, initial state predicate, and transition predicate. More...

class	symbol_exprt
	Expression to hold a symbol (variable) More...

class	decorated_symbol_exprt
	Expression to hold a symbol (variable) More...

class	unary_exprt
	Generic base class for unary expressions. More...

class	abs_exprt
	absolute value More...

class	unary_minus_exprt
	The unary minus expression. More...

class	predicate_exprt
	A generic base class for expressions that are predicates, i.e., boolean-typed. More...

class	unary_predicate_exprt
	A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly one argument. More...

class	sign_exprt
	sign of an expression More...

class	binary_exprt
	A generic base class for binary expressions. More...

class	binary_predicate_exprt
	A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly two arguments. More...

class	binary_relation_exprt
	A generic base class for relations, i.e., binary predicates. More...

class	multi_ary_exprt
	A generic base class for multi-ary expressions. More...

class	plus_exprt
	The plus expression. More...

class	minus_exprt
	binary minus More...

class	mult_exprt
	binary multiplication More...

class	div_exprt
	division (integer and real) More...

class	mod_exprt
	binary modulo More...

class	rem_exprt
	remainder of division More...

class	power_exprt
	exponentiation More...

class	factorial_power_exprt
	falling factorial power More...

class	equal_exprt
	equality More...

class	notequal_exprt
	inequality More...

class	index_exprt
	array index operator More...

class	array_of_exprt
	array constructor from single element More...

class	array_exprt
	array constructor from list of elements More...

class	vector_exprt
	vector constructor from list of elements More...

class	union_exprt
	union constructor from single element More...

class	struct_exprt
	struct constructor from list of elements More...

class	complex_exprt
	complex constructor from a pair of numbers More...

class	object_descriptor_exprt
	split an expression into a base object and a (byte) offset More...

class	dynamic_object_exprt
	TO_BE_DOCUMENTED. More...

class	typecast_exprt
	semantic type conversion More...

class	floatbv_typecast_exprt
	semantic type conversion from/to floating-point formats More...

class	and_exprt
	boolean AND More...

class	implies_exprt
	boolean implication More...

class	or_exprt
	boolean OR More...

class	bitnot_exprt
	Bit-wise negation of bit-vectors. More...

class	bitor_exprt
	Bit-wise OR. More...

class	bitxor_exprt
	Bit-wise XOR. More...

class	bitand_exprt
	Bit-wise AND. More...

class	shift_exprt
	A base class for shift operators. More...

class	shl_exprt
	Left shift. More...

class	ashr_exprt
	Arithmetic right shift. More...

class	lshr_exprt
	Logical right shift. More...

class	replication_exprt
	Bit-vector replication. More...

class	extractbit_exprt
	Extracts a single bit of a bit-vector operand. More...

class	extractbits_exprt
	Extracts a sub-range of a bit-vector operand. More...

class	address_of_exprt
	Operator to return the address of an object. More...

class	not_exprt
	Boolean negation. More...

class	dereference_exprt
	Operator to dereference a pointer. More...

class	if_exprt
	The trinary if-then-else operator. More...

class	with_exprt
	Operator to update elements in structs and arrays. More...

class	index_designatort

class	member_designatort

class	update_exprt
	Operator to update elements in structs and arrays. More...

class	member_exprt
	Extract member of struct or union. More...

class	isnan_exprt
	Evaluates to true if the operand is NaN. More...

class	isinf_exprt
	Evaluates to true if the operand is infinite. More...

class	isfinite_exprt
	Evaluates to true if the operand is finite. More...

class	isnormal_exprt
	Evaluates to true if the operand is a normal number. More...

class	ieee_float_equal_exprt
	IEEE-floating-point equality. More...

class	ieee_float_notequal_exprt
	IEEE floating-point disequality. More...

class	ieee_float_op_exprt
	IEEE floating-point operations. More...

class	type_exprt
	An expression denoting a type. More...

class	constant_exprt
	A constant literal expression. More...

class	true_exprt
	The boolean constant true. More...

class	false_exprt
	The boolean constant false. More...

class	nil_exprt
	The NIL expression. More...

class	null_pointer_exprt
	The null pointer constant. More...

class	function_application_exprt
	application of (mathematical) function More...

class	concatenation_exprt
	Concatenation of bit-vector operands. More...

class	infinity_exprt
	An expression denoting infinity. More...

class	let_exprt
	A let expression. More...

class	forall_exprt
	A forall expression. More...

class	exists_exprt
	An exists expression. More...

Functions
const transt &	to_trans_expr (const exprt &expr)
	Cast a generic exprt to a transt. More...

transt &	to_trans_expr (exprt &expr)

const symbol_exprt &	to_symbol_expr (const exprt &expr)
	Cast a generic exprt to a symbol_exprt. More...

symbol_exprt &	to_symbol_expr (exprt &expr)
	Cast a generic exprt to a symbol_exprt. More...

const unary_exprt &	to_unary_expr (const exprt &expr)
	Cast a generic exprt to a unary_exprt. More...

unary_exprt &	to_unary_expr (exprt &expr)
	Cast a generic exprt to a unary_exprt. More...

const abs_exprt &	to_abs_expr (const exprt &expr)
	Cast a generic exprt to a abs_exprt. More...

abs_exprt &	to_abs_expr (exprt &expr)
	Cast a generic exprt to a abs_exprt. More...

const unary_minus_exprt &	to_unary_minus_expr (const exprt &expr)
	Cast a generic exprt to a unary_minus_exprt. More...

unary_minus_exprt &	to_unary_minus_expr (exprt &expr)
	Cast a generic exprt to a unary_minus_exprt. More...

const binary_exprt &	to_binary_expr (const exprt &expr)
	Cast a generic exprt to a binary_exprt. More...

binary_exprt &	to_binary_expr (exprt &expr)
	Cast a generic exprt to a binary_exprt. More...

const binary_relation_exprt &	to_binary_relation_expr (const exprt &expr)
	Cast a generic exprt to a binary_relation_exprt. More...

binary_relation_exprt &	to_binary_relation_expr (exprt &expr)
	Cast a generic exprt to a binary_relation_exprt. More...

const multi_ary_exprt &	to_multi_ary_expr (const exprt &expr)
	Cast a generic exprt to a multi_ary_exprt. More...

multi_ary_exprt &	to_multi_ary_expr (exprt &expr)
	Cast a generic exprt to a multi_ary_exprt. More...

const plus_exprt &	to_plus_expr (const exprt &expr)
	Cast a generic exprt to a plus_exprt. More...

plus_exprt &	to_plus_expr (exprt &expr)
	Cast a generic exprt to a plus_exprt. More...

const minus_exprt &	to_minus_expr (const exprt &expr)
	Cast a generic exprt to a minus_exprt. More...

minus_exprt &	to_minus_expr (exprt &expr)
	Cast a generic exprt to a minus_exprt. More...

const mult_exprt &	to_mult_expr (const exprt &expr)
	Cast a generic exprt to a mult_exprt. More...

mult_exprt &	to_mult_expr (exprt &expr)
	Cast a generic exprt to a mult_exprt. More...

const div_exprt &	to_div_expr (const exprt &expr)
	Cast a generic exprt to a div_exprt. More...

div_exprt &	to_div_expr (exprt &expr)
	Cast a generic exprt to a div_exprt. More...

const mod_exprt &	to_mod_expr (const exprt &expr)
	Cast a generic exprt to a mod_exprt. More...

mod_exprt &	to_mod_expr (exprt &expr)
	Cast a generic exprt to a mod_exprt. More...

const rem_exprt &	to_rem_expr (const exprt &expr)
	Cast a generic exprt to a rem_exprt. More...

rem_exprt &	to_rem_expr (exprt &expr)
	Cast a generic exprt to a rem_exprt. More...

const power_exprt &	to_power_expr (const exprt &expr)
	Cast a generic exprt to a power_exprt. More...

power_exprt &	to_power_expr (exprt &expr)
	Cast a generic exprt to a power_exprt. More...

const factorial_power_exprt &	to_factorial_power_expr (const exprt &expr)
	Cast a generic exprt to a factorial_power_exprt. More...

factorial_power_exprt &	to_factorial_expr (exprt &expr)
	Cast a generic exprt to a factorial_power_exprt. More...

const equal_exprt &	to_equal_expr (const exprt &expr)
	Cast a generic exprt to an equal_exprt. More...

equal_exprt &	to_equal_expr (exprt &expr)
	Cast a generic exprt to an equal_exprt. More...

const notequal_exprt &	to_notequal_expr (const exprt &expr)
	Cast a generic exprt to an notequal_exprt. More...

notequal_exprt &	to_notequal_expr (exprt &expr)
	Cast a generic exprt to an notequal_exprt. More...

const index_exprt &	to_index_expr (const exprt &expr)
	Cast a generic exprt to an index_exprt. More...

index_exprt &	to_index_expr (exprt &expr)
	Cast a generic exprt to an index_exprt. More...

const array_of_exprt &	to_array_of_expr (const exprt &expr)
	Cast a generic exprt to an array_of_exprt. More...

array_of_exprt &	to_array_of_expr (exprt &expr)
	Cast a generic exprt to an array_of_exprt. More...

const array_exprt &	to_array_expr (const exprt &expr)
	Cast a generic exprt to an array_exprt. More...

array_exprt &	to_array_expr (exprt &expr)
	Cast a generic exprt to an array_exprt. More...

const vector_exprt &	to_vector_expr (const exprt &expr)
	Cast a generic exprt to an vector_exprt. More...

vector_exprt &	to_vector_expr (exprt &expr)
	Cast a generic exprt to an vector_exprt. More...

const union_exprt &	to_union_expr (const exprt &expr)
	Cast a generic exprt to a union_exprt. More...

union_exprt &	to_union_expr (exprt &expr)
	Cast a generic exprt to a union_exprt. More...

const struct_exprt &	to_struct_expr (const exprt &expr)
	Cast a generic exprt to a struct_exprt. More...

struct_exprt &	to_struct_expr (exprt &expr)
	Cast a generic exprt to a struct_exprt. More...

const complex_exprt &	to_complex_expr (const exprt &expr)
	Cast a generic exprt to a complex_exprt. More...

complex_exprt &	to_complex_expr (exprt &expr)
	Cast a generic exprt to a complex_exprt. More...

const object_descriptor_exprt &	to_object_descriptor_expr (const exprt &expr)
	Cast a generic exprt to an object_descriptor_exprt. More...

object_descriptor_exprt &	to_object_descriptor_expr (exprt &expr)
	Cast a generic exprt to an object_descriptor_exprt. More...

const dynamic_object_exprt &	to_dynamic_object_expr (const exprt &expr)
	Cast a generic exprt to a dynamic_object_exprt. More...

dynamic_object_exprt &	to_dynamic_object_expr (exprt &expr)
	Cast a generic exprt to a dynamic_object_exprt. More...

const typecast_exprt &	to_typecast_expr (const exprt &expr)
	Cast a generic exprt to a typecast_exprt. More...

typecast_exprt &	to_typecast_expr (exprt &expr)
	Cast a generic exprt to a typecast_exprt. More...

const floatbv_typecast_exprt &	to_floatbv_typecast_expr (const exprt &expr)
	Cast a generic exprt to a floatbv_typecast_exprt. More...

floatbv_typecast_exprt &	to_floatbv_typecast_expr (exprt &expr)
	Cast a generic exprt to a floatbv_typecast_exprt. More...

exprt	conjunction (const exprt::operandst &)

const and_exprt &	to_and_expr (const exprt &expr)
	Cast a generic exprt to a and_exprt. More...

and_exprt &	to_and_expr (exprt &expr)
	Cast a generic exprt to a and_exprt. More...

const implies_exprt &	to_implies_expr (const exprt &expr)
	Cast a generic exprt to a implies_exprt. More...

implies_exprt &	to_implies_expr (exprt &expr)
	Cast a generic exprt to a implies_exprt. More...

exprt	disjunction (const exprt::operandst &)

const or_exprt &	to_or_expr (const exprt &expr)
	Cast a generic exprt to a or_exprt. More...

or_exprt &	to_or_expr (exprt &expr)
	Cast a generic exprt to a or_exprt. More...

const bitnot_exprt &	to_bitnot_expr (const exprt &expr)
	Cast a generic exprt to a bitnot_exprt. More...

bitnot_exprt &	to_bitnot_expr (exprt &expr)
	Cast a generic exprt to a bitnot_exprt. More...

const bitor_exprt &	to_bitor_expr (const exprt &expr)
	Cast a generic exprt to a bitor_exprt. More...

bitor_exprt &	to_bitor_expr (exprt &expr)
	Cast a generic exprt to a bitor_exprt. More...

const bitxor_exprt &	to_bitxor_expr (const exprt &expr)
	Cast a generic exprt to a bitxor_exprt. More...

bitxor_exprt &	to_bitxor_expr (exprt &expr)
	Cast a generic exprt to a bitxor_exprt. More...

const bitand_exprt &	to_bitand_expr (const exprt &expr)
	Cast a generic exprt to a bitand_exprt. More...

bitand_exprt &	to_bitand_expr (exprt &expr)
	Cast a generic exprt to a bitand_exprt. More...

const shift_exprt &	to_shift_expr (const exprt &expr)
	Cast a generic exprt to a shift_exprt. More...

shift_exprt &	to_shift_expr (exprt &expr)
	Cast a generic exprt to a shift_exprt. More...

const replication_exprt &	to_replication_expr (const exprt &expr)
	Cast a generic exprt to a replication_exprt. More...

replication_exprt &	to_replication_expr (exprt &expr)
	Cast a generic exprt to a replication_exprt. More...

const extractbit_exprt &	to_extractbit_expr (const exprt &expr)
	Cast a generic exprt to an extractbit_exprt. More...

extractbit_exprt &	to_extractbit_expr (exprt &expr)
	Cast a generic exprt to an extractbit_exprt. More...

const extractbits_exprt &	to_extractbits_expr (const exprt &expr)
	Cast a generic exprt to an extractbits_exprt. More...

extractbits_exprt &	to_extractbits_expr (exprt &expr)
	Cast a generic exprt to an extractbits_exprt. More...

const address_of_exprt &	to_address_of_expr (const exprt &expr)
	Cast a generic exprt to an address_of_exprt. More...

address_of_exprt &	to_address_of_expr (exprt &expr)
	Cast a generic exprt to an address_of_exprt. More...

const not_exprt &	to_not_expr (const exprt &expr)
	Cast a generic exprt to an not_exprt. More...

not_exprt &	to_not_expr (exprt &expr)
	Cast a generic exprt to an not_exprt. More...

const dereference_exprt &	to_dereference_expr (const exprt &expr)
	Cast a generic exprt to a dereference_exprt. More...

dereference_exprt &	to_dereference_expr (exprt &expr)
	Cast a generic exprt to a dereference_exprt. More...

const if_exprt &	to_if_expr (const exprt &expr)
	Cast a generic exprt to an if_exprt. More...

if_exprt &	to_if_expr (exprt &expr)
	Cast a generic exprt to an if_exprt. More...

const with_exprt &	to_with_expr (const exprt &expr)
	Cast a generic exprt to a with_exprt. More...

with_exprt &	to_with_expr (exprt &expr)
	Cast a generic exprt to a with_exprt. More...

const index_designatort &	to_index_designator (const exprt &expr)
	Cast a generic exprt to an index_designatort. More...

index_designatort &	to_index_designator (exprt &expr)
	Cast a generic exprt to an index_designatort. More...

const member_designatort &	to_member_designator (const exprt &expr)
	Cast a generic exprt to an member_designatort. More...

member_designatort &	to_member_designator (exprt &expr)
	Cast a generic exprt to an member_designatort. More...

const update_exprt &	to_update_expr (const exprt &expr)
	Cast a generic exprt to an update_exprt. More...

update_exprt &	to_update_expr (exprt &expr)
	Cast a generic exprt to an update_exprt. More...

const member_exprt &	to_member_expr (const exprt &expr)
	Cast a generic exprt to a member_exprt. More...

member_exprt &	to_member_expr (exprt &expr)
	Cast a generic exprt to a member_exprt. More...

const isnan_exprt &	to_isnan_expr (const exprt &expr)
	Cast a generic exprt to a isnan_exprt. More...

isnan_exprt &	to_isnan_expr (exprt &expr)
	Cast a generic exprt to a isnan_exprt. More...

const isinf_exprt &	to_isinf_expr (const exprt &expr)
	Cast a generic exprt to a isinf_exprt. More...

isinf_exprt &	to_isinf_expr (exprt &expr)
	Cast a generic exprt to a isinf_exprt. More...

const isfinite_exprt &	to_isfinite_expr (const exprt &expr)
	Cast a generic exprt to a isfinite_exprt. More...

isfinite_exprt &	to_isfinite_expr (exprt &expr)
	Cast a generic exprt to a isfinite_exprt. More...

const isnormal_exprt &	to_isnormal_expr (const exprt &expr)
	Cast a generic exprt to a isnormal_exprt. More...

isnormal_exprt &	to_isnormal_expr (exprt &expr)
	Cast a generic exprt to a isnormal_exprt. More...

const ieee_float_equal_exprt &	to_ieee_float_equal_expr (const exprt &expr)
	Cast a generic exprt to an ieee_float_equal_exprt. More...

ieee_float_equal_exprt &	to_ieee_float_equal_expr (exprt &expr)
	Cast a generic exprt to an ieee_float_equal_exprt. More...

const ieee_float_notequal_exprt &	to_ieee_float_notequal_expr (const exprt &expr)
	Cast a generic exprt to an ieee_float_notequal_exprt. More...

ieee_float_notequal_exprt &	to_ieee_float_notequal_expr (exprt &expr)
	Cast a generic exprt to an ieee_float_notequal_exprt. More...

const ieee_float_op_exprt &	to_ieee_float_op_expr (const exprt &expr)
	Cast a generic exprt to an ieee_float_op_exprt. More...

ieee_float_op_exprt &	to_ieee_float_op_expr (exprt &expr)
	Cast a generic exprt to an ieee_float_op_exprt. More...

const constant_exprt &	to_constant_expr (const exprt &expr)
	Cast a generic exprt to a constant_exprt. More...

constant_exprt &	to_constant_expr (exprt &expr)
	Cast a generic exprt to a constant_exprt. More...

const function_application_exprt &	to_function_application_expr (const exprt &expr)
	Cast a generic exprt to a function_application_exprt. More...

function_application_exprt &	to_function_application_expr (exprt &expr)
	Cast a generic exprt to a function_application_exprt. More...

const concatenation_exprt &	to_concatenation_expr (const exprt &expr)
	Cast a generic exprt to a concatenation_exprt. More...

concatenation_exprt &	to_concatenation_expr (exprt &expr)
	Cast a generic exprt to a concatenation_exprt. More...

const let_exprt &	to_let_expr (const exprt &expr)
	Cast a generic exprt to a let_exprt. More...

let_exprt &	to_let_expr (exprt &expr)
	Cast a generic exprt to a let_exprt. More...