with_exprt Class Reference

#include <std_expr.h>

Inheritance diagram for with_exprt:

Public Member Functions
	with_exprt (const exprt &_old, const exprt &_where, const exprt &_new_value)
	with_exprt ()
exprt &	old ()
const exprt &	old () const
exprt &	where ()
const exprt &	where () const
exprt &	new_value ()
const exprt &	new_value () const
Public Member Functions inherited from exprt
	exprt ()=default
	exprt (const irep_idt &_id)
	exprt (const irep_idt &_id, const typet &_type)
bool	has_operands () const
operandst &	operands ()
const operandst &	operands () const
const irep_idt &	value () const
void	value (irep_idt val)
exprt &	op0 ()
exprt &	op1 ()
exprt &	op2 ()
exprt &	op3 ()
const exprt &	op0 () const
const exprt &	op1 () const
const exprt &	op2 () const
const exprt &	op3 () const
void	reserve_operands (unsigned n)
void	move_to_operands (exprt &expr)
void	move_to_operands (exprt &e1, exprt &e2)
void	move_to_operands (exprt &e1, exprt &e2, exprt &e3)
void	copy_to_operands (const exprt &expr)
void	copy_to_operands (const exprt &e1, const exprt &e2)
void	copy_to_operands (const exprt &e1, const exprt &e2, const exprt &e3)
void	make_typecast (const typet &_type)
void	make_not ()
void	make_true ()
void	make_false ()
void	make_bool (bool value)
void	negate ()
bool	sum (const exprt &expr)
bool	mul (const exprt &expr)
bool	subtract (const exprt &expr)
bool	is_constant () const
bool	is_true () const
bool	is_false () const
bool	is_zero () const
bool	is_one () const
bool	is_boolean () const
const locationt &	find_location () const
const locationt &	location () const
locationt &	location ()
exprt &	add_expr (const std::string &name)
const exprt &	find_expr (const std::string &name) const
Public Member Functions inherited from irept
void	dump () const
bool	is_nil () const
bool	is_not_nil () const
	irept (const irep_idt &_id)
	irept ()
	irept (const irept &irep)
irept &	operator= (const irept &irep)
	~irept ()
const irep_idt &	id () const
const std::string &	id_string () const
void	id (const irep_idt &_data)
const irept &	find (const irep_idt &name) const
irept &	add (const irep_idt &name)
const std::string &	get_string (const irep_idt &name) const
const irep_idt &	get (const irep_idt &name) const
bool	get_bool (const irep_idt &name) const
void	set (const irep_idt &name, const irep_idt &value)
void	set (const irep_idt &name, const long value)
void	set (const irep_idt &name, const irept &irep)
void	remove (const irep_idt &name)
void	move_to_sub (irept &irep)
void	move_to_named_sub (const irep_idt &name, irept &irep)
typet &	type ()
const typet &	type () const
bool	is_identifier_set () const
const irep_idt &	identifier () const
const irep_idt &	width () const
const irep_idt &	statement () const
const irep_idt &	name () const
const irep_idt &	component_name () const
const irep_idt &	tag () const
const irep_idt &	from () const
const irep_idt &	file () const
const irep_idt &	line () const
const irep_idt &	function () const
const irept &	function_irep () const
const irep_idt &	column () const
const irep_idt &	destination () const
const irep_idt &	access () const
const irep_idt &	base_name () const
const irep_idt &	comment () const
const irep_idt &	event () const
const irept &	event_irep () const
const irep_idt &	literal () const
const irep_idt &	loopid () const
const irep_idt &	mode () const
const irep_idt &	module () const
const irep_idt &	pretty_name () const
const irep_idt &	derived_this_arg () const
bool	base_ctor_derived () const
bool	need_vptr_init () const
const irep_idt &	property () const
const irep_idt &	size () const
const irept &	size_irep () const
const irep_idt &	integer_bits () const
const irep_idt &	to () const
const irep_idt &	failed_symbol () const
const irep_idt &	type_id () const
const irept &	arguments () const
const irept &	components () const
const irept &	cmt_type () const
const irept &	return_type () const
const irept &	body () const
const irept &	member_irep () const
const irept &	labels_irep () const
const irept &	bv () const
const irept &	targets () const
const irept &	variables () const
const irept &	object_type () const
const irept &	initializer () const
const irept &	cmt_size () const
const irept &	code () const
const irept &	guard () const
const irept &	location () const
const irept &	declaration_type () const
const irept &	decl_value () const
const irept &	end_location () const
const irept &	symvalue () const
const irept &	cmt_location () const
const irept &	decl_ident () const
bool	is_decl_ident_set () const
const irept &	elements () const
bool	is_dynamic_set () const
bool	dynamic () const
const irep_idt &	cmt_base_name () const
const irep_idt &	id_class () const
const irep_idt &	cmt_identifier () const
const irep_idt &	cformat () const
const irep_idt &	member_name () const
	Owning class tag of a member function type, e.g.
const irep_idt &	cpp_type () const
	Source-level spelling of a type, e.g.
const irep_idt &	cmt_width () const
const irept &	offsetof_type () const
bool	axiom () const
bool	cmt_constant () const
bool	dfault () const
bool	ellipsis () const
bool	explict () const
bool	file_local () const
bool	hex_or_oct () const
bool	hide () const
bool	implicit () const
bool	incomplete () const
bool	initialization () const
bool	inlined () const
bool	invalid_object () const
bool	is_parameter () const
bool	is_expression () const
bool	is_extern () const
bool	is_macro () const
bool	is_thread_local () const
bool	is_type () const
bool	lvalue () const
bool	reference () const
bool	restricted () const
bool	static_lifetime () const
bool	theorem () const
bool	cmt_unsigned () const
bool	user_provided () const
bool	cmt_volatile () const
bool	zero_initializer () const
void	arguments (const irept &val)
void	decl_ident (const irept &val)
void	identifier (const irep_idt ident)
void	statement (const irep_idt statm)
void	comment (const irep_idt cmt)
void	component_name (const irep_idt name)
void	hex_or_oct (const irep_idt which)
void	hex_or_oct (bool which)
void	cmt_width (const irep_idt width)
void	cmt_width (unsigned int width)
void	width (const irep_idt width)
void	width (unsigned int width)
void	cmt_unsigned (const irep_idt val)
void	cmt_unsigned (bool val)
void	property (const irep_idt prop)
void	cmt_base_name (const irep_idt name)
void	name (const irep_idt val)
void	cformat (const irep_idt val)
void	member_name (const irep_idt val)
void	cpp_type (const irep_idt val)
void	remove_member_name ()
void	flavor (const irep_idt val)
void	function (const irep_idt val)
void	size (const irep_idt val)
void	size (const irept &val)
void	user_provided (const irep_idt val)
void	user_provided (bool val)
void	destination (const irep_idt val)
void	cmt_constant (const irep_idt val)
void	cmt_constant (bool val)
void	cmt_active (const irep_idt val)
void	base_name (const irep_idt val)
void	code (const irept &val)
void	component (const irep_idt val)
void	component (unsigned int val)
void	dfault (bool val)
void	dynamic (bool val)
void	end_location (const irept &val)
void	ellipsis (bool val)
void	axiom (bool val)
void	event (const irep_idt &val)
void	failed_symbol (const irep_idt val)
void	file (const irep_idt val)
void	file_local (bool val)
void	guard (const irept &val)
void	hide (bool val)
void	id_class (unsigned int val)
void	cmt_identifier (const irep_idt val)
void	implicit (bool val)
void	incomplete (bool val)
void	inlined (bool val)
void	invalid_object (bool val)
void	is_parameter (bool val)
void	is_expression (bool val)
void	is_extern (bool val)
void	is_macro (bool val)
void	is_thread_local (bool val)
void	is_type (bool val)
void	label (const irep_idt &val)
void	lhs (bool val)
void	line (const irep_idt &val)
void	line (unsigned int val)
void	location (const irept &val)
void	lvalue (bool val)
void	mode (const irep_idt &val)
void	module (const irep_idt &val)
void	object_type (const irept &val)
void	pretty_name (const irep_idt &val)
void	derived_this_arg (const irep_idt &val)
void	base_ctor_derived (bool val)
void	need_vptr_init (bool val)
void	restricted (bool val)
void	cmt_size (const irept &val)
void	static_lifetime (bool val)
void	tag (const irep_idt &val)
void	theorem (bool val)
void	cmt_type (const irept &val)
void	type_id (unsigned int val)
void	cmt_volatile (bool val)
void	zero_initializer (bool val)
void	components (const irept &val)
void	offsetof_type (const irept &val)
void	declaration_type (const irept &val)
void	bv (const irept &val)
void	initializer (const irept &val)
void	labels (const irept &val)
void	symvalue (const irept &val)
void	member_irep (const irept &val)
void	return_type (const irept &val)
void	variables (const irept &val)
void	targets (const irept &val)
bool	is_address_of () const
bool	is_and () const
bool	is_or () const
bool	is_array () const
bool	is_bool () const
bool	is_code () const
bool	is_function_call () const
bool	is_constant () const
bool	is_dereference () const
bool	is_empty () const
bool	is_fixedbv () const
bool	is_floatbv () const
bool	is_incomplete_array () const
bool	is_index () const
bool	is_member () const
bool	is_not () const
bool	is_notequal () const
bool	is_pointer () const
bool	is_signedbv () const
bool	is_struct () const
bool	is_symbol () const
bool	is_typecast () const
bool	is_union () const
bool	is_unsignedbv () const
bool	is_vector () const
std::string	to_string () const
void	swap (irept &irep)
int	compare (const irept &i) const
void	clear ()
void	make_nil ()
subt &	get_sub ()
const subt &	get_sub () const
named_subt &	get_named_sub ()
const named_subt &	get_named_sub () const
named_subt &	get_comments ()
const named_subt &	get_comments () const
size_t	hash () const
size_t	full_hash () const
std::string	pretty (unsigned indent=0) const

Additional Inherited Members
Public Types inherited from exprt
typedef std::vector< exprt >	operandst
Public Types inherited from irept
typedef std::vector< irept >	subt
typedef std::map< irep_idt, irept >	named_subt
Static Public Attributes inherited from exprt
static irep_idt	trans = irep_idt("trans")
static irep_idt	symbol = irep_idt("symbol")
static irep_idt	plus = irep_idt("+")
static irep_idt	minus = irep_idt("-")
static irep_idt	mult = irep_idt("*")
static irep_idt	div = irep_idt("/")
static irep_idt	mod = irep_idt("mod")
static irep_idt	equality = irep_idt("=")
static irep_idt	notequal = irep_idt("notequal")
static irep_idt	index = irep_idt("index")
static irep_idt	arrayof = irep_idt("array_of")
static irep_idt	objdesc = irep_idt("object_descriptor")
static irep_idt	dynobj = irep_idt("dynamic_object")
static irep_idt	typecast = irep_idt("typecast")
static irep_idt	implies = irep_idt("=>")
static irep_idt	i_and = irep_idt("and")
static irep_idt	i_xor = irep_idt("xor")
static irep_idt	i_or = irep_idt("or")
static irep_idt	i_not = irep_idt("not")
static irep_idt	addrof = irep_idt("address_of")
static irep_idt	deref = irep_idt("dereference")
static irep_idt	i_if = irep_idt("if")
static irep_idt	with = irep_idt("with")
static irep_idt	member = irep_idt("member")
static irep_idt	member_ref = irep_idt("member_ref")
static irep_idt	ptr_mem = irep_idt("ptr_mem")
static irep_idt	isnan = irep_idt("isnan")
static irep_idt	ieee_floateq = irep_idt("ieee_float_equal")
static irep_idt	i_type = irep_idt("type")
static irep_idt	constant = irep_idt("constant")
static irep_idt	i_true = irep_idt("true")
static irep_idt	i_false = irep_idt("false")
static irep_idt	i_lt = irep_idt("<")
static irep_idt	i_gt = irep_idt(">")
static irep_idt	i_le = irep_idt("<=")
static irep_idt	i_ge = irep_idt(">=")
static irep_idt	i_cmp_three_way = irep_idt("<=>")
static irep_idt	i_bitand = irep_idt("bitand")
static irep_idt	i_bitor = irep_idt("bitor")
static irep_idt	i_bitxor = irep_idt("bitxor")
static irep_idt	i_bitnot = irep_idt("bitnot")
static irep_idt	i_ashr = irep_idt("ashr")
static irep_idt	i_lshr = irep_idt("lshr")
static irep_idt	i_shl = irep_idt("shl")
static irep_idt	abs = irep_idt("abs")
static irep_idt	argument = irep_idt("argument")
static irep_idt	a_value = irep_idt("value")
Static Public Attributes inherited from irept
static const irep_idt	s_type = irep_idt("type")
static const irep_idt	s_arguments = irep_idt("arguments")
static const irep_idt	s_components = irep_idt("components")
static const irep_idt	s_return_type = irep_idt("return_type")
static const irep_idt	s_body = irep_idt("body")
static const irep_idt	s_member = irep_idt("member")
static const irep_idt	s_labels = irep_idt("labels")
static const irep_idt	s_bv = irep_idt("bv")
static const irep_idt	s_targets = irep_idt("targets")
static const irep_idt	s_variables = irep_idt("variables")
static const irep_idt	s_initializer = irep_idt("initializer")
static const irep_idt	s_declaration_type = irep_idt("declaration_type")
static const irep_idt	s_decl_value = irep_idt("decl_value")
static const irep_idt	s_symvalue = irep_idt("symvalue")
static const irep_idt	s_cmt_location = irep_idt("#location")
static const irep_idt	s_decl_ident = irep_idt("decl_ident")
static const irep_idt	s_elements = irep_idt("elements")
static const irep_idt	s_offsetof_type = irep_idt("offsetof_type")
static const irep_idt	a_width = irep_idt("width")
static const irep_idt	a_name = irep_idt("name")
static const irep_idt	a_statement = irep_idt("statement")
static const irep_idt	a_identifier = irep_idt("identifier")
static const irep_idt	a_comp_name = irep_idt("component_name")
static const irep_idt	a_tag = irep_idt("tag")
static const irep_idt	a_from = irep_idt("from")
static const irep_idt	a_file = irep_idt("file")
static const irep_idt	a_line = irep_idt("line")
static const irep_idt	a_function = irep_idt("function")
static const irep_idt	a_column = irep_idt("column")
static const irep_idt	a_access = irep_idt("access")
static const irep_idt	a_destination = irep_idt("destination")
static const irep_idt	a_base_name = irep_idt("base_name")
static const irep_idt	a_comment = irep_idt("comment")
static const irep_idt	a_event = irep_idt("event")
static const irep_idt	a_literal = irep_idt("literal")
static const irep_idt	a_loopid = irep_idt("loop-id")
static const irep_idt	a_mode = irep_idt("mode")
static const irep_idt	a_module = irep_idt("module")
static const irep_idt	a_pretty_name = irep_idt("pretty_name")
static const irep_idt	a_property = irep_idt("property")
static const irep_idt	a_size = irep_idt("size")
static const irep_idt	a_integer_bits = irep_idt("integer_bits")
static const irep_idt	a_to = irep_idt("to")
static const irep_idt	a_failed_symbol = irep_idt("#failed_symbol")
static const irep_idt	a_dynamic = irep_idt("#dynamic")
static const irep_idt	a_cmt_base_name = irep_idt("#base_name")
static const irep_idt	a_id_class = irep_idt("#id_class")
static const irep_idt	a_cmt_identifier = irep_idt("#identifier")
static const irep_idt	a_cformat = irep_idt("#cformat")
static const irep_idt	a_cmt_width = irep_idt("#width")
static const irep_idt	a_axiom = irep_idt("axiom")
static const irep_idt	a_member_name = irep_idt("#member_name")
static const irep_idt	a_cpp_type = irep_idt("#cpp_type")
static const irep_idt	a_cmt_constant = irep_idt("#constant")
static const irep_idt	a_default = irep_idt("default")
static const irep_idt	a_ellipsis = irep_idt("ellipsis")
static const irep_idt	a_explicit = irep_idt("explicit")
static const irep_idt	a_file_local = irep_idt("file_local")
static const irep_idt	a_hex_or_oct = irep_idt("#hex_or_oct")
static const irep_idt	a_hide = irep_idt("#hide")
static const irep_idt	a_implicit = irep_idt("#implicit")
static const irep_idt	a_incomplete = irep_idt("#incomplete")
static const irep_idt	a_initialization = irep_idt("initialization")
static const irep_idt	a_inlined = irep_idt("#inlined")
static const irep_idt	a_invalid_object = irep_idt("#invalid_object")
static const irep_idt	a_is_parameter = irep_idt("is_parameter")
static const irep_idt	a_is_expression = irep_idt("#is_expression")
static const irep_idt	a_is_extern = irep_idt("is_extern")
static const irep_idt	a_is_macro = irep_idt("is_macro")
static const irep_idt	a_is_thread_local = irep_idt("is_thread_local")
static const irep_idt	a_is_type = irep_idt("is_type")
static const irep_idt	a_lvalue = irep_idt("lvalue")
static const irep_idt	a_reference = irep_idt("#reference")
static const irep_idt	a_static_lifetime = irep_idt("static_lifetime")
static const irep_idt	a_theorem = irep_idt("theorem")
static const irep_idt	a_cmt_unsigned = irep_idt("#unsigned")
static const irep_idt	a_user_provided = irep_idt("user-provided")
static const irep_idt	a_cmt_volatile = irep_idt("#volatile")
static const irep_idt	a_zero_initializer = irep_idt("#zero_initializer")
static const irep_idt	a_restricted = irep_idt("#restricted")
static const irep_idt	a_flavor = irep_idt("flavor")
static const irep_idt	a_cmt_active = irep_idt("#active")
static const irep_idt	a_code = irep_idt("code")
static const irep_idt	a_component = irep_idt("component")
static const irep_idt	a_end_location = irep_idt("#end_location")
static const irep_idt	a_guard = irep_idt("guard")
static const irep_idt	a_label = irep_idt("label")
static const irep_idt	a_lhs = irep_idt("lhs")
static const irep_idt	a_location = irep_idt("location")
static const irep_idt	a_object_type = irep_idt("object_type")
static const irep_idt	a_cmt_size = irep_idt("#size")
static const irep_idt	a_cmt
static const irep_idt	a_type_id = irep_idt("typeid")
static const irep_idt	a_cmt_type = irep_idt("#type")
static const irep_idt	a_derived_this_arg = irep_idt("#derived_this_arg")
static const irep_idt	a_base_ctor_derived = irep_idt("#base_ctor_derived")
static const irep_idt	a_need_vptr_init = irep_idt("#need_vptr_init")
static const irep_idt	id_address_of = irep_idt("address_of")
static const irep_idt	id_and = irep_idt("and")
static const irep_idt	id_or = irep_idt("or")
static const irep_idt	id_array = irep_idt("array")
static const irep_idt	id_bool = irep_idt("bool")
static const irep_idt	id_code = irep_idt("code")
static const irep_idt	id_constant = irep_idt("constant")
static const irep_idt	id_dereference = irep_idt("dereference")
static const irep_idt	id_empty = irep_idt("empty")
static const irep_idt	id_fixedbv = irep_idt("fixedbv")
static const irep_idt	id_floatbv = irep_idt("floatbv")
static const irep_idt	id_incomplete_array = irep_idt("incomplete_array")
static const irep_idt	id_index = irep_idt("index")
static const irep_idt	id_member = irep_idt("member")
static const irep_idt	id_not = irep_idt("not")
static const irep_idt	id_notequal = irep_idt("notequal")
static const irep_idt	id_pointer = irep_idt("pointer")
static const irep_idt	id_signedbv = irep_idt("signedbv")
static const irep_idt	id_struct = irep_idt("struct")
static const irep_idt	id_symbol = irep_idt("symbol")
static const irep_idt	id_typecast = irep_idt("typecast")
static const irep_idt	id_union = irep_idt("union")
static const irep_idt	id_unsignedbv = irep_idt("unsignedbv")
static const irep_idt	id_vector = irep_idt("vector")
Protected Member Functions inherited from irept
void	remove_ref (dt *old_data)
const dt &	read () const
dt &	write ()
void	detatch ()
Static Protected Member Functions inherited from irept
static bool	is_comment (const irep_idt &name)
Protected Attributes inherited from irept
dt *	data
Static Protected Attributes inherited from exprt
static irep_idt	o_operands = irep_idt("operands")
static irep_idt	o_location = irep_idt("#location")

Constructor & Destructor Documentation

with_exprt() [1/2]

with_exprt::with_exprt ( const exprt & _old, const exprt & _where, const exprt & _new_value )

inline

with_exprt() [2/2]

with_exprt::with_exprt ( )

inline

Member Function Documentation

new_value() [1/2]

exprt & with_exprt::new_value ( )

inline

new_value() [2/2]

const exprt & with_exprt::new_value ( ) const

inline

old() [1/2]

exprt & with_exprt::old ( )

inline

old() [2/2]

const exprt & with_exprt::old ( ) const

inline

where() [1/2]

exprt & with_exprt::where ( )

inline

where() [2/2]

const exprt & with_exprt::where ( ) const

inline

---

The documentation for this class was generated from the following file:

• src/util/irep/std_expr.h