cprover
expr_util.h File Reference

Deprecated expression utility functions. More...

#include "irep.h"
#include <functional>
Include dependency graph for expr_util.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

exprt make_binary (const exprt &)
 splits an expression with >=3 operands into nested binary expressions More...
 
with_exprt make_with_expr (const update_exprt &)
 converts an update expr into a (possibly nested) with expression More...
 
exprt is_not_zero (const exprt &, const namespacet &ns)
 converts a scalar/float expression to C/C++ Booleans More...
 
exprt boolean_negate (const exprt &)
 negate a Boolean expression, possibly removing a not_exprt, and swapping false and true More...
 
bool has_subexpr (const exprt &, const std::function< bool(const exprt &)> &pred)
 returns true if the expression has a subexpression that satisfies pred More...
 
bool has_subexpr (const exprt &, const irep_idt &)
 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 &, const irep_idt &id, const namespacet &)
 returns true if any of the contained types is id More...
 
if_exprt lift_if (const exprt &, std::size_t operand_number)
 lift up an if_exprt one level More...
 

Detailed Description

Deprecated expression utility functions.

Author
Daniel Kroening kroen.nosp@m.ing@.nosp@m.kroen.nosp@m.ing..nosp@m.com
Date
Sun Jul 31 21:54:44 BST 2011

Definition in file expr_util.h.

Function Documentation

◆ boolean_negate()

◆ has_subexpr() [1/2]

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

◆ has_subexpr() [2/2]

bool has_subexpr ( const exprt ,
const irep_idt  
)

returns true if the expression has a subexpression with given ID

Definition at line 133 of file expr_util.cpp.

References has_subexpr(), and irept::id().

◆ has_subtype() [1/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
typea type
preda predicate
nsnamespace 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 139 of file expr_util.cpp.

References struct_union_typet::components(), namespace_baset::follow(), namespace_baset::follow_tag(), irept::id(), stack, typet::subtypes(), to_c_enum_tag_type(), and to_struct_union_type().

Referenced by add_string_equation_to_symbol_resolution(), has_char_pointer_subtype(), has_subtype(), and string_identifiers_resolution_from_equations().

◆ has_subtype() [2/2]

bool has_subtype ( const typet ,
const irep_idt id,
const namespacet  
)

returns true if any of the contained types is id

Definition at line 179 of file expr_util.cpp.

References has_subtype(), and irept::id().

◆ is_not_zero()

◆ lift_if()

◆ make_binary()

exprt make_binary ( const exprt )

◆ make_with_expr()

with_exprt make_with_expr ( const update_exprt )

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

Definition at line 53 of file expr_util.cpp.

References update_exprt::designator(), forall_expr, index_designatort::index(), with_exprt::new_value(), PRECONDITION, to_index_designator(), to_with_expr(), UNREACHABLE, and with_exprt::where().