diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 74aa57557c1..0105b975643 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -156,7 +156,7 @@ static void check_apply_invariants( loop_end->targets.clear(); loop_end->type=ASSUME; if(loop_head->is_goto()) - loop_end->guard.make_false(); + loop_end->guard = false_exprt(); else loop_end->guard.make_not(); } diff --git a/src/goto-instrument/unwind.cpp b/src/goto-instrument/unwind.cpp index a7ef29eb16d..ed570bcacd1 100644 --- a/src/goto-instrument/unwind.cpp +++ b/src/goto-instrument/unwind.cpp @@ -122,8 +122,7 @@ void goto_unwindt::unwind( t--; assert(t->is_backwards_goto()); - exprt exit_cond; - exit_cond.make_false(); // default is false + exprt exit_cond = false_exprt(); // default is false if(!t->guard.is_true()) // cond in backedge { diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp index 9062ab2b4df..0ca8b797b4d 100644 --- a/src/goto-symex/memory_model_tso.cpp +++ b/src/goto-symex/memory_model_tso.cpp @@ -81,9 +81,8 @@ void memory_model_tsot::program_order( event_listt::const_iterator next=e_it; ++next; - exprt mb_guard_r, mb_guard_w; - mb_guard_r.make_false(); - mb_guard_w.make_false(); + exprt mb_guard_r = false_exprt(); + exprt mb_guard_w = false_exprt(); for(event_listt::const_iterator e_it2=next; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index ec7f61a3f43..0e649815bd1 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -224,7 +224,7 @@ void goto_symext::symex_goto(statet &state) // adjust guards if(new_guard.is_true()) { - state.guard.make_false(); + state.guard = false_exprt(); } else { diff --git a/src/jsil/parser.y b/src/jsil/parser.y index 5ea1e3e866b..ac2643519bd 100644 --- a/src/jsil/parser.y +++ b/src/jsil/parser.y @@ -418,7 +418,7 @@ literal: TOK_IDENTIFIER } | TOK_FALSE { - newstack($$).make_false(); + newstack($$) = false_exprt(); } | TOK_FLOATING | TOK_STRING diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 63f0acb8847..e2161a4ded6 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -34,8 +34,7 @@ exprt get_quantifier_var_min( { PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and); - exprt res; - res.make_false(); + exprt res = false_exprt(); if(quantifier_expr.id()==ID_or) { /** @@ -81,8 +80,7 @@ exprt get_quantifier_var_max( const exprt &quantifier_expr) { PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and); - exprt res; - res.make_false(); + exprt res = false_exprt(); if(quantifier_expr.id()==ID_or) { /** diff --git a/src/util/expr.cpp b/src/util/expr.cpp index 7322e124895..c2f1658693d 100644 --- a/src/util/expr.cpp +++ b/src/util/expr.cpp @@ -152,14 +152,6 @@ void exprt::make_true() set(ID_value, ID_true); } -/// Replace the expression by a Boolean expression representing false. -/// \deprecated use constructors instead -void exprt::make_false() -{ - *this=exprt(ID_constant, typet(ID_bool)); - set(ID_value, ID_false); -} - /// Return whether the expression represents a Boolean. /// \return True if is a Boolean, false otherwise. bool exprt::is_boolean() const diff --git a/src/util/expr.h b/src/util/expr.h index 358e106d3fa..a4a091892d5 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -216,7 +216,6 @@ class exprt:public irept void make_not(); void make_true(); - void make_false(); void make_bool(bool value); bool is_constant() const;