cprover
expr_util.h File Reference

Deprecated expression utility functions. More...

#include "irep.h"
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

void make_next_state (exprt &)
 
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 irep_idt &)
 returns true if the expression has a subexpression with given 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()

exprt boolean_negate ( const exprt )

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

Definition at line 120 of file expr_util.cpp.

References irept::id(), exprt::is_false(), exprt::is_true(), exprt::op0(), and exprt::operands().

Referenced by goto_convertt::convert_while(), goto_convertt::generate_conditional_branch(), goto_convertt::generate_ifthenelse(), has_and_or(), and is_empty().

§ has_subexpr()

bool has_subexpr ( const exprt ,
const irep_idt  
)

returns true if the expression has a subexpression with given ID

Definition at line 132 of file expr_util.cpp.

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

Referenced by value_set_dereferencet::has_dereference(), goto_checkt::has_dereference(), and has_subexpr().

§ is_not_zero()

§ lift_if()

§ make_binary()

exprt make_binary ( const exprt )

§ make_next_state()

void make_next_state ( exprt )
Deprecated:
This function will eventually be removed.

Use functions from util/std_expr.h instead.

Definition at line 20 of file expr_util.cpp.

References Forall_operands, irept::id(), and make_next_state().

Referenced by goto_convertt::convert_bp_enforce(), is_empty(), and make_next_state().

§ make_with_expr()

with_exprt make_with_expr ( const update_exprt )

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

Definition at line 60 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().