@@ -81,10 +81,11 @@ std::string graphml_witnesst::convert_assign_rec(
81
81
forall_operands (it, assign.rhs ())
82
82
{
83
83
index_exprt index (
84
- assign.lhs (),
85
- from_integer (i++, signedbv_typet (config.ansi_c .pointer_width )),
86
- type.subtype ());
87
- if (!result.empty ()) result+=' ' ;
84
+ assign.lhs (),
85
+ from_integer (i++, signedbv_typet (config.ansi_c .pointer_width )),
86
+ type.subtype ());
87
+ if (!result.empty ())
88
+ result+=' ' ;
88
89
result+=convert_assign_rec (identifier, code_assignt (index , *it));
89
90
}
90
91
}
@@ -128,10 +129,11 @@ std::string graphml_witnesst::convert_assign_rec(
128
129
assert (it!=assign.rhs ().operands ().end ());
129
130
130
131
member_exprt member (
131
- assign.lhs (),
132
- comp.get_name (),
133
- it->type ());
134
- if (!result.empty ()) result+=' ' ;
132
+ assign.lhs (),
133
+ comp.get_name (),
134
+ it->type ());
135
+ if (!result.empty ())
136
+ result+=' ' ;
135
137
result+=convert_assign_rec (identifier, code_assignt (member, *it));
136
138
++it;
137
139
@@ -181,7 +183,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
181
183
for (goto_tracet::stepst::const_iterator
182
184
it=goto_trace.steps .begin ();
183
185
it!=goto_trace.steps .end ();
184
- it++) // we cannot replace this by a ranged for
186
+ it++) // we cannot replace this by a ranged for
185
187
{
186
188
const source_locationt &source_location=it->pc ->source_location ;
187
189
@@ -248,10 +250,11 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
248
250
goto_tracet::stepst::const_iterator next=it;
249
251
for (++next;
250
252
next!=goto_trace.steps .end () &&
251
- (step_to_node[next->step_nr ]==sink ||
252
- it->pc ==next->pc );
253
+ (step_to_node[next->step_nr ]==sink || it->pc ==next->pc );
253
254
++next)
254
- ;
255
+ {
256
+ // advance
257
+ }
255
258
const std::size_t to=
256
259
next==goto_trace.steps .end ()?
257
260
sink:step_to_node[next->step_nr ];
@@ -345,7 +348,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
345
348
case goto_trace_stept::DEAD:
346
349
case goto_trace_stept::CONSTRAINT:
347
350
case goto_trace_stept::NONE:
348
- ; /* ignore */
351
+ // ignore
352
+ break ;
349
353
}
350
354
351
355
it=next;
@@ -381,7 +385,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
381
385
for (symex_target_equationt::SSA_stepst::const_iterator
382
386
it=equation.SSA_steps .begin ();
383
387
it!=equation.SSA_steps .end ();
384
- it++, step_nr++) // we cannot replace this by a ranged for
388
+ it++, step_nr++) // we cannot replace this by a ranged for
385
389
{
386
390
const source_locationt &source_location=it->source .pc ->source_location ;
387
391
@@ -442,10 +446,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
442
446
std::size_t next_step_nr=step_nr;
443
447
for (++next, ++next_step_nr;
444
448
next!=equation.SSA_steps .end () &&
445
- (step_to_node[next_step_nr]==sink ||
446
- it->source .pc ==next->source .pc );
449
+ (step_to_node[next_step_nr]==sink || it->source .pc ==next->source .pc );
447
450
++next, ++next_step_nr)
448
- ;
451
+ {
452
+ // advance
453
+ }
449
454
const std::size_t to=
450
455
next==equation.SSA_steps .end ()?
451
456
sink:step_to_node[next_step_nr];
@@ -514,10 +519,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
514
519
case goto_trace_stept::DEAD:
515
520
case goto_trace_stept::CONSTRAINT:
516
521
case goto_trace_stept::NONE:
517
- ; /* ignore */
522
+ // ignore
523
+ break ;
518
524
}
519
525
520
- it=next;
526
+ it=next;
521
527
step_nr=next_step_nr;
522
528
}
523
529
}
0 commit comments