Loading...

Searching...

No Matches

expr_util.cpp File Reference

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

+ Include dependency graph for expr_util.cpp:

[フレーム]

Go to the source code of this file.

Functions

bool is_assignable (const exprt &expr)

Returns true iff the argument is one of the following:

exprt make_binary (const exprt &expr)

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

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

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

exprt boolean_negate (const exprt &src)

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

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

returns true if the expression has a subexpression that satisfies pred

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

returns true if the expression has a subexpression with given ID

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

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

returns true if any of the contained types is id

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

lift up an if_exprt one level

const exprt & skip_typecast (const exprt &expr)

find the expression nested inside typecasts, if any

constant_exprt make_boolean_expr (bool value)

returns true_exprt if given true and false_exprt otherwise

exprt make_and (exprt a, exprt b)

Conjunction of two expressions.

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 98 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 110 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 118 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 166 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 124 of file expr_util.cpp.

◆ is_assignable()

bool is_assignable ( const exprt & expr )

Returns true iff the argument is one of the following:

a symbol
a dereference
an array element
a struct member

Definition at line 24 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 69 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 172 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.

Deprecated:: "deprecated since " "2025" "-" "6" "-" "25" "; " "use conjunction(exprt, exprt) instead"

Definition at line 316 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 38 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 308 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 188 of file expr_util.cpp.