CBMC
Loading...
Searching...
No Matches
Classes | Functions
expr_util.h File Reference

Deprecated expression utility functions. More...

#include "deprecate.h"
#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
 
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 exprt &  skip_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.
 

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 98 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 118 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 110 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.

AltStyle によって変換されたページ (->オリジナル) /