cprover
Loading...
Searching...
No Matches
expr_util.h File Reference

Deprecated expression utility functions. More...

#include "irep.h"
#include <functional>
+ Include dependency graph for expr_util.h:

Go to the source code of this file.

Classes

class  can_forward_propagatet
 Determine whether an expression is constant. More...
 

Functions

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

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()

exprt boolean_negate ( const exprt & src)

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

Definition at line 129 of file expr_util.cpp.

◆ has_subexpr() [1/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 149 of file expr_util.cpp.

◆ has_subexpr() [2/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 141 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 197 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
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 155 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 100 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 370 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 203 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 347 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 339 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 69 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 219 of file expr_util.cpp.