File tree Expand file tree Collapse file tree 8 files changed +8
-21
lines changed Expand file tree Collapse file tree 8 files changed +8
-21
lines changed Original file line number Diff line number Diff line change @@ -156,7 +156,7 @@ static void check_apply_invariants(
156
156
loop_end->targets .clear ();
157
157
loop_end->type =ASSUME;
158
158
if (loop_head->is_goto ())
159
- loop_end->guard . make_false ();
159
+ loop_end->guard = false_exprt ();
160
160
else
161
161
loop_end->guard .make_not ();
162
162
}
Original file line number Diff line number Diff line change @@ -122,8 +122,7 @@ void goto_unwindt::unwind(
122
122
t--;
123
123
assert (t->is_backwards_goto ());
124
124
125
- exprt exit_cond;
126
- exit_cond.make_false (); // default is false
125
+ exprt exit_cond = false_exprt (); // default is false
127
126
128
127
if (!t->guard .is_true ()) // cond in backedge
129
128
{
Original file line number Diff line number Diff line change @@ -81,9 +81,8 @@ void memory_model_tsot::program_order(
81
81
event_listt::const_iterator next=e_it;
82
82
++next;
83
83
84
- exprt mb_guard_r, mb_guard_w;
85
- mb_guard_r.make_false ();
86
- mb_guard_w.make_false ();
84
+ exprt mb_guard_r = false_exprt ();
85
+ exprt mb_guard_w = false_exprt ();
87
86
88
87
for (event_listt::const_iterator
89
88
e_it2=next;
Original file line number Diff line number Diff line change @@ -224,7 +224,7 @@ void goto_symext::symex_goto(statet &state)
224
224
// adjust guards
225
225
if (new_guard.is_true ())
226
226
{
227
- state.guard . make_false ();
227
+ state.guard = false_exprt ();
228
228
}
229
229
else
230
230
{
Original file line number Diff line number Diff line change @@ -418,7 +418,7 @@ literal: TOK_IDENTIFIER
418
418
}
419
419
| TOK_FALSE
420
420
{
421
- newstack ($$). make_false ();
421
+ newstack ($$) = false_exprt ();
422
422
}
423
423
| TOK_FLOATING
424
424
| TOK_STRING
Original file line number Diff line number Diff line change @@ -34,8 +34,7 @@ exprt get_quantifier_var_min(
34
34
{
35
35
PRECONDITION (quantifier_expr.id () == ID_or || quantifier_expr.id () == ID_and);
36
36
37
- exprt res;
38
- res.make_false ();
37
+ exprt res = false_exprt ();
39
38
if (quantifier_expr.id ()==ID_or)
40
39
{
41
40
/* *
@@ -81,8 +80,7 @@ exprt get_quantifier_var_max(
81
80
const exprt &quantifier_expr)
82
81
{
83
82
PRECONDITION (quantifier_expr.id () == ID_or || quantifier_expr.id () == ID_and);
84
- exprt res;
85
- res.make_false ();
83
+ exprt res = false_exprt ();
86
84
if (quantifier_expr.id ()==ID_or)
87
85
{
88
86
/* *
Original file line number Diff line number Diff line change @@ -152,14 +152,6 @@ void exprt::make_true()
152
152
set (ID_value, ID_true);
153
153
}
154
154
155
- // / Replace the expression by a Boolean expression representing false.
156
- // / \deprecated use constructors instead
157
- void exprt::make_false ()
158
- {
159
- *this =exprt (ID_constant, typet (ID_bool));
160
- set (ID_value, ID_false);
161
- }
162
-
163
155
// / Return whether the expression represents a Boolean.
164
156
// / \return True if is a Boolean, false otherwise.
165
157
bool exprt::is_boolean () const
Original file line number Diff line number Diff line change @@ -216,7 +216,6 @@ class exprt:public irept
216
216
void make_not ();
217
217
218
218
void make_true ();
219
- void make_false ();
220
219
void make_bool (bool value);
221
220
222
221
bool is_constant () const ;
You can’t perform that action at this time.
0 commit comments