@@ -81,10 +81,11 @@ std::string graphml_witnesst::convert_assign_rec(
8181 forall_operands (it, assign.rhs ())
8282 {
8383 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+=' ' ;
8889 result+=convert_assign_rec (identifier, code_assignt (index, *it));
8990 }
9091 }
@@ -128,10 +129,11 @@ std::string graphml_witnesst::convert_assign_rec(
128129 assert (it!=assign.rhs ().operands ().end ());
129130
130131 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+=' ' ;
135137 result+=convert_assign_rec (identifier, code_assignt (member, *it));
136138 ++it;
137139
@@ -181,7 +183,7 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
181183 for (goto_tracet::stepst::const_iterator
182184 it=goto_trace.steps .begin ();
183185 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
185187 {
186188 const source_locationt &source_location=it->pc ->source_location ;
187189
@@ -248,10 +250,11 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
248250 goto_tracet::stepst::const_iterator next=it;
249251 for (++next;
250252 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 );
253254 ++next)
254- ;
255+ {
256+ // advance
257+ }
255258 const std::size_t to=
256259 next==goto_trace.steps .end ()?
257260 sink:step_to_node[next->step_nr ];
@@ -345,7 +348,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
345348 case goto_trace_stept::DEAD:
346349 case goto_trace_stept::CONSTRAINT:
347350 case goto_trace_stept::NONE:
348- ; /* ignore */
351+ // ignore
352+ break ;
349353 }
350354
351355 it=next;
@@ -381,7 +385,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
381385 for (symex_target_equationt::SSA_stepst::const_iterator
382386 it=equation.SSA_steps .begin ();
383387 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
385389 {
386390 const source_locationt &source_location=it->source .pc ->source_location ;
387391
@@ -442,10 +446,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
442446 std::size_t next_step_nr=step_nr;
443447 for (++next, ++next_step_nr;
444448 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 );
447450 ++next, ++next_step_nr)
448- ;
451+ {
452+ // advance
453+ }
449454 const std::size_t to=
450455 next==equation.SSA_steps .end ()?
451456 sink:step_to_node[next_step_nr];
@@ -514,10 +519,11 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
514519 case goto_trace_stept::DEAD:
515520 case goto_trace_stept::CONSTRAINT:
516521 case goto_trace_stept::NONE:
517- ; /* ignore */
522+ // ignore
523+ break ;
518524 }
519525
520- it=next;
526+ it=next;
521527 step_nr=next_step_nr;
522528 }
523529}
0 commit comments