Merge pull request #3937 from tautschnig/deprecation-while

Construct code_(do)whilet bottom-up [blocks: #3800]

Author: tautschnig

src/goto-instrument/goto_program2code.cpp

@@ -518,10 +518,8 @@ goto_programt::const_targett goto_program2codet::convert_do_while(
 {
   assert(loop_end->is_goto() && loop_end->is_backwards_goto());
 
-  code_dowhilet d;
-  d.cond()=loop_end->guard;
+  code_dowhilet d(loop_end->guard, code_blockt());
   simplify(d.cond(), ns);
-  d.body()=code_blockt();
 
   copy_source_location(loop_end->targets.front(), d);
 
@@ -571,8 +569,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
   if(target==loop_end) // 1: GOTO 1
     return convert_goto_goto(target, dest);
 
-  code_whilet w;
-  w.body()=code_blockt();
+  code_whilet w(true_exprt{}, code_blockt{});
   goto_programt::const_targett after_loop=loop_end;
   ++after_loop;
   assert(after_loop!=goto_program.instructions.end());
@@ -586,12 +583,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
   }
   else if(target->guard.is_true())
   {
-    w.cond()=true_exprt();
     target=convert_goto_goto(target, w.body());
   }
   else
   {
-    w.cond()=true_exprt();
     target=convert_goto_switch(target, loop_end, w.body());
   }
 
@@ -641,12 +636,8 @@ goto_programt::const_targett goto_program2codet::convert_goto_while(
         to_code_ifthenelse(back).cond().is_true() &&
         to_code_ifthenelse(back).then_case().get_statement()==ID_break))
     {
-      code_dowhilet d;
-
-      d.cond()=false_exprt();
-
       w.body().operands().pop_back();
-      d.body().swap(w.body());
+      code_dowhilet d(false_exprt(), w.body());
 
       copy_source_location(target, d);
 

unit/analyses/ai/ai.cpp

@@ -206,11 +206,6 @@ SCENARIO(
 
   f_body.copy_to_operands(make_void_call(h.symbol_expr()));
 
-  code_whilet loop;
-
-  loop.cond() =
-    notequal_exprt(x.symbol_expr(), from_integer(0, signed_int_type()));
-
   code_blockt loop_body;
   loop_body.copy_to_operands(
     code_assignt(
@@ -222,7 +217,9 @@ SCENARIO(
       minus_exprt(y.symbol_expr(), from_integer(1, signed_int_type()))));
   loop_body.copy_to_operands(make_void_call(g.symbol_expr()));
 
-  loop.body() = loop_body;
+  code_whilet loop(
+    notequal_exprt(x.symbol_expr(), from_integer(0, signed_int_type())),
+    loop_body);
 
   f_body.add_to_operands(std::move(loop));