codet now inherits from irept

Author: Daniel Kroening

src/ansi-c/c_typecheck_code.cpp

@@ -30,8 +30,6 @@ void c_typecheck_baset::typecheck_code(codet &code)
     throw 0;
   }
 
-  code.type()=code_typet();
-
   const irep_idt &statement=code.get_statement();
 
   if(statement==ID_expression)

src/ansi-c/c_typecheck_expr.cpp

@@ -771,7 +771,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
     code_declt decl(symbol.symbol_expr());
     decl.add_source_location()=declaration.source_location();
 
-    expr.op0()=decl;
+    expr.get_sub()[0] = decl;
 
     typecheck_expr(expr.op1());
   }
@@ -1012,7 +1012,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
       ID_statement_expression, void_type(), expr.source_location());
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
-    side_effect_expr.copy_to_operands(decl_block);
+    side_effect_expr.get_sub().push_back(decl_block);
     clean_code.clear();
 
     // We merge the side-effect into the operand of the typecast,
@@ -1069,7 +1069,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
       ID_statement_expression, void_type(), expr.source_location());
     auto decl_block=code_blockt::from_list(clean_code);
     decl_block.set_statement(ID_decl_block);
-    side_effect_expr.copy_to_operands(decl_block);
+    side_effect_expr.get_sub().push_back(decl_block);
     clean_code.clear();
 
     // We merge the side-effect into the operand of the typecast,

src/goto-symex/goto_symex.h

@@ -248,6 +248,7 @@ class goto_symext
   // c) clean up byte_extract on the lhs of an assignment
   void clean_expr(
     exprt &, statet &, bool write);
+  void clean_expr(codet &, statet &, bool write);
 
   void trigger_auto_object(const exprt &, statet &);
   void initialize_auto_object(const exprt &, statet &);
@@ -454,7 +455,7 @@ class goto_symext
   virtual void symex_fkt(statet &, const code_function_callt &);
   virtual void symex_macro(statet &, const code_function_callt &);
   virtual void symex_trace(statet &, const code_function_callt &);
-  virtual void symex_printf(statet &, const exprt &rhs);
+  virtual void symex_printf(statet &, const irept &);
   virtual void symex_input(statet &, const codet &);
   virtual void symex_output(statet &, const codet &);
 

src/goto-symex/symex_builtin_functions.cpp

@@ -306,12 +306,11 @@ irep_idt get_string_argument(const exprt &src, const namespacet &ns)
   return get_string_argument_rec(tmp);
 }
 
-void goto_symext::symex_printf(
-  statet &state,
-  const exprt &rhs)
+void goto_symext::symex_printf(statet &state, const irept &rhs)
 {
   PRECONDITION(!rhs.operands().empty());
 
+#if 0
   exprt tmp_rhs=rhs;
   state.rename(tmp_rhs, ns);
   do_simplify(tmp_rhs);
@@ -329,6 +328,7 @@ void goto_symext::symex_printf(
     target.output_fmt(
       state.guard.as_expr(),
       state.source, "printf", format_string, args);
+#endif
 }
 
 void goto_symext::symex_input(

src/linking/static_lifetime_init.cpp

@@ -33,10 +33,8 @@ void static_lifetime_init(
 
   symbolt &init_symbol = symbol_table.get_writeable_ref(INITIALIZE_FUNCTION);
 
-  init_symbol.value=code_blockt();
-  init_symbol.value.add_source_location()=source_location;
-
-  code_blockt &dest=to_code_block(to_code(init_symbol.value));
+  code_blockt dest;
+  dest.add_source_location() = source_location;
 
   // add the magic label to hide
   dest.add(code_labelt("__CPROVER_HIDE", code_skipt()));
@@ -149,4 +147,6 @@ void static_lifetime_init(
       dest.add(function_call);
     }
   }
+
+  init_symbol.value = dest.as_expr();
 }