CBMC: /home/runner/work/cbmc/cbmc/src/util/std

CBMC: /home/runner/work/cbmc/cbmc/src/util/std_expr.h File Reference

API to expression classes. More...

#include "deprecate.h"
#include "expr_cast.h"
#include "invariant.h"
#include "std_types.h"

Classes
class	nullary_exprt
	An expression without operands. More...

class	ternary_exprt
	An expression with three operands. More...

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

struct	std::hash<::symbol_exprt >

class	decorated_symbol_exprt
	Expression to hold a symbol (variable) with extra accessors to ID_c_static_lifetime and ID_C_thread_local. More...

class	nondet_symbol_exprt
	Expression to hold a nondeterministic choice. 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	unary_plus_exprt
	The unary plus expression. More...

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

class	unary_predicate_exprt
	A 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 Predicate is true if _op is negative, false otherwise. More...

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

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

class	binary_relation_exprt
	A base class for relations, i.e., binary predicates whose two operands have the same type. More...

class	greater_than_exprt
	Binary greater than operator expression. More...

class	greater_than_or_equal_exprt
	Binary greater than or equal operator expression. More...

class	less_than_exprt
	Binary less than operator expression. More...

class	less_than_or_equal_exprt
	Binary less than or equal operator expression. More...

class	multi_ary_exprt
	A base class for multi-ary expressions Associativity is not specified. More...

class	plus_exprt
	The plus expression Associativity is not specified. More...

class	minus_exprt
	Binary minus. More...

class	mult_exprt
	Binary multiplication Associativity is not specified. More...

class	div_exprt
	Division. More...

class	mod_exprt
	Modulo defined as lhs-(rhs * truncate(lhs/rhs)). More...

class	euclidean_mod_exprt
	Boute's Euclidean definition of Modulo – to match SMT-LIB2. More...

class	equal_exprt
	Equality. More...

class	notequal_exprt
	Disequality. 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	array_list_exprt
	Array constructor from a list of index-element pairs Operands are index/value pairs, alternating. More...

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

class	union_exprt
	Union constructor from single element. More...

class	empty_union_exprt
	Union constructor to support unions without any member (a GCC/Clang feature). More...

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

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

class	complex_real_exprt
	Real part of the expression describing a complex number. More...

class	complex_imag_exprt
	Imaginary part of the expression describing a complex number. More...

class	typecast_exprt
	Semantic type conversion. More...

class	and_exprt
	Boolean AND All operands must be boolean, and the result is always boolean. More...

class	nand_exprt
	Boolean NAND. More...

class	implies_exprt
	Boolean implication. More...

class	or_exprt
	Boolean OR All operands must be boolean, and the result is always boolean. More...

class	nor_exprt
	Boolean NOR. More...

class	xor_exprt
	Boolean XOR All operands must be boolean, and the result is always boolean. More...

class	xnor_exprt
	Boolean XNOR. More...

class	not_exprt
	Boolean negation. 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	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	infinity_exprt
	An expression denoting infinity. More...

class	binding_exprt
	A base class for variable bindings (quantifiers, let, lambda) More...

class	let_exprt
	A let expression. More...

class	cond_exprt
	this is a parametric version of an if-expression: it returns the value of the first case (using the ordering of the operands) whose condition evaluates to true. More...

class	case_exprt
	Case expression: evaluates to the value corresponding to the first matching case. More...

class	array_comprehension_exprt
	Expression to define a mapping from an argument (index) to elements. More...

class	class_method_descriptor_exprt
	An expression describing a method on a class. More...

class	named_term_exprt
	Expression that introduces a new symbol that is equal to the operand. More...

Namespaces
namespace	std
	STL namespace.

Functions
const ternary_exprt &	to_ternary_expr (const exprt &expr)
	Cast an exprt to a ternary_exprt.

ternary_exprt &	to_ternary_expr (exprt &expr)
	Cast an exprt to a ternary_exprt.

template<>
bool	can_cast_expr< symbol_exprt > (const exprt &base)

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

symbol_exprt &	to_symbol_expr (exprt &expr)
	Cast an exprt to a symbol_exprt.

template<>
bool	can_cast_expr< nondet_symbol_exprt > (const exprt &base)

void	validate_expr (const nondet_symbol_exprt &value)

const nondet_symbol_exprt &	to_nondet_symbol_expr (const exprt &expr)
	Cast an exprt to a nondet_symbol_exprt.

nondet_symbol_exprt &	to_nondet_symbol_expr (exprt &expr)
	Cast an exprt to a nondet_symbol_exprt.

template<>
bool	can_cast_expr< unary_exprt > (const exprt &base)

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

unary_exprt &	to_unary_expr (exprt &expr)
	Cast an exprt to a unary_exprt.

template<>
bool	can_cast_expr< abs_exprt > (const exprt &base)

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

abs_exprt &	to_abs_expr (exprt &expr)
	Cast an exprt to a abs_exprt.

template<>
bool	can_cast_expr< unary_minus_exprt > (const exprt &base)

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

unary_minus_exprt &	to_unary_minus_expr (exprt &expr)
	Cast an exprt to a unary_minus_exprt.

template<>
bool	can_cast_expr< unary_plus_exprt > (const exprt &base)

const unary_plus_exprt &	to_unary_plus_expr (const exprt &expr)
	Cast an exprt to a unary_plus_exprt.

unary_plus_exprt &	to_unary_plus_expr (exprt &expr)
	Cast an exprt to a unary_plus_exprt.

const unary_predicate_exprt &	to_unary_predicate_expr (const exprt &expr)
	Cast an exprt to a unary_predicate_exprt.

unary_predicate_exprt &	to_unary_predicate_expr (exprt &expr)
	Cast an exprt to a unary_predicate_exprt.

template<>
bool	can_cast_expr< sign_exprt > (const exprt &base)

const sign_exprt &	to_sign_expr (const exprt &expr)
	Cast an exprt to a sign_exprt.

sign_exprt &	to_sign_expr (exprt &expr)
	Cast an exprt to a sign_exprt.

template<>
bool	can_cast_expr< binary_exprt > (const exprt &base)

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

binary_exprt &	to_binary_expr (exprt &expr)
	Cast an exprt to a binary_exprt.

const binary_predicate_exprt &	to_binary_predicate_expr (const exprt &expr)
	Cast an exprt to a binary_predicate_exprt.

binary_predicate_exprt &	to_binary_predicate_expr (exprt &expr)
	Cast an exprt to a binary_predicate_exprt.

template<>
bool	can_cast_expr< binary_relation_exprt > (const exprt &base)

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

binary_relation_exprt &	to_binary_relation_expr (exprt &expr)
	Cast an exprt to a binary_relation_exprt.

template<>
bool	can_cast_expr< greater_than_exprt > (const exprt &base)

template<>
bool	can_cast_expr< greater_than_or_equal_exprt > (const exprt &base)

template<>
bool	can_cast_expr< less_than_exprt > (const exprt &base)

template<>
bool	can_cast_expr< less_than_or_equal_exprt > (const exprt &base)

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

multi_ary_exprt &	to_multi_ary_expr (exprt &expr)
	Cast an exprt to a multi_ary_exprt.

template<>
bool	can_cast_expr< plus_exprt > (const exprt &base)

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

plus_exprt &	to_plus_expr (exprt &expr)
	Cast an exprt to a plus_exprt.

template<>
bool	can_cast_expr< minus_exprt > (const exprt &base)

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

minus_exprt &	to_minus_expr (exprt &expr)
	Cast an exprt to a minus_exprt.

template<>
bool	can_cast_expr< mult_exprt > (const exprt &base)

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

mult_exprt &	to_mult_expr (exprt &expr)
	Cast an exprt to a mult_exprt.

template<>
bool	can_cast_expr< div_exprt > (const exprt &base)

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

div_exprt &	to_div_expr (exprt &expr)
	Cast an exprt to a div_exprt.

template<>
bool	can_cast_expr< mod_exprt > (const exprt &base)

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

mod_exprt &	to_mod_expr (exprt &expr)
	Cast an exprt to a mod_exprt.

template<>
bool	can_cast_expr< euclidean_mod_exprt > (const exprt &base)

const euclidean_mod_exprt &	to_euclidean_mod_expr (const exprt &expr)
	Cast an exprt to a euclidean_mod_exprt.

euclidean_mod_exprt &	to_euclidean_mod_expr (exprt &expr)
	Cast an exprt to a euclidean_mod_exprt.

template<>
bool	can_cast_expr< equal_exprt > (const exprt &base)

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

equal_exprt &	to_equal_expr (exprt &expr)
	Cast an exprt to an equal_exprt.

template<>
bool	can_cast_expr< notequal_exprt > (const exprt &base)

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

notequal_exprt &	to_notequal_expr (exprt &expr)
	Cast an exprt to an notequal_exprt.

template<>
bool	can_cast_expr< index_exprt > (const exprt &base)

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

index_exprt &	to_index_expr (exprt &expr)
	Cast an exprt to an index_exprt.

template<>
bool	can_cast_expr< array_of_exprt > (const exprt &base)

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

array_of_exprt &	to_array_of_expr (exprt &expr)
	Cast an exprt to an array_of_exprt.

template<>
bool	can_cast_expr< array_exprt > (const exprt &base)

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

array_exprt &	to_array_expr (exprt &expr)
	Cast an exprt to an array_exprt.

template<>
bool	can_cast_expr< array_list_exprt > (const exprt &base)

const array_list_exprt &	to_array_list_expr (const exprt &expr)

array_list_exprt &	to_array_list_expr (exprt &expr)

template<>
bool	can_cast_expr< vector_exprt > (const exprt &base)

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

vector_exprt &	to_vector_expr (exprt &expr)
	Cast an exprt to an vector_exprt.

template<>
bool	can_cast_expr< union_exprt > (const exprt &base)

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

union_exprt &	to_union_expr (exprt &expr)
	Cast an exprt to a union_exprt.

template<>
bool	can_cast_expr< empty_union_exprt > (const exprt &base)

const empty_union_exprt &	to_empty_union_expr (const exprt &expr)
	Cast an exprt to an empty_union_exprt.

empty_union_exprt &	to_empty_union_expr (exprt &expr)
	Cast an exprt to an empty_union_exprt.

template<>
bool	can_cast_expr< struct_exprt > (const exprt &base)

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

struct_exprt &	to_struct_expr (exprt &expr)
	Cast an exprt to a struct_exprt.

template<>
bool	can_cast_expr< complex_exprt > (const exprt &base)

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

complex_exprt &	to_complex_expr (exprt &expr)
	Cast an exprt to a complex_exprt.

template<>
bool	can_cast_expr< complex_real_exprt > (const exprt &base)

const complex_real_exprt &	to_complex_real_expr (const exprt &expr)
	Cast an exprt to a complex_real_exprt.

complex_real_exprt &	to_complex_real_expr (exprt &expr)
	Cast an exprt to a complex_real_exprt.

template<>
bool	can_cast_expr< complex_imag_exprt > (const exprt &base)

const complex_imag_exprt &	to_complex_imag_expr (const exprt &expr)
	Cast an exprt to a complex_imag_exprt.

complex_imag_exprt &	to_complex_imag_expr (exprt &expr)
	Cast an exprt to a complex_imag_exprt.

template<>
bool	can_cast_expr< typecast_exprt > (const exprt &base)

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

typecast_exprt &	to_typecast_expr (exprt &expr)
	Cast an exprt to a typecast_exprt.

exprt	conjunction (const exprt::operandst &)
	1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise

exprt	conjunction (exprt a, exprt b)
	Conjunction of two expressions.

template<>
bool	can_cast_expr< and_exprt > (const exprt &base)

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

and_exprt &	to_and_expr (exprt &expr)
	Cast an exprt to a and_exprt.

const nand_exprt &	to_nand_expr (const exprt &expr)
	Cast an exprt to a nand_exprt.

nand_exprt &	to_nand_expr (exprt &expr)
	Cast an exprt to a nand_exprt.

template<>
bool	can_cast_expr< implies_exprt > (const exprt &base)

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

implies_exprt &	to_implies_expr (exprt &expr)
	Cast an exprt to a implies_exprt.

exprt	disjunction (const exprt::operandst &)
	1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise

template<>
bool	can_cast_expr< or_exprt > (const exprt &base)

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

or_exprt &	to_or_expr (exprt &expr)
	Cast an exprt to a or_exprt.

const nor_exprt &	to_nor_expr (const exprt &expr)
	Cast an exprt to a nor_exprt.

nor_exprt &	to_nor_expr (exprt &expr)
	Cast an exprt to a nor_exprt.

template<>
bool	can_cast_expr< xor_exprt > (const exprt &base)

const xor_exprt &	to_xor_expr (const exprt &expr)
	Cast an exprt to a xor_exprt.

xor_exprt &	to_xor_expr (exprt &expr)
	Cast an exprt to a xor_exprt.

template<>
bool	can_cast_expr< xnor_exprt > (const exprt &base)

const xnor_exprt &	to_xnor_expr (const exprt &expr)
	Cast an exprt to a xnor_exprt.

xnor_exprt &	to_xnor_expr (exprt &expr)
	Cast an exprt to a xnor_exprt.

template<>
bool	can_cast_expr< not_exprt > (const exprt &base)

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

not_exprt &	to_not_expr (exprt &expr)
	Cast an exprt to an not_exprt.

template<>
bool	can_cast_expr< if_exprt > (const exprt &base)

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

if_exprt &	to_if_expr (exprt &expr)
	Cast an exprt to an if_exprt.

template<>
bool	can_cast_expr< with_exprt > (const exprt &base)

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

with_exprt &	to_with_expr (exprt &expr)
	Cast an exprt to a with_exprt.

template<>
bool	can_cast_expr< index_designatort > (const exprt &base)

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

index_designatort &	to_index_designator (exprt &expr)
	Cast an exprt to an index_designatort.

template<>
bool	can_cast_expr< member_designatort > (const exprt &base)

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

member_designatort &	to_member_designator (exprt &expr)
	Cast an exprt to an member_designatort.

template<>
bool	can_cast_expr< update_exprt > (const exprt &base)

void	validate_expr (const update_exprt &value)

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

update_exprt &	to_update_expr (exprt &expr)
	Cast an exprt to an update_exprt.

template<>
bool	can_cast_expr< member_exprt > (const exprt &base)

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

member_exprt &	to_member_expr (exprt &expr)
	Cast an exprt to a member_exprt.

template<>
bool	can_cast_expr< type_exprt > (const exprt &base)

const type_exprt &	to_type_expr (const exprt &expr)
	Cast an exprt to an type_exprt.

type_exprt &	to_type_expr (exprt &expr)
	Cast an exprt to an type_exprt.

template<>
bool	can_cast_expr< constant_exprt > (const exprt &base)

void	validate_expr (const constant_exprt &value)

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

constant_exprt &	to_constant_expr (exprt &expr)
	Cast an exprt to a constant_exprt.

bool	operator== (const exprt &lhs, bool rhs)
	Return whether the expression `lhs` is a constant of Boolean type that is representing the Boolean value `rhs`.

bool	operator!= (const exprt &lhs, bool rhs)
	Return whether the expression `lhs` is not a constant of Boolean type or is not representing the Boolean value `rhs`.

bool	operator== (const exprt &lhs, int rhs)
	Return whether the expression `lhs` is a constant representing the numeric value `rhs`; only values 0 and 1 are supported for `rhs`.

bool	operator!= (const exprt &lhs, int rhs)
	Returns the negation of operator==(const exprt &, int).

bool	operator== (const exprt &lhs, std::nullptr_t)
	Return whether the expression `lhs` is a constant representing the NULL pointer.

bool	operator!= (const exprt &lhs, std::nullptr_t)
	Returns the negation of operator==(const exprt &, std::nullptr_t).

template<>
bool	can_cast_expr< nil_exprt > (const exprt &base)

template<>
bool	can_cast_expr< binding_exprt > (const exprt &base)

const binding_exprt &	to_binding_expr (const exprt &expr)
	Cast an exprt to a binding_exprt.

binding_exprt &	to_binding_expr (exprt &expr)
	Cast an exprt to a binding_exprt.

template<>
bool	can_cast_expr< let_exprt > (const exprt &base)

void	validate_expr (const let_exprt &let_expr)

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

let_exprt &	to_let_expr (exprt &expr)
	Cast an exprt to a let_exprt.

template<>
bool	can_cast_expr< cond_exprt > (const exprt &base)

void	validate_expr (const cond_exprt &value)

const cond_exprt &	to_cond_expr (const exprt &expr)
	Cast an exprt to a cond_exprt.

cond_exprt &	to_cond_expr (exprt &expr)
	Cast an exprt to a cond_exprt.

template<>
bool	can_cast_expr< case_exprt > (const exprt &base)

const case_exprt &	to_case_expr (const exprt &expr)
	Cast an exprt to a case_exprt.

case_exprt &	to_case_expr (exprt &expr)
	Cast an exprt to a case_exprt.

template<>
bool	can_cast_expr< array_comprehension_exprt > (const exprt &base)

const array_comprehension_exprt &	to_array_comprehension_expr (const exprt &expr)
	Cast an exprt to a array_comprehension_exprt.

array_comprehension_exprt &	to_array_comprehension_expr (exprt &expr)
	Cast an exprt to a array_comprehension_exprt.

void	validate_expr (const class class_method_descriptor_exprt &value)

const class_method_descriptor_exprt &	to_class_method_descriptor_expr (const exprt &expr)
	Cast an exprt to a class_method_descriptor_exprt.

template<>
bool	can_cast_expr< class_method_descriptor_exprt > (const exprt &base)

template<>
bool	can_cast_expr< named_term_exprt > (const exprt &base)

const named_term_exprt &	to_named_term_expr (const exprt &expr)
	Cast an exprt to a named_term_exprt.

named_term_exprt &	to_named_term_expr (exprt &expr)
	Cast an exprt to a array_comprehension_exprt.

API to expression classes.

Definition in file std_expr.h.

◆ can_cast_expr< abs_exprt >()

◆ can_cast_expr< and_exprt >()

◆ can_cast_expr< array_comprehension_exprt >()

◆ can_cast_expr< array_exprt >()

◆ can_cast_expr< array_list_exprt >()

◆ can_cast_expr< array_of_exprt >()

◆ can_cast_expr< binary_exprt >()

◆ can_cast_expr< binary_relation_exprt >()

◆ can_cast_expr< binding_exprt >()

◆ can_cast_expr< case_exprt >()

◆ can_cast_expr< class_method_descriptor_exprt >()

◆ can_cast_expr< complex_exprt >()

◆ can_cast_expr< complex_imag_exprt >()

◆ can_cast_expr< complex_real_exprt >()

◆ can_cast_expr< cond_exprt >()

◆ can_cast_expr< constant_exprt >()

◆ can_cast_expr< div_exprt >()

◆ can_cast_expr< empty_union_exprt >()

◆ can_cast_expr< equal_exprt >()

◆ can_cast_expr< euclidean_mod_exprt >()

◆ can_cast_expr< greater_than_exprt >()

◆ can_cast_expr< greater_than_or_equal_exprt >()

◆ can_cast_expr< if_exprt >()

◆ can_cast_expr< implies_exprt >()

◆ can_cast_expr< index_designatort >()

◆ can_cast_expr< index_exprt >()

◆ can_cast_expr< less_than_exprt >()

◆ can_cast_expr< less_than_or_equal_exprt >()

◆ can_cast_expr< let_exprt >()

◆ can_cast_expr< member_designatort >()

◆ can_cast_expr< member_exprt >()

◆ can_cast_expr< minus_exprt >()

◆ can_cast_expr< mod_exprt >()

◆ can_cast_expr< mult_exprt >()

◆ can_cast_expr< named_term_exprt >()

◆ can_cast_expr< nil_exprt >()

◆ can_cast_expr< nondet_symbol_exprt >()

◆ can_cast_expr< not_exprt >()

◆ can_cast_expr< notequal_exprt >()

◆ can_cast_expr< or_exprt >()

◆ can_cast_expr< plus_exprt >()

◆ can_cast_expr< sign_exprt >()

◆ can_cast_expr< struct_exprt >()

◆ can_cast_expr< symbol_exprt >()

◆ can_cast_expr< type_exprt >()

◆ can_cast_expr< typecast_exprt >()

◆ can_cast_expr< unary_exprt >()

◆ can_cast_expr< unary_minus_exprt >()

◆ can_cast_expr< unary_plus_exprt >()

◆ can_cast_expr< union_exprt >()

◆ can_cast_expr< update_exprt >()

◆ can_cast_expr< vector_exprt >()

◆ can_cast_expr< with_exprt >()

◆ can_cast_expr< xnor_exprt >()

◆ can_cast_expr< xor_exprt >()

◆ conjunction() [1/2]

1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise

Definition at line 275 of file std_expr.cpp.

◆ conjunction() [2/2]

Conjunction of two expressions.

If the second is already an and_exprt add to its operands instead of creating a new expression. If one is true, return the other expression. If one is false returns false.

Definition at line 252 of file std_expr.cpp.

◆ disjunction()

1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise

Definition at line 240 of file std_expr.cpp.

◆ operator!=() [1/3]

Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolean value rhs.

Definition at line 37 of file std_expr.cpp.

◆ operator!=() [2/3]

◆ operator!=() [3/3]

◆ operator==() [1/3]

Return whether the expression lhs is a constant of Boolean type that is representing the Boolean value rhs.

Definition at line 32 of file std_expr.cpp.

◆ operator==() [2/3]

Return whether the expression lhs is a constant representing the numeric value rhs; only values 0 and 1 are supported for rhs.

For value 0 we consider the following types: ID_integer, ID_natural, ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv, ID_floatbv, ID_pointer.
For ID_pointer, returns true iff the value is a zero string or a null pointer.
For value 1 we consider the following types: ID_integer, ID_natural, ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv, ID_floatbv.
For all other types, return false.

Definition at line 52 of file std_expr.cpp.

◆ operator==() [3/3]

Return whether the expression lhs is a constant representing the NULL pointer.

Classes

Namespaces

Functions