From 7f4a79ecc4c1c80b3d12b474929ce0f819a4ceb0 Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Fri, 21 Apr 2017 11:26:40 +0100
Subject: [PATCH 1/2] Tidy up C symbol factory code

Correct a comment, replace "symbolt const" with "const symbolt", use
const pointers in for loops, add the location to the declaration of
the main symbol and wrap function header comments better
---
 src/ansi-c/c_nondet_symbol_factory.cpp | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 2b51ce8fb05..cb6d0ef5788 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -61,7 +61,7 @@ static exprt c_get_nondet_bool(const typet &type)
 
 class symbol_factoryt
 {
-  std::vector<symbolt const *> &symbols_created;
+  std::vector<const symbolt *> &symbols_created;
   symbol_tablet &symbol_table;
   const source_locationt &loc;
   const bool assume_non_null;
@@ -69,7 +69,7 @@ class symbol_factoryt
 
 public:
   symbol_factoryt(
-    std::vector<symbolt const *> &_symbols_created,
+    std::vector<const symbolt *> &_symbols_created,
     symbol_tablet &_symbol_table,
     const source_locationt &loc,
     const bool _assume_non_null):
@@ -171,7 +171,7 @@ void symbol_factoryt::gen_nondet_init(
     else
     {
       // Add the following code to assignments:
-      //           IF !(NONDET(_Bool) == FALSE) THEN GOTO <label1>
+      //           IF !NONDET(_Bool) THEN GOTO <label1>
       //           <expr> = <null pointer>
       //           GOTO <label2>
       // <label1>: <expr> = &tmp$<temporary_counter>;
@@ -233,13 +233,15 @@ exprt c_nondet_symbol_factory(
   main_symbol.name=identifier;
   main_symbol.base_name=base_name;
   main_symbol.type=type;
+  main_symbol.location=loc;
+
+  symbol_exprt main_symbol_expr=main_symbol.symbol_expr();
 
   symbolt *main_symbol_ptr;
   bool moving_symbol_failed=symbol_table.move(main_symbol, main_symbol_ptr);
   assert(!moving_symbol_failed);
 
-  std::vector<symbolt const *> symbols_created;
-  symbol_exprt main_symbol_expr=(*main_symbol_ptr).symbol_expr();
+  std::vector<const symbolt *> symbols_created;
   symbols_created.push_back(main_symbol_ptr);
 
   symbol_factoryt state(
@@ -252,7 +254,7 @@ exprt c_nondet_symbol_factory(
 
   // Add the following code to init_code for each symbol that's been created:
   //   <type> <identifier>;
-  for(symbolt const *symbol_ptr : symbols_created)
+  for(const symbolt * const symbol_ptr : symbols_created)
   {
     code_declt decl(symbol_ptr->symbol_expr());
     decl.add_source_location()=loc;

From cf4eeb2186dc114ed73d051e072253ef49757892 Mon Sep 17 00:00:00 2001
From: Owen Jones <owen.jones@diffblue.com>
Date: Fri, 21 Apr 2017 11:46:02 +0100
Subject: [PATCH 2/2] Move code into code block instead of copying it

---
 src/ansi-c/c_nondet_symbol_factory.cpp | 10 +++++-----
 src/util/std_code.h                    |  5 +++++
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index cb6d0ef5788..105af6a2213 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -125,7 +125,7 @@ exprt symbol_factoryt::allocate_object(
   //   <target_expr> = &tmp$<temporary_counter>
   code_assignt assign(target_expr, aoe);
   assign.add_source_location()=loc;
-  assignments.add(assign);
+  assignments.move(assign);
 
   return aoe;
 }
@@ -186,7 +186,7 @@ void symbol_factoryt::gen_nondet_init(
       null_check.then_case()=set_null_inst;
       null_check.else_case()=non_null_inst;
 
-      assignments.add(null_check);
+      assignments.move(null_check);
     }
   }
   // TODO(OJones): Add support for structs and arrays
@@ -202,7 +202,7 @@ void symbol_factoryt::gen_nondet_init(
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
 
-    assignments.add(assign);
+    assignments.move(assign);
   }
 }
 
@@ -258,7 +258,7 @@ exprt c_nondet_symbol_factory(
   {
     code_declt decl(symbol_ptr->symbol_expr());
     decl.add_source_location()=loc;
-    init_code.add(decl);
+    init_code.move(decl);
   }
 
   init_code.append(assignments);
@@ -275,7 +275,7 @@ exprt c_nondet_symbol_factory(
         from_integer(0, index_type())));
     input_code.op1()=symbol_ptr->symbol_expr();
     input_code.add_source_location()=loc;
-    init_code.add(input_code);
+    init_code.move(input_code);
   }
 
   return main_symbol_expr;
diff --git a/src/util/std_code.h b/src/util/std_code.h
index cd017a658ba..eed132a71dd 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -78,6 +78,11 @@ class code_blockt:public codet
       o.push_back(*it);
   }
 
+  void move(codet &code)
+  {
+    move_to_operands(code);
+  }
+
   void add(const codet &code)
   {
     copy_to_operands(code);