@@ -114,13 +114,15 @@ void goto_convertt::rewrite_boolean(exprt &expr)
114
114
" ' must be Boolean, but got " ,
115
115
irep_pretty_diagnosticst{expr});
116
116
117
+ const source_locationt source_location = expr.find_source_location ();
118
+
117
119
// re-write "a ==> b" into a?b:1
118
120
if (auto implies = expr_try_dynamic_cast<implies_exprt>(expr))
119
121
{
120
122
expr = if_exprt{
121
123
std::move (implies->lhs ()),
122
124
std::move (implies->rhs ()),
123
- true_exprt{},
125
+ true_exprt{}. with_source_location (source_location) ,
124
126
bool_typet{}};
125
127
return ;
126
128
}
@@ -135,6 +137,8 @@ void goto_convertt::rewrite_boolean(exprt &expr)
135
137
else // ID_or
136
138
tmp = false_exprt ();
137
139
140
+ tmp.add_source_location () = source_location;
141
+
138
142
exprt::operandst &ops = expr.operands ();
139
143
140
144
// start with last one
@@ -146,17 +150,21 @@ void goto_convertt::rewrite_boolean(exprt &expr)
146
150
DATA_INVARIANT_WITH_DIAGNOSTICS (
147
151
op.is_boolean (),
148
152
" boolean operators must have only boolean operands" ,
149
- expr. find_source_location () );
153
+ source_location );
150
154
151
155
if (expr.id () == ID_and)
152
156
{
153
- if_exprt if_e (op, tmp, false_exprt ());
157
+ exprt if_e =
158
+ if_exprt{op, tmp, false_exprt{}.with_source_location (source_location)}
159
+ .with_source_location (source_location);
154
160
tmp.swap (if_e);
155
161
continue ;
156
162
}
157
163
if (expr.id () == ID_or)
158
164
{
159
- if_exprt if_e (op, true_exprt (), tmp);
165
+ exprt if_e =
166
+ if_exprt{op, true_exprt{}.with_source_location (source_location), tmp}
167
+ .with_source_location (source_location);
160
168
tmp.swap (if_e);
161
169
continue ;
162
170
}
0 commit comments