#include "expr_util.h"
#include "arith_tools.h"
#include "c_types.h"
#include "config.h"
#include "expr_iterator.h"
#include "namespace.h"
#include "pointer_expr.h"
#include "std_expr.h"
#include <algorithm>
#include <unordered_set>

Include dependency graph for expr_util.cpp:

Functions
bool	is_assignable (const exprt &expr)
	Returns true iff the argument is one of the following: More...

exprt	make_binary (const exprt &expr)
	splits an expression with >=3 operands into nested binary expressions More...

with_exprt	make_with_expr (const update_exprt &src)
	converts an update expr into a (possibly nested) with expression More...

exprt	is_not_zero (const exprt &src, const namespacet &ns)
	converts a scalar/float expression to C/C++ Booleans More...

exprt	boolean_negate (const exprt &src)
	negate a Boolean expression, possibly removing a not_exprt, and swapping false and true More...

bool	has_subexpr (const exprt &expr, const std::function< bool(const exprt &)> &pred)
	returns true if the expression has a subexpression that satisfies pred More...

bool	has_subexpr (const exprt &src, const irep_idt &id)
	returns true if the expression has a subexpression with given ID More...

bool	has_subtype (const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
	returns true if any of the contained types satisfies pred More...

bool	has_subtype (const typet &type, const irep_idt &id, const namespacet &ns)
	returns true if any of the contained types is id More...

if_exprt	lift_if (const exprt &src, std::size_t operand_number)
	lift up an if_exprt one level More...

const exprt &	skip_typecast (const exprt &expr)
	find the expression nested inside typecasts, if any More...

constant_exprt	make_boolean_expr (bool value)
	returns true_exprt if given true and false_exprt otherwise More...

exprt	make_and (exprt a, exprt b)
	Conjunction of two expressions. More...

bool	is_null_pointer (const constant_exprt &expr)
	Returns true if `expr` has a pointer type and a value NULL; it also returns true when `expr` has value zero and NULL_is_zero is true; returns false in all other cases. More...

Function Documentation

◆ boolean_negate()

exprt boolean_negate ( const exprt & src )

negate a Boolean expression, possibly removing a not_exprt, and swapping false and true

Definition at line 127 of file expr_util.cpp.

◆ has_subexpr() [1/2]

bool has_subexpr	(	const exprt &	expr,
		const std::function< bool(const exprt &)> &	pred
	)

returns true if the expression has a subexpression that satisfies pred

Definition at line 139 of file expr_util.cpp.

◆ has_subexpr() [2/2]

bool has_subexpr	(	const exprt &	src,
		const irep_idt &	id
	)

returns true if the expression has a subexpression with given ID

Definition at line 147 of file expr_util.cpp.

◆ has_subtype() [1/2]

bool has_subtype	(	const typet &	type,
		const irep_idt &	id,
		const namespacet &	ns
	)

returns true if any of the contained types is id

Definition at line 195 of file expr_util.cpp.

◆ has_subtype() [2/2]

bool has_subtype	(	const typet &	type,
		const std::function< bool(const typet &)> &	pred,
		const namespacet &	ns
	)

returns true if any of the contained types satisfies pred

Parameters

type	a type
pred	a predicate
ns	namespace for symbol type lookups

Returns: true if one of the subtype of type satisfies predicate pred. The meaning of "subtype" is in the algebraic datatype sense: for example, the subtypes of a struct are the types of its components, the subtype of a pointer is the type it points to, etc... For instance in the type t defined by { int a; char[] b; double * c; { bool d} e}, int, char, double and bool are subtypes of t.

Definition at line 153 of file expr_util.cpp.

◆ is_assignable()

bool is_assignable ( const exprt & )

Returns true iff the argument is one of the following:

a symbol
a dereference
an array element
a struct member

Definition at line 22 of file expr_util.cpp.

◆ is_not_zero()

exprt is_not_zero	(	const exprt &	src,
		const namespacet &	ns
	)

converts a scalar/float expression to C/C++ Booleans

Definition at line 98 of file expr_util.cpp.

◆ is_null_pointer()

bool is_null_pointer ( const constant_exprt & expr )

Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value zero and NULL_is_zero is true; returns false in all other cases.

Definition at line 315 of file expr_util.cpp.

◆ lift_if()

if_exprt lift_if	(	const exprt &	src,
		std::size_t	operand_number
	)

lift up an if_exprt one level

Definition at line 201 of file expr_util.cpp.

◆ make_and()

exprt make_and	(	exprt	a,
		exprt	b
	)

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 292 of file expr_util.cpp.

◆ make_binary()

exprt make_binary ( const exprt & expr )

splits an expression with >=3 operands into nested binary expressions

Definition at line 36 of file expr_util.cpp.

◆ make_boolean_expr()

constant_exprt make_boolean_expr ( bool value )

returns true_exprt if given true and false_exprt otherwise

Definition at line 284 of file expr_util.cpp.

◆ make_with_expr()

with_exprt make_with_expr ( const update_exprt & src )

converts an update expr into a (possibly nested) with expression

Definition at line 67 of file expr_util.cpp.

◆ skip_typecast()

const exprt& skip_typecast ( const exprt & expr )

find the expression nested inside typecasts, if any

Definition at line 217 of file expr_util.cpp.

Functions